diff options
Diffstat (limited to 'src/aig/saig/saigSimExt.c')
-rw-r--r-- | src/aig/saig/saigSimExt.c | 249 |
1 files changed, 241 insertions, 8 deletions
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index 22d5d6b8..9828d17e 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -21,6 +21,9 @@ #include "saig.h" #include "ssw.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -49,13 +52,13 @@ static inline int Saig_ManSimInfoAnd( int Value0, int Value1 ) static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) { - unsigned * pInfo = Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1)); } static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) { - unsigned * pInfo = Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); assert( Value >= SAIG_ZER && Value <= SAIG_UND ); Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame ); pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1)); @@ -107,7 +110,7 @@ int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) SeeAlso [] ***********************************************************************/ -int Saig_ManSimDataInit( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ) +int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ) { Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, f, Entry, iBit = 0; @@ -146,7 +149,7 @@ int Saig_ManSimDataInit( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, SeeAlso [] ***********************************************************************/ -int Saig_ManExtendOne( Aig_Man_t * p, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, +int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 ) { Aig_Obj_t * pFanout, * pObj = Aig_ManPi(p, iPi); @@ -247,7 +250,7 @@ void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExample0( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) { Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; @@ -297,14 +300,244 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_C SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExample1( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +{ + Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; + int i, f, Value; +// assert( Aig_ManRegNum(p) > 0 ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + // start simulation data + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); + assert( Value == SAIG_ONE ); + // select the result + vRes = Vec_IntAlloc( 1000 ); + vResInv = Vec_IntAlloc( 1000 ); + vVis = Vec_IntAlloc( 1000 ); + vVis2 = Vec_IntAlloc( 1000 ); + vUndo = Vec_IntAlloc( 1000 ); + for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- ) + { + Vec_IntClear( vUndo ); + for ( f = pCex->iFrame; f >= 0; f-- ) + if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) + { + Saig_ManExtendUndo( p, vSimInfo, vUndo ); + break; + } + if ( f >= 0 ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + Vec_IntFree( vVis ); + Vec_IntFree( vVis2 ); + Vec_IntFree( vUndo ); + // resimulate to make sure it is valid + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); + assert( Value == SAIG_ONE ); + Vec_IntFree( vResInv ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExample2( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +{ + Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; + int i, f, Value; +// assert( Aig_ManRegNum(p) > 0 ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + // start simulation data + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); + assert( Value == SAIG_ONE ); + // select the result + vRes = Vec_IntAlloc( 1000 ); + vResInv = Vec_IntAlloc( 1000 ); + vVis = Vec_IntAlloc( 1000 ); + vVis2 = Vec_IntAlloc( 1000 ); + vUndo = Vec_IntAlloc( 1000 ); + for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) + { + if ( i % 2 == 0 ) + continue; + Vec_IntClear( vUndo ); + for ( f = pCex->iFrame; f >= 0; f-- ) + if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) + { + Saig_ManExtendUndo( p, vSimInfo, vUndo ); + break; + } + if ( f >= 0 ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) + { + if ( i % 2 == 1 ) + continue; + Vec_IntClear( vUndo ); + for ( f = pCex->iFrame; f >= 0; f-- ) + if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) + { + Saig_ManExtendUndo( p, vSimInfo, vUndo ); + break; + } + if ( f >= 0 ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + Vec_IntFree( vVis ); + Vec_IntFree( vVis2 ); + Vec_IntFree( vUndo ); + // resimulate to make sure it is valid + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); + assert( Value == SAIG_ONE ); + Vec_IntFree( vResInv ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExample3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +{ + Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; + int i, f, Value; +// assert( Aig_ManRegNum(p) > 0 ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + // start simulation data + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); + assert( Value == SAIG_ONE ); + // select the result + vRes = Vec_IntAlloc( 1000 ); + vResInv = Vec_IntAlloc( 1000 ); + vVis = Vec_IntAlloc( 1000 ); + vVis2 = Vec_IntAlloc( 1000 ); + vUndo = Vec_IntAlloc( 1000 ); + for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- ) + { + if ( i % 2 == 0 ) + continue; + Vec_IntClear( vUndo ); + for ( f = pCex->iFrame; f >= 0; f-- ) + if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) + { + Saig_ManExtendUndo( p, vSimInfo, vUndo ); + break; + } + if ( f >= 0 ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- ) + { + if ( i % 2 == 1 ) + continue; + Vec_IntClear( vUndo ); + for ( f = pCex->iFrame; f >= 0; f-- ) + if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) + { + Saig_ManExtendUndo( p, vSimInfo, vUndo ); + break; + } + if ( f >= 0 ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + Vec_IntFree( vVis ); + Vec_IntFree( vVis2 ); + Vec_IntFree( vUndo ); + // resimulate to make sure it is valid + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); + assert( Value == SAIG_ONE ); + Vec_IntFree( vResInv ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +{ + Vec_Int_t * vRes0 = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + Vec_Int_t * vRes1 = Saig_ManExtendCounterExample1( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + Vec_Int_t * vRes2 = Saig_ManExtendCounterExample2( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + Vec_Int_t * vRes3 = Saig_ManExtendCounterExample3( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + Vec_Int_t * vRes = vRes0; +// if ( fVerbose ) + printf( "Removable flops: Order0 =%3d. Order1 =%3d. Order2 =%3d. Order3 =%3d.\n", + Vec_IntSize(vRes0), Vec_IntSize(vRes1), Vec_IntSize(vRes2), Vec_IntSize(vRes3) ); + if ( Vec_IntSize(vRes1) < Vec_IntSize(vRes) ) + vRes = vRes1; + if ( Vec_IntSize(vRes2) < Vec_IntSize(vRes) ) + vRes = vRes2; + if ( Vec_IntSize(vRes3) < Vec_IntSize(vRes) ) + vRes = vRes3; + vRes = Vec_IntDup( vRes ); + Vec_IntFree( vRes0 ); + Vec_IntFree( vRes1 ); + Vec_IntFree( vRes2 ); + Vec_IntFree( vRes3 ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; int clk; + if ( Saig_ManPiNum(p) != pCex->nPis ) + { + printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n", + Aig_ManPiNum(p), pCex->nPis ); + return NULL; + } Aig_ManFanoutStart( p ); vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); + Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); + clk = clock(); +// vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { @@ -314,8 +547,6 @@ ABC_PRT( "Time", clock() - clk ); Vec_PtrFree( vSimInfo ); Aig_ManFanoutStop( p ); return vRes; -// Vec_IntFree( vRes ); -// return NULL; } //////////////////////////////////////////////////////////////////////// @@ -323,3 +554,5 @@ ABC_PRT( "Time", clock() - clk ); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + |