diff options
Diffstat (limited to 'src')
70 files changed, 992 insertions, 719 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index bff4f9f1..aea5a62d 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -413,6 +413,7 @@ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcCheck.c ==========================================================*/ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); +extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); /*=== abcCollapse.c ==========================================================*/ diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index c5f644d2..1d23d7ed 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -25,6 +25,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ); static bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk ); static bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk ); static bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk ); @@ -54,6 +55,38 @@ static bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fCo ***********************************************************************/ bool Abc_NtkCheck( Abc_Ntk_t * pNtk ) { + return !Abc_FrameIsFlagEnabled( "check" ) || Abc_NtkDoCheck( pNtk ); +} + +/**Function************************************************************* + + Synopsis [Checks the integrity of the network after reading.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk ) +{ + return !Abc_FrameIsFlagEnabled( "checkread" ) || Abc_NtkDoCheck( pNtk ); +} + +/**Function************************************************************* + + Synopsis [Checks the integrity of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ) +{ Abc_Obj_t * pObj, * pNet, * pNode; int i; @@ -402,6 +435,9 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) } } + if ( !Abc_FrameIsFlagEnabled("checkfio") ) + return Value; + // make sure fanins are not duplicated for ( i = 0; i < pObj->vFanins.nSize; i++ ) for ( k = i + 1; k < pObj->vFanins.nSize; k++ ) @@ -412,7 +448,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) } // save time: do not check large fanout lists - if ( pObj->vFanouts.nSize > 20 ) + if ( pObj->vFanouts.nSize > 100 ) return Value; // make sure fanouts are not duplicated diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 77fbeb38..08ee93bb 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -41,7 +41,6 @@ ***********************************************************************/ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pFanin; int i, k; @@ -65,7 +64,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) // duplicate EXDC if ( pNtk->pExdc ) pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc ); - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" ); return pNtkNew; } @@ -146,7 +145,6 @@ Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin; char * pNameCo; @@ -214,7 +212,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) // duplicate EXDC if ( pNtk->pExdc ) pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc ); - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" ); return pNtkNew; } @@ -232,7 +230,6 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pFanin, * pNodeNew; int i, k; @@ -289,7 +286,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ) else pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); } - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkAigToLogicSop(): Network check has failed.\n" ); return pNtkNew; } @@ -307,7 +304,6 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pFanin; Vec_Ptr_t * vNodes; @@ -360,7 +356,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ) // duplicate the EXDC Ntk if ( pNtk->pExdc ) printf( "Warning: The EXDc network is skipped.\n" ); - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkAigToLogicSopBench(): Network check has failed.\n" ); return pNtkNew; } diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index f869abf3..40c6e7a5 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [abcCreate.c] + FileName [abcObj.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: abcCreate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abcObj.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index ee59cf43..20a64246 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -23,6 +23,7 @@ #endif #include "abc.h" +#include "main.h" #include "io.h" //////////////////////////////////////////////////////////////////////// @@ -195,22 +196,26 @@ void Abc_ShowFile( char * FileNameDot ) char * FileGeneric; char FileNamePs[200]; char CommandDot[1000]; -#ifndef WIN32 - char CommandPs[1000]; -#endif - char * pProgDotName; - char * pProgGsViewName; + char * pDotName; + char * pDotNameWin = "dot.exe"; + char * pDotNameUnix = "dot"; + char * pGsNameWin = "gsview32.exe"; + char * pGsNameUnix = "gv"; int RetValue; + // get DOT names from the resource file + if ( Abc_FrameReadFlag("dotwin") ) + pDotNameWin = Abc_FrameReadFlag("dotwin"); + if ( Abc_FrameReadFlag("dotunix") ) + pDotNameUnix = Abc_FrameReadFlag("dotunix"); + #ifdef WIN32 - pProgDotName = "dot.exe"; - pProgGsViewName = NULL; + pDotName = pDotNameWin; #else - pProgDotName = "dot"; - pProgGsViewName = "gv"; + pDotName = pDotNameUnix; #endif - // check that the input file is okay + // check if the input DOT file is okay if ( (pFile = fopen( FileNameDot, "r" )) == NULL ) { fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); @@ -218,27 +223,20 @@ void Abc_ShowFile( char * FileNameDot ) } fclose( pFile ); - // get the generic file name - FileGeneric = Extra_FileNameGeneric( FileNameDot ); // create the PostScript file name + FileGeneric = Extra_FileNameGeneric( FileNameDot ); sprintf( FileNamePs, "%s.ps", FileGeneric ); free( FileGeneric ); - // generate the DOT file - sprintf( CommandDot, "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); + // generate the PostScript file using DOT + sprintf( CommandDot, "%s -Tps -o %s %s", pDotName, FileNamePs, FileNameDot ); RetValue = system( CommandDot ); -#ifdef WIN32 - _unlink( FileNameDot ); -#else - unlink( FileNameDot ); -#endif if ( RetValue == -1 ) { - fprintf( stdout, "Cannot find \"%s\".\n", pProgDotName ); + fprintf( stdout, "Command \"%s\" did not succeed.\n", CommandDot ); return; } - - // check that the input file is okay + // check that the input PostScript file is okay if ( (pFile = fopen( FileNamePs, "r" )) == NULL ) { fprintf( stdout, "Cannot open intermediate file \"%s\".\n", FileNamePs ); @@ -246,20 +244,33 @@ void Abc_ShowFile( char * FileNameDot ) } fclose( pFile ); + + // get GSVIEW names from the resource file + if ( Abc_FrameReadFlag("gsviewwin") ) + pGsNameWin = Abc_FrameReadFlag("gsviewwin"); + if ( Abc_FrameReadFlag("gsviewunix") ) + pGsNameUnix = Abc_FrameReadFlag("gsviewunix"); + + // spawn the viewer #ifdef WIN32 - if ( _spawnl( _P_NOWAIT, "gsview32.exe", "gsview32.exe", FileNamePs, NULL ) == -1 ) + _unlink( FileNameDot ); + if ( _spawnl( _P_NOWAIT, pGsNameWin, pGsNameWin, FileNamePs, NULL ) == -1 ) if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 ) { - fprintf( stdout, "Cannot find \"%s\".\n", "gsview32.exe" ); + fprintf( stdout, "Cannot find \"%s\".\n", pGsNameWin ); return; } #else - sprintf( CommandPs, "%s %s &", pProgGsViewName, FileNamePs ); - if ( system( CommandPs ) == -1 ) { - fprintf( stdout, "Cannot execute \"%s\".\n", FileNamePs ); - return; + char CommandPs[1000]; + unlink( FileNameDot ); + sprintf( CommandPs, "%s %s &", pGsNameUnix, FileNamePs ); + if ( system( CommandPs ) == -1 ) + { + fprintf( stdout, "Cannot execute \"%s\".\n", CommandPs ); + return; + } } #endif } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 30047d23..c9e0df68 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -546,7 +546,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !fProfile && !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "This command works only for AIGs.\n" ); + fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" ); return 1; } @@ -597,18 +597,23 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ); + int fVerbose; + extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -621,26 +626,25 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - if ( !Abc_NtkIsComb(pNtk) ) { fprintf( pErr, "This command works only for combinational networks.\n" ); return 1; } - if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "This command works only for AIGs.\n" ); + fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" ); return 1; } - vSuppFun = Sim_ComputeFunSupp( pNtk ); + vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose ); free( vSuppFun->pArray[0] ); Vec_PtrFree( vSuppFun ); return 0; usage: - fprintf( pErr, "usage: print_supp [-h]\n" ); + fprintf( pErr, "usage: print_supp [-vh]\n" ); fprintf( pErr, "\t prints the supports of the CO nodes\n" ); + fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -706,7 +710,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "This command works only for AIGs.\n" ); + fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" ); return 1; } Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose ); @@ -715,7 +719,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: print_symm [-nbvh]\n" ); fprintf( pErr, "\t computes symmetries of the PO functions\n" ); - fprintf( pErr, "\t-b : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" ); + fprintf( pErr, "\t-b : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "bdd": "sat" ); fprintf( pErr, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" ); fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -867,7 +871,7 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Visualizing cuts only works for AIGs.\n" ); + fprintf( pErr, "Visualizing cuts only works for AIGs (run \"strash\").\n" ); return 1; } if ( argc != util_optind + 1 ) @@ -942,7 +946,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" ); + fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" ); return 1; } Abc_NtkShowAig( pNtk ); @@ -1002,7 +1006,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Can only collapse a logic network.\n" ); + fprintf( pErr, "Can only collapse a logic network or an AIG.\n" ); return 1; } @@ -1262,7 +1266,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Cannot renode a network that is not an AIG.\n" ); + fprintf( pErr, "Cannot renode a network that is not an AIG (run \"strash\").\n" ); return 1; } @@ -1504,7 +1508,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsLogic(pNtk) ) { - fprintf( pErr, "Fast extract can only be applied to a logic network.\n" ); + fprintf( pErr, "Fast extract can only be applied to a logic network (run \"renode\").\n" ); Abc_NtkFxuFreeInfo( p ); return 1; } @@ -1717,7 +1721,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "This command can only be applied to an AIG.\n" ); + fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" ); return 1; } if ( Abc_NtkGetChoiceNum(pNtk) ) @@ -1826,7 +1830,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "This command can only be applied to an AIG.\n" ); + fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" ); return 1; } if ( Abc_NtkGetChoiceNum(pNtk) ) @@ -2322,7 +2326,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsLogic(pNtk) ) { - fprintf( stdout, "This command can only be applied to logic network.\n" ); + fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" ); return 0; } if ( Abc_NtkIsMappedLogic(pNtk) ) @@ -2397,7 +2401,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( stdout, "This command works only for AIGs.\n" ); + fprintf( stdout, "This command works only for AIGs (run \"strash\").\n" ); return 0; } if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) ) @@ -2751,7 +2755,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Cut computation is available only for AIGs.\n" ); + fprintf( pErr, "Cut computation is available only for AIGs (run \"strash\").\n" ); return 1; } pCutMan = Abc_NtkCuts( pNtk, pParams ); @@ -3606,7 +3610,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Works only for the AIG representation.\n" ); + fprintf( pErr, "Works only for the AIG representation (run \"strash\").\n" ); return 1; } @@ -3785,7 +3789,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Works only for AIG.\n" ); + fprintf( pErr, "Works only for AIG (run \"strash\").\n" ); return 1; } diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c index a8e06555..6ee1fb90 100644 --- a/src/base/abci/abcAttach.c +++ b/src/base/abci/abcAttach.c @@ -56,7 +56,6 @@ static int s_nPerms; ***********************************************************************/ int Abc_NtkAttach( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Mio_Library_t * pGenlib; unsigned ** puTruthGates; unsigned uTruths[6][2]; @@ -149,7 +148,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk ) printf( "Library gates are successfully attached to the nodes.\n" ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkAttach: The network check has failed.\n" ); return 0; diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 5042d0d5..40701e41 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -46,7 +46,6 @@ static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSupe ***********************************************************************/ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ) { - int fCheck = 1; Abc_Ntk_t * pNtkAig; assert( Abc_NtkIsStrash(pNtk) ); // perform balancing @@ -54,7 +53,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ) Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate ); Abc_NtkFinalize( pNtk, pNtkAig ); // make sure everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkAig ) ) + if ( !Abc_NtkCheck( pNtkAig ) ) { printf( "Abc_NtkBalance: The network check has failed.\n" ); Abc_NtkDelete( pNtkAig ); diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 4e359506..40370eff 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -44,7 +44,6 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, ***********************************************************************/ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); @@ -71,7 +70,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) Abc_NtkMinimumBase( pNtkNew ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkCollapse: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 013b7ac4..67665ad6 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -55,7 +55,6 @@ static int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int n ***********************************************************************/ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); @@ -78,7 +77,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool pNtk->pManGlob = NULL; // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkDsdGlobal: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); @@ -304,7 +303,6 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode ***********************************************************************/ int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive ) { - int fCheck = 1; Dsd_Manager_t * pManDsd; DdManager * dd = pNtk->pManFunc; Vec_Ptr_t * vNodes; @@ -328,7 +326,7 @@ int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive ) Dsd_ManagerStop( pManDsd ); // make sure everything is okay - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkDsdRecursive: The network check has failed.\n" ); return 0; diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c index f30325c0..55ae23ff 100644 --- a/src/base/abci/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -46,12 +46,11 @@ static Abc_Obj_t * Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNo ***********************************************************************/ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose ) { - int fCheck = 1; + int fShowSwitching = 1; Abc_Ntk_t * pNtkNew; Fpga_Man_t * pMan; Vec_Int_t * vSwitching; float * pSwitching = NULL; - int fShowSwitching = 0; assert( Abc_NtkIsStrash(pNtk) ); @@ -90,7 +89,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fV Abc_NtkMinimumBase( pNtkNew ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkFpga: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index fbe676a3..e82065fc 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -51,7 +51,6 @@ static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); ***********************************************************************/ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) { - int fCheck = 1; Fraig_Params_t * pPars = pParams; Abc_Ntk_t * pNtkNew; Fraig_Man_t * pMan; @@ -64,7 +63,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); Fraig_ManFree( pMan ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkFraig: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); @@ -249,7 +248,6 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai ***********************************************************************/ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; if ( !Abc_NtkIsSopLogic(pNtk) ) @@ -273,7 +271,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ) printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkFraigTrust: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); @@ -420,7 +418,6 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ) ***********************************************************************/ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) { - Abc_Frame_t * p; Abc_Ntk_t * pStore; int nAndsOld; @@ -431,8 +428,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) } // get the network currently stored - p = Abc_FrameGetGlobalFrame(); - pStore = Abc_FrameReadNtkStore(p); + pStore = Abc_FrameReadNtkStore(); if ( pStore == NULL ) { // start the stored network @@ -443,8 +439,8 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) return 0; } // save the parameters - Abc_FrameSetNtkStore( p, pStore ); - Abc_FrameSetNtkStoreSize( p, 1 ); + Abc_FrameSetNtkStore( pStore ); + Abc_FrameSetNtkStoreSize( 1 ); nAndsOld = 0; } else @@ -457,7 +453,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) return 0; } // set the number of networks stored - Abc_FrameSetNtkStoreSize( p, Abc_FrameReadNtkStoreSize(p) + 1 ); + Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 ); } printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); return 1; @@ -476,22 +472,20 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkFraigRestore() { - Abc_Frame_t * p; Fraig_Params_t Params; Abc_Ntk_t * pStore, * pFraig; int nWords1, nWords2, nWordsMin; // get the stored network - p = Abc_FrameGetGlobalFrame(); - pStore = Abc_FrameReadNtkStore(p); - Abc_FrameSetNtkStore( p, NULL ); + pStore = Abc_FrameReadNtkStore(); + Abc_FrameSetNtkStore( NULL ); if ( pStore == NULL ) { printf( "There are no network currently in storage.\n" ); return NULL; } printf( "Currently stored %d networks with %d nodes will be fraiged.\n", - Abc_FrameReadNtkStoreSize(p), Abc_NtkNodeNum(pStore) ); + Abc_FrameReadNtkStoreSize(), Abc_NtkNodeNum(pStore) ); // to determine the number of simulation patterns // use the following strategy @@ -536,14 +530,12 @@ Abc_Ntk_t * Abc_NtkFraigRestore() ***********************************************************************/ void Abc_NtkFraigStoreClean() { - Abc_Frame_t * p; Abc_Ntk_t * pStore; // get the stored network - p = Abc_FrameGetGlobalFrame(); - pStore = Abc_FrameReadNtkStore(p); + pStore = Abc_FrameReadNtkStore(); if ( pStore ) Abc_NtkDelete( pStore ); - Abc_FrameSetNtkStore( p, NULL ); + Abc_FrameSetNtkStore( NULL ); } /**Function************************************************************* diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index 0c8994e1..3a70862f 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -52,8 +52,6 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p ); ***********************************************************************/ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) { - int fCheck = 1; - assert( Abc_NtkIsLogic(pNtk) ); // convert nodes to SOPs if ( Abc_NtkIsMappedLogic(pNtk) ) @@ -81,7 +79,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) // update the network Abc_NtkFxuReconstruct( pNtk, p ); // make sure everything is okay - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) printf( "Abc_NtkFastExtract: The network check has failed.\n" ); return 1; } diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 45f600ed..ec5352cb 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -56,7 +56,6 @@ static Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Sup ***********************************************************************/ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Map_Man_t * pMan; Vec_Int_t * vSwitching; @@ -106,7 +105,7 @@ clk = clock(); Map_ManFree( pMan ); return NULL; } - Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk ); +// Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk ); // reconstruct the network after mapping pNtkNew = Abc_NtkFromMap( pMan, pNtk ); @@ -115,7 +114,7 @@ clk = clock(); Map_ManFree( pMan ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkMap: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); @@ -440,7 +439,6 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Map_Man_t * pMan; @@ -483,7 +481,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ) Map_ManFree( pMan ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkMap: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 0d75ba1f..68dccd18 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -77,7 +77,6 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) { - int fCheck = 1; char Buffer[100]; Abc_Ntk_t * pNtkMiter; @@ -96,7 +95,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkMiter ) ) + if ( !Abc_NtkCheck( pNtkMiter ) ) { printf( "Abc_NtkMiter: The network check has failed.\n" ); Abc_NtkDelete( pNtkMiter ); @@ -312,7 +311,6 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt ***********************************************************************/ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ) { - int fCheck = 1; char Buffer[100]; Abc_Ntk_t * pNtkMiter; Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter; @@ -357,7 +355,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkMiter ) ) + if ( !Abc_NtkCheck( pNtkMiter ) ) { printf( "Abc_NtkMiter: The network check has failed.\n" ); Abc_NtkDelete( pNtkMiter ); @@ -470,7 +468,6 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) { - int fCheck = 1; char Buffer[100]; ProgressBar * pProgress; Abc_Ntk_t * pNtkFrames; @@ -531,7 +528,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) } } // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkFrames ) ) + if ( !Abc_NtkCheck( pNtkFrames ) ) { printf( "Abc_NtkFrames: The network check has failed.\n" ); Abc_NtkDelete( pNtkFrames ); diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 61c1a110..6362a925 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -119,14 +119,13 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo ***********************************************************************/ Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsBddLogic(pNtk) ); pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP ); Abc_NtkBddToMuxesPerform( pNtk, pNtkNew ); Abc_NtkFinalize( pNtk, pNtkNew ); // make sure everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkBddToMuxes: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c index 766c14f3..60a02aed 100644 --- a/src/base/abci/abcReconv.c +++ b/src/base/abci/abcReconv.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [abcRes.c] + FileName [abcReconv.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - Synopsis [Reconvergence=driven cut computation.] + Synopsis [Computation of reconvergence-driven cuts.] Author [Alan Mishchenko] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abcReconv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 791d2d53..92d497fc 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [abcResRef.c] + FileName [abcRefactor.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - Synopsis [Resynthesis based on refactoring.] + Synopsis [Resynthesis based on collapsing and refactoring.] Author [Alan Mishchenko] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abcRefactor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -82,7 +82,6 @@ static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec ***********************************************************************/ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose ) { - int fCheck = 1; ProgressBar * pProgress; Abc_ManRef_t * pManRef; Abc_ManCut_t * pManCut; @@ -110,6 +109,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool // skip the constant node if ( Abc_NodeIsConst(pNode) ) continue; + // skip the nodes with many fanouts + if ( Abc_ObjFanoutNum(pNode) > 1000 ) + continue; // stop if all nodes have been tried once if ( i >= nNodes ) break; @@ -140,7 +142,7 @@ pManRef->timeTotal = clock() - clkStart; Abc_NtkManRefStop( pManRef ); Abc_NtkStopReverseLevels( pNtk ); // check - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkRefactor: The network check has failed.\n" ); return 0; diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index c77c0d70..165777f8 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [Procedures which transform an AIG into the network of nodes.] + Synopsis [Procedures which transform an AIG into the network of SOP logic nodes.] Author [Alan Mishchenko] @@ -52,7 +52,6 @@ static void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone ); ***********************************************************************/ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); @@ -93,7 +92,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn //printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) ); // make sure everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkRenode: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index 75fe1627..ea221296 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [abcRes.c] + FileName [abcRewrite.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - Synopsis [Technology-independent resynthesis of the AIG.] + Synopsis [Technology-independent resynthesis of the AIG based on DAG aware rewriting.] Author [Alan Mishchenko] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abcRewrite.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -22,6 +22,12 @@ #include "rwr.h" #include "dec.h" +/* + The ideas realized in this package are inspired by the paper: + Per Bjesse, Arne Boralv, "DAG-aware circuit compression for + formal verification", Proc. ICCAD 2004, pp. 42-49. +*/ + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,7 +52,6 @@ static void Abc_NodePrintCuts( Abc_Obj_t * pNode ); ***********************************************************************/ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose ) { - int fCheck = 1; int fDrop = 0; ProgressBar * pProgress; Cut_Man_t * pManCut; @@ -81,6 +86,9 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk ); // skip the constant node if ( Abc_NodeIsConst(pNode) ) continue; + // skip the nodes with many fanouts + if ( Abc_ObjFanoutNum(pNode) > 1000 ) + continue; // for each cut, try to resynthesize it nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros ); if ( nGain > 0 || nGain == 0 && fUseZeros ) @@ -104,7 +112,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); pNtk->pManCut = NULL; Abc_NtkStopReverseLevels( pNtk ); // check - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkRewrite: The network check has failed.\n" ); return 0; diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 935f1300..de87a1e9 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -51,7 +51,6 @@ extern char * Mio_GateReadSop( void * pGate ); ***********************************************************************/ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) { - int fCheck = 1; Abc_Ntk_t * pNtkAig; int nNodes; @@ -74,7 +73,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) if ( pNtk->pExdc ) pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 ); // make sure everything is okay - if ( fCheck && !Abc_NtkCheck( pNtkAig ) ) + if ( !Abc_NtkCheck( pNtkAig ) ) { printf( "Abc_NtkStrash: The network check has failed.\n" ); Abc_NtkDelete( pNtkAig ); @@ -99,7 +98,6 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) ***********************************************************************/ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) { - int fCheck = 1; Abc_Obj_t * pObj; int i; // the first network should be an AIG @@ -118,7 +116,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) // add pNtk2 to pNtk1 while strashing Abc_NtkStrashPerform( pNtk2, pNtk1, 1 ); // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtk1 ) ) + if ( !Abc_NtkCheck( pNtk1 ) ) { printf( "Abc_NtkAppend: The network check has failed.\n" ); return 0; diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index ca9bd34e..7000ecad 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -56,7 +56,6 @@ static void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF ***********************************************************************/ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) { - int fCheck = 1; Fraig_Params_t Params; Abc_Ntk_t * pNtkAig; Fraig_Man_t * pMan; @@ -83,7 +82,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) // cleanup the dangling nodes Abc_NtkCleanup( pNtk, fVerbose ); // check - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkFraigSweep: The network check has failed.\n" ); return 0; @@ -394,7 +393,6 @@ int Abc_NodeDroppingCost( Abc_Obj_t * pNode ) ***********************************************************************/ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ) { - int fCheck = 1; Vec_Ptr_t * vNodes; Abc_Obj_t * pNode; int i, Counter; @@ -423,7 +421,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ) if ( fVerbose ) printf( "Cleanup removed %d dangling nodes.\n", Counter ); // check - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkCleanup: The network check has failed.\n" ); return -1; @@ -447,7 +445,6 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ) ***********************************************************************/ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) { - int fCheck = 1; Abc_Obj_t * pNode; int i, fConvert, nSwept, nSweptNew; assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsBddLogic(pNtk) ); @@ -481,7 +478,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) if ( fVerbose ) printf( "Sweep removed %d nodes.\n", nSwept ); // check - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheck( pNtk ) ) { printf( "Abc_NtkSweep: The network check has failed.\n" ); return -1; diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c index f9229639..f1e427c0 100644 --- a/src/base/abci/abcSymm.c +++ b/src/base/abci/abcSymm.c @@ -46,7 +46,7 @@ static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms ) ***********************************************************************/ void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose ) { - if ( fUseBdds || fNaive ) + if ( fUseBdds ) Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose ); else Abc_NtkSymmetriesUsingSandS( pNtk, fVerbose ); @@ -65,8 +65,8 @@ void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose ***********************************************************************/ void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose ) { - extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ); - int nSymms = Sim_ComputeTwoVarSymms( pNtk ); + extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose ); + int nSymms = Sim_ComputeTwoVarSymms( pNtk, fVerbose ); printf( "The total number of symmetries is %d.\n", nSymms ); } @@ -123,12 +123,14 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer Abc_Obj_t * pNode; DdNode * bFunc; int nSymms = 0; + int nSupps = 0; int i; // compute symmetry info for each PO Abc_NtkForEachCo( pNtk, pNode, i ) { bFunc = pNtk->vFuncsGlob->pArray[i]; + nSupps += Cudd_SupportSize( dd, bFunc ); if ( Cudd_IsConstant(bFunc) ) continue; if ( fNaive ) @@ -144,7 +146,8 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer //Extra_SymmPairsPrint( pSymms ); Extra_SymmPairsDissolve( pSymms ); } - printf( "The total number of symmetries is %d.\n", nSymms ); + printf( "Total number of vars in functional supports = %8d.\n", nSupps ); + printf( "Total number of two-variable symmetries = %8d.\n", nSymms ); } /**Function************************************************************* diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 0fe3ec63..abc02cc3 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -46,7 +46,6 @@ static Abc_Ntk_t * Abc_NtkConstructExdc ( DdManager * dd, Abc_Ntk_t * pNtk, ***********************************************************************/ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) { - int fCheck = 1; int fReorder = 1; DdManager * dd; DdNode * bRelation, * bInitial, * bUnreach; @@ -94,7 +93,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) pNtk->pManGlob = NULL; // make sure that everything is okay - if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) ) + if ( !Abc_NtkCheck( pNtk->pExdc ) ) { printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" ); Abc_NtkDelete( pNtk->pExdc ); diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c index d6b1b8e5..a41edac1 100644 --- a/src/base/abcs/abcSeq.c +++ b/src/base/abcs/abcSeq.c @@ -60,7 +60,6 @@ static void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches ); ***********************************************************************/ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Abc_Aig_t * pManNew; Vec_Ptr_t * vNodes; @@ -176,7 +175,7 @@ printf( "\n" ); if ( pNtk->pExdc ) fprintf( stdout, "Warning: EXDC is dropped when converting to sequential AIG.\n" ); - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" ); return pNtkNew; } @@ -194,7 +193,6 @@ printf( "\n" ); ***********************************************************************/ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) { - int fCheck = 1; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pFanin, * pFaninNew; int i, k, c; @@ -233,7 +231,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) // duplicate the EXDC network if ( pNtk->pExdc ) fprintf( stdout, "Warning: EXDC network is not copied.\n" ); - if ( fCheck && !Abc_NtkCheck( pNtkNew ) ) + if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" ); return pNtkNew; } diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 84c330bf..9195554a 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -29,7 +29,6 @@ static int CmdCommandTime ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandEcho ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandQuit ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int CmdCommandUsage ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandWhich ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandHistory ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandAlias ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -70,7 +69,6 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "time", CmdCommandTime, 0); Cmd_CommandAdd( pAbc, "Basic", "echo", CmdCommandEcho, 0); Cmd_CommandAdd( pAbc, "Basic", "quit", CmdCommandQuit, 0); -// Cmd_CommandAdd( pAbc, "Basic", "usage", CmdCommandUsage, 0); Cmd_CommandAdd( pAbc, "Basic", "history", CmdCommandHistory, 0); Cmd_CommandAdd( pAbc, "Basic", "alias", CmdCommandAlias, 0); Cmd_CommandAdd( pAbc, "Basic", "unalias", CmdCommandUnalias, 0); @@ -79,7 +77,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "set", CmdCommandSetVariable, 0); Cmd_CommandAdd( pAbc, "Basic", "unset", CmdCommandUnsetVariable, 0); Cmd_CommandAdd( pAbc, "Basic", "undo", CmdCommandUndo, 0); -// Cmd_CommandAdd( pAbc, "Basic", "recall", CmdCommandRecall, 0); + Cmd_CommandAdd( pAbc, "Basic", "recall", CmdCommandRecall, 0); Cmd_CommandAdd( pAbc, "Basic", "empty", CmdCommandEmpty, 0); #ifdef WIN32 Cmd_CommandAdd( pAbc, "Basic", "ls", CmdCommandLs, 0 ); @@ -275,45 +273,6 @@ int CmdCommandQuit( Abc_Frame_t * pAbc, int argc, char **argv ) SeeAlso [] ******************************************************************************/ -int CmdCommandUsage( Abc_Frame_t * pAbc, int argc, char **argv ) -{ - int c; - - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) - { - switch ( c ) - { - case 'h': - goto usage; - break; - default: - goto usage; - } - } - - if ( argc != util_optind ) - goto usage; - util_print_cpu_stats( pAbc->Out ); - return 0; - - usage: - fprintf( pAbc->Err, "usage: usage [-h]\n" ); - fprintf( pAbc->Err, " -h \t\tprint the command usage\n" ); - return 1; -} - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ int CmdCommandWhich( Abc_Frame_t * pAbc, int argc, char **argv ) { return 0; @@ -332,11 +291,9 @@ int CmdCommandWhich( Abc_Frame_t * pAbc, int argc, char **argv ) ******************************************************************************/ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) { - int i, num; - int size; - int c; - num = 50; + int i, c, num, size; + num = 20; util_getopt_reset(); while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) { @@ -344,23 +301,28 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) { case 'h': goto usage; - break; + default : + goto usage; } } - - if ( argc > 3 ) + if ( argc > 2 ) goto usage; + // get the number of commands to print + if ( argc == util_optind + 1 ) + num = atoi(argv[util_optind]); + // print the commands size = pAbc->aHistory->nSize; num = ( num < size ) ? num : size; for ( i = size - num; i < size; i++ ) fprintf( pAbc->Out, "%s", pAbc->aHistory->pArray[i] ); return 0; - usage: - fprintf( pAbc->Err, "usage: history [-h] [num]\n" ); - fprintf( pAbc->Err, " -h \t\tprint the command usage\n" ); - fprintf( pAbc->Err, " num \t\tprint the last num commands\n" ); +usage: + fprintf( pAbc->Err, "usage: history [-h] <num>\n" ); + fprintf( pAbc->Err, " prints the latest command entered on the command line\n" ); + fprintf( pAbc->Err, " -h : print the command usage\n" ); + fprintf( pAbc->Err, "num : print the last num commands\n" ); return ( 1 ); } @@ -378,7 +340,6 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv ) { char *key, *value; - st_generator *gen; int c; util_getopt_reset(); @@ -397,8 +358,7 @@ int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv ) if ( argc == 1 ) { - st_foreach_item( pAbc->tAliases, gen, &key, &value ) - CmdCommandAliasPrint( pAbc, ( Abc_Alias * ) value ); + CmdPrintTable( pAbc->tAliases, 1 ); return 0; } @@ -712,7 +672,6 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) { char *flag_value, *key, *value; - st_generator *gen; int c; util_getopt_reset(); @@ -722,7 +681,6 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) { case 'h': goto usage; - break; default: goto usage; } @@ -733,10 +691,7 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) } else if ( argc == 1 ) { - st_foreach_item( pAbc->tFlags, gen, &key, &value ) - { - fprintf( pAbc->Out, "%s\t%s\n", key, value ); - } + CmdPrintTable( pAbc->tFlags, 0 ); return 0; } else @@ -749,25 +704,18 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) } flag_value = argc == 2 ? util_strsav( "" ) : util_strsav( argv[2] ); - - ( void ) st_insert( pAbc->tFlags, util_strsav( argv[1] ), - flag_value ); +// flag_value = argc == 2 ? NULL : util_strsav(argv[2]); + st_insert( pAbc->tFlags, util_strsav(argv[1]), flag_value ); if ( strcmp( argv[1], "abcout" ) == 0 ) { if ( pAbc->Out != stdout ) - { - ( void ) fclose( pAbc->Out ); - } + fclose( pAbc->Out ); if ( strcmp( flag_value, "" ) == 0 ) - { flag_value = "-"; - } pAbc->Out = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); if ( pAbc->Out == NULL ) - { pAbc->Out = stdout; - } #if HAVE_SETVBUF setvbuf( pAbc->Out, ( char * ) NULL, _IOLBF, 0 ); #endif @@ -775,18 +723,12 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) if ( strcmp( argv[1], "abcerr" ) == 0 ) { if ( pAbc->Err != stderr ) - { - ( void ) fclose( pAbc->Err ); - } + fclose( pAbc->Err ); if ( strcmp( flag_value, "" ) == 0 ) - { flag_value = "-"; - } pAbc->Err = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); if ( pAbc->Err == NULL ) - { pAbc->Err = stderr; - } #if HAVE_SETVBUF setvbuf( pAbc->Err, ( char * ) NULL, _IOLBF, 0 ); #endif @@ -794,28 +736,21 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) if ( strcmp( argv[1], "history" ) == 0 ) { if ( pAbc->Hst != NIL( FILE ) ) - { - ( void ) fclose( pAbc->Hst ); - } + fclose( pAbc->Hst ); if ( strcmp( flag_value, "" ) == 0 ) - { pAbc->Hst = NIL( FILE ); - } else { - pAbc->Hst = - CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); + pAbc->Hst = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); if ( pAbc->Hst == NULL ) - { pAbc->Hst = NIL( FILE ); - } } } return 0; } usage: - fprintf( pAbc->Err, "usage: set [-h] [name] [value]\n" ); + fprintf( pAbc->Err, "usage: set [-h] <name> <value>\n" ); fprintf( pAbc->Err, "\t sets the value of parameter <name>\n" ); fprintf( pAbc->Err, "\t-h : print the command usage\n" ); return 1; @@ -870,8 +805,9 @@ int CmdCommandUnsetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) usage: - fprintf( pAbc->Err, "usage: unset [-h] variables \n" ); - fprintf( pAbc->Err, " -h \t\tprint the command usage\n" ); + fprintf( pAbc->Err, "usage: unset [-h] <name> \n" ); + fprintf( pAbc->Err, "\t removes the value of parameter <name>\n" ); + fprintf( pAbc->Err, "\t-h : print the command usage\n" ); return 1; } @@ -1014,9 +950,10 @@ int CmdCommandRecall( Abc_Frame_t * pAbc, int argc, char **argv ) usage: - fprintf( pAbc->Err, "usage: recall <num>\n" ); + fprintf( pAbc->Err, "usage: recall -h <num>\n" ); fprintf( pAbc->Err, " set the current network to be one of the previous networks\n" ); fprintf( pAbc->Err, "<num> : level to return to [default = previous]\n" ); + fprintf( pAbc->Err, " -h : print the command usage\n"); return 1; } @@ -1260,7 +1197,9 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) { FILE * pFile; FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkNew; + Abc_Ntk_t * pNtk, * pNtkNew, * pNetlist; + char * pNameWin = "sis.exe"; + char * pNameUnix = "sis"; char Command[1000], Buffer[100]; char * pSisName; int i; @@ -1288,23 +1227,28 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) if ( strcmp( argv[1], "-?" ) == 0 ) goto usage; + // get the names from the resource file + if ( Cmd_FlagReadByName(pAbc, "siswin") ) + pNameWin = Cmd_FlagReadByName(pAbc, "siswin"); + if ( Cmd_FlagReadByName(pAbc, "sisunix") ) + pNameUnix = Cmd_FlagReadByName(pAbc, "sisunix"); + // check if SIS is available - if ( (pFile = fopen( "sis.exe", "r" )) ) - pSisName = "sis.exe"; - else if ( (pFile = fopen( "sis", "r" )) ) - pSisName = "sis"; + if ( (pFile = fopen( pNameWin, "r" )) ) + pSisName = pNameWin; + else if ( (pFile = fopen( pNameUnix, "r" )) ) + pSisName = pNameUnix; else if ( pFile == NULL ) { - fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", "sis.exe", "sis" ); + fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pNameWin, pNameUnix ); goto usage; } fclose( pFile ); - if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); - // write out the current network - Io_WriteBlifLogic( pNtk, "_sis_in.blif", 1 ); + pNetlist = Abc_NtkLogicToNetlist(pNtk); + Io_WriteBlif( pNetlist, "_sis_in.blif", 1 ); + Abc_NtkDelete( pNetlist ); // create the file for sis sprintf( Command, "%s -x -c ", pSisName ); @@ -1383,8 +1327,10 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) { FILE * pFile; FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkNew; + Abc_Ntk_t * pNtk, * pNtkNew, * pNetlist; char Command[1000], Buffer[100]; + char * pNameWin = "mvsis.exe"; + char * pNameUnix = "mvsis"; char * pMvsisName; int i; @@ -1411,23 +1357,29 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) if ( strcmp( argv[1], "-?" ) == 0 ) goto usage; + // get the names from the resource file + if ( Cmd_FlagReadByName(pAbc, "mvsiswin") ) + pNameWin = Cmd_FlagReadByName(pAbc, "mvsiswin"); + if ( Cmd_FlagReadByName(pAbc, "mvsisunix") ) + pNameUnix = Cmd_FlagReadByName(pAbc, "mvsisunix"); + // check if MVSIS is available - if ( (pFile = fopen( "mvsis.exe", "r" )) ) - pMvsisName = "mvsis.exe"; - else if ( (pFile = fopen( "mvsis", "r" )) ) - pMvsisName = "mvsis"; + if ( (pFile = fopen( pNameWin, "r" )) ) + pMvsisName = pNameWin; + else if ( (pFile = fopen( pNameUnix, "r" )) ) + pMvsisName = pNameUnix; else if ( pFile == NULL ) { - fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", "mvsis.exe", "mvsis" ); + fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pNameWin, pNameUnix ); goto usage; } fclose( pFile ); - if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk); // write out the current network - Io_WriteBlifLogic( pNtk, "_mvsis_in.blif", 1 ); + pNetlist = Abc_NtkLogicToNetlist(pNtk); + Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 ); + Abc_NtkDelete( pNetlist ); // create the file for MVSIS sprintf( Command, "%s -x -c ", pMvsisName ); diff --git a/src/base/cmd/cmdAlias.c b/src/base/cmd/cmdAlias.c index 37220ef0..59a8b87e 100644 --- a/src/base/cmd/cmdAlias.c +++ b/src/base/cmd/cmdAlias.c @@ -68,7 +68,7 @@ void CmdCommandAliasAdd( Abc_Frame_t * pAbc, char * sName, int argc, char ** arg void CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias ) { int i; - fprintf(pAbc->Out, "%s\t", pAlias->sName); + fprintf(pAbc->Out, "%-15s", pAlias->sName); for(i = 0; i < pAlias->argc; i++) fprintf( pAbc->Out, " %s", pAlias->argv[i] ); fprintf( pAbc->Out, "\n" ); diff --git a/src/base/cmd/cmdFlag.c b/src/base/cmd/cmdFlag.c index 96f1f251..63a0389d 100644 --- a/src/base/cmd/cmdFlag.c +++ b/src/base/cmd/cmdFlag.c @@ -43,14 +43,10 @@ ******************************************************************************/ char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag ) { - char *value; - - if (st_lookup(pAbc->tFlags, flag, &value)) { - return value; - } - else { - return NIL(char); - } + char * value; + if ( st_lookup(pAbc->tFlags, flag, &value) ) + return value; + return NULL; } @@ -65,19 +61,17 @@ char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag ) ******************************************************************************/ void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value ) { - char *oldValue, *newValue; - - if (!key) - return; - if (value) - newValue = util_strsav(value); - else - newValue = util_strsav(""); - - if (st_delete(pAbc->tFlags, &key, &oldValue)) - FREE(oldValue); - - st_insert(pAbc->tFlags, key, newValue); + char * oldValue, * newValue; + if ( !key ) + return; + if ( value ) + newValue = util_strsav(value); + else + newValue = util_strsav(""); +// newValue = NULL; + if ( st_delete(pAbc->tFlags, &key, &oldValue) ) + FREE(oldValue); + st_insert( pAbc->tFlags, key, newValue ); } @@ -92,15 +86,14 @@ void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value ) ******************************************************************************/ void Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, char * key ) { - char *value; - - if (!key) - return; - - if (st_delete(pAbc->tFlags, &key, &value)) { - FREE(key); - FREE(value); - } + char *value; + if ( !key ) + return; + if ( st_delete( pAbc->tFlags, &key, &value ) ) + { + FREE(key); + FREE(value); + } } diff --git a/src/base/cmd/cmdInt.h b/src/base/cmd/cmdInt.h index f0289ad4..d110b634 100644 --- a/src/base/cmd/cmdInt.h +++ b/src/base/cmd/cmdInt.h @@ -73,6 +73,7 @@ extern FILE * CmdFileOpen( Abc_Frame_t * pAbc, char * sFileName, char * sMod extern void CmdFreeArgv( int argc, char ** argv ); extern void CmdCommandFree( Abc_Command * pCommand ); extern void CmdCommandPrint( Abc_Frame_t * pAbc, bool fPrintAll ); +extern void CmdPrintTable( st_table * tTable, int fAliases ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index 67a290a2..71396d3e 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -110,7 +110,7 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv ) // get the backup network if the command is going to change the network if ( pCommand->fChange ) { - if ( pAbc->pNtkCur ) + if ( pAbc->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) ) { pNetCopy = Abc_NtkDup( pAbc->pNtkCur ); Abc_FrameSetCurrentNetwork( pAbc, pNetCopy ); @@ -122,15 +122,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv ) // execute the command clk = util_cpu_time(); - pFunc = ( int (*)( Abc_Frame_t *, int, char ** ) ) pCommand->pFunc; + pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc; fError = (*pFunc)( pAbc, argc, argv ); pAbc->TimeCommand += (util_cpu_time() - clk); -// if ( !fError && pCommand->fChange && pAbc->pNtkCur ) -// { -// Cmd_HistoryAddSnapshot(pAbc, pAbc->pNet); -// } - // automatic execution of arbitrary command after each command // usually this is a passive command ... if ( fError == 0 && !pAbc->fAutoexac ) @@ -592,6 +587,62 @@ int CmdCommandPrintCompare( Abc_Command ** ppC1, Abc_Command ** ppC2 ) assert( 0 ); return 0; } + +/**Function************************************************************* + + Synopsis [Comparision function used for sorting commands.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int CmdNamePrintCompare( char ** ppC1, char ** ppC2 ) +{ + return strcmp( *ppC1, *ppC2 ); +} + +/**Function************************************************************* + + Synopsis [Comparision function used for sorting commands.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CmdPrintTable( st_table * tTable, int fAliases ) +{ + st_generator * gen; + char ** ppNames; + char * key, * value; + int nNames, i; + + // collect keys in the array + ppNames = ALLOC( char *, st_count(tTable) ); + nNames = 0; + st_foreach_item( tTable, gen, &key, &value ) + ppNames[nNames++] = key; + + // sort array by name + qsort( (void *)ppNames, nNames, sizeof(char *), + (int (*)(const void *, const void *))CmdNamePrintCompare ); + + // print in this order + for ( i = 0; i < nNames; i++ ) + { + st_lookup( tTable, ppNames[i], &value ); + if ( fAliases ) + CmdCommandAliasPrint( Abc_FrameGetGlobalFrame(), (Abc_Alias *)value ); + else + fprintf( stdout, "%-15s %-15s\n", ppNames[i], value ); + } + free( ppNames ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index dd571f91..393b2216 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck ) return NULL; // make sure that everything is okay with the network structure - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheckRead( pNtk ) ) { printf( "Io_ReadBench: The network check has failed.\n" ); Abc_NtkDelete( pNtk ); diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index b5dc2fa8..946de42b 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -109,7 +109,7 @@ Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ) Io_ReadBlifFree( p ); // make sure that everything is okay with the network structure - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheckRead( pNtk ) ) { printf( "Io_ReadBlif: The network check has failed.\n" ); Abc_NtkDelete( pNtk ); diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c index 172849bd..48a1722b 100644 --- a/src/base/io/ioReadEdif.c +++ b/src/base/io/ioReadEdif.c @@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ) return NULL; // make sure that everything is okay with the network structure - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheckRead( pNtk ) ) { printf( "Io_ReadEdif: The network check has failed.\n" ); Abc_NtkDelete( pNtk ); diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c index 54890729..20d30a1a 100644 --- a/src/base/io/ioReadEqn.c +++ b/src/base/io/ioReadEqn.c @@ -61,7 +61,7 @@ Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ) return NULL; // make sure that everything is okay with the network structure - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheckRead( pNtk ) ) { printf( "Io_ReadEqn: The network check has failed.\n" ); Abc_NtkDelete( pNtk ); diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index c4b4084c..1e54db5f 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck ) return NULL; // make sure that everything is okay with the network structure - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheckRead( pNtk ) ) { printf( "Io_ReadPla: The network check has failed.\n" ); Abc_NtkDelete( pNtk ); diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c index 53299a0c..f4855dde 100644 --- a/src/base/io/ioReadVerilog.c +++ b/src/base/io/ioReadVerilog.c @@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ) return NULL; // make sure that everything is okay with the network structure - if ( fCheck && !Abc_NtkCheck( pNtk ) ) + if ( fCheck && !Abc_NtkCheckRead( pNtk ) ) { printf( "Io_ReadVerilog: The network check has failed.\n" ); Abc_NtkDelete( pNtk ); diff --git a/src/base/main/main.c b/src/base/main/main.c index a3fd979a..0622a3bd 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -231,29 +231,22 @@ usage: Synopsis [Returns 1 if s is a file type recognized, else returns 0.] - Description [Returns 1 if s is a file type recognized by VIS, else returns - 0. Recognized types are "blif", "blif_mv", "blif_mvs", and "none".] + Description [Returns 1 if s is a file type recognized by ABC, else returns 0. + Recognized types are "blif", "bench", "pla", and "none".] SideEffects [] ******************************************************************************/ -static int -TypeCheck( - Abc_Frame_t * pAbc, - char * s) +static int TypeCheck( Abc_Frame_t * pAbc, char * s ) { - if (strcmp(s, "blif") == 0) { + if (strcmp(s, "blif") == 0) return 1; - } - else if (strcmp(s, "blif_mv") == 0) { + else if (strcmp(s, "bench") == 0) return 1; - } - else if (strcmp(s, "blif_mvs") == 0) { + else if (strcmp(s, "pla") == 0) return 1; - } - else if (strcmp(s, "none") == 0) { + else if (strcmp(s, "none") == 0) return 1; - } else { fprintf( pAbc->Err, "unknown type %s\n", s ); return 0; diff --git a/src/base/main/main.h b/src/base/main/main.h index 72eec599..0d47dec5 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -90,21 +90,22 @@ extern void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p ); extern void Abc_FrameSetGlobalFrame( Abc_Frame_t * p ); extern Abc_Frame_t * Abc_FrameGetGlobalFrame(); -extern Abc_Ntk_t * Abc_FrameReadNtkStore ( Abc_Frame_t * pFrame ); -extern int Abc_FrameReadNtkStoreSize ( Abc_Frame_t * pFrame ); -extern void Abc_FrameSetNtkStore ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk ); -extern void Abc_FrameSetNtkStoreSize ( Abc_Frame_t * pFrame, int nStored ); - -extern void * Abc_FrameReadLibLut ( Abc_Frame_t * pFrame ); -extern void * Abc_FrameReadLibGen ( Abc_Frame_t * pFrame ); -extern void * Abc_FrameReadLibSuper ( Abc_Frame_t * pFrame ); -extern void Abc_FrameSetLibLut ( Abc_Frame_t * pFrame, void * pLib ); -extern void Abc_FrameSetLibGen ( Abc_Frame_t * pFrame, void * pLib ); -extern void Abc_FrameSetLibSuper ( Abc_Frame_t * pFrame, void * pLib ); - -extern void * Abc_FrameReadManDd ( Abc_Frame_t * pFrame ); -extern void * Abc_FrameReadManDec ( Abc_Frame_t * pFrame ); - +extern Abc_Ntk_t * Abc_FrameReadNtkStore(); +extern int Abc_FrameReadNtkStoreSize(); +extern void * Abc_FrameReadLibLut(); +extern void * Abc_FrameReadLibGen(); +extern void * Abc_FrameReadLibSuper(); +extern void * Abc_FrameReadManDd(); +extern void * Abc_FrameReadManDec(); +extern char * Abc_FrameReadFlag( char * pFlag ); +extern bool Abc_FrameIsFlagEnabled( char * pFlag ); + +extern void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); +extern void Abc_FrameSetNtkStoreSize( int nStored ); +extern void Abc_FrameSetLibLut( void * pLib ); +extern void Abc_FrameSetLibGen( void * pLib ); +extern void Abc_FrameSetLibSuper( void * pLib ); +extern void Abc_FrameSetFlag( char * pFlag, char * pValue ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 09a750ea..77c9f579 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -26,7 +26,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Frame_t * Abc_FrameGlobalFrame = 0; +static Abc_Frame_t * s_GlobalFrame = NULL; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -34,6 +34,57 @@ static Abc_Frame_t * Abc_FrameGlobalFrame = 0; /**Function************************************************************* + Synopsis [APIs to access parameters in the flobal frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_FrameReadNtkStore() { return s_GlobalFrame->pStored; } +int Abc_FrameReadNtkStoreSize() { return s_GlobalFrame->nStored; } +void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut; } +void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; } +void * Abc_FrameReadLibSuper() { return s_GlobalFrame->pLibSuper; } +void * Abc_FrameReadManDd() { return s_GlobalFrame->dd; } +void * Abc_FrameReadManDec() { return s_GlobalFrame->pManDec; } +char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); } + +void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored = pNtk; } +void Abc_FrameSetNtkStoreSize( int nStored ) { s_GlobalFrame->nStored = nStored; } +void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; } +void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; } +void Abc_FrameSetLibSuper( void * pLib ) { s_GlobalFrame->pLibSuper = pLib; } +void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue ); } + +/**Function************************************************************* + + Synopsis [Returns 1 if the flag is enabled without value or with value 1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_FrameIsFlagEnabled( char * pFlag ) +{ + char * pValue; + // if flag is not defined, it is not enabled + pValue = Abc_FrameReadFlag( pFlag ); + if ( pValue == NULL ) + return 0; + // if flag is defined but value is not empty (no parameter) or "1", it is not enabled + if ( strcmp(pValue, "") && strcmp(pValue, "1") ) + return 0; + return 1; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -311,7 +362,7 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk ) return; // transfer the parameters to the new network - if ( p->pNtkCur ) + if ( p->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) ) { Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) ); Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) ); @@ -322,6 +373,9 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk ) { Abc_NtkSetBackup( pNtk, NULL ); Abc_NtkSetStep( pNtk, ++p->nSteps ); + // delete the current network if present but backup is disabled + if ( p->pNtkCur ) + Abc_NtkDelete( p->pNtkCur ); } // set the new current network p->pNtkCur = pNtk; @@ -385,7 +439,7 @@ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p ) ***********************************************************************/ void Abc_FrameSetGlobalFrame( Abc_Frame_t * p ) { - Abc_FrameGlobalFrame = p; + s_GlobalFrame = p; } /**Function************************************************************* @@ -401,43 +455,17 @@ void Abc_FrameSetGlobalFrame( Abc_Frame_t * p ) ***********************************************************************/ Abc_Frame_t * Abc_FrameGetGlobalFrame() { - if ( Abc_FrameGlobalFrame == 0 ) + if ( s_GlobalFrame == 0 ) { // start the framework - Abc_FrameGlobalFrame = Abc_FrameAllocate(); + s_GlobalFrame = Abc_FrameAllocate(); // perform initializations - Abc_FrameInit( Abc_FrameGlobalFrame ); + Abc_FrameInit( s_GlobalFrame ); } - return Abc_FrameGlobalFrame; + return s_GlobalFrame; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_FrameReadNtkStore ( Abc_Frame_t * pFrame ) { return pFrame->pStored; } -int Abc_FrameReadNtkStoreSize ( Abc_Frame_t * pFrame ) { return pFrame->nStored; } -void Abc_FrameSetNtkStore ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk ) { pFrame->pStored = pNtk; } -void Abc_FrameSetNtkStoreSize ( Abc_Frame_t * pFrame, int nStored ) { pFrame->nStored = nStored;} - -void * Abc_FrameReadLibLut ( Abc_Frame_t * pFrame ) { return pFrame->pLibLut; } -void * Abc_FrameReadLibGen ( Abc_Frame_t * pFrame ) { return pFrame->pLibGen; } -void * Abc_FrameReadLibSuper ( Abc_Frame_t * pFrame ) { return pFrame->pLibSuper; } -void Abc_FrameSetLibLut ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibLut = pLib; } -void Abc_FrameSetLibGen ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibGen = pLib; } -void Abc_FrameSetLibSuper ( Abc_Frame_t * pFrame, void * pLib ) { pFrame->pLibSuper = pLib; } - -void * Abc_FrameReadManDd ( Abc_Frame_t * pFrame ) { return pFrame->dd; } -void * Abc_FrameReadManDec ( Abc_Frame_t * pFrame ) { return pFrame->pManDec; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 95d5b22d..6b929854 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -32,7 +32,7 @@ //////////////////////////////////////////////////////////////////////// // the current version -#define ABC_VERSION "UC Berkeley, ABC 1.0" +#define ABC_VERSION "UC Berkeley, ABC 1.01" // the maximum length of an input line #define MAX_STR 32768 @@ -53,8 +53,8 @@ struct Abc_Frame_t_ // the functionality Abc_Ntk_t * pNtkCur; // the current network int nSteps; // the counter of different network processed - // when this flag is 1, the current command is executed in autoexec mode - int fAutoexac; + int fAutoexac; // marks the autoexec mode + int fBatchMode; // are we invoked in batch mode? // output streams FILE * Out; FILE * Err; @@ -62,14 +62,13 @@ struct Abc_Frame_t_ // used for runtime measurement int TimeCommand; // the runtime of the last command int TimeTotal; // the total runtime of all commands - int fBatchMode; // are we invoked in batch mode? // temporary storage for structural choices Abc_Ntk_t * pStored; // the stored networks int nStored; // the number of stored networks // decomposition package - DdManager * dd; // temporary BDD package void * pManDec; // decomposition manager - + DdManager * dd; // temporary BDD package + // libraries for mapping void * pLibLut; // the current LUT library void * pLibGen; // the current genlib void * pLibSuper; // the current supergate library diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index 35d3c364..9d1201fa 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -161,8 +161,14 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc ) Cmd_CommandExecute( pAbc, "source -s abc.rc" ); } #endif //WIN32 - - return; + { + // reset command history + char * pName; + int i; + Vec_PtrForEachEntry( pAbc->aHistory, pName, i ) + free( pName ); + pAbc->aHistory->nSize = 0; + } } /**Function******************************************************************** diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c index 6b107498..3d2ca913 100644 --- a/src/map/fpga/fpga.c +++ b/src/map/fpga/fpga.c @@ -56,9 +56,9 @@ static int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) void Fpga_Init( Abc_Frame_t * pAbc ) { // set the default library - //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} }; - Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} }; - Abc_FrameSetLibLut( pAbc, Fpga_LutLibDup(&s_LutLib) ); + //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} }; + Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} }; + Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) ); Cmd_CommandAdd( pAbc, "FPGA mapping", "read_lut", Fpga_CommandReadLibrary, 0 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "print_lut", Fpga_CommandPrintLibrary, 0 ); @@ -150,8 +150,8 @@ int Fpga_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) goto usage; } // replace the current library - Fpga_LutLibFree( Abc_FrameReadLibLut(Abc_FrameGetGlobalFrame()) ); - Abc_FrameSetLibLut( Abc_FrameGetGlobalFrame(), pLib ); + Fpga_LutLibFree( Abc_FrameReadLibLut() ); + Abc_FrameSetLibLut( pLib ); return 0; usage: diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c index 95b9ca49..9ca65379 100644 --- a/src/map/fpga/fpgaCore.c +++ b/src/map/fpga/fpgaCore.c @@ -97,7 +97,7 @@ int Fpga_Mapping( Fpga_Man_t * p ) ***********************************************************************/ int Fpga_MappingPostProcess( Fpga_Man_t * p ) { - int fShowSwitching = 0; + int fShowSwitching = 1; int fRecoverAreaFlow = 1; int fRecoverArea = 1; float aAreaTotalCur, aAreaTotalCur2; diff --git a/src/map/fpga/fpgaSwitch.c b/src/map/fpga/fpgaSwitch.c index 0d2ec3fc..8cc77990 100644 --- a/src/map/fpga/fpgaSwitch.c +++ b/src/map/fpga/fpgaSwitch.c @@ -22,8 +22,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static float Fpga_CutGetSwitching( Fpga_Cut_t * pCut ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -64,10 +62,10 @@ float Fpga_CutRefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pC Fpga_Node_t * pNodeChild; float aArea; int i; - if ( pCut->nLeaves == 1 ) - return 0; // start the area of this cut - aArea = Fpga_CutGetSwitching( pCut ); + aArea = pNode->Switching; + if ( pCut->nLeaves == 1 ) + return aArea; // go through the children for ( i = 0; i < pCut->nLeaves; i++ ) { @@ -96,10 +94,10 @@ float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * Fpga_Node_t * pNodeChild; float aArea; int i; - if ( pCut->nLeaves == 1 ) - return 0; // start the area of this cut - aArea = Fpga_CutGetSwitching( pCut ); + aArea = pNode->Switching; + if ( pCut->nLeaves == 1 ) + return aArea; // go through the children for ( i = 0; i < pCut->nLeaves; i++ ) { @@ -112,27 +110,6 @@ float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * return aArea; } -/**function************************************************************* - - synopsis [Computes the exact area associated with the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -float Fpga_CutGetSwitching( Fpga_Cut_t * pCut ) -{ - float Result; - int i; - Result = 0.0; - for ( i = 0; i < pCut->nLeaves; i++ ) - Result += pCut->ppLeaves[i]->Switching; - return Result; -} - /**Function************************************************************* Synopsis [Computes the array of mapping.] @@ -153,10 +130,8 @@ float Fpga_MappingGetSwitching( Fpga_Man_t * pMan, Fpga_NodeVec_t * vMapping ) for ( i = 0; i < vMapping->nSize; i++ ) { pNode = vMapping->pArray[i]; - if ( !Fpga_NodeIsAnd(pNode) ) - continue; // at least one phase has the best cut assigned - assert( pNode->pCutBest != NULL ); + assert( !Fpga_NodeIsAnd(pNode) || pNode->pCutBest != NULL ); // at least one phase is used in the mapping assert( pNode->nRefs > 0 ); // compute the array due to the supergate diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c index 3ea1f2f1..db0f9623 100644 --- a/src/map/fpga/fpgaUtils.c +++ b/src/map/fpga/fpgaUtils.c @@ -314,7 +314,7 @@ float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan ) // reconnect the nodes in reverse topological order pMan->vMapping->nSize = 0; - for ( i = LevelMax; i > 0; i-- ) + for ( i = LevelMax; i >= 0; i-- ) for ( pNode = ppStore[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 ) Fpga_NodeVecPush( pMan->vMapping, pNode ); free( ppStore ); diff --git a/src/map/mapper/mapper.c b/src/map/mapper/mapper.c index 546186a2..e59fa4a3 100644 --- a/src/map/mapper/mapper.c +++ b/src/map/mapper/mapper.c @@ -149,13 +149,13 @@ int Map_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) // replace the current library // Map_SuperLibFree( s_pSuperLib ); // s_pSuperLib = pLib; - Map_SuperLibFree( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) ); - Abc_FrameSetLibSuper( Abc_FrameGetGlobalFrame(), pLib ); + Map_SuperLibFree( Abc_FrameReadLibSuper() ); + Abc_FrameSetLibSuper( pLib ); // replace the current genlib library // if ( s_pLib ) Mio_LibraryDelete( s_pLib ); // s_pLib = s_pSuperLib->pGenlib; - Mio_LibraryDelete( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) ); - Abc_FrameSetLibGen( Abc_FrameGetGlobalFrame(), pLib->pGenlib ); + Mio_LibraryDelete( Abc_FrameReadLibGen() ); + Abc_FrameSetLibGen( pLib->pGenlib ); return 0; usage: diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c index 5fea1f00..a9e9e29b 100644 --- a/src/map/mapper/mapperLib.c +++ b/src/map/mapper/mapperLib.c @@ -139,15 +139,9 @@ void Map_SuperLibFree( Map_SuperLib_t * p ) if ( p == NULL ) return; if ( p->pGenlib ) { -// if ( s_pLib == p->pGenlib ) -// s_pLib = NULL; -// if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == p->pGenlib ) -// Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL); -// Mio_LibraryDelete( p->pGenlib ); - - assert( p->pGenlib == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) ); + assert( p->pGenlib == Abc_FrameReadLibGen() ); Mio_LibraryDelete( p->pGenlib ); - Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL); + Abc_FrameSetLibGen( NULL ); } if ( p->tTableC ) Map_SuperTableFree( p->tTableC ); diff --git a/src/map/mapper/mapperRefs.c b/src/map/mapper/mapperRefs.c index e4adadae..baaebfa1 100644 --- a/src/map/mapper/mapperRefs.c +++ b/src/map/mapper/mapperRefs.c @@ -542,7 +542,7 @@ float Map_MappingGetArea( Map_Man_t * pMan, Map_NodeVec_t * vMapping ) (pNode->pCutBest[1] == NULL && pNode->nRefAct[1] > 0) ) Area += pMan->pSuperLib->AreaInv; } - // add buffer for each CO driven by a CI + // add buffers for each CO driven by a CI for ( i = 0; i < pMan->nOutputs; i++ ) if ( Map_NodeIsVar(pMan->pOutputs[i]) && !Map_IsComplement(pMan->pOutputs[i]) ) Area += pMan->pSuperLib->AreaBuf; diff --git a/src/map/mapper/mapperSwitch.c b/src/map/mapper/mapperSwitch.c index 02f38396..13168b47 100644 --- a/src/map/mapper/mapperSwitch.c +++ b/src/map/mapper/mapperSwitch.c @@ -23,7 +23,6 @@ //////////////////////////////////////////////////////////////////////// static float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, int fReference ); -static float Map_CutGetSwitching( Map_Cut_t * pCut ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -100,11 +99,13 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i Map_Cut_t * pCutChild; float aSwitchActivity; int i, fPhaseChild; + + // start switching activity for the node + aSwitchActivity = pNode->Switching; // consider the elementary variable if ( pCut->nLeaves == 1 ) - return 0; - // start the area of this cut - aSwitchActivity = Map_CutGetSwitching( pCut ); + return aSwitchActivity; + // go through the children assert( pCut->M[fPhase].pSuperBest ); for ( i = 0; i < pCut->nLeaves; i++ ) @@ -127,7 +128,7 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i // inverter should be added if the phase // (a) has no reference and (b) is implemented using other phase if ( pNodeChild->nRefAct[fPhaseChild]++ == 0 && pNodeChild->pCutBest[fPhaseChild] == NULL ) - aSwitchActivity += pNodeChild->Switching; + aSwitchActivity += pNodeChild->Switching; // inverter switches the same as the node // if the node is referenced, there is no recursive call if ( pNodeChild->nRefAct[2]++ > 0 ) continue; @@ -147,7 +148,7 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i // inverter should be added if the phase // (a) has no reference and (b) is implemented using other phase if ( --pNodeChild->nRefAct[fPhaseChild] == 0 && pNodeChild->pCutBest[fPhaseChild] == NULL ) - aSwitchActivity += pNodeChild->Switching; + aSwitchActivity += pNodeChild->Switching; // inverter switches the same as the node // if the node is referenced, there is no recursive call if ( --pNodeChild->nRefAct[2] > 0 ) continue; @@ -169,27 +170,6 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i return aSwitchActivity; } -/**function************************************************************* - - synopsis [Computes the exact area associated with the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -float Map_CutGetSwitching( Map_Cut_t * pCut ) -{ - float Result; - int i; - Result = 0.0; - for ( i = 0; i < pCut->nLeaves; i++ ) - Result += pCut->ppLeaves[i]->Switching; - return Result; -} - /**Function************************************************************* Synopsis [Computes the array of mapping.] @@ -227,9 +207,9 @@ float Map_MappingGetSwitching( Map_Man_t * pMan, Map_NodeVec_t * vMapping ) // count switching of the interver if we need to implement one phase with another phase if ( (pNode->pCutBest[0] == NULL && pNode->nRefAct[0] > 0) || (pNode->pCutBest[1] == NULL && pNode->nRefAct[1] > 0) ) - Switch += pNode->Switching; + Switch += pNode->Switching; // inverter switches the same as the node } - // add buffer for each CO driven by a CI + // add buffers for each CO driven by a CI for ( i = 0; i < pMan->nOutputs; i++ ) if ( Map_NodeIsVar(pMan->pOutputs[i]) && !Map_IsComplement(pMan->pOutputs[i]) ) Switch += pMan->pOutputs[i]->Switching; diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c index a01aeaa9..bb6dbba1 100644 --- a/src/map/mio/mio.c +++ b/src/map/mio/mio.c @@ -83,7 +83,7 @@ void Mio_Init( Abc_Frame_t * pAbc ) fclose( pFile ); // read genlib from file pLibGen = Mio_LibraryRead( pAbc, pFileTemp, NULL, 0 ); - Abc_FrameSetLibGen( pAbc, pLibGen ); + Abc_FrameSetLibGen( pLibGen ); #ifdef WIN32 _unlink( pFileTemp ); #else @@ -186,15 +186,15 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) extern void Map_SuperLibFree( Map_SuperLib_t * p ); // Map_SuperLibFree( s_pSuperLib ); // s_pSuperLib = NULL; - Map_SuperLibFree( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) ); - Abc_FrameSetLibSuper(Abc_FrameGetGlobalFrame(), NULL); + Map_SuperLibFree( Abc_FrameReadLibSuper() ); + Abc_FrameSetLibSuper( NULL ); } // replace the current library // Mio_LibraryDelete( s_pLib ); // s_pLib = pLib; - Mio_LibraryDelete( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) ); - Abc_FrameSetLibGen( Abc_FrameGetGlobalFrame(), pLib ); + Mio_LibraryDelete( Abc_FrameReadLibGen() ); + Abc_FrameSetLibGen( pLib ); return 0; usage: diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 14a3d950..f36b113f 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -185,6 +185,8 @@ extern void Extra_BitMatrixDelete2( Extra_BitMat_t * p, int i, int k ); extern void Extra_BitMatrixOr( Extra_BitMat_t * p, int i, unsigned * pInfo ); extern void Extra_BitMatrixOrTwo( Extra_BitMat_t * p, int i, int j ); extern int Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p ); +extern int Extra_BitMatrixIsDisjoint( Extra_BitMat_t * p1, Extra_BitMat_t * p2 ); +extern int Extra_BitMatrixIsClique( Extra_BitMat_t * p ); /*=== extraUtilFile.c ========================================================*/ diff --git a/src/misc/extra/extraUtilBitMatrix.c b/src/misc/extra/extraUtilBitMatrix.c index f0532dba..93cbbeac 100644 --- a/src/misc/extra/extraUtilBitMatrix.c +++ b/src/misc/extra/extraUtilBitMatrix.c @@ -28,14 +28,14 @@ struct Extra_BitMat_t_ { - unsigned ** ppData; - int nSize; - int nWords; - int nBitShift; - unsigned uMask; - int nLookups; - int nInserts; - int nDeletes; + unsigned ** ppData; // bit data + int nSize; // the number of bits in one dimension + int nWords; // the number of words in one dimension + int nBitShift; // the number of bits to shift to get words + unsigned uMask; // the mask to get the number of bits in the word + int nLookups; // the number of lookups + int nInserts; // the number of inserts + int nDeletes; // the number of deletions }; /*---------------------------------------------------------------------------*/ @@ -352,6 +352,62 @@ int Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p ) return nTotal; } +/**Function************************************************************* + + Synopsis [Returns 1 if the matrices have no entries in common.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_BitMatrixIsDisjoint( Extra_BitMat_t * p1, Extra_BitMat_t * p2 ) +{ + int i, w; + assert( p1->nSize == p2->nSize ); + for ( i = 0; i < p1->nSize; i++ ) + for ( w = 0; w < p1->nWords; w++ ) + if ( p1->ppData[i][w] & p2->ppData[i][w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the matrix is a set of cliques.] + + Description [For example pairwise symmetry info should satisfy this property.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_BitMatrixIsClique( Extra_BitMat_t * pMat ) +{ + int v, u, i; + for ( v = 0; v < pMat->nSize; v++ ) + for ( u = v+1; u < pMat->nSize; u++ ) + { + if ( !Extra_BitMatrixLookup1( pMat, v, u ) ) + continue; + // v and u are symmetric + for ( i = 0; i < pMat->nSize; i++ ) + { + if ( i == v || i == u ) + continue; + // i is neither v nor u + // the symmetry status of i is the same w.r.t. to v and u + if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) ) + return 0; + } + } + return 1; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c index e7d6fec6..a21dd520 100644 --- a/src/opt/rwr/rwrMan.c +++ b/src/opt/rwr/rwrMan.c @@ -78,13 +78,13 @@ clk = clock(); if ( fPrecompute ) { // precompute subgraphs Rwr_ManPrecompute( p ); +// Rwr_ManPrint( p ); Rwr_ManWriteToArray( p ); - Rwr_ManPrint( p ); } else { // load saved subgraphs Rwr_ManLoadFromArray( p, 0 ); - Rwr_ManPrint( p ); +// Rwr_ManPrint( p ); Rwr_ManPreprocess( p ); } p->timeStart = clock() - clk; diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h index 9b4d9699..afed7190 100644 --- a/src/opt/sim/sim.h +++ b/src/opt/sim/sim.h @@ -21,6 +21,12 @@ #ifndef __SIM_H__ #define __SIM_H__ +/* + The ideas realized in this package are described in the paper: + "Detecting Symmetries in Boolean Functions using Circuit Representation, + Simulation, and Satisfiability". +*/ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -45,7 +51,8 @@ struct Sym_Man_t_ int nSimWords; // the number of bits in simulation info Vec_Ptr_t * vSim; // simulation info // support information - Vec_Ptr_t * vSuppFun; // functional supports + Vec_Ptr_t * vSuppFun; // bit representation + Vec_Vec_t * vSupports; // integer representation // symmetry info for each output Vec_Ptr_t * vMatrSymms; // symmetric pairs Vec_Ptr_t * vMatrNonSymms; // non-symmetric pairs @@ -56,6 +63,14 @@ struct Sym_Man_t_ unsigned * uPatRand; unsigned * uPatCol; unsigned * uPatRow; + // temporary + Vec_Int_t * vVarsU; + Vec_Int_t * vVarsV; + int iOutput; + int iVar1; + int iVar2; + int iVar1Old; + int iVar2Old; // internal data structures int nSatRuns; int nSatRunsSat; @@ -64,8 +79,12 @@ struct Sym_Man_t_ int nPairsSymm; int nPairsSymmStr; int nPairsNonSymm; + int nPairsRem; int nPairsTotal; // runtime statistics + int timeStruct; + int timeCount; + int timeMatr; int timeSim; int timeFraig; int timeSat; @@ -91,6 +110,7 @@ struct Sim_Man_t_ Vec_Ptr_t * vSuppFun; // functional supports // simulation targets Vec_Vec_t * vSuppTargs; // support targets + int iInput; // the input current processed // internal data structures Extra_MmFixed_t * pMmPat; Vec_Ptr_t * vFifo; @@ -148,7 +168,7 @@ struct Sim_Pat_t_ //////////////////////////////////////////////////////////////////////// /*=== simMan.c ==========================================================*/ -extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ); +extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose ); extern void Sym_ManStop( Sym_Man_t * p ); extern void Sym_ManPrintStats( Sym_Man_t * p ); extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ); @@ -158,11 +178,13 @@ extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ); extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ); /*=== simSupp.c ==========================================================*/ extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ); -extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ); +extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ); /*=== simSym.c ==========================================================*/ -extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ); +extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose ); +/*=== simSymSat.c ==========================================================*/ +extern int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern ); /*=== simSymStr.c ==========================================================*/ -extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ); +extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun ); /*=== simSymSim.c ==========================================================*/ extern void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym ); /*=== simUtil.c ==========================================================*/ @@ -180,7 +202,8 @@ extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ); extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ); extern void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ); extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ); -extern int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters ); +extern void Sim_UtilCountPairsAll( Sym_Man_t * p ); +extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c index 02d59343..780ecfd8 100644 --- a/src/opt/sim/simMan.c +++ b/src/opt/sim/simMan.c @@ -40,10 +40,10 @@ SeeAlso [] ***********************************************************************/ -Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ) +Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose ) { Sym_Man_t * p; - int i; + int i, v; // start the manager p = ALLOC( Sym_Man_t, 1 ); memset( p, 0, sizeof(Sym_Man_t) ); @@ -69,8 +69,15 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ) p->uPatRand = ALLOC( unsigned, p->nSimWords ); p->uPatCol = ALLOC( unsigned, p->nSimWords ); p->uPatRow = ALLOC( unsigned, p->nSimWords ); + p->vVarsU = Vec_IntStart( 100 ); + p->vVarsV = Vec_IntStart( 100 ); // compute supports - p->vSuppFun = Sim_ComputeFunSupp( pNtk ); + p->vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose ); + p->vSupports = Vec_VecStart( p->nOutputs ); + for ( i = 0; i < p->nOutputs; i++ ) + for ( v = 0; v < p->nInputs; v++ ) + if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) ) + Vec_VecPush( p->vSupports, i, (void *)v ); return p; } @@ -92,11 +99,14 @@ void Sym_ManStop( Sym_Man_t * p ) if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); if ( p->vSim ) Sim_UtilInfoFree( p->vSim ); if ( p->vNodes ) Vec_PtrFree( p->vNodes ); + if ( p->vSupports ) Vec_VecFree( p->vSupports ); for ( i = 0; i < p->nOutputs; i++ ) { Extra_BitMatrixStop( p->vMatrSymms->pArray[i] ); Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] ); } + Vec_IntFree( p->vVarsU ); + Vec_IntFree( p->vVarsV ); Vec_PtrFree( p->vMatrSymms ); Vec_PtrFree( p->vMatrNonSymms ); Vec_IntFree( p->vPairsTotal ); @@ -121,17 +131,18 @@ void Sym_ManStop( Sym_Man_t * p ) ***********************************************************************/ void Sym_ManPrintStats( Sym_Man_t * p ) { - printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", - Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); -/* - printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); - printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); - printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) ); - printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); -*/ - printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat ); - printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat ); +// printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", +// Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); + printf( "Total symm = %8d.\n", p->nPairsSymm ); + printf( "Structural symm = %8d.\n", p->nPairsSymmStr ); + printf( "Total non-sym = %8d.\n", p->nPairsNonSymm ); + printf( "Total var pairs = %8d.\n", p->nPairsTotal ); + printf( "Sat runs SAT = %8d.\n", p->nSatRunsSat ); + printf( "Sat runs UNSAT = %8d.\n", p->nSatRunsUnsat ); + PRT( "Structural ", p->timeStruct ); PRT( "Simulation ", p->timeSim ); + PRT( "Matrix ", p->timeMatr ); + PRT( "Counting ", p->timeCount ); PRT( "Fraiging ", p->timeFraig ); PRT( "SAT ", p->timeSat ); PRT( "TOTAL ", p->timeTotal ); @@ -217,14 +228,12 @@ void Sim_ManStop( Sim_Man_t * p ) ***********************************************************************/ void Sim_ManPrintStats( Sim_Man_t * p ) { - printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", - Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); - printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); - printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); - printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) ); - printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); - printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat ); - printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat ); +// printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", +// Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); + printf( "Total func supps = %8d.\n", Sim_UtilCountSuppSizes(p, 0) ); + printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) ); + printf( "Sat runs SAT = %8d.\n", p->nSatRunsSat ); + printf( "Sat runs UNSAT = %8d.\n", p->nSatRunsUnsat ); PRT( "Simulation ", p->timeSim ); PRT( "Traversal ", p->timeTrav ); PRT( "Fraiging ", p->timeFraig ); diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c index 2f380866..576e19cc 100644 --- a/src/opt/sim/simSupp.c +++ b/src/opt/sim/simSupp.c @@ -99,13 +99,12 @@ Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ) +Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ) { Sim_Man_t * p; Vec_Ptr_t * vResult; int nSolved, i, clk = clock(); -// srand( time(NULL) ); srand( 0xABC ); // start the simulation manager @@ -117,35 +116,40 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ) // set the support targets Sim_ComputeSuppSetTargets( p ); -printf( "Initial targets = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) ); +if ( fVerbose ) + printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) ); if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) goto exit; for ( i = 0; i < 1; i++ ) { - // compute patterns using one round of random simulation - Sim_UtilAssignRandom( p ); - nSolved = Sim_ComputeSuppRound( p, 1 ); -printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) ); - if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) - goto exit; - } + // compute patterns using one round of random simulation + Sim_UtilAssignRandom( p ); + nSolved = Sim_ComputeSuppRound( p, 1 ); + if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) + goto exit; +if ( fVerbose ) + printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n", + Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) ); + } - // simulate until saturation + // try to solve the support targets while ( Vec_VecSizeSize(p->vSuppTargs) > 0 ) { - // solve randomly a given number of targets + // solve targets until the first disproved one (which gives counter-example) Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords ); // compute additional functional support -// Sim_UtilAssignRandom( p ); Sim_UtilAssignFromFifo( p ); nSolved = Sim_ComputeSuppRound( p, 1 ); -printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n", + +if ( fVerbose ) + printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns ); } exit: +p->timeTotal = clock() - clk; vResult = p->vSuppFun; // p->vSuppFun = NULL; Sim_ManStop( p ); @@ -166,7 +170,6 @@ exit: int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ) { Vec_Int_t * vTargets; - Abc_Obj_t * pNode; int i, Counter = 0; int clk; // perform one round of random simulation @@ -174,7 +177,7 @@ clk = clock(); Sim_UtilSimulate( p, 0 ); p->timeSim += clock() - clk; // iterate through the CIs and detect COs that depend on them - Abc_NtkForEachCi( p->pNtk, pNode, i ) + for ( i = p->iInput; i < p->nInputs; i++ ) { vTargets = p->vSuppTargs->pArray[i]; if ( fUseTargets && vTargets->nSize == 0 ) @@ -207,7 +210,8 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) int fFirst = 1; int clk; // collect nodes by level in the TFO of the CI - // (this procedure increments TravId of the collected nodes) + // this proceduredoes not collect the CIs and COs + // but it increments TravId of the collected nodes and CIs/COs clk = clock(); pNodeCi = Abc_NtkCi( p->pNtk, iNumCi ); vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 ); @@ -232,13 +236,10 @@ p->timeSim += clock() - clk; // get the target output Output = vTargets->pArray[i]; // get the target node - pNode = Abc_NtkCo( p->pNtk, Output ); + pNode = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) ); // the output should be in the cone assert( Abc_NodeIsTravIdCurrent(pNode) ); - // simulate the node - Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); - // skip if the simulation info is equal if ( Sim_UtilInfoCompare( p, pNode ) ) continue; @@ -283,12 +284,13 @@ printf( "\n" ); { if ( !Abc_NodeIsTravIdCurrent( pNode ) ) continue; - Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); - if ( !Sim_UtilInfoCompare( p, pNode ) ) + if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) ) { if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ) + { Counter++; - Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); + Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); + } } } } @@ -365,7 +367,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p ) Abc_Obj_t * pNode; Sim_Pat_t * pPat; unsigned * pSimInfo; - int iWord, iWordLim, i, w; + int nWordsNew, iWord, iWordLim, i, w; int iBeg, iEnd; int Counter = 0; // go through the patterns and fill in the dist-1 minterms for each @@ -379,7 +381,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p ) // get the first word of the next series iWordLim = iWord + 1; // set the pattern for all PIs from iBit to iWord + p->nInputs - iBeg = ABC_MAX( 0, pPat->Input - 16 ); + iBeg = p->iInput; iEnd = ABC_MIN( iBeg + 32, p->nInputs ); // for ( i = iBeg; i < iEnd; i++ ) Abc_NtkForEachCi( p->pNtk, pNode, i ) @@ -397,9 +399,12 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p ) } else { + // get the number of words for the remaining inputs + nWordsNew = p->nSuppWords; +// nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput ); // get the first word of the next series - iWordLim = (iWord + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords; - // set the pattern for all PIs from iBit to iWord + p->nInputs + iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords; + // set the pattern for all CIs from iWord to iWord + nWordsNew Abc_NtkForEachCi( p->pNtk, pNode, i ) { pSimInfo = p->vSim0->pArray[pNode->Id]; @@ -413,8 +418,10 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p ) for ( w = iWord; w < iWordLim; w++ ) pSimInfo[w] = 0; } - // flip one bit Sim_XorBit( pSimInfo + iWord, i ); + // flip one bit +// if ( i >= p->iInput ) +// Sim_XorBit( pSimInfo + iWord, i-p->iInput ); } } Sim_ManPatFree( p, pPat ); @@ -456,10 +463,11 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) { p->nSatRuns++; Output = (int)pEntry; + // set up the miter for the two cofactors of this output w.r.t. this input pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 ); - // transform the target into a fraig + // transform the miter into a fraig Fraig_ParamsSetDefault( &Params ); Params.fInternal = 1; clk = clock(); @@ -502,23 +510,23 @@ p->timeSat += clock() - clk; Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) if ( pModel[v] ) Sim_SetBit( pPat->pData, v ); - Sim_XorBit( pPat->pData, Input ); // flip the given bit + Sim_XorBit( pPat->pData, Input ); // add this bit in the opposite polarity Vec_PtrPush( p->vFifo, pPat ); */ Counter++; } // delete the fraig manager Fraig_ManFree( pMan ); - // delete the target + // delete the miter Abc_NtkDelete( pMiter ); + // makr the input, which we are processing + p->iInput = Input; + // stop when we found enough patterns // if ( Counter == Limit ) if ( Counter == 1 ) return; - // switch to the next input if we found one model - if ( pModel ) - break; } } diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c index 06b730fc..b43597f3 100644 --- a/src/opt/sim/simSwitch.c +++ b/src/opt/sim/simSwitch.c @@ -72,8 +72,8 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) vNodes = Abc_AigDfs( pNtk, 1, 0 ); Vec_PtrForEachEntry( vNodes, pNode, i ) { - Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords ); pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); + Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords ); pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); } Vec_PtrFree( vNodes ); diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c index 706b13dc..c452bb1b 100644 --- a/src/opt/sim/simSym.c +++ b/src/opt/sim/simSym.c @@ -40,52 +40,100 @@ SeeAlso [] ***********************************************************************/ -int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ) +int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose ) { Sym_Man_t * p; Vec_Ptr_t * vResult; int Result; - int i, clk = clock(); + int i, clk, clkTotal = clock(); -// srand( time(NULL) ); srand( 0xABC ); // start the simulation manager - p = Sym_ManStart( pNtk ); - p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal ); + p = Sym_ManStart( pNtk, fVerbose ); + p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal ); + if ( fVerbose ) + printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); // detect symmetries using circuit structure - Sim_SymmsStructCompute( pNtk, p->vMatrSymms ); - p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym ); +clk = clock(); + Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun ); +p->timeStruct = clock() - clk; -printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n", - p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm ); + Sim_UtilCountPairsAll( p ); + p->nPairsSymmStr = p->nPairsSymm; + if ( fVerbose ) + printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); // detect symmetries using simulation for ( i = 1; i <= 1000; i++ ) { - // generate random pattern - Sim_UtilGetRandom( p->uPatRand, p->nSimWords ); // simulate this pattern + Sim_UtilGetRandom( p->uPatRand, p->nSimWords ); Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); - if ( i % 100 != 0 ) + if ( i % 50 != 0 ) continue; + // check disjointness + assert( Sim_UtilMatrsAreDisjoint( p ) ); // count the number of pairs - p->nPairsSymm = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym ); - p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym ); + Sim_UtilCountPairsAll( p ); + if ( i % 500 != 0 ) + continue; + if ( fVerbose ) + printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); + } -printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n", - p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm ); + // detect symmetries using SAT + for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ ) + { + // simulate this pattern in four polarities + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + Sim_XorBit( p->uPatRand, p->iVar1 ); + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + Sim_XorBit( p->uPatRand, p->iVar2 ); + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + Sim_XorBit( p->uPatRand, p->iVar1 ); + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + Sim_XorBit( p->uPatRand, p->iVar2 ); +/* + // try the previuos pair + Sim_XorBit( p->uPatRand, p->iVar1Old ); + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + Sim_XorBit( p->uPatRand, p->iVar2Old ); + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + Sim_XorBit( p->uPatRand, p->iVar1Old ); + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); +*/ + if ( i % 10 != 0 ) + continue; + // check disjointness + assert( Sim_UtilMatrsAreDisjoint( p ) ); + // count the number of pairs + Sim_UtilCountPairsAll( p ); + if ( i % 50 != 0 ) + continue; + if ( fVerbose ) + printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); } + // count the number of pairs + Sim_UtilCountPairsAll( p ); + if ( fVerbose ) + printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); + Result = p->nPairsSymm; vResult = p->vMatrSymms; +p->timeTotal = clock() - clkTotal; // p->vMatrSymms = NULL; Sym_ManStop( p ); return Result; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c index 88e33161..db9917b3 100644 --- a/src/opt/sim/simSymSat.c +++ b/src/opt/sim/simSymSat.c @@ -20,13 +20,14 @@ #include "abc.h" #include "sim.h" +#include "fraig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 ); -static int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ); +extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern ); +extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -34,95 +35,88 @@ static int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ) /**Function************************************************************* - Synopsis [Performs the SAT based check.] + Synopsis [Tries to prove the remaining pairs using SAT.] - Description [Given two bit matrices, with symm info and non-symm info, - checks the remaining pairs.] + Description [Continues to prove as long as it encounters symmetric pairs. + Returns 1 if a non-symmetric pair is found (which gives a counter-example). + Returns 0 if it finishes considering all pairs for all outputs.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym ) +int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern ) { - int VarsU[512], VarsV[512]; - int nVarsU, nVarsV; - int v, u, i, k; - int Counter = 0; - int satCalled = 0; - int satProved = 0; - double Density; - int clk = clock(); - - extern int symsSat; - extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); - - - // count undecided pairs - for ( v = 0; v < p->vInputs->nSize; v++ ) - for ( u = v+1; u < p->vInputs->nSize; u++ ) - { - if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) - continue; - Counter++; - } - // compute the density of 1's in the input space of the functions - Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32; - - printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ", - p->vInputs->nSize, Counter, Density ); + Vec_Int_t * vSupport; + Extra_BitMat_t * pMatSym, * pMatNonSym; + int Index1, Index2, Index3, IndexU, IndexV; + int v, u, i, k, b, out; - - // go through the remaining variable pairs - for ( v = 0; v < p->vInputs->nSize; v++ ) - for ( u = v+1; u < p->vInputs->nSize; u++ ) + // iterate through outputs + for ( out = p->iOutput; out < p->nOutputs; out++ ) { - if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) - continue; - symsSat++; - satCalled++; - - // collect the variables that are symmetric with each - nVarsU = nVarsV = 0; - for ( i = 0; i < p->vInputs->nSize; i++ ) + pMatSym = Vec_PtrEntry( p->vMatrSymms, out ); + pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out ); + + // go through the remaining variable pairs + vSupport = Vec_VecEntry( p->vSupports, out ); + Vec_IntForEachEntry( vSupport, v, Index1 ) + Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 ) { - if ( Extra_BitMatrixLookup1( pMatSym, u, i ) ) - VarsU[nVarsU++] = i; - if ( Extra_BitMatrixLookup1( pMatSym, v, i ) ) - VarsV[nVarsV++] = i; - } + if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) + continue; + p->nSatRuns++; - if ( Fraig_SymmsSatProveOne( p, v, u ) ) - { // update the symmetric variable info -//printf( "%d sym %d\n", v, u ); - for ( i = 0; i < nVarsU; i++ ) - for ( k = 0; k < nVarsV; k++ ) + // collect the support variables that are symmetric with u and v + Vec_IntClear( p->vVarsU ); + Vec_IntClear( p->vVarsV ); + Vec_IntForEachEntry( vSupport, b, Index3 ) { - Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1 - Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1 - Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 2 + if ( Extra_BitMatrixLookup1( pMatSym, u, b ) ) + Vec_IntPush( p->vVarsU, b ); + if ( Extra_BitMatrixLookup1( pMatSym, v, b ) ) + Vec_IntPush( p->vVarsV, b ); } - satProved++; - } - else - { // update the assymmetric variable info -//printf( "%d non-sym %d\n", v, u ); - for ( i = 0; i < nVarsU; i++ ) - for ( k = 0; k < nVarsV; k++ ) - { - Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3 - Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3 + + if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) ) + { // update the symmetric variable info + p->nSatRunsUnsat++; + Vec_IntForEachEntry( p->vVarsU, i, IndexU ) + Vec_IntForEachEntry( p->vVarsV, k, IndexV ) + { + Extra_BitMatrixInsert1( pMatSym, i, k ); // Theorem 1 + Extra_BitMatrixInsert2( pMatSym, i, k ); // Theorem 1 + Extra_BitMatrixOrTwo( pMatNonSym, i, k ); // Theorem 2 + } + } + else + { // update the assymmetric variable info + p->nSatRunsSat++; + Vec_IntForEachEntry( p->vVarsU, i, IndexU ) + Vec_IntForEachEntry( p->vVarsV, k, IndexV ) + { + Extra_BitMatrixInsert1( pMatNonSym, i, k ); // Theorem 3 + Extra_BitMatrixInsert2( pMatNonSym, i, k ); // Theorem 3 + } + + // remember the out + p->iOutput = out; + p->iVar1Old = p->iVar1; + p->iVar2Old = p->iVar2; + p->iVar1 = v; + p->iVar2 = u; + return 1; + } } -//Extra_BitMatrixPrint( pMatSym ); -//Extra_BitMatrixPrint( pMatNonSym ); + // make sure that the symmetry matrix contains only cliques + assert( Extra_BitMatrixIsClique( pMatSym ) ); } -printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved ); -PRT( "Time", clock() - clk ); - // make sure that the symmetry matrix contains only cliques - assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) ); + // mark that we finished all outputs + p->iOutput = p->nOutputs; + return 0; } /**Function************************************************************* @@ -136,65 +130,68 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 ) -{ - Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2; - int RetValue; - int nSatRuns = p->nSatCalls; - int nSatProof = p->nSatProof; - - p->nBTLimit = 10; // set the backtrack limit - - pVar1 = p->vInputs->pArray[Var1]; - pVar2 = p->vInputs->pArray[Var2]; - pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) ); - pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 ); - -//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof ); - -// RetValue = (pCof01 == pCof10); -// RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 ); - RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [A sanity check procedure.] - - Description [Makes sure that the symmetry information in the matrix - is closed w.r.t. the relationship of transitivity (that is the symmetry - graph is composed of cliques).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ) +int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern ) { - int v, u, i; - for ( v = 0; v < p->vInputs->nSize; v++ ) - for ( u = v+1; u < p->vInputs->nSize; u++ ) + Fraig_Params_t Params; + Fraig_Man_t * pMan; + Abc_Ntk_t * pMiter; + int RetValue, i, clk; + int * pModel; + + // get the miter for this problem + pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 ); + // transform the miter into a fraig + Fraig_ParamsSetDefault( &Params ); + Params.fInternal = 1; + Params.nPatsRand = 512; + Params.nPatsDyna = 512; + +clk = clock(); + pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); +p->timeFraig += clock() - clk; +clk = clock(); + Fraig_ManProveMiter( pMan ); +p->timeSat += clock() - clk; + + // analyze the result + RetValue = Fraig_ManCheckMiter( pMan ); +// assert( RetValue >= 0 ); + // save the pattern + if ( RetValue == 0 ) { - if ( !Extra_BitMatrixLookup1( pMat, v, u ) ) - continue; - // v and u are symmetric - for ( i = 0; i < p->vInputs->nSize; i++ ) - { - if ( i == v || i == u ) - continue; - // i is neither v nor u - // the symmetry status of i is the same w.r.t. to v and u - if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) ) - return 0; - } + // get the pattern + pModel = Fraig_ManReadModel( pMan ); + assert( pModel != NULL ); +//printf( "Disproved by SAT: out = %d pair = (%d, %d)\n", Out, Var1, Var2 ); + // transfer the model into the pattern + for ( i = 0; i < p->nSimWords; i++ ) + pPattern[i] = 0; + for ( i = 0; i < p->nInputs; i++ ) + if ( pModel[i] ) + Sim_SetBit( pPattern, i ); + // make sure these variables have the same value (1) + Sim_SetBit( pPattern, Var1 ); + Sim_SetBit( pPattern, Var2 ); } - return 1; + else if ( RetValue == -1 ) + { + // this should never happen; if it happens, such is life + // we are conservative and assume that there is no symmetry +//printf( "STRANGE THING: out = %d %s pair = (%d %s, %d %s)\n", +// Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)), +// Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)), +// Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) ); + memset( pPattern, 0, sizeof(unsigned) * p->nSimWords ); + RetValue = 0; + } + // delete the fraig manager + Fraig_ManFree( pMan ); + // delete the miter + Abc_NtkDelete( pMiter ); + return RetValue; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c index 53fc4ac2..94028c47 100644 --- a/src/opt/sim/simSymSim.c +++ b/src/opt/sim/simSymSim.c @@ -26,7 +26,7 @@ //////////////////////////////////////////////////////////////////////// static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ); -static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output ); +static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -46,26 +46,36 @@ static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNo void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym ) { Abc_Obj_t * pNode; - int i; + int i, nPairsTotal, nPairsSym, nPairsNonSym; + int clk; + // create the simulation matrix Sim_SymmsCreateSquare( p, pPat ); // simulate each node in the DFS order +clk = clock(); Vec_PtrForEachEntry( p->vNodes, pNode, i ) { if ( Abc_NodeIsConst(pNode) ) continue; Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords ); } +p->timeSim += clock() - clk; // collect info into the CO matrices +clk = clock(); Abc_NtkForEachCo( p->pNtk, pNode, i ) { pNode = Abc_ObjFanin0(pNode); if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) ) continue; - if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,i) ) + nPairsTotal = Vec_IntEntry(p->vPairsTotal, i); + nPairsSym = Vec_IntEntry(p->vPairsSym, i); + nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i); + assert( nPairsTotal >= nPairsSym + nPairsNonSym ); + if ( nPairsTotal == nPairsSym + nPairsNonSym ) continue; - Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i ); + Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i ); } +p->timeMatr += clock() - clk; } /**Function************************************************************* @@ -114,40 +124,44 @@ void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ) SeeAlso [] ***********************************************************************/ -void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output ) +void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output ) { - unsigned * pSuppInfo; + Extra_BitMat_t * pMat; + Vec_Int_t * vSupport; + unsigned * pSupport; unsigned * pSimInfo; - int i, w; - // get the simuation info for the node + int i, w, Index; + // get the matrix, the support, and the simulation info + pMat = Vec_PtrEntry( vMatrsNonSym, Output ); + vSupport = Vec_VecEntry( p->vSupports, Output ); + pSupport = Vec_PtrEntry( p->vSuppFun, Output ); pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id ); - pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output ); // generate vectors A1 and A2 for ( w = 0; w < p->nSimWords; w++ ) { - p->uPatCol[w] = pSuppInfo[w] & pPat[w] & pSimInfo[w]; - p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w]; + p->uPatCol[w] = pSupport[w] & pPat[w] & pSimInfo[w]; + p->uPatRow[w] = pSupport[w] & pPat[w] & ~pSimInfo[w]; } // add two dimensions - for ( i = 0; i < p->nInputs; i++ ) + Vec_IntForEachEntry( vSupport, i, Index ) if ( Sim_HasBit( p->uPatCol, i ) ) Extra_BitMatrixOr( pMat, i, p->uPatRow ); // add two dimensions - for ( i = 0; i < p->nInputs; i++ ) + Vec_IntForEachEntry( vSupport, i, Index ) if ( Sim_HasBit( p->uPatRow, i ) ) Extra_BitMatrixOr( pMat, i, p->uPatCol ); // generate vectors B1 and B2 for ( w = 0; w < p->nSimWords; w++ ) { - p->uPatCol[w] = pSuppInfo[w] & ~pPat[w] & pSimInfo[w]; - p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w]; + p->uPatCol[w] = pSupport[w] & ~pPat[w] & pSimInfo[w]; + p->uPatRow[w] = pSupport[w] & ~pPat[w] & ~pSimInfo[w]; } // add two dimensions - for ( i = 0; i < p->nInputs; i++ ) + Vec_IntForEachEntry( vSupport, i, Index ) if ( Sim_HasBit( p->uPatCol, i ) ) Extra_BitMatrixOr( pMat, i, p->uPatRow ); // add two dimensions - for ( i = 0; i < p->nInputs; i++ ) + Vec_IntForEachEntry( vSupport, i, Index ) if ( Sim_HasBit( p->uPatRow, i ) ) Extra_BitMatrixOr( pMat, i, p->uPatCol ); } diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c index c3059d84..ed7e93bf 100644 --- a/src/opt/sim/simSymStr.c +++ b/src/opt/sim/simSymStr.c @@ -37,7 +37,7 @@ static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, V static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ); static void Sim_SymmsPrint( Vec_Int_t * vSymms ); static void Sim_SymmsTrans( Vec_Int_t * vSymms ); -static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ); +static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport ); static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// @@ -55,7 +55,7 @@ static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ); SeeAlso [] ***********************************************************************/ -void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ) +void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun ) { Vec_Ptr_t * vNodes; Abc_Obj_t * pTemp; @@ -84,7 +84,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ) pTemp = Abc_ObjFanin0(pTemp); if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) ) continue; - Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) ); + Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) ); } // clean the intermediate results Sim_UtilInfoFree( pNtk->vSupps ); @@ -92,7 +92,8 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ) Abc_NtkForEachCi( pNtk, pTemp, i ) Vec_IntFree( SIM_READ_SYMMS(pTemp) ); Vec_PtrForEachEntry( vNodes, pTemp, i ) - Vec_IntFree( SIM_READ_SYMMS(pTemp) ); + if ( !Abc_NodeIsConst(pTemp) ) + Vec_IntFree( SIM_READ_SYMMS(pTemp) ); Vec_PtrFree( vNodes ); free( pMap ); } @@ -429,7 +430,7 @@ void Sim_SymmsTrans( Vec_Int_t * vSymms ) SeeAlso [] ***********************************************************************/ -void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ) +void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport ) { int i, Ind1, Ind2, nInputs; unsigned uSymm; @@ -443,6 +444,10 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ) uSymm = (unsigned)vSymms->pArray[i]; Ind1 = (uSymm & 0xffff); Ind2 = (uSymm >> 16); + // skip variables that are not in the true support + assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) ); + if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) ) + continue; Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 ); Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 ); } diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c index 5a57ca2d..4b89c650 100644 --- a/src/opt/sim/simUtils.c +++ b/src/opt/sim/simUtils.c @@ -436,18 +436,80 @@ int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCou SeeAlso [] ***********************************************************************/ -int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters ) +int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport ) { - Extra_BitMat_t * vMat; - int Counter, nPairs, i; - Counter = 0; - Vec_PtrForEachEntry( vMatrs, vMat, i ) + int i, k, Index1, Index2; + int Counter = 0; +// int Counter2; + Vec_IntForEachEntry( vSupport, i, Index1 ) + Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 ) + Counter += Extra_BitMatrixLookup1( pMat, i, k ); +// Counter2 = Extra_BitMatrixCountOnesUpper(pMat); +// assert( Counter == Counter2 ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of entries in the array of matrices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilCountPairsAll( Sym_Man_t * p ) +{ + int nPairsTotal, nPairsSym, nPairsNonSym, i, clk; +clk = clock(); + p->nPairsSymm = 0; + p->nPairsNonSymm = 0; + for ( i = 0; i < p->nOutputs; i++ ) { - nPairs = Extra_BitMatrixCountOnesUpper( vMat ); - Vec_IntWriteEntry( vCounters, i, nPairs ); - Counter += nPairs; + nPairsTotal = Vec_IntEntry(p->vPairsTotal, i); + nPairsSym = Vec_IntEntry(p->vPairsSym, i); + nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i); + assert( nPairsTotal >= nPairsSym + nPairsNonSym ); + if ( nPairsTotal == nPairsSym + nPairsNonSym ) + { + p->nPairsSymm += nPairsSym; + p->nPairsNonSymm += nPairsNonSym; + continue; + } + nPairsSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) ); + nPairsNonSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntry(p->vSupports, i) ); + assert( nPairsTotal >= nPairsSym + nPairsNonSym ); + Vec_IntWriteEntry( p->vPairsSym, i, nPairsSym ); + Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym ); + p->nPairsSymm += nPairsSym; + p->nPairsNonSymm += nPairsNonSym; +// printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym ); } - return Counter; +//printf( "\n" ); + p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm; +p->timeCount += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p ) +{ + int i; + for ( i = 0; i < p->nOutputs; i++ ) + if ( !Extra_BitMatrixIsDisjoint( Vec_PtrEntry(p->vMatrSymms,i), Vec_PtrEntry(p->vMatrNonSymms,i) ) ) + return 0; + return 1; } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 242de8e2..b030caef 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -28,8 +28,9 @@ struct CSAT_ManagerStruct_t { // information about the problem stmm_table * tName2Node; // the hash table mapping names to nodes + stmm_table * tNode2Name; // the hash table mapping nodes to names Abc_Ntk_t * pNtk; // the starting ABC network - Abc_Ntk_t * pTarget; // the AIG of the target + Abc_Ntk_t * pTarget; // the AIG representing the target char * pDumpFileName; // the name of the file to dump the target network // solving parameters int mode; // 0 = baseline; 1 = resource-aware fraiging @@ -44,6 +45,7 @@ struct CSAT_ManagerStruct_t static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ); static void CSAT_TargetResFree( CSAT_Target_ResultT * p ); +static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ); // some external procedures extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); @@ -72,8 +74,9 @@ CSAT_Manager CSAT_InitManager() mng->pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP ); mng->pNtk->pName = util_strsav("csat_network"); mng->tName2Node = stmm_init_table(strcmp, stmm_strhash); - mng->vNodes = Vec_PtrAlloc( 100 ); - mng->vValues = Vec_IntAlloc( 100 ); + mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); + mng->vNodes = Vec_PtrAlloc( 100 ); + mng->vValues = Vec_IntAlloc( 100 ); return mng; } @@ -90,6 +93,7 @@ CSAT_Manager CSAT_InitManager() ***********************************************************************/ void CSAT_QuitManager( CSAT_Manager mng ) { + if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); if ( mng->pNtk ) Abc_NtkDelete( mng->pNtk ); if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); @@ -151,7 +155,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; } // create the PI pObj = Abc_NtkCreatePi( mng->pNtk ); - pObj->pNext = (Abc_Obj_t *)name; + stmm_insert( mng->tNode2Name, (char *)pObj, name ); break; case CSAT_CONST: case CSAT_BAND: @@ -234,7 +238,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } // create the PO pObj = Abc_NtkCreatePo( mng->pNtk ); - pObj->pNext = (Abc_Obj_t *)name; + stmm_insert( mng->tNode2Name, (char *)pObj, name ); // connect to the PO fanin if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) ) { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } @@ -270,13 +274,13 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) // this procedure also finalizes construction of the ABC network Abc_NtkFixNonDrivenNets( pNtk ); Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext ); + Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext ); + Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); // make sure everything is okay with the network structure - if ( !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheckRead( pNtk ) ) { printf( "CSAT_Check_Integrity: The internal network check has failed.\n" ); return 0; @@ -520,7 +524,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // create the array of PI names and values for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->names[i] = (char *)Abc_NtkCi(mng->pNtk, i)->pNext; // returns the same string that was given + mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given mng->pResult->values[i] = pModel[i]; } } @@ -623,6 +627,27 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Dumps the target AIG into the BENCH file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ) +{ + char * pName = NULL; + if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) ) + { + assert( 0 ); + } + return pName; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 39c6fae8..901bbac9 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -36,6 +36,7 @@ typedef struct Fraig_NodeStruct_t_ Fraig_Node_t; typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t; typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t; typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t; +typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t; struct Fraig_ParamsStruct_t_ { @@ -99,6 +100,9 @@ extern int Fraig_ManReadDoSparse( Fraig_Man_t * p ); extern int Fraig_ManReadChoicing( Fraig_Man_t * p ); extern int Fraig_ManReadVerbose( Fraig_Man_t * p ); extern int * Fraig_ManReadModel( Fraig_Man_t * p ); +extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ); +extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ); +extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ); extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed ); extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack ); @@ -124,6 +128,8 @@ extern int Fraig_NodeReadNumRefs( Fraig_Node_t * p ); extern int Fraig_NodeReadNumFanouts( Fraig_Node_t * p ); extern int Fraig_NodeReadSimInv( Fraig_Node_t * p ); extern int Fraig_NodeReadNumOnes( Fraig_Node_t * p ); +extern unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ); +extern unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p ); extern void Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData ); extern void Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData ); diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index c9e6960c..b92f6afd 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [fraigAccess.c] + FileName [fraigApi.c] PackageName [FRAIG: Functionally reduced AND-INV graphs.] @@ -58,6 +58,12 @@ int Fraig_ManReadDoSparse( Fraig_Man_t * p ) { int Fraig_ManReadChoicing( Fraig_Man_t * p ) { return p->fChoicing; } int Fraig_ManReadVerbose( Fraig_Man_t * p ) { return p->fVerbose; } int * Fraig_ManReadModel( Fraig_Man_t * p ) { return p->pModel; } +// returns the number of patterns used for random simulation (this number is fixed for the FRAIG run) +int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ) { return p->nWordsRand * 32; } +// returns the number of dynamic patterns accumulated at runtime (include SAT solver counter-examples and distance-1 patterns derived from them) +int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { return p->iWordStart * 32; } +// returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns) +int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; } /**Function************************************************************* @@ -104,6 +110,12 @@ int Fraig_NodeReadNumRefs( Fraig_Node_t * p ) { retu int Fraig_NodeReadNumFanouts( Fraig_Node_t * p ) { return p->nFanouts; } int Fraig_NodeReadSimInv( Fraig_Node_t * p ) { return p->fInv; } int Fraig_NodeReadNumOnes( Fraig_Node_t * p ) { return p->nOnes; } +// returns the pointer to the random simulation patterns (their number is returned by Fraig_ManReadPatternNumRandom) +// memory pointed to by this and the following procedure is maintained by the FRAIG package and exists as long as the package runs +unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ) { return p->puSimR; } +// returns the pointer to the dynamic simulation patterns (their number is returned by Fraig_ManReadPatternNumDynamic or Fraig_ManReadPatternNumDynamicFiltered) +// if the number of patterns is not evenly divisible by 32, the patterns beyond the given number contain garbage +unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p ) { return p->puSimD; } /**Function************************************************************* diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index ae20531d..5a7d0563 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [fraigAnd.c] + FileName [fraigCanon.c] PackageName [FRAIG: Functionally reduced AND-INV graphs.] diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 1c765c12..131b750c 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -259,8 +259,6 @@ struct Fraig_NodeStruct_t_ Fraig_Node_t * pRepr; // the canonical functional representative of the node // simulation data -// Fraig_Sims_t * pSimsR; // the random simulation info -// Fraig_Sims_t * pSimsD; // the systematic simulation info unsigned uHashR; // the hash value for random information unsigned uHashD; // the hash value for dynamic information unsigned * puSimR; // the simulation information (random) diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index cfdba619..e5979c93 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -53,7 +53,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) pParams->fChoicing = 0; // enables recording structural choices pParams->fTryProve = 1; // tries to solve the final miter pParams->fVerbose = 0; // the verbosiness flag - pParams->fVerboseP = 0; + pParams->fVerboseP = 0; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run } /**Function************************************************************* diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c index 9da9b88c..a6c1d5a6 100644 --- a/src/sat/fraig/fraigNode.c +++ b/src/sat/fraig/fraigNode.c @@ -113,6 +113,10 @@ clk = clock(); { // generate the simulation info pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED; + // for reasons that take very long to explain, it makes sense to have (0000000...) + // pattern in the set (this helps if we need to return the counter-examples) + if ( i == 0 ) + pNode->puSimR[i] <<= 1; // compute the hash key pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i]; } diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c index 7a8af749..d0f22acd 100644 --- a/src/sat/fraig/fraigTable.c +++ b/src/sat/fraig/fraigTable.c @@ -355,7 +355,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor return 0; // check the simulation info for ( i = 0; i < iWordLast; i++ ) - if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) + if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) return 0; } else @@ -365,7 +365,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor return 0; // check the simulation info for ( i = 0; i < iWordLast; i++ ) - if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) + if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) return 0; } return 1; |