luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixed a corner-case when 'sim3 -a' does not work for costant POs.

This commit is contained in:
Alan Mishchenko 2013-01-25 06:49:49 +07:00
parent edd4b2a29c
commit 853222ee7b
2 changed files with 32 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/base/abci/abc.c
View File

@ -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;

32
src/proof/ssw/sswRarity.c
View File

@ -421,6 +421,28 @@ 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_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.]
@ -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 );