giaSim2.c File Reference

#include "gia.h"

Include dependency graph for giaSim2.c:

Go to the source code of this file.

Classes
struct	Gia_Sim2_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Gia_Sim2_t_	Gia_Sim2_t
	DECLARATIONS ///.

Functions
void	Gia_ManResetRandom (Gia_ParSim_t *pPars)
void	Gia_Sim2Delete (Gia_Sim2_t *p)
	FUNCTION DEFINITIONS ///.
Gia_Sim2_t *	Gia_Sim2Create (Gia_Man_t *pAig, Gia_ParSim_t *pPars)
int	Gia_Sim2CompareEqual (unsigned *p0, unsigned *p1, int nWords, int fCompl)
int	Gia_Sim2CompareZero (unsigned *p0, int nWords, int fCompl)
void	Gia_Sim2ClassCreate (Gia_Man_t *p, Vec_Int_t *vClass)
int	Gia_Sim2ClassRefineOne (Gia_Sim2_t *p, int i)
int	Gia_Sim2HashKey (unsigned *pSim, int nWords, int nTableSize)
void	Gia_Sim2ProcessRefined (Gia_Sim2_t *p, Vec_Int_t *vRefined)
void	Gia_Sim2InfoRefineEquivs (Gia_Sim2_t *p)
Abc_Cex_t *	Gia_Sim2GenerateCounter (Gia_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat)
int	Gia_ManSimSimulateEquiv (Gia_Man_t *pAig, Gia_ParSim_t *pPars)

Typedef Documentation

Gia_Sim2_t

typedef typedefABC_NAMESPACE_IMPL_START struct Gia_Sim2_t_ Gia_Sim2_t

DECLARATIONS ///.

CFile****************************************************************

