diff options
Diffstat (limited to 'src/proof/cec/cecClass.c')
| -rw-r--r-- | src/proof/cec/cecClass.c | 931 |
1 files changed, 931 insertions, 0 deletions
diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c new file mode 100644 index 00000000..46e585a9 --- /dev/null +++ b/src/proof/cec/cecClass.c @@ -0,0 +1,931 @@ +/**CFile**************************************************************** + + FileName [cecClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Equivalence class refinement.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline unsigned * Cec_ObjSim( Cec_ManSim_t * p, int Id ) { return p->pMems + p->pSimInfo[Id] + 1; } +static inline void Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n ) { p->pSimInfo[Id] = n; } + +static inline float Cec_MemUsage( Cec_ManSim_t * p ) { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Compares simulation info of one node with constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimCompareConst( unsigned * p, int nWords ) +{ + int w; + if ( p[0] & 1 ) + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != ~0 ) + return 0; + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != 0 ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [Compares simulation info of two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords ) +{ + int w; + if ( (p0[0] & 1) == (p1[0] & 1) ) + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != p1[w] ) + return 0; + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != ~p1[w] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [Returns the number of the first non-equal bit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords ) +{ + int w; + if ( p[0] & 1 ) + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != ~0 ) + return 32*w + Gia_WordFindFirstBit( ~p[w] ); + return -1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != 0 ) + return 32*w + Gia_WordFindFirstBit( p[w] ); + return -1; + } +} + +/**Function************************************************************* + + Synopsis [Compares simulation info of two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords ) +{ + int w; + if ( (p0[0] & 1) == (p1[0] & 1) ) + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != p1[w] ) + return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] ); + return -1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != ~p1[w] ) + return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] ); + return -1; + } +} + +/**Function************************************************************* + + Synopsis [Returns the number of the first non-equal bit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimCompareConstScore( unsigned * p, int nWords, int * pScores ) +{ + int w, b; + if ( p[0] & 1 ) + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != ~0 ) + for ( b = 0; b < 32; b++ ) + if ( ((~p[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != 0 ) + for ( b = 0; b < 32; b++ ) + if ( ((p[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } +} + +/**Function************************************************************* + + Synopsis [Compares simulation info of two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimCompareEqualScore( unsigned * p0, unsigned * p1, int nWords, int * pScores ) +{ + int w, b; + if ( (p0[0] & 1) == (p1[0] & 1) ) + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != p1[w] ) + for ( b = 0; b < 32; b++ ) + if ( ((p0[w] ^ p1[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != ~p1[w] ) + for ( b = 0; b < 32; b++ ) + if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } +} + +/**Function************************************************************* + + Synopsis [Creates equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) +{ + int Repr = GIA_VOID, EntPrev = -1, Ent, i; + assert( Vec_IntSize(vClass) > 0 ); + Vec_IntForEachEntry( vClass, Ent, i ) + { + if ( i == 0 ) + { + Repr = Ent; + Gia_ObjSetRepr( p, Ent, GIA_VOID ); + EntPrev = Ent; + } + else + { + assert( Repr < Ent ); + Gia_ObjSetRepr( p, Ent, Repr ); + Gia_ObjSetNext( p, EntPrev, Ent ); + EntPrev = Ent; + } + } + Gia_ObjSetNext( p, EntPrev, 0 ); +} + +/**Function************************************************************* + + Synopsis [Refines one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i ) +{ + unsigned * pSim0, * pSim1; + int Ent; + Vec_IntClear( p->vClassOld ); + Vec_IntClear( p->vClassNew ); + Vec_IntPush( p->vClassOld, i ); + pSim0 = Cec_ObjSim(p, i); + Gia_ClassForEachObj1( p->pAig, i, Ent ) + { + pSim1 = Cec_ObjSim(p, Ent); + if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) ) + Vec_IntPush( p->vClassOld, Ent ); + else + { + Vec_IntPush( p->vClassNew, Ent ); + if ( p->pBestState ) + Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores ); + } + } + if ( Vec_IntSize( p->vClassNew ) == 0 ) + return 0; + Cec_ManSimClassCreate( p->pAig, p->vClassOld ); + Cec_ManSimClassCreate( p->pAig, p->vClassNew ); + if ( Vec_IntSize(p->vClassNew) > 1 ) + return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Refines one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ) +{ + int iRepr, Ent; + if ( Gia_ObjIsConst(p->pAig, i) ) + { + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); + return 1; + } + if ( !Gia_ObjIsClass(p->pAig, i) ) + return 0; + assert( Gia_ObjIsClass(p->pAig, i) ); + iRepr = Gia_ObjRepr( p->pAig, i ); + if ( iRepr == GIA_VOID ) + iRepr = i; + // collect nodes + Vec_IntClear( p->vClassOld ); + Vec_IntClear( p->vClassNew ); + Gia_ClassForEachObj( p->pAig, iRepr, Ent ) + { + if ( Ent == i ) + Vec_IntPush( p->vClassNew, Ent ); + else + Vec_IntPush( p->vClassOld, Ent ); + } + assert( Vec_IntSize( p->vClassNew ) == 1 ); + Cec_ManSimClassCreate( p->pAig, p->vClassOld ); + Cec_ManSimClassCreate( p->pAig, p->vClassNew ); + assert( !Gia_ObjIsClass(p->pAig, i) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes hash key of the simuation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize ) +{ + static int s_Primes[16] = { + 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, + 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; + unsigned uHash = 0; + int i; + if ( pSim[0] & 1 ) + for ( i = 0; i < nWords; i++ ) + uHash ^= ~pSim[i] * s_Primes[i & 0xf]; + else + for ( i = 0; i < nWords; i++ ) + uHash ^= pSim[i] * s_Primes[i & 0xf]; + return (int)(uHash % nTableSize); + +} + +/**Function************************************************************* + + Synopsis [Resets pointers to the simulation memory.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimMemRelink( Cec_ManSim_t * p ) +{ + unsigned * pPlace, Ent; + pPlace = (unsigned *)&p->MemFree; + for ( Ent = p->nMems * (p->nWords + 1); + Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc; + Ent += p->nWords + 1 ) + { + *pPlace = Ent; + pPlace = p->pMems + Ent; + } + *pPlace = 0; + p->nWordsOld = p->nWords; +} + +/**Function************************************************************* + + Synopsis [References simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i ) +{ + unsigned * pSim; + assert( p->pSimInfo[i] == 0 ); + if ( p->MemFree == 0 ) + { + if ( p->nWordsAlloc == 0 ) + { + assert( p->pMems == NULL ); + p->nWordsAlloc = (1<<17); // -> 1Mb + p->nMems = 1; + } + p->nWordsAlloc *= 2; + p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc ); + Cec_ManSimMemRelink( p ); + } + p->pSimInfo[i] = p->MemFree; + pSim = p->pMems + p->MemFree; + p->MemFree = pSim[0]; + pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) ); + p->nMems++; + if ( p->nMemsMax < p->nMems ) + p->nMemsMax = p->nMems; + return pSim; +} + +/**Function************************************************************* + + Synopsis [Dereferences simulaton info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i ) +{ + unsigned * pSim; + assert( p->pSimInfo[i] > 0 ); + pSim = p->pMems + p->pSimInfo[i]; + if ( --pSim[0] == 0 ) + { + pSim[0] = p->MemFree; + p->MemFree = p->pSimInfo[i]; + p->pSimInfo[i] = 0; + p->nMems--; + } + return pSim; +} + +/**Function************************************************************* + + Synopsis [Refines nodes belonging to candidate constant class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined ) +{ + unsigned * pSim; + int * pTable, nTableSize, i, k, Key; + if ( Vec_IntSize(vRefined) == 0 ) + return; + nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); + pTable = ABC_CALLOC( int, nTableSize ); + Vec_IntForEachEntry( vRefined, i, k ) + { + pSim = Cec_ObjSim( p, i ); + assert( !Cec_ManSimCompareConst( pSim, p->nWords ) ); + Key = Cec_ManSimHashKey( pSim, p->nWords, nTableSize ); + if ( pTable[Key] == 0 ) + { + assert( Gia_ObjRepr(p->pAig, i) == 0 ); + assert( Gia_ObjNext(p->pAig, i) == 0 ); + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); + } + else + { + Gia_ObjSetNext( p->pAig, pTable[Key], i ); + Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) ); + if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID ) + Gia_ObjSetRepr( p->pAig, i, pTable[Key] ); + assert( Gia_ObjRepr(p->pAig, i) > 0 ); + } + pTable[Key] = i; + } + Vec_IntForEachEntry( vRefined, i, k ) + { + if ( Gia_ObjIsHead( p->pAig, i ) ) + Cec_ManSimClassRefineOne( p, i ); + } + Vec_IntForEachEntry( vRefined, i, k ) + Cec_ManSimSimDeref( p, i ); + ABC_FREE( pTable ); +} + + +/**Function************************************************************* + + Synopsis [Saves the input pattern with the given number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) +{ + unsigned * pInfo; + int i; + assert( p->pCexComb == NULL ); + assert( iPat >= 0 && iPat < 32 * p->nWords ); + p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char, + sizeof(Abc_Cex_t) + sizeof(unsigned) * Abc_BitWordNum(Gia_ManCiNum(p->pAig)) ); + p->pCexComb->iPo = p->iOut; + p->pCexComb->nPis = Gia_ManCiNum(p->pAig); + p->pCexComb->nBits = Gia_ManCiNum(p->pAig); + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i ); + if ( Abc_InfoHasBit( pInfo, iPat ) ) + Abc_InfoSetBit( p->pCexComb->pData, i ); + } +} + +/**Function************************************************************* + + Synopsis [Find the best pattern using the scores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) +{ + unsigned * pInfo; + int i, ScoreBest = 0, iPatBest = 1; // set the first pattern + // find the best pattern + for ( i = 0; i < 32 * p->nWords; i++ ) + if ( ScoreBest < p->pScores[i] ) + { + ScoreBest = p->pScores[i]; + iPatBest = i; + } + // compare this with the available patterns - and save + if ( p->pBestState->iPo <= ScoreBest ) + { + assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) ); + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); + if ( Abc_InfoHasBit(p->pBestState->pData, i) != Abc_InfoHasBit(pInfo, iPatBest) ) + Abc_InfoXorBit( p->pBestState->pData, i ); + } + p->pBestState->iPo = ScoreBest; + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if computation should stop.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) +{ + unsigned * pInfo, * pInfo2; + int i; + if ( !p->pPars->fCheckMiter ) + return 0; + assert( p->vCoSimInfo != NULL ); + // compare outputs with 0 + if ( p->pPars->fDualOut ) + { + assert( (Gia_ManPoNum(p->pAig) & 1) == 0 ); + for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i ); + pInfo2 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, ++i ); + if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) ) + { + if ( p->iOut == -1 ) + { + p->iOut = i/2; + Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) ); + } + if ( p->pCexes == NULL ) + p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 ); + if ( p->pCexes[i/2] == NULL ) + { + p->nOuts++; + p->pCexes[i/2] = (void *)1; + } + } + } + } + else + { + for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i ); + if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) ) + { + if ( p->iOut == -1 ) + { + p->iOut = i; + Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) ); + } + if ( p->pCexes == NULL ) + p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) ); + if ( p->pCexes[i] == NULL ) + { + p->nOuts++; + p->pCexes[i] = (void *)1; + } + } + } + } + return p->pCexes != NULL; +} + +/**Function************************************************************* + + Synopsis [Simulates one round.] + + Description [Returns the number of PO entry if failed; 0 otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) +{ + Gia_Obj_t * pObj; + unsigned * pRes0, * pRes1, * pRes; + int i, k, w, Ent, iCiId = 0, iCoId = 0; + // prepare internal storage + if ( p->nWordsOld != p->nWords ) + Cec_ManSimMemRelink( p ); + p->nMemsMax = 0; + // allocate score counters + ABC_FREE( p->pScores ); + if ( p->pBestState ) + p->pScores = ABC_CALLOC( int, 32 * p->nWords ); + // simulate nodes + Vec_IntClear( p->vRefinedC ); + if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) ) + { + pRes = Cec_ManSimSimRef( p, 0 ); + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = 0; + } + Gia_ManForEachObj1( p->pAig, pObj, i ) + { + if ( Gia_ObjIsCi(pObj) ) + { + if ( Gia_ObjValue(pObj) == 0 ) + { + iCiId++; + continue; + } + pRes = Cec_ManSimSimRef( p, i ); + if ( vInfoCis ) + { + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ ); + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = pRes0[w-1]; + } + else + { + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = Gia_ManRandom( 0 ); + } + // make sure the first pattern is always zero + pRes[1] ^= (pRes[1] & 1); + goto references; + } + if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin + { + pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); + if ( vInfoCos ) + { + pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ ); + if ( Gia_ObjFaninC0(pObj) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w-1] = ~pRes0[w]; + else + for ( w = 1; w <= p->nWords; w++ ) + pRes[w-1] = pRes0[w]; + } + continue; + } + assert( Gia_ObjValue(pObj) ); + pRes = Cec_ManSimSimRef( p, i ); + pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); + pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) ); + +// Abc_Print( 1, "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) ); + + if ( Gia_ObjFaninC0(pObj) ) + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = ~(pRes0[w] | pRes1[w]); + else + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = ~pRes0[w] & pRes1[w]; + } + else + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = pRes0[w] & ~pRes1[w]; + else + for ( w = 1; w <= p->nWords; w++ ) + pRes[w] = pRes0[w] & pRes1[w]; + } + +references: + // if this node is candidate constant, collect it + if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) ) + { + pRes[0]++; + Vec_IntPush( p->vRefinedC, i ); + if ( p->pBestState ) + Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores ); + } + // if the node belongs to a class, save it + if ( Gia_ObjIsClass(p->pAig, i) ) + pRes[0]++; + // if this is the last node of the class, process it + if ( Gia_ObjIsTail(p->pAig, i) ) + { + Vec_IntClear( p->vClassTemp ); + Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent ) + Vec_IntPush( p->vClassTemp, Ent ); + Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) ); + Vec_IntForEachEntry( p->vClassTemp, Ent, k ) + Cec_ManSimSimDeref( p, Ent ); + } + } + + if ( p->pPars->fConstCorr ) + { + Vec_IntForEachEntry( p->vRefinedC, i, k ) + { + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); + Cec_ManSimSimDeref( p, i ); + } + Vec_IntClear( p->vRefinedC ); + } + + if ( Vec_IntSize(p->vRefinedC) > 0 ) + Cec_ManSimProcessRefined( p, p->vRefinedC ); + assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) ); + assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) ); + assert( p->nMems == 1 ); + if ( p->nMems != 1 ) + Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" ); + if ( p->pPars->fVeryVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + if ( p->pBestState ) + Cec_ManSimFindBestPattern( p ); +/* + if ( p->nMems > 1 ) { + for ( i = 1; i < p->nObjs; i++ ) + if ( p->pSims[i] ) { + int x = 0; + } + } +*/ + return Cec_ManSimAnalyzeOutputs( p ); +} + + + +/**Function************************************************************* + + Synopsis [Creates simulation info for this round.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) +{ + unsigned * pRes0, * pRes1; + int i, w; + if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 ) + { + assert( vInfoCis && vInfoCos ); + for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) + { + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i ); + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = Gia_ManRandom( 0 ); + } + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i ); + pRes1 = (unsigned *)Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i ); + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = pRes1[w]; + } + } + else + { + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + { + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i ); + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = Gia_ManRandom( 0 ); + } + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the bug is found.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ) +{ + Gia_Obj_t * pObj; + int i; + assert( p->pAig->pReprs == NULL ); + // allocate representation + p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) ); + p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); + // create references + Gia_ManSetRefs( p->pAig ); + // set starting representative of internal nodes to be constant 0 + if ( p->pPars->fLatchCorr ) + Gia_ManForEachObj( p->pAig, pObj, i ) + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); + else if ( LevelMax == -1 ) + Gia_ManForEachObj( p->pAig, pObj, i ) + Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID ); + else + { + Gia_ManLevelNum( p->pAig ); + Gia_ManForEachObj( p->pAig, pObj, i ) + Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID ); + Vec_IntFreeP( &p->pAig->vLevels ); + } + // if sequential simulation, set starting representative of ROs to be constant 0 + if ( p->pPars->fSeqSimulate ) + Gia_ManForEachRo( p->pAig, pObj, i ) + if ( pObj->Value ) + Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 ); + // perform simulation + p->nWords = 1; + do { + if ( p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + for ( i = 0; i < 4; i++ ) + { + Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; + } + p->nWords = 2 * p->nWords + 1; + } + while ( p->nWords <= p->pPars->nWords ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the bug is found.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimClassesRefine( Cec_ManSim_t * p ) +{ + int i; + Gia_ManSetRefs( p->pAig ); + p->nWords = p->pPars->nWords; + for ( i = 0; i < p->pPars->nRounds; i++ ) + { + if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; + } + if ( p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + return 0; +} +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |