giaEra.c File Reference

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

Include dependency graph for giaEra.c:

Go to the source code of this file.

Classes
struct	Gia_ObjEra_t_
struct	Gia_ManEra_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Gia_ObjEra_t_	Gia_ObjEra_t
	DECLARATIONS ///.
typedef struct Gia_ManEra_t_	Gia_ManEra_t

Functions
Gia_ManEra_t *	Gia_ManEraCreate (Gia_Man_t *pAig)
	FUNCTION DEFINITIONS ///.
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)
void	Gia_ManEraHashResize (Gia_ManEra_t *p)
void	Gia_ManInsertState (Gia_ManEra_t *p, Gia_ObjEra_t *pState)
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

Gia_ManEra_t

typedef struct Gia_ManEra_t_ Gia_ManEra_t

Definition at line 43 of file giaEra.c.

Gia_ObjEra_t

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

Gia_ManAnalyzeResult()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManCollectBugTrace()

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

Here is the caller graph for this function:

Gia_ManCollectReachable()

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

Here is the call graph for this function:

Gia_ManCountDepth()

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

Here is the caller graph for this function:

Gia_ManEraCreate()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManEraCreateState()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManEraFree()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManEraHashResize()

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

Here is the caller graph for this function:

Gia_ManEraStateHash()

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

Here is the caller graph for this function:

Gia_ManInsertState()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManPerformOneIter()

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

Here is the caller graph for this function: