diff options
Diffstat (limited to 'src/proof/cec/cecCorr_updated.c')
| -rw-r--r-- | src/proof/cec/cecCorr_updated.c | 1028 |
1 files changed, 0 insertions, 1028 deletions
diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c deleted file mode 100644 index 0d441629..00000000 --- a/src/proof/cec/cecCorr_updated.c +++ /dev/null @@ -1,1028 +0,0 @@ -/**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 = Gia_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 = Gia_UtilStrsav( p->pName ); - 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 = Gia_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 = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Gia_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, Gia_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 = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Gia_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, Gia_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 = Gia_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 ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); - pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "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 = Gia_UtilStrsav( p->pName ); - 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 = Gia_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 ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); - pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "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, int * pInitState ) -{ - unsigned * pInfo; - int k, w, nWords; - nWords = Vec_PtrReadWordsSimInfo( vInfo ); - assert( nFlops <= Vec_PtrSize(vInfo) ); - for ( k = 0; k < nFlops; k++ ) - { - pInfo = Vec_PtrEntry( vInfo, k ); - if ( pInitState && Gia_InfoHasBit(pInitState, k) ) - { - for ( w = 0; w < nWords; w++ ) - pInfo[w] = ~0; -// pInfo[0] <<= 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - pInfo[w] = 0; - } - } - for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ ) - { - pInfo = 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 = 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) ); -// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) ); - // transfer info from the representative - pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); - for ( w = 0; w < nWords; w++ ) - pInfoObj[w] = pInfoRepr[w]; - } -// printf( "\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) ); -// printf( "%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, int * pInitState ) -{ - unsigned * pInfoObj, * pInfoRepr; - int w, i, iObj, iRepr, nWords; - nWords = Vec_PtrReadWordsSimInfo( vInfo ); - Vec_IntForEachEntry( vPairs, iRepr, i ) - { - iObj = Vec_IntEntry( vPairs, ++i ); - pInfoObj = Vec_PtrEntry( vInfo, iObj ); - pInfoRepr = Vec_PtrEntry( vInfo, iRepr ); - for ( w = 0; w < nWords; w++ ) - { - assert( pInitState || 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 = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Gia_InfoHasBit( pPres, iBit ) && - Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - return 0; - } - for ( i = 0; i < nLits; i++ ) - { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Gia_InfoSetBit( pPres, iBit ); - if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Gia_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, iBit = 1, kMax = 0; - 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++ ); -// printf( "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 = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); - if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) - Gia_InfoXorBit( pInfo, iBit ); - } - if ( ++iBit == nBits ) - break; - } -// printf( "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, int * pInitState ) -{ - Vec_Int_t * vPairs; - Vec_Ptr_t * vSimInfo; - int RetValue = 0, iStart = 0; - vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); - Gia_ManSetRefs( pSim->pAig ); -// pSim->pPars->nWords = 63; - pSim->pPars->nRounds = 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), pInitState ); - iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); -// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); -// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); - Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState ); - 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_ManSetRefs( pSim->pAig ); - pSim->pPars->nRounds = 1; - vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); - while ( iStart < Vec_IntSize(vCexStore) ) - { - Cec_ManStartSimInfo( vSimInfo, 0, NULL ); - 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) ) -// printf( "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 ) ) -// printf( "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 ) -// printf( "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 = Gia_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 = Gia_UtilStrsav( p->pName ); - 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, clock_t 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 ) - printf( "BMC : " ); - else - printf( "%3d : ", iIter ); - printf( "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++; - } - printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail ); - ABC_PRT( "T", Time ); -} - -/**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; - printf( "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; -// pObj->fMark1 = 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, Gia_BitWordNum(Gia_ManRegNum(pAig)) ); - Gia_ManForEachRo( pAig, pObj, i ) - { - if ( pObj->fMark1 ) - Gia_InfoSetBit( pInitState, i ); -// printf( "%d", pObj->fMark1 ); - } -// printf( "\n" ); - Gia_ManCleanMark1( pAig ); - return pInitState; -} - -/**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 - 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; - unsigned * pInitState = NULL; - int r, RetValue; - clock_t clkTotal = clock(); - clock_t clkSat = 0, clkSim = 0, clkSrm = 0; - clock_t clk2, clk = clock(); - ABC_FREE( pAig->pReprs ); - ABC_FREE( pAig->pNexts ); - if ( Gia_ManRegNum(pAig) == 0 ) - { - printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); - return 0; - } - Gia_ManRandom( 1 ); - // derive initial state for resimulation - if ( pPars->nPrefix ) -// pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) ); - pInitState = Cec_ManComputeInitState( pAig, 100 ); - // prepare simulation manager - Cec_ManSimSetDefaultParams( pParsSim ); - pParsSim->nWords = pPars->nWords; - pParsSim->nRounds = pPars->nRounds; - pParsSim->fVerbose = pPars->fVerbose; - pParsSim->fLatchCorr = pPars->fLatchCorr; - pParsSim->fSeqSimulate = 1; - // create equivalence classes of registers - pSim = Cec_ManSimStart( pAig, pParsSim, pInitState ); - Cec_ManSimClassesPrepare( pSim ); - Cec_ManSimClassesRefine( pSim ); - // prepare SAT solving - Cec_ManSatSetDefaultParams( pParsSat ); - pParsSat->nBTLimit = pPars->nBTLimit; - pParsSat->fVerbose = pPars->fVerbose; - if ( pPars->fVerbose ) - { - printf( "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, clock() - clk ); - } - // perform refinement of equivalence classes - for ( r = 0; r < nIterMax; r++ ) - { - clk = clock(); - // perform speculative reduction - clk2 = 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 += 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 = clock(); - if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); - else - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - Gia_ManStop( pSrm ); - clkSat += clock() - clk2; - if ( Vec_IntSize(vCexStore) == 0 ) - { - Vec_IntFree( vCexStore ); - Vec_StrFree( vStatus ); - Vec_IntFree( vOutputs ); - break; - } - // refine classes with these counter-examples - clk2 = clock(); - RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState ); - Vec_IntFree( vCexStore ); - clkSim += clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk ); - Vec_StrFree( vStatus ); - Vec_IntFree( vOutputs ); -//Gia_ManEquivPrintClasses( pAig, 1, 0 ); - } - ABC_FREE( pInitState ); - // check the base case - if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix ) - { - int fChanges = 1; - while ( fChanges ) - { - clock_t clkBmc = clock(); - fChanges = 0; - pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); - if ( Gia_ManPoNum(pSrm) == 0 ) - { - Gia_ManStop( pSrm ); - Vec_IntFree( vOutputs ); - break; - } - pParsSat->nBTLimit *= 10; - if ( pPars->nPrefix ) - { - pParsSat->nBTLimit = 10000; - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - } - else if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); - else - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - // refine classes with these counter-examples - if ( Vec_IntSize(vCexStore) ) - { - clk2 = clock(); - RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames + pPars->nPrefix, NULL ); - clkSim += clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); - fChanges = 1; - } - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc ); - // recycle - Vec_IntFree( vCexStore ); - Vec_StrFree( vStatus ); - Gia_ManStop( pSrm ); - Vec_IntFree( vOutputs ); - } - } - else - { - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); - } - // check the overflow - if ( r == nIterMax ) - printf( "The refinement was not finished. The result may be incorrect.\n" ); - Cec_ManSimStop( pSim ); - clkTotal = 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_PRT( "TOTAL", clkTotal ); - } - return 1; -} - -/**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; - int RetValue; - RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); - // derive reduced AIG - if ( pPars->fMakeChoices ) - { - pNew = Gia_ManEquivToChoices( pAig, 1 ); - Gia_ManHasChoices( pNew ); - } - else - { - Gia_ManEquivImprove( pAig ); - pNew = Gia_ManCorrReduce( pAig ); - pNew = Gia_ManSeqCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); - } - // report the results - if ( pPars->fVerbose ) - { - printf( "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) ); - } - return pNew; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |