/**CFile**************************************************************** FileName [cecCorr.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Combinational equivalence checking.] Synopsis [Latch/signal correspondence computation.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "cecInt.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Computes the real value of the literal w/o spec reduction.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) { if ( Gia_ObjIsAnd(pObj) ) { Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix ); return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); } if ( f == 0 ) { assert( Gia_ObjIsRo(p, pObj) ); return Gia_ObjCopyF(p, f, pObj); } assert( f && Gia_ObjIsRo(p, pObj) ); pObj = Gia_ObjRoToRi( p, pObj ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix ); return Gia_ObjFanin0CopyF( p, f-1, pObj ); } /**Function************************************************************* Synopsis [Recursively performs speculative reduction for the object.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) { Gia_Obj_t * pRepr; int iLitNew; if ( ~Gia_ObjCopyF(p, f, pObj) ) return; if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) { Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix ); iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); Gia_ObjSetCopyF( p, f, pObj, iLitNew ); return; } assert( Gia_ObjIsCand(pObj) ); iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); Gia_ObjSetCopyF( p, f, pObj, iLitNew ); } /**Function************************************************************* Synopsis [Derives SRM for signal correspondence.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pRepr; Vec_Int_t * vXorLits; int f, i, iPrev, iObj, iPrevNew, iObjNew; assert( nFrames > 0 ); assert( Gia_ManRegNum(p) > 0 ); assert( p->pReprs != NULL ); p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); Gia_ManHashAlloc( pNew ); Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 ); Gia_ManForEachRo( p, pObj, i ) Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) ); Gia_ManForEachRo( p, pObj, i ) if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) ); for ( f = 0; f < nFrames+fScorr; f++ ) { Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); Gia_ManForEachPi( p, pObj, i ) Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); } *pvOutputs = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 ); if ( fRings ) { Gia_ManForEachObj1( p, pObj, i ) { if ( Gia_ObjIsConst( p, i ) ) { iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); if ( iObjNew != 0 ) { Vec_IntPush( *pvOutputs, 0 ); Vec_IntPush( *pvOutputs, i ); Vec_IntPush( vXorLits, iObjNew ); } } else if ( Gia_ObjIsHead( p, i ) ) { iPrev = i; Gia_ClassForEachObj1( p, i, iObj ) { iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) { Vec_IntPush( *pvOutputs, iPrev ); Vec_IntPush( *pvOutputs, iObj ); Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) ); } iPrev = iObj; } iObj = i; iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) { Vec_IntPush( *pvOutputs, iPrev ); Vec_IntPush( *pvOutputs, iObj ); Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) ); } } } } else { Gia_ManForEachObj1( p, pObj, i ) { pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) continue; iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); if ( iPrevNew != iObjNew ) { Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); } } } Vec_IntForEachEntry( vXorLits, iObjNew, i ) Gia_ManAppendCo( pNew, iObjNew ); Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); ABC_FREE( p->pCopies ); //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); pNew = Gia_ManCleanup( pTemp = pNew ); //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); Gia_ManStop( pTemp ); return pNew; } /**Function************************************************************* Synopsis [Derives SRM for signal correspondence.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pRepr; Vec_Int_t * vXorLits; int f, i, iPrevNew, iObjNew; assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); assert( Gia_ManRegNum(p) > 0 ); assert( p->pReprs != NULL ); p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) { Gia_ManAppendCi(pNew); Gia_ObjSetCopyF( p, 0, pObj, 0 ); } for ( f = 0; f < nFrames+nPrefix+fScorr; f++ ) { Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); Gia_ManForEachPi( p, pObj, i ) Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); } *pvOutputs = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 ); for ( f = nPrefix; f < nFrames+nPrefix; f++ ) { Gia_ManForEachObj1( p, pObj, i ) { pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) continue; iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix ); iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); if ( iPrevNew != iObjNew ) { Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); } } } Vec_IntForEachEntry( vXorLits, iObjNew, i ) Gia_ManAppendCo( pNew, iObjNew ); Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); ABC_FREE( p->pCopies ); //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); pNew = Gia_ManCleanup( pTemp = pNew ); //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); Gia_ManStop( pTemp ); return pNew; } /**Function************************************************************* Synopsis [Initializes simulation info for lcorr/scorr counter-examples.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops ) { unsigned * pInfo; int k, w, nWords; nWords = Vec_PtrReadWordsSimInfo( vInfo ); assert( nFlops <= Vec_PtrSize(vInfo) ); for ( k = 0; k < nFlops; k++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = 0; } for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_ManRandom( 0 ); } } /**Function************************************************************* Synopsis [Remaps simulation info from SRM to the original AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo ) { Gia_Obj_t * pObj, * pRepr; unsigned * pInfoObj, * pInfoRepr; int i, w, nWords; nWords = Vec_PtrReadWordsSimInfo( vInfo ); Gia_ManForEachRo( p, pObj, i ) { // skip ROs without representatives pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) continue; pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, i ); for ( w = 0; w < nWords; w++ ) assert( pInfoObj[w] == 0 ); // skip ROs with constant representatives if ( Gia_ObjIsConst0(pRepr) ) continue; assert( Gia_ObjIsRo(p, pRepr) ); // Abc_Print( 1, "%d -> %d ", i, Gia_ObjId(p, pRepr) ); // transfer info from the representative pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); for ( w = 0; w < nWords; w++ ) pInfoObj[w] = pInfoRepr[w]; } // Abc_Print( 1, "\n" ); } /**Function************************************************************* Synopsis [Collects information about remapping.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p ) { Vec_Int_t * vPairs; Gia_Obj_t * pObj, * pRepr; int i; vPairs = Vec_IntAlloc( 100 ); Gia_ManForEachRo( p, pObj, i ) { // skip ROs without representatives pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) // if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) ) continue; assert( Gia_ObjIsRo(p, pRepr) ); // Abc_Print( 1, "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) ); // remember the pair Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); Vec_IntPush( vPairs, i ); } return vPairs; } /**Function************************************************************* Synopsis [Remaps simulation info from SRM to the original AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo ) { unsigned * pInfoObj, * pInfoRepr; int w, i, iObj, iRepr, nWords; nWords = Vec_PtrReadWordsSimInfo( vInfo ); Vec_IntForEachEntry( vPairs, iRepr, i ) { iObj = Vec_IntEntry( vPairs, ++i ); pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, iObj ); pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, iRepr ); for ( w = 0; w < nWords; w++ ) { assert( pInfoObj[w] == 0 ); pInfoObj[w] = pInfoRepr[w]; } } } /**Function************************************************************* Synopsis [Packs one counter-examples into the array of simulation info.] Description [] SideEffects [] SeeAlso [] *************************************`**********************************/ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits ) { unsigned * pInfo, * pPres; int i; for ( i = 0; i < nLits; i++ ) { pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); if ( Abc_InfoHasBit( pPres, iBit ) && Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); Abc_InfoSetBit( pPres, iBit ); if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) Abc_InfoXorBit( pInfo, iBit ); } return 1; } /**Function************************************************************* Synopsis [Performs bitpacking of counter-examples.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) { Vec_Int_t * vPat; Vec_Ptr_t * vPres; int nWords = Vec_PtrReadWordsSimInfo(vInfo); int nBits = 32 * nWords; int k, nSize, kMax = 0;//, iBit = 1; vPat = Vec_IntAlloc( 100 ); vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords ); Vec_PtrCleanSimInfo( vPres, 0, nWords ); while ( iStart < Vec_IntSize(vCexStore) ) { // skip the output number iStart++; // get the number of items nSize = Vec_IntEntry( vCexStore, iStart++ ); if ( nSize <= 0 ) continue; // extract pattern Vec_IntClear( vPat ); for ( k = 0; k < nSize; k++ ) Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) ); // add pattern to storage for ( k = 1; k < nBits; k++ ) if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) break; kMax = Abc_MaxInt( kMax, k ); if ( k == nBits-1 ) break; } Vec_PtrFree( vPres ); Vec_IntFree( vPat ); return iStart; } /**Function************************************************************* Synopsis [Performs bitpacking of counter-examples.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) { unsigned * pInfo; int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo); int k, iLit, nLits, Out, iBit = 1; while ( iStart < Vec_IntSize(vCexStore) ) { // skip the output number // iStart++; Out = Vec_IntEntry( vCexStore, iStart++ ); // Abc_Print( 1, "iBit = %d. Out = %d.\n", iBit, Out ); // get the number of items nLits = Vec_IntEntry( vCexStore, iStart++ ); if ( nLits <= 0 ) continue; // add pattern to storage for ( k = 0; k < nLits; k++ ) { iLit = Vec_IntEntry( vCexStore, iStart++ ); pInfo = (unsigned *)Vec_PtrEntry( vInfo, Abc_Lit2Var(iLit) ); if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(iLit) ) Abc_InfoXorBit( pInfo, iBit ); } if ( ++iBit == nBits ) break; } // Abc_Print( 1, "added %d bits\n", iBit-1 ); return iStart; } /**Function************************************************************* Synopsis [Resimulates counter-examples derived by the SAT solver.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames ) { Vec_Int_t * vPairs; Vec_Ptr_t * vSimInfo; int RetValue = 0, iStart = 0; vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); Gia_ManCreateValueRefs( pSim->pAig ); // pSim->pPars->nWords = 63; pSim->pPars->nFrames = nFrames; vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords ); while ( iStart < Vec_IntSize(vCexStore) ) { Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) ); iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); // iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); // Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); Gia_ManCorrPerformRemapping( vPairs, vSimInfo ); RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); // Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL ); } //Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); assert( iStart == Vec_IntSize(vCexStore) ); Vec_PtrFree( vSimInfo ); Vec_IntFree( vPairs ); return RetValue; } /**Function************************************************************* Synopsis [Resimulates counter-examples derived by the SAT solver.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore ) { Vec_Ptr_t * vSimInfo; int RetValue = 0, iStart = 0; Gia_ManCreateValueRefs( pSim->pAig ); pSim->pPars->nFrames = 1; vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); while ( iStart < Vec_IntSize(vCexStore) ) { Cec_ManStartSimInfo( vSimInfo, 0 ); iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); } assert( iStart == Vec_IntSize(vCexStore) ); Vec_PtrFree( vSimInfo ); return RetValue; } /**Function************************************************************* Synopsis [Updates equivalence classes by marking those that timed out.] Description [Returns 1 if all ndoes are proved.] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings ) { int i, status, iRepr, iObj; int Counter = 0; assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) ); Vec_StrForEachEntry( vStatus, status, i ) { iRepr = Vec_IntEntry( vOutputs, 2*i ); iObj = Vec_IntEntry( vOutputs, 2*i+1 ); if ( status == 1 ) continue; if ( status == 0 ) { if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) Counter++; // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) // Abc_Print( 1, "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj ); // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) // Cec_ManSimClassRemoveOne( pSim, iObj ); continue; } if ( status == -1 ) { // if ( !Gia_ObjFailed( p, iObj ) ) // Abc_Print( 1, "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" ); // Gia_ObjSetFailed( p, iRepr ); // Gia_ObjSetFailed( p, iObj ); // if ( fRings ) // Cec_ManSimClassRemoveOne( pSim, iRepr ); Cec_ManSimClassRemoveOne( pSim, iObj ); continue; } } // if ( Counter ) // Abc_Print( 1, "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter ); return 1; } /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) { Gia_Obj_t * pRepr; if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) { Gia_ManCorrReduce_rec( pNew, p, pRepr ); pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } /**Function************************************************************* Synopsis [Reduces AIG using equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); return pNew; } /**Function************************************************************* Synopsis [Prints statistics during solving.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time ) { int nLits, CounterX = 0, Counter0 = 0, Counter = 0; int i, Entry, nProve = 0, nDispr = 0, nFail = 0; for ( i = 1; i < Gia_ManObjNum(p); i++ ) { if ( Gia_ObjIsNone(p, i) ) CounterX++; else if ( Gia_ObjIsConst(p, i) ) Counter0++; else if ( Gia_ObjIsHead(p, i) ) Counter++; } CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; if ( iIter == -1 ) Abc_Print( 1, "BMC : " ); else Abc_Print( 1, "%3d : ", iIter ); Abc_Print( 1, "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); if ( vStatus ) Vec_StrForEachEntry( vStatus, Entry, i ) { if ( Entry == 1 ) nProve++; else if ( Entry == 0 ) nDispr++; else if ( Entry == -1 ) nFail++; } Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail ); Abc_Print( 1, "%c ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' ); Abc_PrintTime( 1, "T", Time ); } /**Function************************************************************* Synopsis [Runs BMC for the equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs ) { Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Vec_Str_t * vStatus; Vec_Int_t * vOutputs; Vec_Int_t * vCexStore; Cec_ManSim_t * pSim; Gia_Man_t * pSrm; int fChanges, RetValue; // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; pParsSim->nFrames = pPars->nRounds; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = pPars->fLatchCorr; pParsSim->fSeqSimulate = 1; pSim = Cec_ManSimStart( pAig, pParsSim ); // prepare SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->fVerbose = pPars->fVerbose; fChanges = 1; while ( fChanges ) { abctime clkBmc = Abc_Clock(); fChanges = 0; pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); if ( Gia_ManPoNum(pSrm) == 0 ) { Gia_ManStop( pSrm ); Vec_IntFree( vOutputs ); break; } pParsSat->nBTLimit *= 10; if ( pPars->fUseCSat ) vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); // refine classes with these counter-examples if ( Vec_IntSize(vCexStore) ) { RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs ); Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); fChanges = 1; } if ( pPars->fVerbose ) Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, Abc_Clock() - clkBmc ); // recycle Vec_IntFree( vCexStore ); Vec_StrFree( vStatus ); Gia_ManStop( pSrm ); Vec_IntFree( vOutputs ); } Cec_ManSimStop( pSim ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_ManLSCorrAnalyzeDependence( Gia_Man_t * p, Vec_Int_t * vEquivs, Vec_Str_t * vStatus ) { Gia_Obj_t * pObj, * pObjRo; int i, Iter, iObj, iRepr, fPrev, Total, Count0, Count1; assert( Vec_StrSize(vStatus) * 2 == Vec_IntSize(vEquivs) ); Total = 0; Gia_ManForEachObj( p, pObj, i ) { assert( pObj->fMark1 == 0 ); if ( Gia_ObjHasRepr(p, i) ) Total++; } Count0 = 0; for ( i = 0; i < Vec_StrSize(vStatus); i++ ) { iRepr = Vec_IntEntry(vEquivs, 2*i); iObj = Vec_IntEntry(vEquivs, 2*i+1); assert( iRepr == Gia_ObjRepr(p, iObj) ); if ( Vec_StrEntry(vStatus, i) != 1 ) // disproved or undecided { Gia_ManObj(p, iObj)->fMark1 = 1; Count0++; } } for ( Iter = 0; Iter < 100; Iter++ ) { int fChanges = 0; Gia_ManForEachObj1( p, pObj, i ) { if ( Gia_ObjIsCi(pObj) ) continue; assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ); // fPrev = pObj->fMark1; if ( Gia_ObjIsAnd(pObj) ) pObj->fMark1 |= Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1; else pObj->fMark1 |= Gia_ObjFanin0(pObj)->fMark1; // fChanges += fPrev ^ pObj->fMark1; } Gia_ManForEachRiRo( p, pObj, pObjRo, i ) { fPrev = pObjRo->fMark1; pObjRo->fMark1 = pObj->fMark1; fChanges += fPrev ^ pObjRo->fMark1; } if ( fChanges == 0 ) break; } Count1 = 0; Gia_ManForEachObj( p, pObj, i ) { if ( pObj->fMark1 && Gia_ObjHasRepr(p, i) ) Count1++; pObj->fMark1 = 0; } printf( "%5d -> %5d (%3d) ", Count0, Count1, Iter ); return 0; } /**Function************************************************************* Synopsis [Internal procedure for register correspondence.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { int nIterMax = 100000; int nAddFrames = 1; // additional timeframes to simulate int fRunBmcFirst = 1; Vec_Str_t * vStatus; Vec_Int_t * vOutputs; Vec_Int_t * vCexStore; Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Cec_ManSim_t * pSim; Gia_Man_t * pSrm; int r, RetValue; abctime clkTotal = Abc_Clock(); abctime clkSat = 0, clkSim = 0, clkSrm = 0; abctime clk2, clk = Abc_Clock(); if ( Gia_ManRegNum(pAig) == 0 ) { Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); return 0; } Gia_ManRandom( 1 ); // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; pParsSim->nFrames = pPars->nFrames; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = pPars->fLatchCorr; pParsSim->fConstCorr = pPars->fConstCorr; pParsSim->fSeqSimulate = 1; // create equivalence classes of registers pSim = Cec_ManSimStart( pAig, pParsSim ); if ( pAig->pReprs == NULL ) { Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax ); Cec_ManSimClassesRefine( pSim ); } // prepare SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->fVerbose = pPars->fVerbose; // limit the number of conflicts in the circuit-based solver if ( pPars->fUseCSat ) pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 ); if ( pPars->fVerbose ) { Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk ); } // check the base case if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); if ( pPars->pFunc ) { ((int (*)(void *))pPars->pFunc)( pPars->pData ); ((int (*)(void *))pPars->pFunc)( pPars->pData ); } if ( pPars->nStepsMax == 0 ) { Abc_Print( 1, "Stopped signal correspondence after BMC.\n" ); Cec_ManSimStop( pSim ); return 1; } // perform refinement of equivalence classes for ( r = 0; r < nIterMax; r++ ) { if ( pPars->nStepsMax == r ) { Cec_ManSimStop( pSim ); Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r ); return 1; } clk = Abc_Clock(); // perform speculative reduction clk2 = Abc_Clock(); pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) ); clkSrm += Abc_Clock() - clk2; if ( Gia_ManCoNum(pSrm) == 0 ) { Vec_IntFree( vOutputs ); Gia_ManStop( pSrm ); break; } //Gia_DumpAiger( pSrm, "corrsrm", r, 2 ); // found counter-examples to speculation clk2 = Abc_Clock(); if ( pPars->fUseCSat ) vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); Gia_ManStop( pSrm ); clkSat += Abc_Clock() - clk2; if ( Vec_IntSize(vCexStore) == 0 ) { Vec_IntFree( vCexStore ); Vec_StrFree( vStatus ); Vec_IntFree( vOutputs ); break; } // Cec_ManLSCorrAnalyzeDependence( pAig, vOutputs, vStatus ); // refine classes with these counter-examples clk2 = Abc_Clock(); RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames ); Vec_IntFree( vCexStore ); clkSim += Abc_Clock() - clk2; Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); if ( pPars->fVerbose ) Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk ); Vec_StrFree( vStatus ); Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); if ( pPars->pFunc ) ((int (*)(void *))pPars->pFunc)( pPars->pData ); // quit if const is no longer there if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) ) { printf( "Iterative refinement is stopped after iteration %d\n", r ); printf( "because the property output is no longer a candidate constant.\n" ); Cec_ManSimStop( pSim ); return 0; } } if ( pPars->fVerbose ) Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk ); // check the overflow if ( r == nIterMax ) Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); // check the base case if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); clkTotal = Abc_Clock() - clkTotal; // report the results if ( pPars->fVerbose ) { ABC_PRTP( "Srm ", clkSrm, clkTotal ); ABC_PRTP( "Sat ", clkSat, clkTotal ); ABC_PRTP( "Sim ", clkSim, clkTotal ); ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); Abc_PrintTime( 1, "TOTAL", clkTotal ); } return 1; } /**Function************************************************************* Synopsis [Computes new initial state.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) { Gia_Obj_t * pObj, * pObjRo, * pObjRi; unsigned * pInitState; int i, f; Gia_ManRandom( 1 ); // Abc_Print( 1, "Simulating %d timeframes.\n", nFrames ); Gia_ManForEachRo( pAig, pObj, i ) pObj->fMark1 = 0; for ( f = 0; f < nFrames; f++ ) { Gia_ManConst0(pAig)->fMark1 = 0; Gia_ManForEachPi( pAig, pObj, i ) pObj->fMark1 = Gia_ManRandom(0) & 1; Gia_ManForEachAnd( pAig, pObj, i ) pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)); Gia_ManForEachRi( pAig, pObj, i ) pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)); Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i ) pObjRo->fMark1 = pObjRi->fMark1; } pInitState = ABC_CALLOC( unsigned, Abc_BitWordNum(Gia_ManRegNum(pAig)) ); Gia_ManForEachRo( pAig, pObj, i ) { if ( pObj->fMark1 ) Abc_InfoSetBit( pInitState, i ); // Abc_Print( 1, "%d", pObj->fMark1 ); } // Abc_Print( 1, "\n" ); Gia_ManCleanMark1( pAig ); return pInitState; } /**Function************************************************************* Synopsis [Prints flop equivalences.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cec_ManPrintFlopEquivs( Gia_Man_t * p ) { Gia_Obj_t * pObj, * pRepr; int i; assert( p->vNamesIn != NULL ); Gia_ManForEachRo( p, pObj, i ) { if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) ) Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) ); else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) { if ( Gia_ObjIsCi(pRepr) ) Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) ); else Abc_Print( 1, "Original flop %s is proved equivalent to internal node %d.\n", Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) ); } } } /**Function************************************************************* Synopsis [Top-level procedure for register correspondence.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { Gia_Man_t * pNew, * pTemp; unsigned * pInitState; int RetValue; ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pNexts ); if ( pPars->nPrefix == 0 ) { RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); if ( RetValue == 0 ) return Gia_ManDup( pAig ); } else { // compute the cycles AIG pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix ); pTemp = Gia_ManDupFlip( pAig, (int *)pInitState ); ABC_FREE( pInitState ); // compute classes of this AIG RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars ); // transfer the class info pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL; pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL; // perform additional BMC pPars->fUseCSat = 0; pPars->nBTLimit = Abc_MaxInt( pPars->nBTLimit, 1000 ); Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix ); /* // transfer the class info back pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL; pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL; // continue refining RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars ); // transfer the class info pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL; pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL; */ Gia_ManStop( pTemp ); } // derive reduced AIG if ( pPars->fMakeChoices ) { pNew = Gia_ManEquivToChoices( pAig, 1 ); // Gia_ManHasChoices_very_old( pNew ); } else { // Gia_ManEquivImprove( pAig ); pNew = Gia_ManCorrReduce( pAig ); pNew = Gia_ManSeqCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 ); } // report the results if ( pPars->fVerbose ) { Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); } if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) ) Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix ); // print verbose info about equivalences if ( pPars->fVerboseFlops ) { if ( pAig->vNamesIn == NULL ) Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" ); else Cec_ManPrintFlopEquivs( pAig ); } return pNew; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END