diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaSim2.c | 705 |
1 files changed, 705 insertions, 0 deletions
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c new file mode 100644 index 00000000..4131f942 --- /dev/null +++ b/src/aig/gia/giaSim2.c @@ -0,0 +1,705 @@ +/**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 = Gia_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 = Gia_ManAllocCounterExample( 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 ( Gia_InfoHasBit( pData, iPat ) ) + Gia_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; + int i, clkTotal = clock(); + int RetValue = 0, iOut, iPat; + 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*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, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); + if ( !Gia_ManVerifyCounterExample( 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 ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) + { + 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", clock() - clkTotal ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |