summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-01-25 06:49:49 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-01-25 06:49:49 +0700
commit853222ee7bf8e1f79120666707ce754cd9169564 (patch)
tree5bebbb9245ee6b46895697614072aef47da8aec4
parentedd4b2a29c3a75709b6394fd205384dd0fe90e5d (diff)
downloadabc-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.c5
-rw-r--r--src/proof/ssw/sswRarity.c32
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 );