diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 48 | ||||
-rw-r--r-- | src/base/abci/abcAttach.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcBalance.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcDsd.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcFpga.c | 5 | ||||
-rw-r--r-- | src/base/abci/abcFraig.c | 30 | ||||
-rw-r--r-- | src/base/abci/abcFxu.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcMap.c | 8 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 9 | ||||
-rw-r--r-- | src/base/abci/abcNtbdd.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcReconv.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcRefactor.c | 12 | ||||
-rw-r--r-- | src/base/abci/abcRenode.c | 5 | ||||
-rw-r--r-- | src/base/abci/abcRewrite.c | 18 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcSweep.c | 9 | ||||
-rw-r--r-- | src/base/abci/abcSymm.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcUnreach.c | 3 |
19 files changed, 90 insertions, 102 deletions
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 ); |