diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-30 20:19:28 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-30 20:19:28 +0700 |
| commit | 43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2 (patch) | |
| tree | dfad6e5d82a5866529e93a18b171a3a96de6f0e8 /src | |
| parent | b8de7a28e08a68860a9b88ee47a27841f83b5083 (diff) | |
| download | abc-43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2.tar.gz abc-43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2.tar.bz2 abc-43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2.zip | |
Changes to enable smarter simulation.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/ssw/sswRarity.c | 8 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 8 |
2 files changed, 15 insertions, 1 deletions
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c index f3c0b967..365e4b6a 100644 --- a/src/aig/ssw/sswRarity.c +++ b/src/aig/ssw/sswRarity.c @@ -833,7 +833,12 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex // record the new pattern vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) ); Saig_ManForEachLo( pAig, pObj, i ) + { +//printf( "%d", pObj->fMarkB ); Vec_IntPush( vInit, pObj->fMarkB ); + } +//printf( "\n" ); + Aig_ManCleanMarkB( pAig ); return vInit; } @@ -975,7 +980,10 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize // compute starting state if needed assert( p->vInits == NULL ); if ( pCex ) + { p->vInits = Ssw_RarFindStartingState( pAig, pCex ); + printf( "Beginning simulation from the state derived using the counter-example.\n" ); + } else p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) ); // duplicate the array diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 980ba7ed..3e2f720e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -25438,6 +25438,11 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fUseCex ) { + if ( pAbc->pCex == NULL ) + { + Abc_Print( 0, "Abc_CommandAbc9Equiv3(): Counter-example is not available.\n" ); + return 0; + } if ( pAbc->pCex->nPis != Gia_ManPiNum(pAbc->pGia) ) { Abc_Print( -1, "Abc_CommandAbc9Equiv3(): The number of PIs differs in cex (%d) and in AIG (%d).\n", @@ -25450,7 +25455,8 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) // 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 ); + if ( pAbc->pGia->pCexSeq ) + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: |