From 9a2a0f2912e296e866ba220dce6ccf25018cf29b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 21 Jul 2011 17:55:44 +0700 Subject: Changes to enable smarter simulation. --- src/aig/saig/saigMiter.c | 2 +- src/aig/ssw/ssw.h | 3 + src/aig/ssw/sswRarity.c | 159 +++++++++++++++++++++++++++++++++++++++-------- src/aig/ssw/sswSim.c | 8 ++- src/base/abci/abc.c | 153 +++++++++++++++++++++++++++++++++++++++++---- src/base/abci/abcDar.c | 46 ++++++++++++++ 6 files changed, 331 insertions(+), 40 deletions(-) diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 4a430a60..c50eaac5 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -1234,7 +1234,7 @@ int Saig_ManDemiterNew( Aig_Man_t * pMan ) vSuper = Vec_PtrAlloc( 100 ); Saig_ManForEachPo( pMan, pObj, i ) { - if ( pMan->nConstrs && i >= pMan->nConstrs ) + if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs ) break; printf( "Output %3d : ", i ); if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 07c31a74..6f453041 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -115,6 +115,8 @@ extern int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ); extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); +/*=== sswRarity.c ===================================================*/ +extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, 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 ); @@ -125,6 +127,7 @@ extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p ); extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ); extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); extern void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit ); +extern int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p ); extern Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p ); diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c index f07b0f2a..64f82278 100644 --- a/src/aig/ssw/sswRarity.c +++ b/src/aig/ssw/sswRarity.c @@ -94,11 +94,12 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n p->nFrames = nFrames; p->nBinSize = nBinSize; p->fVerbose = fVerbose; - p->nGroups = Aig_ManRegNum(pAig) / nBinSize; - p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); - p->pGroupValues = ABC_CALLOC( int, (Aig_ManRegNum(pAig) / nBinSize) ); + p->nGroups = Aig_ManRegNum(pAig) / nBinSize; + p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); + p->pGroupValues = ABC_CALLOC( int, p->nGroups ); p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 ); p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords ); + p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml ); return p; } @@ -115,8 +116,8 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n ***********************************************************************/ void Ssw_RarManStop( Ssw_RarMan_t * p ) { - Ssw_SmlStop( p->pSml ); - Ssw_ClassesStop( p->ppClasses ); + if ( p->pSml ) Ssw_SmlStop( p->pSml ); + if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); Vec_PtrFreeP( &p->vSimInfo ); Vec_IntFreeP( &p->vInits ); ABC_FREE( p->pGroupValues ); @@ -142,19 +143,34 @@ void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) Aig_Obj_t * pObj; unsigned * pData; int i, k; +/* + Saig_ManForEachLi( p->pAig, pObj, i ) + { + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" ); + } +*/ for ( k = 0; k < p->nWords * 32; k++ ) { for ( i = 0; i < p->nGroups; i++ ) p->pGroupValues[i] = 0; Saig_ManForEachLi( p->pAig, pObj, i ) { - pData = Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ); - if ( Aig_InfoHasBit(pData, k) ) + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); } for ( i = 0; i < p->nGroups; i++ ) Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] ); } +/* + for ( i = 0; i < p->nGroups; i++ ) + { + for ( k = 0; k < (1 << p->nBinSize); k++ ) + printf( "%d ", Ssw_RarGetBinPat(p, i, k) ); + printf( "\n" ); + } +*/ } /**Function************************************************************* @@ -173,21 +189,36 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) Aig_Obj_t * pObj; unsigned * pData; int i, k, Value; - for ( i = 0; i < p->nWords * 32; i++ ) - p->pPatCosts[i] = 0.0; - for ( i = 0; i < p->nGroups; i++ ) + + // for each pattern + for ( k = 0; k < p->nWords * 32; k++ ) { - for ( k = 0; k < p->nWords * 32; k++ ) + for ( i = 0; i < p->nGroups; i++ ) + p->pGroupValues[i] = 0; + // compute its group values + Saig_ManForEachLi( p->pAig, pObj, i ) + { + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) + p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); + } + // find the cost of its values + p->pPatCosts[k] = 0.0; + for ( i = 0; i < p->nGroups; i++ ) { - Value = Ssw_RarGetBinPat( p, i, k ); - if ( Value == 0 ) - continue; + Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] ); + assert( Value > 0 ); p->pPatCosts[k] += 1.0/(Value*Value); +// printf( "%d ", Value ); } +// printf( "\n" ); + // print the result +// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); } + // choose as many as there are words Vec_IntClear( vInits ); - for ( i = 0; i < p->nFrames; i++ ) + for ( i = 0; i < p->nWords; i++ ) { // select the best int iPatBest = -1; @@ -202,13 +233,15 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) assert( iPatBest >= 0 ); p->pPatCosts[iPatBest] = -ABC_INFINITY; // set the flops - Saig_ManForEachLo( p->pAig, pObj, k ) + Saig_ManForEachLi( p->pAig, pObj, k ) { - pData = Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ); + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) ); } +//printf( "Best pattern %5d\n", iPatBest ); + } - assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nFrames ); + assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); } @@ -265,15 +298,14 @@ Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) Synopsis [Filter equivalence classes of nodes.] - Description [Unrolls at most nFramesMax frames. Works with nConfMax - conflicts until the first undefined SAT call. Verbose prints the message.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int nRounds, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int nRounds, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { Ssw_RarMan_t * p; int r, i, k, clkTotal = clock(); @@ -281,7 +313,7 @@ void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSiz assert( Aig_ManConstrNum(pAig) == 0 ); // consider the case of empty AIG if ( Aig_ManNodeNum(pAig) == 0 ) - return; + return -1; // reset random numbers Aig_ManRandom( 1 ); // create manager @@ -299,13 +331,11 @@ void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSiz else p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) ); // duplicate the array - for ( i = 1; i < nFrames; i++ ) + for ( i = 1; i < nWords; i++ ) for ( k = 0; k < Aig_ManRegNum(pAig); k++ ) Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) ); - assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nFrames ); + assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords ); // initialize simulation manager - p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords ); - p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml ); Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // print the stats if ( fVerbose ) @@ -349,6 +379,83 @@ void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSiz } // cleanup Ssw_RarManStop( p ); + return -1; +} + + + +/**Function************************************************************* + + Synopsis [Perform sequential simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) +{ + int fMiter = 1; + Ssw_RarMan_t * p; + int r, clk, clkTotal = clock(); + int RetValue = -1; + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManConstrNum(pAig) == 0 ); + // consider the case of empty AIG + if ( Aig_ManNodeNum(pAig) == 0 ) + return -1; + if ( fVerbose ) + printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d timeout.\n", + nWords, nFrames, nBinSize, nRounds, TimeOut ); + // reset random numbers + Aig_ManRandom( 1 ); + // create manager + p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); + p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); + Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); + // perform simulation rounds + for ( r = 0; r < nRounds; r++ ) + { + clk = clock(); + // simulate + Ssw_SmlSimulateOne( p->pSml ); + if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) + { + if ( fVerbose ) printf( "\n" ); + printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + RetValue = 0; + break; + } + // get initialization patterns + Ssw_RarUpdateCounters( p ); + Ssw_RarTransferPatterns( p, p->vInits ); + Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); + // printout + if ( fVerbose ) + { +// printf( "Round %3d: ", r ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + printf( "." ); + } + // check timeout + if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + { + if ( fVerbose ) printf( "\n" ); + printf( "Reached timeout (%d seconds).\n", TimeOut ); + break; + } + } + if ( r == nRounds ) + { + if ( fVerbose ) printf( "\n" ); + printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + } + // cleanup + Ssw_RarManStop( p ); + return RetValue; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 37fc16af..daee24ec 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -928,11 +928,11 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit ) { Aig_Obj_t * pObj; - int Entry, i, k, nRegs; + int Entry, i, nRegs; nRegs = Aig_ManRegNum(p->pAig); assert( nRegs > 0 ); assert( nRegs <= Aig_ManPiNum(p->pAig) ); - assert( Vec_IntSize(vInit) == nRegs * p->nFrames ); + assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame ); // assign random info for primary inputs Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_SmlAssignRandom( p, pObj ); @@ -982,8 +982,12 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p ) Aig_Obj_t * pObj; int i; Saig_ManForEachPo( p->pAig, pObj, i ) + { + if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs ) + return 0; if ( !Ssw_SmlNodeIsZero(p, pObj) ) return 1; + } return 0; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 209433df..c7bd3634 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -247,6 +247,7 @@ static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSim2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -666,6 +667,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 ); + Cmd_CommandAdd( pAbc, "Sequential", "sim2", Abc_CommandSim2, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 ); @@ -15764,6 +15766,135 @@ usage: return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSim2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + int c; + int nFrames; + int nWords; + int nBinSize; + int nRounds; + int TimeOut; + int fVerbose; + extern int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); + // set defaults + nFrames = 20; + nWords = 50; + nBinSize = 8; + nRounds = 80; + TimeOut = 0; + fVerbose = 1; + // parse command line + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTvh" ) ) != 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 '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 ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "Only works for strashed networks.\n" ); + return 1; + } + ABC_FREE( pNtk->pSeqModel ); + pAbc->Status = Abc_NtkDarSeqSim2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ); + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + return 0; + +usage: + Abc_Print( -2, "usage: sim2 [-FWBRT 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-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 [] @@ -24632,30 +24763,30 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Gia_ManSimSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFRTmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWRTmvh" ) ) != EOF ) { switch ( c ) { - case 'W': + case 'F': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - pPars->nWords = atoi(argv[globalUtilOptind]); + pPars->nIters = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nWords < 0 ) + if ( pPars->nIters < 0 ) goto usage; break; - case 'F': + case 'W': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); goto usage; } - pPars->nIters = atoi(argv[globalUtilOptind]); + pPars->nWords = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nIters < 0 ) + if ( pPars->nWords < 0 ) goto usage; break; case 'R': @@ -24713,11 +24844,11 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &sim [-WFRT num] [-mvh]\n" ); + Abc_Print( -2, "usage: &sim [-FWRT 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-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); 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-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" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 97ee8c42..ff8aac38 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3007,6 +3007,52 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in return RetValue; } +/**Function************************************************************* + + Synopsis [Performs random simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) +{ + Aig_Man_t * pMan; + int status, RetValue = -1, clk = clock(); + if ( Abc_NtkGetChoiceNum(pNtk) ) + { + printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) ); + Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc); + } + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ) ) + { + if ( pMan->pSeqModel ) + { + printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", + nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame ); + status = Saig_ManVerifyCex( pMan, pMan->pSeqModel ); + if ( status == 0 ) + printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); + } + ABC_FREE( pNtk->pModel ); + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; + RetValue = 0; + } + else + { + printf( "Simulation of %d frames with %d words did not assert the outputs. ", + nFrames, nWords ); + } + ABC_PRT( "Time", clock() - clk ); + Aig_ManStop( pMan ); + return RetValue; +} + /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] -- cgit v1.2.3