#include "gia.h"
#include "misc/mem/mem.h"

Data Structures
struct	Gia_ObjEra_t_

struct	Gia_ManEra_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Gia_ObjEra_t_	Gia_ObjEra_t
	DECLARATIONS ///. More...

typedef struct Gia_ManEra_t_	Gia_ManEra_t

Functions
static unsigned *	Gia_ManEraData (Gia_ManEra_t *p, int i)

static Gia_ObjEra_t *	Gia_ManEraState (Gia_ManEra_t *p, int i)

Gia_ManEra_t *	Gia_ManEraCreate (Gia_Man_t *pAig)
	FUNCTION DEFINITIONS ///. More...

void	Gia_ManEraFree (Gia_ManEra_t *p)

Gia_ObjEra_t *	Gia_ManEraCreateState (Gia_ManEra_t *p)

int	Gia_ManEraStateHash (unsigned *pState, int nWordsSim, int nTableSize)

static unsigned *	Gia_ManEraHashFind (Gia_ManEra_t p, Gia_ObjEra_t pState, int *pStateNum)

void	Gia_ManEraHashResize (Gia_ManEra_t *p)

void	Gia_ManInsertState (Gia_ManEra_t p, Gia_ObjEra_t pState)

static int	Gia_ManOutputAsserted (Gia_ManEra_t p, Gia_Obj_t pObj)

static void	Gia_ManSimulateCo (Gia_ManEra_t p, Gia_Obj_t pObj)

static void	Gia_ManSimulateNode (Gia_ManEra_t p, Gia_Obj_t pObj)

void	Gia_ManPerformOneIter (Gia_ManEra_t *p)

Vec_Int_t *	Gia_ManCollectBugTrace (Gia_ManEra_t p, Gia_ObjEra_t pState, int iCond)

int	Gia_ManCountDepth (Gia_ManEra_t *p)

int	Gia_ManAnalyzeResult (Gia_ManEra_t p, Gia_ObjEra_t pState, int fMiter, int fStgDump)

int	Gia_ManCollectReachable (Gia_Man_t *pAig, int nStatesMax, int fMiter, int fDumpFile, int fVerbose)

Typedef Documentation

typedef struct Gia_ManEra_t_ Gia_ManEra_t

Definition at line 43 of file giaEra.c.

typedef typedefABC_NAMESPACE_IMPL_START struct Gia_ObjEra_t_ Gia_ObjEra_t

DECLARATIONS ///.

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

]

Definition at line 32 of file giaEra.c.

Function Documentation

int Gia_ManAnalyzeResult	(	Gia_ManEra_t *	p,
		Gia_ObjEra_t *	pState,
		int	fMiter,
		int	fStgDump
	)

Function*************************************************************

Synopsis [Analized reached states.]

Description []

SideEffects []

SeeAlso []

Definition at line 449 of file giaEra.c.

 {
     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;
 }

Vec_Int_t* Gia_ManCollectBugTrace	(	Gia_ManEra_t *	p,
		Gia_ObjEra_t *	pState,
		int	iCond
	)

Function*************************************************************

Synopsis [Performs one iteration of reachability analysis.]

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file giaEra.c.

 {
     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;
 }

int Gia_ManCollectReachable	(	Gia_Man_t *	pAig,
		int	nStatesMax,
		int	fMiter,
		int	fDumpFile,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Resizes the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 527 of file giaEra.c.

 { 
     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;
 }

int Gia_ManCountDepth ( Gia_ManEra_t * p )

Function*************************************************************

Synopsis [Counts the depth of state transitions leading ot this state.]

Description []

SideEffects []

SeeAlso []

Definition at line 426 of file giaEra.c.

 {
     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;
 }

Gia_ManEra_t* Gia_ManEraCreate ( Gia_Man_t * pAig )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Creates reachability manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file giaEra.c.

 {
     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;
 }

Gia_ObjEra_t* Gia_ManEraCreateState ( Gia_ManEra_t * p )

Function*************************************************************

Synopsis [Creates new state.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file giaEra.c.

 {
     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;
 }

static unsigned* Gia_ManEraData	(	Gia_ManEra_t *	p,
		int	i
	)

inlinestatic

Definition at line 61 of file giaEra.c.

61 { return p->pDataSim + i * p->nWordsSim; }

Gia_ManEra_t_::nWordsSim

int nWordsSim

Definition: giaEra.c:47

Gia_ManEra_t_::pDataSim

unsigned * pDataSim

Definition: giaEra.c:49

void Gia_ManEraFree ( Gia_ManEra_t * p )

Function*************************************************************

Synopsis [Deletes reachability manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file giaEra.c.

 {
     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 );
 }

static unsigned* Gia_ManEraHashFind	(	Gia_ManEra_t *	p,
		Gia_ObjEra_t *	pState,
		int *	pStateNum
	)

inlinestatic

Function*************************************************************

Synopsis [Returns the place of this state in the table or NULL if it exists.]

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file giaEra.c.

 {
     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;
 }

void Gia_ManEraHashResize ( Gia_ManEra_t * p )

Function*************************************************************

Synopsis [Resizes the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file giaEra.c.

 {
     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 );
 }

static Gia_ObjEra_t* Gia_ManEraState	(	Gia_ManEra_t *	p,
		int	i
	)

inlinestatic

Definition at line 62 of file giaEra.c.

62 { return (Gia_ObjEra_t *)Vec_PtrEntry(p->vStates, i); }

Gia_ObjEra_t

typedefABC_NAMESPACE_IMPL_START struct Gia_ObjEra_t_ Gia_ObjEra_t

DECLARATIONS ///.

Definition: giaEra.c:32

Vec_PtrEntry

static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)

Definition: vecPtr.h:362

Gia_ManEra_t_::vStates

Vec_Ptr_t * vStates

Definition: giaEra.c:51

int Gia_ManEraStateHash	(	unsigned *	pState,
		int	nWordsSim,
		int	nTableSize
	)

Function*************************************************************

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file giaEra.c.

 {
     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;
 }

void Gia_ManInsertState	(	Gia_ManEra_t *	p,
		Gia_ObjEra_t *	pState
	)

Function*************************************************************

Synopsis [Initialize register output to the given state.]

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file giaEra.c.

 {
     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 );
     }
 }

static int Gia_ManOutputAsserted	(	Gia_ManEra_t *	p,
		Gia_Obj_t *	pObj
	)

inlinestatic

Function*************************************************************

Synopsis [Returns -1 if outputs are not asserted.]

Description []

SideEffects []

SeeAlso []

Definition at line 296 of file giaEra.c.

 {
     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;
 }

void Gia_ManPerformOneIter ( Gia_ManEra_t * p )

Function*************************************************************

Synopsis [Performs one iteration of reachability analysis.]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file giaEra.c.

 {
     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 );
     }
 }

static void Gia_ManSimulateCo	(	Gia_ManEra_t *	p,
		Gia_Obj_t *	pObj
	)

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file giaEra.c.

 {
     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];
 }

static void Gia_ManSimulateNode	(	Gia_ManEra_t *	p,
		Gia_Obj_t *	pObj
	)

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file giaEra.c.

 {
     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];
     }
 }

Data Structures

Typedefs

Functions

Typedef Documentation

Function Documentation