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

Trying to add BMC to random simulation.

This commit is contained in:
Alan Mishchenko 2011-11-06 23:13:52 -08:00
parent 6a939b6382
commit 9382c8fdd1
3 changed files with 55 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/saig/saig.h
View File

@ -168,6 +168,7 @@ extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t *
extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigInd.c ==========================================================*/

44
src/aig/saig/saigDup.c
View File

@ -350,6 +350,50 @@ int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
return RetValue;
}
/**Function*************************************************************
Synopsis [Duplicates while ORing the POs of sequential circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj;
int i;
assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
pAigNew->pName = Aig_UtilStrsav( pAig->pName );
pAigNew->nConstrs = pAig->nConstrs;
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pAigNew );
// update the flop variables
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_NotCond( pObj->pData, Vec_IntEntry(vInit, i) );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// transfer to register outputs
Saig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
// update the flop variables
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreatePo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
// finalize
Aig_ManCleanup( pAigNew );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

10
src/aig/ssw/sswRarity.c
View File

@ -892,11 +892,13 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
***********************************************************************/
int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
{
int fTryBmc = 1;
int fMiter = 1;
Ssw_RarMan_t * p;
int r, f, clk, clkTotal = clock();
int nTimeToStop = time(NULL) + TimeOut;
int RetValue = -1;
int iFrameFail = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
// consider the case of empty AIG
@ -919,6 +921,14 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
for ( r = 0; r < nRounds; r++ )
{
clk = clock();
if ( fTryBmc )
{
Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail );
// if ( pNewAig->pSeqModel != NULL )
// printf( "BMC has found a counter-example in frame %d.\n", iFrameFail );
Aig_ManStop( pNewAig );
}
// simulate
for ( f = 0; f < nFrames; f++ )
{