FileName [giaSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Fast sequential simulator.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 30 of file giaSim2.c.

Function Documentation

Gia_ManResetRandom()

void Gia_ManResetRandom ( Gia_ParSim_t * pPars )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 580 of file giaSim.c.

{
    int i;
    Gia_ManRandom( 1 );
    for ( i = 0; i < pPars->RandSeed; i++ )
        Gia_ManRandom( 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManSimSimulateEquiv()

int Gia_ManSimSimulateEquiv	(	Gia_Man_t *	pAig,
		Gia_ParSim_t *	pPars )

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

Synopsis [Performs simulation to refine equivalence classes.]

Description [Returns 1 if counter-example is detected.]

SideEffects []

SeeAlso []

Definition at line 638 of file giaSim2.c.

{
    Gia_Sim2_t * p;
    Gia_Obj_t * pObj;
    abctime clkTotal = Abc_Clock();
    int i, RetValue = 0, iOut, iPat;
    abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
    assert( pAig->pReprs && pAig->pNexts );
    ABC_FREE( pAig->pCexSeq );
    p = Gia_Sim2Create( pAig, pPars );
    Gia_ManResetRandom( pPars );
    Gia_ManForEachRo( p->pAig, pObj, i )
        Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
    for ( i = 0; i < pPars->nIters; i++ )
    {
        Gia_Sim2SimulateRound( p );
        if ( pPars->fVerbose )
        {
            Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
            if ( pAig->pReprs && pAig->pNexts )
                Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
            Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
        }
        if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
        {
            Gia_ManResetRandom( pPars );
            pPars->iOutFail = iOut;
            pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", iOut, pAig->pName, i );
            if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
            {
//                Abc_Print( 1, "\n" );
                Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
//                Abc_Print( 1, "\n" );
            }
            else
            {
//                Abc_Print( 1, "\n" );
//                if ( pPars->fVerbose )
//                Abc_Print( 1, "\nGenerated counter-example is verified correctly.         " );
//                Abc_Print( 1, "\n" );
            }
            RetValue = 1;
            break;
        }
        if ( pAig->pReprs && pAig->pNexts )
            Gia_Sim2InfoRefineEquivs( p );
        if ( Abc_Clock() > nTimeToStop )
        {
            i++;
            break;
        }
        if ( i < pPars->nIters - 1 )
            Gia_Sim2InfoTransfer( p );
    }
    Gia_Sim2Delete( p );
    if ( pAig->pCexSeq == NULL )
        Abc_Print( 1, "No bug detected after simulating %d frames with %d words.  ", i, pPars->nWords );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_Sim2ClassCreate()

void Gia_Sim2ClassCreate	(	Gia_Man_t *	p,
		Vec_Int_t *	vClass )

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

Synopsis [Creates equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file giaSim2.c.

{
    int Repr = GIA_VOID, EntPrev = -1, Ent, i;
    assert( Vec_IntSize(vClass) > 0 );
    Vec_IntForEachEntry( vClass, Ent, i )
    {
        if ( i == 0 )
        {
            Repr = Ent;
            Gia_ObjSetRepr( p, Ent, GIA_VOID );
            EntPrev = Ent;
        }
        else
        {
            assert( Repr < Ent );
            Gia_ObjSetRepr( p, Ent, Repr );
            Gia_ObjSetNext( p, EntPrev, Ent );
            EntPrev = Ent;
        }
    }
    Gia_ObjSetNext( p, EntPrev, 0 );
}

Here is the caller graph for this function:

Gia_Sim2ClassRefineOne()

int Gia_Sim2ClassRefineOne	(	Gia_Sim2_t *	p,
		int	i )

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

Synopsis [Refines one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file giaSim2.c.

{
    Gia_Obj_t * pObj0, * pObj1;
    unsigned * pSim0, * pSim1;
    int Ent;
    Vec_IntClear( p->vClassOld );
    Vec_IntClear( p->vClassNew );
    Vec_IntPush( p->vClassOld, i );
    pObj0 = Gia_ManObj( p->pAig, i );
    pSim0 = Gia_Sim2Data( p, i );
    Gia_ClassForEachObj1( p->pAig, i, Ent )
    {
        pObj1 = Gia_ManObj( p->pAig, Ent );
        pSim1 = Gia_Sim2Data( p, Ent );
        if ( Gia_Sim2CompareEqual( pSim0, pSim1, p->nWords, Gia_ObjPhase(pObj0) ^ Gia_ObjPhase(pObj1) ) )
            Vec_IntPush( p->vClassOld, Ent );
        else
            Vec_IntPush( p->vClassNew, Ent );
    }
    if ( Vec_IntSize( p->vClassNew ) == 0 )
        return 0;
    Gia_Sim2ClassCreate( p->pAig, p->vClassOld );
    Gia_Sim2ClassCreate( p->pAig, p->vClassNew );
    if ( Vec_IntSize(p->vClassNew) > 1 )
        return 1 + Gia_Sim2ClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_Sim2CompareEqual()

int Gia_Sim2CompareEqual	(	unsigned *	p0,
		unsigned *	p1,
		int	nWords,
		int	fCompl )

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

Synopsis [Compares simulation info of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file giaSim2.c.

{
    int w;
    if ( !fCompl )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != p1[w] )
                return 0;
        return 1;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != ~p1[w] )
                return 0;
        return 1;
    }
}

Here is the caller graph for this function:

Gia_Sim2CompareZero()

int Gia_Sim2CompareZero	(	unsigned *	p0,
		int	nWords,
		int	fCompl )

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

Synopsis [Compares simulation info of one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file giaSim2.c.

{
    int w;
    if ( !fCompl )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != 0 )
                return 0;
        return 1;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != ~0 )
                return 0;
        return 1;
    }
}

Here is the caller graph for this function:

Gia_Sim2Create()

Gia_Sim2_t * Gia_Sim2Create	(	Gia_Man_t *	pAig,
		Gia_ParSim_t *	pPars )

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

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file giaSim2.c.

{
    Gia_Sim2_t * p;
    Gia_Obj_t * pObj;
    int i;
    p = ABC_CALLOC( Gia_Sim2_t, 1 );
    p->pAig      = pAig;
    p->pPars     = pPars;
    p->nWords    = pPars->nWords;
    p->pDataSim  = ABC_ALLOC( unsigned, p->nWords * Gia_ManObjNum(p->pAig) );
    if ( !p->pDataSim  )
    { 
        Abc_Print( 1, "Simulator could not allocate %.2f GB for simulation info.\n", 
            4.0 * p->nWords * Gia_ManObjNum(p->pAig) / (1<<30) );
        Gia_Sim2Delete( p );
        return NULL;
    }
    p->vClassOld = Vec_IntAlloc( 100 );
    p->vClassNew = Vec_IntAlloc( 100 );
    if ( pPars->fVerbose )
        Abc_Print( 1, "Memory: AIG = %7.2f MB.  SimInfo = %7.2f MB.\n", 
            12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*Gia_ManObjNum(p->pAig)/(1<<20) );
    // prepare AIG
    Gia_ManSetPhase( pAig );
    Gia_ManForEachObj( pAig, pObj, i )
        pObj->Value = i;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_Sim2Delete()

void Gia_Sim2Delete

(

Gia_Sim2_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file giaSim2.c.

{
    Vec_IntFreeP( &p->vClassOld );
    Vec_IntFreeP( &p->vClassNew );
    ABC_FREE( p->pDataSim );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Gia_Sim2GenerateCounter()

Abc_Cex_t * Gia_Sim2GenerateCounter	(	Gia_Man_t *	pAig,
		int	iFrame,
		int	iOut,
		int	nWords,
		int	iPat )

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

Synopsis [Returns the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 604 of file giaSim2.c.

{
    Abc_Cex_t * p;
    unsigned * pData;
    int f, i, w, Counter;
    p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
    p->iFrame = iFrame;
    p->iPo = iOut;
    // fill in the binary data
    Counter = p->nRegs;
    pData = ABC_ALLOC( unsigned, nWords );
    for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
    for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
    {
        for ( w = nWords-1; w >= 0; w-- )
            pData[w] = Gia_ManRandom( 0 );
        if ( Abc_InfoHasBit( pData, iPat ) )
            Abc_InfoSetBit( p->pData, Counter + i );
    }
    ABC_FREE( pData );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_Sim2HashKey()

int Gia_Sim2HashKey	(	unsigned *	pSim,
		int	nWords,
		int	nTableSize )

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

Synopsis [Computes hash key of the simuation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file giaSim2.c.

{
    static int s_Primes[16] = { 
        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
    unsigned uHash = 0;
    int i;
    if ( pSim[0] & 1 )
        for ( i = 0; i < nWords; i++ )
            uHash ^= ~pSim[i] * s_Primes[i & 0xf];
    else
        for ( i = 0; i < nWords; i++ )
            uHash ^= pSim[i] * s_Primes[i & 0xf];
    return (int)(uHash % nTableSize);
 
}

Here is the caller graph for this function:

Gia_Sim2InfoRefineEquivs()

void Gia_Sim2InfoRefineEquivs

(

Gia_Sim2_t *

p

)

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

Synopsis [Refines equivalences after one simulation round.]

Description []

SideEffects []

SeeAlso []

Definition at line 516 of file giaSim2.c.

{
    Vec_Int_t * vRefined;
    Gia_Obj_t * pObj;
    unsigned * pSim;
    int i, Count = 0;
    // process constant candidates
    vRefined = Vec_IntAlloc( 100 );
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( !Gia_ObjIsConst(p->pAig, i) )
            continue;
        pSim = Gia_Sim2Data( p, i );
//Extra_PrintBinary( stdout, pSim, 32 * p->nWords );  printf( "\n" );
        if ( !Gia_Sim2CompareZero( pSim, p->nWords, Gia_ObjPhase(pObj) ) )
        {
            Vec_IntPush( vRefined, i );
            Count++;
        }
    }
    Gia_Sim2ProcessRefined( p, vRefined );
    Vec_IntFree( vRefined );
    // process other classes
    Gia_ManForEachClass( p->pAig, i )
        Count += Gia_Sim2ClassRefineOne( p, i );
//    if ( Count )
//        printf( "Refined %d times.\n", Count );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_Sim2ProcessRefined()

void Gia_Sim2ProcessRefined	(	Gia_Sim2_t *	p,
		Vec_Int_t *	vRefined )

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

Synopsis [Refines nodes belonging to candidate constant class.]

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file giaSim2.c.

{
    unsigned * pSim;
    int * pTable, nTableSize, i, k, Key;
    if ( Vec_IntSize(vRefined) == 0 )
        return;
    nTableSize = Abc_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
    pTable = ABC_CALLOC( int, nTableSize );
    Vec_IntForEachEntry( vRefined, i, k )
    {
        pSim = Gia_Sim2Data( p, i );
        Key = Gia_Sim2HashKey( pSim, p->nWords, nTableSize );
        if ( pTable[Key] == 0 )
        {
            assert( Gia_ObjRepr(p->pAig, i) == 0 );
            assert( Gia_ObjNext(p->pAig, i) == 0 );
            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
        }
        else
        {
            Gia_ObjSetNext( p->pAig, pTable[Key], i );
            Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
            if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
                Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
            assert( Gia_ObjRepr(p->pAig, i) > 0 );
        }
        pTable[Key] = i;
    }
/*
    Vec_IntForEachEntry( vRefined, i, k )
    {
        if ( Gia_ObjIsHead( p->pAig, i ) )
            Gia_Sim2ClassRefineOne( p, i );
    }
*/
    ABC_FREE( pTable );
}

Here is the call graph for this function:

Here is the caller graph for this function: