diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 24 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c | 5 |
3 files changed, 28 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c2eead14..78519d40 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6293,7 +6293,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // pNtkRes = Abc_NtkDar( pNtk ); - pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 ); + pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -10974,12 +10974,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int nFramesP; int nFramesK; + int nMaxImps; int fExdc; int fUseImps; int fRewrite; int fLatchCorr; int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10988,13 +10989,14 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nFramesP = 0; nFramesK = 1; + nMaxImps = 5000; fExdc = 1; fUseImps = 0; fRewrite = 0; fLatchCorr = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PFeirlvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF ) { switch ( c ) { @@ -11020,6 +11022,17 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFramesK <= 0 ) goto usage; break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nMaxImps = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nMaxImps <= 0 ) + goto usage; + break; case 'e': fExdc ^= 1; break; @@ -11061,7 +11074,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -11072,10 +11085,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-P num] [-F num] [-ilrvh]\n" ); + fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); + fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" ); fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 99217030..ce783c95 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -892,11 +892,12 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; Aig_Man_t * pMan, * pTemp; + int clk = clock(); // preprocess the miter by fraiging it // (note that for each functional class, fraiging leaves one representative; @@ -905,13 +906,17 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in Params.nBTLimit = 100000; pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); // pNtkFraig = Abc_NtkDup( pNtk ); +if ( fVerbose ) +{ +PRT( "Initial fraiging time", clock() - clk ); +} pMan = Abc_NtkToDar( pNtkFraig, 1 ); Abc_NtkDelete( pNtkFraig ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) @@ -1033,7 +1038,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return NULL; - pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose ); + pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 ); Aig_ManStop( pTemp ); // pMan = Aig_ManReduceLaches( pMan, 1 ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 4c061637..004d1f39 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -127,13 +127,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) /* { FILE * pTable; - pTable = fopen( "iscas/seqmap__stats.txt", "a+" ); + pTable = fopen( "xs/reg_stats.txt", "a+" ); fprintf( pTable, "%s ", pNtk->pName ); - fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) ); - fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) ); fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) ); fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) ); - fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) ); fprintf( pTable, "\n" ); fclose( pTable ); } |