diff options
Diffstat (limited to 'src/aig/cec/cecClass.c')
| -rw-r--r-- | src/aig/cec/cecClass.c | 931 |
1 files changed, 0 insertions, 931 deletions
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c deleted file mode 100644 index b6118038..00000000 --- a/src/aig/cec/cecClass.c +++ /dev/null @@ -1,931 +0,0 @@ -/**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 = Gia_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) * Gia_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 ( Gia_InfoHasBit( pInfo, iPat ) ) - Gia_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 ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) ) - Gia_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 - |