/**CFile**************************************************************** FileName [saigSimExt2.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: saigSimExt2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "saig.h" #include "ssw.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #define SAIG_ZER_NEW 0 // 0 not visited #define SAIG_ONE_NEW 1 // 1 not visited #define SAIG_ZER_OLD 2 // 0 visited #define SAIG_ONE_OLD 3 // 1 visited static inline int Saig_ManSimInfo2IsOld( int Value ) { return Value == SAIG_ZER_OLD || Value == SAIG_ONE_OLD; } static inline int Saig_ManSimInfo2SetOld( int Value ) { if ( Value == SAIG_ZER_NEW ) return SAIG_ZER_OLD; if ( Value == SAIG_ONE_NEW ) return SAIG_ONE_OLD; assert( 0 ); return 0; } static inline int Saig_ManSimInfo2Not( int Value ) { if ( Value == SAIG_ZER_NEW ) return SAIG_ONE_NEW; if ( Value == SAIG_ONE_NEW ) return SAIG_ZER_NEW; if ( Value == SAIG_ZER_OLD ) return SAIG_ONE_OLD; if ( Value == SAIG_ONE_OLD ) return SAIG_ZER_OLD; assert( 0 ); return 0; } static inline int Saig_ManSimInfo2And( int Value0, int Value1 ) { if ( Value0 == SAIG_ZER_NEW || Value1 == SAIG_ZER_NEW ) return SAIG_ZER_NEW; if ( Value0 == SAIG_ONE_NEW && Value1 == SAIG_ONE_NEW ) return SAIG_ONE_NEW; assert( 0 ); return 0; } static inline int Saig_ManSimInfo2Get( 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_ManSimInfo2Set( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) { unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); Value ^= Saig_ManSimInfo2Get( vSimInfo, pObj, iFrame ); pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1)); } // performs ternary simulation extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Performs ternary simulation for one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Saig_ManExtendOneEval2( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) { int Value0, Value1, Value; Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); if ( Aig_ObjFaninC0(pObj) ) Value0 = Saig_ManSimInfo2Not( Value0 ); if ( Aig_ObjIsPo(pObj) ) { Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value0 ); return Value0; } assert( Aig_ObjIsNode(pObj) ); Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pObj), iFrame ); if ( Aig_ObjFaninC1(pObj) ) Value1 = Saig_ManSimInfo2Not( Value1 ); Value = Saig_ManSimInfo2And( Value0, Value1 ); Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value ); return Value; } /**Function************************************************************* Synopsis [Performs sensitization analysis for one design.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo ) { Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, f, iBit = 0; Saig_ManForEachLo( p, pObj, i ) Saig_ManSimInfo2Set( vSimInfo, pObj, 0, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); for ( f = 0; f <= pCex->iFrame; f++ ) { Saig_ManSimInfo2Set( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE_NEW ); Saig_ManForEachPi( p, pObj, i ) Saig_ManSimInfo2Set( vSimInfo, pObj, f, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); Aig_ManForEachNode( p, pObj, i ) Saig_ManExtendOneEval2( vSimInfo, pObj, f ); Aig_ManForEachPo( p, pObj, i ) Saig_ManExtendOneEval2( vSimInfo, pObj, f ); if ( f == pCex->iFrame ) break; Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) Saig_ManSimInfo2Set( vSimInfo, pObjLo, f+1, Saig_ManSimInfo2Get(vSimInfo, pObjLi, f) ); } // make sure the output of the property failed pObj = Aig_ManPo( p, pCex->iPo ); return Saig_ManSimInfo2Get( vSimInfo, pObj, pCex->iFrame ); } /**Function************************************************************* Synopsis [Drive implications of the given node towards primary outputs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Saig_ManSetAndDriveImplications_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Vec_Ptr_t * vSimInfo ) { Aig_Obj_t * pFanout; int k, iFanout, Value0, Value1; int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f ); assert( !Saig_ManSimInfo2IsOld( Value ) ); Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) ); if ( (Aig_ObjIsPo(pObj) && f == fMax) || Saig_ObjIsPo(p, pObj) ) return; if ( Saig_ObjIsLi( p, pObj ) ) { assert( f < fMax ); pFanout = Saig_ObjLiToLo(p, pObj); Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f+1 ); if ( !Saig_ManSimInfo2IsOld( Value ) ) Saig_ManSetAndDriveImplications_rec( p, pFanout, f+1, fMax, vSimInfo ); return; } assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ); Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k ) { Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f ); if ( Saig_ManSimInfo2IsOld( Value ) ) continue; if ( Aig_ObjIsPo(pFanout) ) { Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo ); continue; } assert( Aig_ObjIsNode(pFanout) ); Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pFanout), f ); Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pFanout), f ); if ( Aig_ObjFaninC0(pFanout) ) Value0 = Saig_ManSimInfo2Not( Value0 ); if ( Aig_ObjFaninC1(pFanout) ) Value1 = Saig_ManSimInfo2Not( Value1 ); if ( Value0 == SAIG_ZER_OLD || Value1 == SAIG_ZER_OLD || (Value0 == SAIG_ONE_OLD && Value1 == SAIG_ONE_OLD) ) Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo ); } } /**Function************************************************************* Synopsis [Performs recursive sensetization analysis.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Vec_Ptr_t * vSimInfo ) { int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f ); if ( Saig_ManSimInfo2IsOld( Value ) ) return; Saig_ManSetAndDriveImplications_rec( p, pObj, f, fMax, vSimInfo ); assert( !Aig_ObjIsConst1(pObj) ); if ( Saig_ObjIsLo(p, pObj) && f == 0 ) return; if ( Saig_ObjIsPi(p, pObj) ) { // propagate implications of this assignment int i, iPiNum = Aig_ObjPioNum(pObj); for ( i = fMax; i >= 0; i-- ) if ( i != f ) Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, iPiNum), i, fMax, vSimInfo ); return; } if ( Saig_ObjIsLo( p, pObj ) ) { assert( f > 0 ); Saig_ManExplorePaths_rec( p, Saig_ObjLoToLi(p, pObj), f-1, fMax, vSimInfo ); return; } if ( Aig_ObjIsPo(pObj) ) { Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo ); return; } assert( Aig_ObjIsNode(pObj) ); if ( Value == SAIG_ZER_OLD ) { // if ( (Aig_ObjId(pObj) & 1) == 0 ) Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo ); // else // Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, fMax, vSimInfo ); } else { Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo ); Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, fMax, vSimInfo ); } } /**Function************************************************************* Synopsis [Returns the array of PIs for flops that should not be absracted.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) { Aig_Obj_t * pObj; Vec_Int_t * vRes, * vResInv; 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_ManSimDataInit2( p, pCex, vSimInfo ); assert( Value == SAIG_ONE_NEW ); // derive implications of constants and primary inputs Saig_ManForEachLo( p, pObj, i ) Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo ); for ( f = pCex->iFrame; f >= 0; f-- ) { Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo ); for ( i = 0; i < iFirstFlopPi; i++ ) Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo ); } // recursively compute justification Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); // select the result vRes = Vec_IntAlloc( 1000 ); vResInv = Vec_IntAlloc( 1000 ); for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) { for ( f = pCex->iFrame; f >= 0; f-- ) { Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f ); if ( Saig_ManSimInfo2IsOld( Value ) ) break; } if ( f >= 0 ) Vec_IntPush( vRes, i ); else Vec_IntPush( vResInv, i ); } // 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_ManExtendCounterExampleTest2( 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_ManExtendCounterExampleTest2(): 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_ManProcessCex( 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; } /**Function************************************************************* Synopsis [Returns the array of PIs for flops that should not be absracted.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) { Abc_Cex_t * pCare; Aig_Obj_t * pObj; Vec_Int_t * vRes, * vResInv; 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_ManSimDataInit2( p, pCex, vSimInfo ); assert( Value == SAIG_ONE_NEW ); // derive implications of constants and primary inputs Saig_ManForEachLo( p, pObj, i ) Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo ); for ( f = pCex->iFrame; f >= 0; f-- ) { Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo ); for ( i = 0; i < iFirstFlopPi; i++ ) Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo ); } // recursively compute justification Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); // create CEX pCare = Abc_CexDup( pCex, pCex->nRegs ); memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); // select the result vRes = Vec_IntAlloc( 1000 ); vResInv = Vec_IntAlloc( 1000 ); for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) { int fFound = 0; for ( f = pCex->iFrame; f >= 0; f-- ) { Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f ); if ( Saig_ManSimInfo2IsOld( Value ) ) { fFound = 1; Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ); } } if ( fFound ) Vec_IntPush( vRes, i ); else Vec_IntPush( vResInv, i ); } // resimulate to make sure it is valid Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); assert( Value == SAIG_ONE ); Vec_IntFree( vResInv ); Vec_IntFree( vRes ); return pCare; } /**Function************************************************************* Synopsis [Returns the array of PIs for flops that should not be absracted.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose ) { Abc_Cex_t * pCare; Vec_Ptr_t * vSimInfo; int clk; if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest2(): 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(); pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { // printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); Abc_CexPrintStats( pCex ); Abc_CexPrintStats( pCare ); ABC_PRT( "Time", clock() - clk ); } Vec_PtrFree( vSimInfo ); Aig_ManFanoutStop( p ); return pCare; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END