diff options
Diffstat (limited to 'src/aig/gia/giaEra.c')
| -rw-r--r-- | src/aig/gia/giaEra.c | 561 |
1 files changed, 561 insertions, 0 deletions
diff --git a/src/aig/gia/giaEra.c b/src/aig/gia/giaEra.c new file mode 100644 index 00000000..ec3e1b1b --- /dev/null +++ b/src/aig/gia/giaEra.c @@ -0,0 +1,561 @@ +/**CFile**************************************************************** + + FileName [giaEra.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Explicit reachability analysis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaEra.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "mem.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// explicit state representation +typedef struct Gia_ObjEra_t_ Gia_ObjEra_t; +struct Gia_ObjEra_t_ +{ + int Num; // ID of this state + int Cond; // input condition + int iPrev; // previous state + int iNext; // next state in the hash table + unsigned pData[0]; // state bits +}; + +// explicit state reachability +typedef struct Gia_ManEra_t_ Gia_ManEra_t; +struct Gia_ManEra_t_ +{ + Gia_Man_t * pAig; // user's AIG manager + int nWordsSim; // 2^(PInum) + int nWordsDat; // Gia_BitWordNum + unsigned * pDataSim; // simulation data + Mem_Fixed_t * pMemory; // memory manager + Vec_Ptr_t * vStates; // reached states + Gia_ObjEra_t * pStateNew; // temporary state + int iCurState; // the current state + Vec_Int_t * vBugTrace; // the sequence of transitions + // hash table for states + int nBins; + unsigned * pBins; +}; + +static inline unsigned * Gia_ManEraData( Gia_ManEra_t * p, int i ) { return p->pDataSim + i * p->nWordsSim; } +static inline Gia_ObjEra_t * Gia_ManEraState( Gia_ManEra_t * p, int i ) { return (Gia_ObjEra_t *)Vec_PtrEntry(p->vStates, i); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates reachability manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig ) +{ + Vec_Ptr_t * vTruths; + Gia_ManEra_t * p; + unsigned * pTruth, * pSimInfo; + int i; + p = ABC_CALLOC( Gia_ManEra_t, 1 ); + p->pAig = pAig; + p->nWordsSim = Gia_TruthWordNum( Gia_ManPiNum(pAig) ); + p->nWordsDat = Gia_BitWordNum( Gia_ManRegNum(pAig) ); + p->pDataSim = ABC_ALLOC( unsigned, p->nWordsSim*Gia_ManObjNum(pAig) ); + p->pMemory = Mem_FixedStart( sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat ); + p->vStates = Vec_PtrAlloc( 100000 ); + p->nBins = Gia_PrimeCudd( 100000 ); + p->pBins = ABC_CALLOC( unsigned, p->nBins ); + Vec_PtrPush( p->vStates, NULL ); + // assign primary input values + vTruths = Vec_PtrAllocTruthTables( Gia_ManPiNum(pAig) ); + Vec_PtrForEachEntry( unsigned *, vTruths, pTruth, i ) + { + pSimInfo = Gia_ManEraData( p, Gia_ObjId(pAig, Gia_ManPi(pAig, i)) ); + memcpy( pSimInfo, pTruth, sizeof(unsigned) * p->nWordsSim ); + } + Vec_PtrFree( vTruths ); + // assign constant zero node + pSimInfo = Gia_ManEraData( p, 0 ); + memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deletes reachability manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEraFree( Gia_ManEra_t * p ) +{ + Mem_FixedStop( p->pMemory, 0 ); + Vec_PtrFree( p->vStates ); + if ( p->vBugTrace ) Vec_IntFree( p->vBugTrace ); + ABC_FREE( p->pDataSim ); + ABC_FREE( p->pBins ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Creates new state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_ObjEra_t * Gia_ManEraCreateState( Gia_ManEra_t * p ) +{ + Gia_ObjEra_t * pNew; + pNew = (Gia_ObjEra_t *)Mem_FixedEntryFetch( p->pMemory ); + pNew->Num = Vec_PtrSize( p->vStates ); + pNew->iPrev = 0; + Vec_PtrPush( p->vStates, pNew ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManEraStateHash( unsigned * pState, int nWordsSim, int nTableSize ) +{ + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned uHash; + int i; + uHash = 0; + for ( i = 0; i < nWordsSim; i++ ) + uHash ^= pState[i] * s_FPrimes[i & 0x7F]; + return uHash % nTableSize; +} + +/**Function************************************************************* + + Synopsis [Returns the place of this state in the table or NULL if it exists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned * Gia_ManEraHashFind( Gia_ManEra_t * p, Gia_ObjEra_t * pState ) +{ + Gia_ObjEra_t * pThis; + unsigned * pPlace = p->pBins + Gia_ManEraStateHash( pState->pData, p->nWordsDat, p->nBins ); + for ( pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL; pThis; + pPlace = (unsigned *)&pThis->iNext, pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL ) + if ( !memcmp( pState->pData, pThis->pData, sizeof(unsigned) * p->nWordsDat ) ) + return NULL; + return pPlace; +} + +/**Function************************************************************* + + Synopsis [Resizes the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEraHashResize( Gia_ManEra_t * p ) +{ + Gia_ObjEra_t * pThis; + unsigned * pBinsOld, * piPlace; + int nBinsOld, iNext, Counter, i; + assert( p->pBins != NULL ); + // replace the table + pBinsOld = p->pBins; + nBinsOld = p->nBins; + p->nBins = Gia_PrimeCudd( 3 * p->nBins ); + p->pBins = ABC_CALLOC( unsigned, p->nBins ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < nBinsOld; i++ ) + for ( pThis = (pBinsOld[i]? Gia_ManEraState(p, pBinsOld[i]) : NULL), + iNext = (pThis? pThis->iNext : 0); + pThis; pThis = (iNext? Gia_ManEraState(p, iNext) : NULL), + iNext = (pThis? pThis->iNext : 0) ) + { + assert( pThis->Num ); + pThis->iNext = 0; + piPlace = Gia_ManEraHashFind( p, pThis ); + assert( *piPlace == 0 ); // should not be there + *piPlace = pThis->Num; + Counter++; + } + assert( Counter == Vec_PtrSize( p->vStates ) - 1 ); + ABC_FREE( pBinsOld ); +} + +/**Function************************************************************* + + Synopsis [Initialize register output to the given state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManInsertState( Gia_ManEra_t * p, Gia_ObjEra_t * pState ) +{ + Gia_Obj_t * pObj; + unsigned * pSimInfo; + int i; + Gia_ManForEachRo( p->pAig, pObj, i ) + { + pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); + if ( Gia_InfoHasBit(pState->pData, i) ) + memset( pSimInfo, 0xff, sizeof(unsigned) * p->nWordsSim ); + else + memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim ); + } +} + +/**Function************************************************************* + + Synopsis [Returns -1 if outputs are not asserted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManOutputAsserted( Gia_ManEra_t * p, Gia_Obj_t * pObj ) +{ + unsigned * pInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); + int w; + for ( w = 0; w < p->nWordsSim; w++ ) + if ( pInfo[w] ) + return 32*w + Gia_WordFindFirstBit( pInfo[w] ); + return -1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManSimulateCo( Gia_ManEra_t * p, Gia_Obj_t * pObj ) +{ + int Id = Gia_ObjId(p->pAig, pObj); + unsigned * pInfo = Gia_ManEraData( p, Id ); + unsigned * pInfo0 = Gia_ManEraData( p, Gia_ObjFaninId0(pObj, Id) ); + int w; + if ( Gia_ObjFaninC0(pObj) ) + for ( w = p->nWordsSim-1; w >= 0; w-- ) + pInfo[w] = ~pInfo0[w]; + else + for ( w = p->nWordsSim-1; w >= 0; w-- ) + pInfo[w] = pInfo0[w]; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManSimulateNode( Gia_ManEra_t * p, Gia_Obj_t * pObj ) +{ + int Id = Gia_ObjId(p->pAig, pObj); + unsigned * pInfo = Gia_ManEraData( p, Id ); + unsigned * pInfo0 = Gia_ManEraData( p, Gia_ObjFaninId0(pObj, Id) ); + unsigned * pInfo1 = Gia_ManEraData( p, Gia_ObjFaninId1(pObj, Id) ); + int w; + if ( Gia_ObjFaninC0(pObj) ) + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = p->nWordsSim-1; w >= 0; w-- ) + pInfo[w] = ~(pInfo0[w] | pInfo1[w]); + else + for ( w = p->nWordsSim-1; w >= 0; w-- ) + pInfo[w] = ~pInfo0[w] & pInfo1[w]; + } + else + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = p->nWordsSim-1; w >= 0; w-- ) + pInfo[w] = pInfo0[w] & ~pInfo1[w]; + else + for ( w = p->nWordsSim-1; w >= 0; w-- ) + pInfo[w] = pInfo0[w] & pInfo1[w]; + } +} + +/**Function************************************************************* + + Synopsis [Performs one iteration of reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPerformOneIter( Gia_ManEra_t * p ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObj1( p->pAig, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManSimulateNode( p, pObj ); + else if ( Gia_ObjIsCo(pObj) ) + Gia_ManSimulateCo( p, pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Performs one iteration of reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCollectBugTrace( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int iCond ) +{ + Vec_Int_t * vTrace; + vTrace = Vec_IntAlloc( 10 ); + Vec_IntPush( vTrace, iCond ); + for ( ; pState; pState = pState->iPrev ? Gia_ManEraState(p, pState->iPrev) : NULL ) + Vec_IntPush( vTrace, pState->Cond ); + Vec_IntReverseOrder( vTrace ); + return vTrace; +} + +/**Function************************************************************* + + Synopsis [Counts the depth of state transitions leading ot this state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCountDepth( Gia_ManEra_t * p ) +{ + Gia_ObjEra_t * pState; + int Counter = 0; + pState = (Gia_ObjEra_t *)Vec_PtrEntryLast( p->vStates ); + if ( pState->iPrev == 0 && Vec_PtrSize(p->vStates) > 3 ) + pState = (Gia_ObjEra_t *)Vec_PtrEntry( p->vStates, Vec_PtrSize(p->vStates) - 2 ); + for ( ; pState; pState = pState->iPrev ? Gia_ManEraState(p, pState->iPrev) : NULL ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Analized reached states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter ) +{ + Gia_Obj_t * pObj; + unsigned * pSimInfo, * piPlace; + int i, k, iCond, nMints; + // check if the miter is asserted + if ( fMiter ) + { + Gia_ManForEachPo( p->pAig, pObj, i ) + { + iCond = Gia_ManOutputAsserted( p, pObj ); + if ( iCond >= 0 ) + { + p->vBugTrace = Gia_ManCollectBugTrace( p, pState, iCond ); + return 1; + } + } + } + // collect reached states + nMints = (1 << Gia_ManPiNum(p->pAig)); + for ( k = 0; k < nMints; k++ ) + { + if ( p->pStateNew == NULL ) + p->pStateNew = Gia_ManEraCreateState( p ); + p->pStateNew->pData[p->nWordsDat-1] = 0; + Gia_ManForEachRi( p->pAig, pObj, i ) + { + pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); + if ( Gia_InfoHasBit(p->pStateNew->pData, i) != Gia_InfoHasBit(pSimInfo, k) ) + Gia_InfoXorBit( p->pStateNew->pData, i ); + } + piPlace = Gia_ManEraHashFind( p, p->pStateNew ); + if ( piPlace == NULL ) + continue; +//printf( "Inserting %d ", Vec_PtrSize(p->vStates) ); +//Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) ); printf( "\n" ); + assert( *piPlace == 0 ); + *piPlace = p->pStateNew->Num; + p->pStateNew->Cond = k; + p->pStateNew->iPrev = pState->Num; + p->pStateNew->iNext = 0; + p->pStateNew = NULL; + // expand hash table if needed + if ( Vec_PtrSize(p->vStates) > 2 * p->nBins ) + Gia_ManEraHashResize( p ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Resizes the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ) +{ + Gia_ManEra_t * p; + Gia_ObjEra_t * pState; + int Hash, clk = clock(); + int RetValue = 1; + assert( Gia_ManPiNum(pAig) <= 12 ); + assert( Gia_ManRegNum(pAig) > 0 ); + p = Gia_ManEraCreate( pAig ); + // create init state + pState = Gia_ManEraCreateState( p ); + pState->Cond = 0; + pState->iPrev = 0; + pState->iNext = 0; + memset( pState->pData, 0, sizeof(unsigned) * p->nWordsDat ); + Hash = Gia_ManEraStateHash(pState->pData, p->nWordsDat, p->nBins); + p->pBins[ Hash ] = pState->Num; + // process reachable states + while ( p->iCurState < Vec_PtrSize( p->vStates ) - 1 ) + { + if ( Vec_PtrSize(p->vStates) >= nStatesMax ) + { + printf( "Reached the limit on states traversed (%d). ", nStatesMax ); + RetValue = -1; + break; + } + pState = Gia_ManEraState( p, ++p->iCurState ); + if ( p->iCurState > 1 && pState->iPrev == 0 ) + continue; +//printf( "Extracting %d ", p->iCurState ); +//Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) ); printf( "\n" ); + Gia_ManInsertState( p, pState ); + Gia_ManPerformOneIter( p ); + if ( Gia_ManAnalyzeResult( p, pState, fMiter ) && fMiter ) + { + RetValue = 0; + printf( "Miter failed in state %d after %d transitions. ", + p->iCurState, Vec_IntSize(p->vBugTrace)-1 ); + break; + } + if ( fVerbose && p->iCurState % 5000 == 0 ) + { + printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f Mb. ", + p->iCurState, Vec_PtrSize(p->vStates), 1.0*p->iCurState/Vec_PtrSize(p->vStates), Gia_ManCountDepth(p), + (1.0/(1<<20))*(1.0*Vec_PtrSize(p->vStates)*(sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat) + + 1.0*p->nBins*sizeof(unsigned) + 1.0*p->vStates->nCap * sizeof(void*)) ); + ABC_PRT( "Time", clock() - clk ); + } + } + printf( "Reachability analysis traversed %d states with depth %d. ", p->iCurState-1, Gia_ManCountDepth(p) ); + ABC_PRT( "Time", clock() - clk ); + Gia_ManEraFree( p ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |