diff options
Diffstat (limited to 'src/aig/saig/saigSimExt.c')
| -rw-r--r-- | src/aig/saig/saigSimExt.c | 556 |
1 files changed, 0 insertions, 556 deletions
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c deleted file mode 100644 index 1a5ec7e5..00000000 --- a/src/aig/saig/saigSimExt.c +++ /dev/null @@ -1,556 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigSimExt.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Extending simulation trace to contain ternary values.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigSimExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "proof/ssw/ssw.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline int Saig_ManSimInfoNot( int Value ) -{ - if ( Value == SAIG_ZER ) - return SAIG_ONE; - if ( Value == SAIG_ONE ) - return SAIG_ZER; - return SAIG_UND; -} - -static inline int Saig_ManSimInfoAnd( int Value0, int Value1 ) -{ - if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER ) - return SAIG_ZER; - if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE ) - return SAIG_ONE; - return SAIG_UND; -} - -static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) -{ - 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 = (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)); -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs ternary simulation for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) -{ - int Value0, Value1, Value; - Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); - if ( Aig_ObjFaninC0(pObj) ) - Value0 = Saig_ManSimInfoNot( Value0 ); - if ( Aig_ObjIsCo(pObj) ) - { - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); - return Value0; - } - assert( Aig_ObjIsNode(pObj) ); - Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame ); - if ( Aig_ObjFaninC1(pObj) ) - Value1 = Saig_ManSimInfoNot( Value1 ); - Value = Saig_ManSimInfoAnd( Value0, Value1 ); - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); - return Value; -} - -/**Function************************************************************* - - Synopsis [Performs ternary simulation for one design.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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; - Saig_ManForEachLo( p, pObj, i ) - Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); - for ( f = 0; f <= pCex->iFrame; f++ ) - { - Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE ); - Saig_ManForEachPi( p, pObj, i ) - Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); - if ( vRes ) - Vec_IntForEachEntry( vRes, Entry, i ) - Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND ); - Aig_ManForEachNode( p, pObj, i ) - Saig_ManExtendOneEval( vSimInfo, pObj, f ); - Aig_ManForEachCo( p, pObj, i ) - Saig_ManExtendOneEval( vSimInfo, pObj, f ); - if ( f == pCex->iFrame ) - break; - Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) ); - } - // make sure the output of the property failed - pObj = Aig_ManCo( p, pCex->iPo ); - return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); -} - -/**Function************************************************************* - - Synopsis [Tries to assign ternary value to one of the primary inputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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_ManCi(p, iPi); - int i, k, f, iFanout = -1, Value, Value2, Entry; - // save original value - Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame ); - assert( Value == SAIG_ZER || Value == SAIG_ONE ); - Vec_IntPush( vUndo, Aig_ObjId(pObj) ); - Vec_IntPush( vUndo, iFrame ); - Vec_IntPush( vUndo, Value ); - // update original value - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, SAIG_UND ); - // traverse - Vec_IntClear( vVis ); - Vec_IntPush( vVis, Aig_ObjId(pObj) ); - for ( f = iFrame; f <= pCex->iFrame; f++ ) - { - Vec_IntClear( vVis2 ); - Vec_IntForEachEntry( vVis, Entry, i ) - { - pObj = Aig_ManObj( p, Entry ); - Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k ) - { - assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) ); - Value = Saig_ManSimInfoGet( vSimInfo, pFanout, f ); - if ( Value == SAIG_UND ) - continue; - Value2 = Saig_ManExtendOneEval( vSimInfo, pFanout, f ); - if ( Value2 == Value ) - continue; - assert( Value2 == SAIG_UND ); -// assert( Vec_IntFind(vVis, Aig_ObjId(pFanout)) == -1 ); - if ( Aig_ObjIsNode(pFanout) ) - Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) ); - else if ( Saig_ObjIsLi(p, pFanout) ) - Vec_IntPush( vVis2, Aig_ObjId(pFanout) ); - Vec_IntPush( vUndo, Aig_ObjId(pFanout) ); - Vec_IntPush( vUndo, f ); - Vec_IntPush( vUndo, Value ); - } - } - if ( Vec_IntSize(vVis2) == 0 ) - break; - if ( f == pCex->iFrame ) - break; - // transfer - Vec_IntClear( vVis ); - Vec_IntForEachEntry( vVis2, Entry, i ) - { - pObj = Aig_ManObj( p, Entry ); - assert( Saig_ObjIsLi(p, pObj) ); - pFanout = Saig_ObjLiToLo( p, pObj ); - Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) ); - Value = Saig_ManSimInfoGet( vSimInfo, pObj, f ); - Saig_ManSimInfoSet( vSimInfo, pFanout, f+1, Value ); - } - } - // check the output - pObj = Aig_ManCo( p, pCex->iPo ); - Value = Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); - assert( Value == SAIG_ONE || Value == SAIG_UND ); - return (int)(Value == SAIG_ONE); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo ) -{ - Aig_Obj_t * pObj; - int i, iFrame, Value; - for ( i = 0; i < Vec_IntSize(vUndo); i += 3 ) - { - pObj = Aig_ManObj( p, Vec_IntEntry(vUndo, i) ); - iFrame = Vec_IntEntry(vUndo, i+1); - Value = Vec_IntEntry(vUndo, i+2); - assert( Saig_ManSimInfoGet(vSimInfo, pObj, iFrame) == SAIG_UND ); - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); - } -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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; -// assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_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++ ) - { - 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_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) >= Abc_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) >= Abc_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) >= Abc_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 fTryFour, int fVerbose ) -{ - Vec_Int_t * vRes; - Vec_Ptr_t * vSimInfo; - clock_t 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_ManCiNum(p), pCex->nPis ); - return NULL; - } - Aig_ManFanoutStart( p ); - vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); - Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); - -clk = clock(); - if ( fTryFour ) - vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - else - vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - if ( fVerbose ) - { - printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); - } - Vec_PtrFree( vSimInfo ); - Aig_ManFanoutStop( p ); - return vRes; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |