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