/**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 $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Gia_Sim2_t_ Gia_Sim2_t;
struct Gia_Sim2_t_
{
Gia_Man_t * pAig;
Gia_ParSim_t * pPars;
int nWords;
unsigned * pDataSim;
Vec_Int_t * vClassOld;
Vec_Int_t * vClassNew;
};
static inline unsigned * Gia_Sim2Data( Gia_Sim2_t * p, int i ) { return p->pDataSim + i * p->nWords; }
extern void Gia_ManResetRandom( Gia_ParSim_t * pPars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_Sim2Delete( Gia_Sim2_t * p )
{
Vec_IntFreeP( &p->vClassOld );
Vec_IntFreeP( &p->vClassNew );
ABC_FREE( p->pDataSim );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Creates fast simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Sim2_t * Gia_Sim2Create( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2InfoRandom( Gia_Sim2_t * p, unsigned * pInfo )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2InfoZero( Gia_Sim2_t * p, unsigned * pInfo )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2InfoOne( Gia_Sim2_t * p, unsigned * pInfo )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = ~0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2InfoCopy( Gia_Sim2_t * p, unsigned * pInfo, unsigned * pInfo0 )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = pInfo0[w];
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2SimulateCo( Gia_Sim2_t * p, Gia_Obj_t * pObj )
{
unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
int w;
if ( Gia_ObjFaninC0(pObj) )
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = ~pInfo0[w];
else
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = pInfo0[w];
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2SimulateNode( Gia_Sim2_t * p, Gia_Obj_t * pObj )
{
unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
unsigned * pInfo1 = Gia_Sim2Data( p, Gia_ObjFaninId1(pObj, Gia_ObjValue(pObj)) );
int w;
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
else
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = ~pInfo0[w] & pInfo1[w];
}
else
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = pInfo0[w] & ~pInfo1[w];
else
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = pInfo0[w] & pInfo1[w];
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2InfoTransfer( Gia_Sim2_t * p )
{
Gia_Obj_t * pObjRo, * pObjRi;
unsigned * pInfo0, * pInfo1;
int i;
Gia_ManForEachRiRo( p->pAig, pObjRi, pObjRo, i )
{
pInfo0 = Gia_Sim2Data( p, Gia_ObjValue(pObjRo) );
pInfo1 = Gia_Sim2Data( p, Gia_ObjValue(pObjRi) );
Gia_Sim2InfoCopy( p, pInfo0, pInfo1 );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_Sim2SimulateRound( Gia_Sim2_t * p )
{
Gia_Obj_t * pObj;
int i;
pObj = Gia_ManConst0(p->pAig);
assert( Gia_ObjValue(pObj) == 0 );
Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
Gia_ManForEachPi( p->pAig, pObj, i )
Gia_Sim2InfoRandom( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
Gia_ManForEachAnd( p->pAig, pObj, i )
{
assert( Gia_ObjValue(pObj) == i );
Gia_Sim2SimulateNode( p, pObj );
}
Gia_ManForEachCo( p->pAig, pObj, i )
Gia_Sim2SimulateCo( p, pObj );
}
/**Function*************************************************************
Synopsis [Compares simulation info of two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_Sim2CompareEqual( unsigned * p0, unsigned * p1, int nWords, int fCompl )
{
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;
}
}
/**Function*************************************************************
Synopsis [Compares simulation info of one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_Sim2CompareZero( unsigned * p0, int nWords, int fCompl )
{
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;
}
}
/**Function*************************************************************
Synopsis [Creates equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_Sim2ClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
{
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 );
}
/**Function*************************************************************
Synopsis [Refines one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_Sim2ClassRefineOne( Gia_Sim2_t * p, int i )
{
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;
}
/**Function*************************************************************
Synopsis [Computes hash key of the simuation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_Sim2HashKey( unsigned * pSim, int nWords, int nTableSize )
{
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);
}
/**Function*************************************************************
Synopsis [Refines nodes belonging to candidate constant class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
{
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 );
}
/**Function*************************************************************
Synopsis [Refines equivalences after one simulation round.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_Sim2InfoRefineEquivs( Gia_Sim2_t * p )
{
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 );
}
/**Function*************************************************************
Synopsis [Returns index of the first pattern that failed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Gia_Sim2InfoIsZero( Gia_Sim2_t * p, unsigned * pInfo )
{
int w;
for ( w = 0; w < p->nWords; w++ )
if ( pInfo[w] )
return 32*w + Gia_WordFindFirstBit( pInfo[w] );
return -1;
}
/**Function*************************************************************
Synopsis [Returns index of the PO and pattern that failed it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Gia_Sim2CheckPos( Gia_Sim2_t * p, int * piPo, int * piPat )
{
Gia_Obj_t * pObj;
int i, iPat;
Gia_ManForEachPo( p->pAig, pObj, i )
{
iPat = Gia_Sim2InfoIsZero( p, Gia_Sim2Data( p, Gia_ObjValue(pObj) ) );
if ( iPat >= 0 )
{
*piPo = i;
*piPat = iPat;
return 1;
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Returns the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat )
{
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;
}
/**Function*************************************************************
Synopsis [Performs simulation to refine equivalence classes.]
Description [Returns 1 if counter-example is detected.]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
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;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END