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