diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 10 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaSim.c | 113 |
3 files changed, 122 insertions, 3 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 039628bf..fcdb3941 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -150,6 +150,7 @@ struct Gia_Man_t_ Vec_Ptr_t * vSeqModelVec; // sequential counter-examples Vec_Int_t vCopies; // intermediate copies Vec_Int_t vCopies2; // intermediate copies + Vec_Int_t * vVar2Obj; // mapping of variables into objects Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vGateClasses; // classes of gates for abstraction @@ -209,6 +210,11 @@ struct Gia_Man_t_ Vec_Wrd_t * vSimsPi; Vec_Int_t * vClassOld; Vec_Int_t * vClassNew; + // incremental simulation + int fIncrSim; + int iNextPi; + int iTimeStamp; + Vec_Int_t * vTimeStamps; // truth table computation for small functions int nTtVars; // truth table variables int nTtWords; // truth table words @@ -1518,6 +1524,10 @@ extern int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0 extern void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 ); extern void Gia_ManBuiltInSimResimulate( Gia_Man_t * p ); extern int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat ); +extern void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs ); +extern void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits ); +extern int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ); +extern int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 7d0ef288..bc270168 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -92,6 +92,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vClassOld ); Vec_WrdFreeP( &p->vSims ); Vec_WrdFreeP( &p->vSimsPi ); + Vec_IntFreeP( &p->vTimeStamps ); Vec_FltFreeP( &p->vTiming ); Vec_VecFreeP( &p->vClockDoms ); Vec_IntFreeP( &p->vCofVars ); @@ -118,6 +119,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vTruths ); Vec_IntErase( &p->vCopies ); Vec_IntErase( &p->vCopies2 ); + Vec_IntFreeP( &p->vVar2Obj ); Vec_IntErase( &p->vCopiesTwo ); Vec_IntErase( &p->vSuppVars ); Vec_WrdFreeP( &p->vSuppWords ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 192184c8..228f6fb4 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -800,7 +800,7 @@ void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj ) word * pInfo = Gia_ManBuiltInData( p, iObj ); word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) ); word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); - assert( p->fBuiltInSim ); + assert( p->fBuiltInSim || p->fIncrSim ); if ( Gia_ObjFaninC0(pObj) ) { if ( Gia_ObjFaninC1(pObj) ) @@ -860,7 +860,7 @@ int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ) { word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) ); word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w; - assert( p->fBuiltInSim ); + assert( p->fBuiltInSim || p->fIncrSim ); // printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); // Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" ); @@ -903,7 +903,7 @@ int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ) { word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) ); word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w; - assert( p->fBuiltInSim ); + assert( p->fBuiltInSim || p->fIncrSim ); // printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); // Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" ); @@ -1113,6 +1113,113 @@ int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vOb return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs ); } + + + + +/**Function************************************************************* + + Synopsis [Bit-parallel simulation during AIG construction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManIncrSimUpdate( Gia_Man_t * p ) +{ + int i, k; + // extend timestamp info + assert( Vec_IntSize(p->vTimeStamps) <= Gia_ManObjNum(p) ); + Vec_IntFillExtra( p->vTimeStamps, Gia_ManObjNum(p), 0 ); + // extend simulation info + assert( Vec_WrdSize(p->vSims) <= Gia_ManObjNum(p) * p->nSimWords ); + Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p) * p->nSimWords, 0 ); + // extend PI info + assert( p->iNextPi <= Gia_ManCiNum(p) ); + for ( i = p->iNextPi; i < Gia_ManCiNum(p); i++ ) + { + word * pSims = Gia_ManBuiltInData( p, Gia_ManCiIdToId(p, i) ); + for ( k = 0; k < p->nSimWords; k++ ) + pSims[k] = Gia_ManRandomW(0); + } + p->iNextPi = Gia_ManCiNum(p); +} +void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs ) +{ + assert( !p->fIncrSim ); + p->fIncrSim = 1; + p->iPatsPi = 0; + p->nSimWords = nWords; + // init time stamps + p->iTimeStamp = 1; + p->vTimeStamps = Vec_IntAlloc( p->nSimWords ); + // init object sim info + p->iNextPi = 0; + p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs ); + Gia_ManRandomW( 1 ); +} +void Gia_ManIncrSimStop( Gia_Man_t * p ) +{ + assert( p->fIncrSim ); + p->fIncrSim = 0; + p->iPatsPi = 0; + p->nSimWords = 0; + p->iTimeStamp = 1; + Vec_IntFreeP( &p->vTimeStamps ); + Vec_WrdFreeP( &p->vSims ); +} +void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits ) +{ + int i, iLit; + assert( Vec_IntSize(vObjLits) > 0 ); + p->iTimeStamp++; + Vec_IntForEachEntry( vObjLits, iLit, i ) + { + word * pSims = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit) ); + if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) ) + continue; + //assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 ); + //Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp); + if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) ) + Abc_TtXorBit(pSims, p->iPatsPi); + } + p->iPatsPi = (p->iPatsPi == p->nSimWords * 64 - 1) ? 0 : p->iPatsPi + 1; +} +void Gia_ManIncrSimCone_rec( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + return; + if ( Vec_IntEntry(p->vTimeStamps, iObj) == p->iTimeStamp ) + return; + assert( Vec_IntEntry(p->vTimeStamps, iObj) < p->iTimeStamp ); + Vec_IntWriteEntry( p->vTimeStamps, iObj, p->iTimeStamp ); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId0(pObj, iObj) ); + Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId1(pObj, iObj) ); + Gia_ManBuiltInSimPerformInt( p, iObj ); +} +int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + assert( iLit0 > 1 && iLit1 > 1 ); + Gia_ManIncrSimUpdate( p ); + Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) ); + Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) ); + return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 ); +} +int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + assert( iLit0 > 1 && iLit1 > 1 ); + Gia_ManIncrSimUpdate( p ); + Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) ); + Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) ); + return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |