diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 06:49:49 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 06:49:49 +0700 |
| commit | 853222ee7bf8e1f79120666707ce754cd9169564 (patch) | |
| tree | 5bebbb9245ee6b46895697614072aef47da8aec4 | |
| parent | edd4b2a29c3a75709b6394fd205384dd0fe90e5d (diff) | |
| download | abc-853222ee7bf8e1f79120666707ce754cd9169564.tar.gz abc-853222ee7bf8e1f79120666707ce754cd9169564.tar.bz2 abc-853222ee7bf8e1f79120666707ce754cd9169564.zip | |
Fixed a corner-case when 'sim3 -a' does not work for costant POs.
| -rw-r--r-- | src/base/abci/abc.c | 5 | ||||
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 32 |
2 files changed, 32 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 25a7638c..e7a3991e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17884,6 +17884,11 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Only works for strashed networks.\n" ); return 1; } + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + Abc_Print( -1, "Only works for sequential networks.\n" ); + return 1; + } ABC_FREE( pNtk->pSeqModel ); pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ); // pAbc->nFrames = pAbc->pCex->iFrame; diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index d2c6451e..67501d97 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -432,6 +432,28 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) SeeAlso [] ***********************************************************************/ +int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj ) +{ + Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; + word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + int w; + for ( w = 0; w < p->nWords; w++ ) + if ( pSim[w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj ) { Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; @@ -558,7 +580,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFr break; if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; - if ( Ssw_RarManObjIsConst(p, pObj) ) + if ( Ssw_RarManPoIsConst0(p, pObj) ) continue; RetValue = 1; p->iFailPo = i; @@ -936,11 +958,11 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in assert( Aig_ManConstrNum(pAig) == 0 ); ABC_FREE( pAig->pSeqModel ); // consider the case of empty AIG - if ( Aig_ManNodeNum(pAig) == 0 ) - return -1; +// if ( Aig_ManNodeNum(pAig) == 0 ) +// return -1; // check trivially SAT miters - if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) - return 0; +// if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) +// return 0; if ( fVerbose ) Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", nWords, nFrames, nRounds, nRandSeed, TimeOut ); |