| /**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 "misc/mem/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; // Abc_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 |
| Vec_Int_t * vStgDump; // STG written into a file |
| // 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 = Abc_TruthWordNum( Gia_ManPiNum(pAig) ); |
| p->nWordsDat = Abc_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 = Abc_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 ); |
| p->vStgDump = Vec_IntAlloc( 1000 ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Deletes reachability manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEraFree( Gia_ManEra_t * p ) |
| { |
| Mem_FixedStop( p->pMemory, 0 ); |
| Vec_IntFree( p->vStgDump ); |
| 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, int * pStateNum ) |
| { |
| 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 ) ) |
| { |
| if ( pStateNum ) |
| *pStateNum = pThis->Num; |
| return NULL; |
| } |
| if ( pStateNum ) |
| *pStateNum = -1; |
| 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 = Abc_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, NULL ); |
| 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 ( Abc_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, int fStgDump ) |
| { |
| Gia_Obj_t * pObj; |
| unsigned * pSimInfo, * piPlace, uOutput = 0; |
| int i, k, iCond, nMints, iNextState; |
| // 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 ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) ) |
| Abc_InfoXorBit( p->pStateNew->pData, i ); |
| } |
| if ( fStgDump ) |
| { |
| uOutput = 0; |
| Gia_ManForEachPo( p->pAig, pObj, i ) |
| { |
| pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); |
| if ( Abc_InfoHasBit(pSimInfo, k) && i < 32 ) |
| Abc_InfoXorBit( &uOutput, i ); |
| } |
| } |
| piPlace = Gia_ManEraHashFind( p, p->pStateNew, &iNextState ); |
| if ( fStgDump ) Vec_IntPush( p->vStgDump, k ); |
| if ( fStgDump ) Vec_IntPush( p->vStgDump, pState->Num ); |
| if ( piPlace == NULL ) |
| { |
| if ( fStgDump ) Vec_IntPush( p->vStgDump, iNextState ); |
| if ( fStgDump ) Vec_IntPush( p->vStgDump, uOutput ); |
| continue; |
| } |
| if ( fStgDump ) Vec_IntPush( p->vStgDump, p->pStateNew->Num ); |
| if ( fStgDump ) Vec_IntPush( p->vStgDump, uOutput ); |
| //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 fDumpFile, int fVerbose ) |
| { |
| Gia_ManEra_t * p; |
| Gia_ObjEra_t * pState; |
| int Hash; |
| abctime clk = Abc_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, fDumpFile ) && 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", Abc_Clock() - clk ); |
| } |
| } |
| printf( "Reachability analysis traversed %d states with depth %d. ", p->iCurState-1, Gia_ManCountDepth(p) ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| if ( fDumpFile ) |
| { |
| char * pFileName = "test.stg"; |
| FILE * pFile = fopen( pFileName, "wb" ); |
| if ( pFile == NULL ) |
| printf( "Cannot open file \"%s\" for writing.\n", pFileName ); |
| else |
| { |
| Gia_ManStgPrint( pFile, p->vStgDump, Gia_ManPiNum(pAig), Gia_ManPoNum(pAig), p->iCurState-1 ); |
| fclose( pFile ); |
| printf( "Extracted STG was written into file \"%s\".\n", pFileName ); |
| } |
| } |
| Gia_ManEraFree( p ); |
| return RetValue; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
