From 2ea0ded0bced0c24ed3ec498ca8d7701315b7408 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 30 Jul 2011 13:30:04 +0700 Subject: Changes to enable smarter simulation. --- src/aig/ssw/ssw.h | 4 +- src/aig/ssw/sswRarity.c | 10 +-- src/aig/ssw/sswRarity2.c | 171 ++++++++++++++++++++++++++------------ src/base/abci/abc.c | 212 ++++++++++++++++++++++++++++++++++++++++++----- src/base/abci/abcDar.c | 4 +- 5 files changed, 319 insertions(+), 82 deletions(-) diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 7632d923..1361893a 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -119,8 +119,8 @@ extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); /*=== sswRarity2.c ===================================================*/ -extern int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); -extern int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); +extern int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); +extern int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); /*=== sswSim.c ===================================================*/ extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c index f24e2d85..3026cf6b 100644 --- a/src/aig/ssw/sswRarity.c +++ b/src/aig/ssw/sswRarity.c @@ -261,7 +261,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex int f, i, iBit; // assign register outputs Saig_ManForEachLi( pAig, pObj, i ) - pObj->fMarkB = 0; + pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i ); // simulate the timeframes iBit = pCex->nRegs; for ( f = 0; f <= pCex->iFrame; f++ ) @@ -304,7 +304,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex SeeAlso [] ***********************************************************************/ -int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) +int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) { int fMiter = 1; Ssw_RarMan_t * p; @@ -381,7 +381,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { int fMiter = 0; Ssw_RarMan_t * p; @@ -486,7 +486,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { Aig_Man_t * pAig; int RetValue; @@ -497,7 +497,7 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize ABC_FREE( p->pReprs ); ABC_FREE( p->pNexts ); } - RetValue = Ssw_RarSignalFilter( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); + RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); Gia_ManReprFromAigRepr( pAig, p ); Aig_ManStop( pAig ); return RetValue; diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c index c0305931..59f59f93 100644 --- a/src/aig/ssw/sswRarity2.c +++ b/src/aig/ssw/sswRarity2.c @@ -87,6 +87,25 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6 /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Prepares random number generator.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_RarManPrepareRandom( int nRandSeed ) +{ + int i; + Aig_ManRandom( 1 ); + for ( i = 0; i < nRandSeed; i++ ) + Aig_ManRandom( 0 ); +} + /**Function************************************************************* Synopsis [Initializes random primary inputs.] @@ -133,7 +152,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin // compute the pattern sequence iPatThis = iPatFinal; vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 ); - Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatFinal ); + Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis ); for ( r = iFrame / p->nFrames - 1; r >= 0; r-- ) { iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 ); @@ -145,7 +164,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin pCex->iPo = iPo; // insert the bits iBit = Aig_ManRegNum(p->pAig); - for ( f = 0; f < iFrame; f++ ) + for ( f = 0; f <= iFrame; f++ ) { Ssw_RarManAssingRandomPis( p ); iPatThis = Vec_IntEntry( vTrace, f / p->nFrames ); @@ -158,6 +177,19 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin } } Vec_IntFree( vTrace ); + assert( iBit == pCex->nBits ); + // verify the counter example + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) + { + printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" ); + Abc_CexFree( pCex ); + pCex = NULL; + } + else + { +// printf( "Counter-example verification is successful.\n" ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + } return pCex; } @@ -383,34 +415,6 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) } } -/**Function************************************************************* - - Synopsis [Returns 1 if simulation info is composed of all zeros.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) -{ - word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - word Flip = pObj->fPhase ? ~0 : 0; - int w, i; - for ( w = 0; w < p->nWords; w++ ) - if ( pSim[w] ^ Flip ) - { - for ( i = 0; i < 64; i++ ) - if ( ((pSim[w] ^ Flip) >> i) & 1 ) - break; - assert( i < 64 ); - return w * 64 + i; - } - return -1; -} - /**Function************************************************************* Synopsis [Returns 1 if simulation info is composed of all zeros.] @@ -494,6 +498,34 @@ unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) return uHash; } +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) +{ + word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + word Flip = pObj->fPhase ? ~0 : 0; + int w, i; + for ( w = 0; w < p->nWords; w++ ) + if ( pSim[w] ^ Flip ) + { + for ( i = 0; i < 64; i++ ) + if ( ((pSim[w] ^ Flip) >> i) & 1 ) + break; + assert( i < 64 ); + return w * 64 + i; + } + return -1; +} + /**Function************************************************************* Synopsis [Check if any of the POs becomes non-constant.] @@ -509,7 +541,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) { Aig_Obj_t * pObj; int i; - p->iFailPo = -1; + p->iFailPo = -1; p->iFailPat = -1; Saig_ManForEachPo( p->pAig, pObj, i ) { @@ -772,7 +804,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex int f, i, iBit; // assign register outputs Saig_ManForEachLi( pAig, pObj, i ) - pObj->fMarkB = 0; + pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i ); // simulate the timeframes iBit = pCex->nRegs; for ( f = 0; f <= pCex->iFrame; f++ ) @@ -815,7 +847,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex SeeAlso [] ***********************************************************************/ -int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) +int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) { int fMiter = 1; Ssw_RarMan_t * p; @@ -827,10 +859,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", - nWords, nFrames, nBinSize, nRounds, TimeOut ); + printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", + nWords, nFrames, nRounds, nRandSeed, TimeOut ); // reset random numbers - Aig_ManRandom( 1 ); + Ssw_RarManPrepareRandom( nRandSeed ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); @@ -847,7 +879,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) { if ( fVerbose ) printf( "\n" ); - printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); +// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + Ssw_RarManPrepareRandom( nRandSeed ); ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); RetValue = 0; @@ -872,7 +905,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i } } finish: - if ( r == nRounds ) + if ( r == nRounds && f == nFrames ) { if ( fVerbose ) printf( "\n" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); @@ -884,6 +917,30 @@ finish: } +/**Function************************************************************* + + Synopsis [Perform sequential simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) +{ + Aig_Man_t * pAig; + int RetValue; + pAig = Gia_ManToAigSimple( p ); + RetValue = Ssw_RarSimulate2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); + // save counter-example + Abc_CexFree( p->pCexSeq ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + return RetValue; +} + /**Function************************************************************* Synopsis [Filter equivalence classes of nodes.] @@ -895,9 +952,8 @@ finish: SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { - int fMiter = 0; Ssw_RarMan_t * p; int r, f, i, k, clkTotal = clock(); int RetValue = -1; @@ -907,10 +963,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", - nWords, nFrames, nBinSize, nRounds, TimeOut ); + printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", + nWords, nFrames, nRounds, nRandSeed, TimeOut ); // reset random numbers - Aig_ManRandom( 1 ); + Ssw_RarManPrepareRandom( nRandSeed ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); @@ -953,9 +1009,11 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f ); if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - ABC_FREE( pAig->pSeqModel ); + if ( !fVerbose ) + printf( "\r" ); +// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + Ssw_RarManPrepareRandom( nRandSeed ); + Abc_CexFree( pAig->pSeqModel ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); RetValue = 0; goto finish; @@ -968,25 +1026,31 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz goto finish; } } + // get initialization patterns + Ssw_RarTransferPatterns( p, p->vInits ); // printout if ( fVerbose ) { printf( "Round %3d: ", r ); Ssw_ClassesPrint( p->ppClasses, 0 ); } - // get initialization patterns - Ssw_RarTransferPatterns( p, p->vInits ); + else + { + printf( "." ); + } } finish: // report - if ( r == nRounds ) + if ( r == nRounds && f == nFrames ) { + if ( !fVerbose ) + printf( "\r" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup Ssw_RarManStop( p ); - return -1; + return RetValue; } /**Function************************************************************* @@ -1000,7 +1064,7 @@ finish: SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { Aig_Man_t * pAig; int RetValue; @@ -1011,8 +1075,11 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz ABC_FREE( p->pReprs ); ABC_FREE( p->pNexts ); } - RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); + RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose ); Gia_ManReprFromAigRepr( pAig, p ); + // save counter-example + Abc_CexFree( p->pCexSeq ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); return RetValue; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7756dbdc..e319c4f8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -337,6 +337,7 @@ static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Sim3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -758,6 +759,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sim3", Abc_CommandAbc9Sim3, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&resim", Abc_CommandAbc9Resim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&speci", Abc_CommandAbc9SpecI, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv", Abc_CommandAbc9Equiv, 0 ); @@ -15795,19 +15797,21 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nWords; int nBinSize; int nRounds; + int nRandSeed; int TimeOut; int fVerbose; - extern int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); + extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); // set defaults nFrames = 20; nWords = 50; nBinSize = 8; nRounds = 80; + nRandSeed = 0; TimeOut = 0; - fVerbose = 1; + fVerbose = 0; // parse command line Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTvh" ) ) != EOF ) { switch ( c ) { @@ -15855,6 +15859,17 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nRounds < 0 ) goto usage; break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nRandSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRandSeed < 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -15886,17 +15901,19 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } ABC_FREE( pNtk->pSeqModel ); - pAbc->Status = Abc_NtkDarSeqSim2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ); + pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); +// pAbc->nFrames = pAbc->pCex->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); return 0; usage: - Abc_Print( -2, "usage: sim3 [-FWBRT num] [-vh]\n" ); + Abc_Print( -2, "usage: sim3 [-FWBRNT num] [-vh]\n" ); Abc_Print( -2, "\t performs random simulation of the sequential miter\n" ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize ); Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", nRounds ); + Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -24644,7 +24661,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Gia_ManSimSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWRTmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWNTmvh" ) ) != EOF ) { switch ( c ) { @@ -24670,10 +24687,10 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nWords < 0 ) goto usage; break; - case 'R': + case 'N': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } pPars->RandSeed = atoi(argv[globalUtilOptind]); @@ -24725,12 +24742,12 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &sim [-FWRT num] [-mvh]\n" ); + Abc_Print( -2, "usage: &sim [-FWNT num] [-mvh]\n" ); Abc_Print( -2, "\t performs random simulation of the sequential miter\n" ); Abc_Print( -2, "\t (if candidate equivalences are defined, performs refinement)\n" ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); - Abc_Print( -2, "\t-R num : random number seed (1 <= num <= 10000) [default = %d]\n", pPars->RandSeed ); + Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", pPars->RandSeed ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -24738,6 +24755,142 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c; + int nFrames; + int nWords; + int nBinSize; + int nRounds; + int nRandSeed; + int TimeOut; + int fVerbose; + extern int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); + // set defaults + nFrames = 20; + nWords = 50; + nBinSize = 8; + nRounds = 80; + nRandSeed = 0; + TimeOut = 0; + fVerbose = 0; + // parse command line + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nWords < 0 ) + goto usage; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + nBinSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBinSize < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRounds = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRounds < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nRandSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRandSeed < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + TimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOut < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" ); + return 1; + } + pAbc->Status = Ssw_RarSimulate2Gia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); +// pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + return 0; + +usage: + Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-vh]\n" ); + Abc_Print( -2, "\t performs random simulation of the sequential miter\n" ); + Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); + Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize ); + Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", nRounds ); + Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); + Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + /**Function************************************************************* Synopsis [] @@ -25156,21 +25309,22 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) { -// extern int Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); - extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); - extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); +// extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); + extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); int c; int nFrames = 20; int nWords = 50; int nBinSize = 8; int nRounds = 80; + int nRandSeed = 0; int TimeOut = 0; + int fMiter = 0; int fUseCex = 0; int fLatchOnly = 0; int fNewAlgo = 1; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTmxlavh" ) ) != EOF ) { switch ( c ) { @@ -25218,6 +25372,17 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nRounds < 0 ) goto usage; break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nRandSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRandSeed < 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -25229,6 +25394,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( TimeOut < 0 ) goto usage; break; + case 'm': + fMiter ^= 1; + break; case 'x': fUseCex ^= 1; break; @@ -25266,22 +25434,24 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } } - if ( fNewAlgo ) - pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); - else - pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); -// pAbc->nFrames = pAbc->pCex->iFrame; -// Abc_FrameReplaceCex( pAbc, &pAbc->pCex ); +// if ( fNewAlgo ) + pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); +// else +// pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); +// pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &equiv3 [-FWRT num] [-xlvh]\n" ); + Abc_Print( -2, "usage: &equiv3 [-FWRNT num] [-mxlvh]\n" ); Abc_Print( -2, "\t computes candidate equivalence classes\n" ); Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFrames ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); // Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize ); Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds ); + Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeOut ); + Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "circuit" ); Abc_Print( -2, "\t-x : toggle using the current CEX to perform refinement [default = %s]\n", fUseCex? "yes": "no" ); Abc_Print( -2, "\t-l : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "yes": "no" ); Abc_Print( -2, "\t-a : toggle using a new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 0f1ee007..4232ab1f 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3017,7 +3017,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in SeeAlso [] ***********************************************************************/ -int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) +int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) { Aig_Man_t * pMan; int status, RetValue = -1, clk = clock(); @@ -3027,7 +3027,7 @@ int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc); } pMan = Abc_NtkToDar( pNtk, 0, 1 ); - if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ) == 0 ) + if ( Ssw_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 ) { if ( pMan->pSeqModel ) { -- cgit v1.2.3