diff options
author | Baruch Sterin <baruchs@gmail.com> | 2011-01-13 22:42:54 +0200 |
---|---|---|
committer | Baruch Sterin <baruchs@gmail.com> | 2011-01-13 22:42:54 +0200 |
commit | ab80b015a4efdf196334aafc19d589d48778f0bb (patch) | |
tree | 0a4af678193d4d84de98d0ecb0e141c17fa8ae87 /src/aig/gia | |
parent | 811f5631a812968ccdbe157549f2445747053d50 (diff) | |
parent | ae4b51351c93983a1285ce1028e3bbd90a6d5721 (diff) | |
download | abc-ab80b015a4efdf196334aafc19d589d48778f0bb.tar.gz abc-ab80b015a4efdf196334aafc19d589d48778f0bb.tar.bz2 abc-ab80b015a4efdf196334aafc19d589d48778f0bb.zip |
merge changes from main branch
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 5 | ||||
-rw-r--r-- | src/aig/gia/giaSim.c | 29 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 4 | ||||
-rw-r--r-- | src/aig/gia/module.make | 1 |
5 files changed, 37 insertions, 3 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 3358ca76..e3546686 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -179,6 +179,7 @@ struct Gia_ParSim_t_ // user-controlled parameters int nWords; // the number of machine words int nIters; // the number of timeframes + int RandSeed; // seed to generate random numbers int TimeLimit; // time limit in seconds int fCheckMiter; // check if miter outputs are non-zero int fVerbose; // enables verbose output diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 4c19b4f5..581383ea 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1049,6 +1049,11 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n break; if ( f == nFramesMax ) break; + if ( Gia_ManAndNum(pFrames) > 500000 ) + { + Gia_ManStop( pFrames ); + return NULL; + } Gia_ManStop( pFrames ); pFrames = NULL; } diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 68b50fb6..1de1a2d4 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -65,6 +65,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p ) // user-controlled parameters p->nWords = 8; // the number of machine words p->nIters = 32; // the number of timeframes + p->RandSeed = 0; // the seed to generate random numbers p->TimeLimit = 60; // time limit in seconds p->fCheckMiter = 0; // check if miter outputs are non-zero p->fVerbose = 0; // enables verbose output @@ -437,9 +438,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int int f, i, w, iPioId, Counter; p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; - p->iPo = iOut; + p->iPo = iOut; // fill in the binary data - Gia_ManRandom( 1 ); Counter = p->nRegs; pData = ABC_ALLOC( unsigned, nWords ); for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) @@ -468,14 +468,36 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int SeeAlso [] ***********************************************************************/ +void Gia_ManResetRandom( Gia_ParSim_t * pPars ) +{ + int i; + Gia_ManRandom( 1 ); + for ( i = 0; i < pPars->RandSeed; i++ ) + Gia_ManRandom( 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) { + extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); Gia_ManSim_t * p; int i, clkTotal = clock(); int iOut, iPat, RetValue = 0; + if ( pAig->pReprs && pAig->pNexts ) + return Gia_ManSimSimulateEquiv( pAig, pPars ); ABC_FREE( pAig->pCexSeq ); p = Gia_ManSimCreate( pAig, pPars ); - Gia_ManRandom( 1 ); + Gia_ManResetRandom( pPars ); Gia_ManSimInfoInit( p ); for ( i = 0; i < pPars->nIters; i++ ) { @@ -487,6 +509,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) } if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) ) { + Gia_ManResetRandom( pPars ); pPars->iOutFail = iOut; pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 002e766d..82bdb367 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -952,8 +952,12 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); Gia_ManForEachCo( pAig, pObj, k ) pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + { pObjRo->fMark0 = pObjRi->fMark0; + } } assert( iBit == p->nBits ); if ( fDualOut ) diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index fc1c5c73..fd0e0a5e 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -29,6 +29,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaShrink.c \ src/aig/gia/giaSim.c \ + src/aig/gia/giaSim2.c \ src/aig/gia/giaSort.c \ src/aig/gia/giaSpeedup.c \ src/aig/gia/giaSupMin.c \ |