| /**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_ManCreateValueRefs( 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_ManCreateValueRefs( 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 | |