From c60852f4a935f72bb399414853b130eb49b79804 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 30 Jul 2011 13:37:02 +0700 Subject: Changes to enable smarter simulation. --- src/aig/ssw/ssw.h | 7 +- src/aig/ssw/sswRarity.c | 835 +++++++++++++++++++++++++++++++++++++++-------- src/aig/ssw/sswRarity2.c | 835 ++++++++--------------------------------------- src/base/abci/abc.c | 8 +- src/base/abci/abcDar.c | 48 +-- 5 files changed, 842 insertions(+), 891 deletions(-) diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 1361893a..22b6c6e5 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -116,11 +116,8 @@ extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); /*=== sswRarity.c ===================================================*/ -extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); -extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); -/*=== sswRarity2.c ===================================================*/ -extern int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); -extern int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); +extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); +extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); /*=== sswSim.c ===================================================*/ extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c index 3026cf6b..3ebc7799 100644 --- a/src/aig/ssw/sswRarity.c +++ b/src/aig/ssw/sswRarity.c @@ -37,19 +37,27 @@ struct Ssw_RarMan_t_ int nBinSize; // the number of flops in one group int fVerbose; // the verbosiness flag int nGroups; // the number of flop groups + int nWordsReg; // the number of words in the registers // internal data Aig_Man_t * pAig; // AIG with equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes - Ssw_Sml_t * pSml; // simulation manager - Vec_Ptr_t * vSimInfo; // simulation info from pSml manager Vec_Int_t * vInits; // initial state + // simulation data + word * pObjData; // simulation info for each obj + word * pPatData; // pattern data for each reg + // candidates to update + Vec_Ptr_t * vUpdConst; // constant 1 candidates + Vec_Ptr_t * vUpdClass; // class representatives // rarity data int * pRarity; // occur counts for patterns in groups - int * pGroupValues; // occur counts in each group double * pPatCosts; // pattern costs - + // best patterns + Vec_Int_t * vPatBests; // best patterns + int iFailPo; // failed primary output + int iFailPat; // failed pattern }; + static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); @@ -69,13 +77,19 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) p->pRarity[iBin * (1 << p->nBinSize) + iPat]++; } +static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); } + +static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id; } +static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; } + + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Prepares random number generator.] Description [] @@ -84,29 +98,17 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) SeeAlso [] ***********************************************************************/ -static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) +void Ssw_RarManPrepareRandom( int nRandSeed ) { - Ssw_RarMan_t * p; - if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 ) - return NULL; - p = ABC_CALLOC( Ssw_RarMan_t, 1 ); - p->pAig = pAig; - p->nWords = nWords; - p->nFrames = nFrames; - p->nBinSize = nBinSize; - p->fVerbose = fVerbose; - p->nGroups = Aig_ManRegNum(pAig) / nBinSize; - p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); - p->pGroupValues = ABC_CALLOC( int, p->nGroups ); - p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 ); - p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords ); - p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml ); - return p; + int i; + Aig_ManRandom( 1 ); + for ( i = 0; i < nRandSeed; i++ ) + Aig_ManRandom( 0 ); } /**Function************************************************************* - Synopsis [] + Synopsis [Initializes random primary inputs.] Description [] @@ -115,22 +117,112 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames SeeAlso [] ***********************************************************************/ -static void Ssw_RarManStop( Ssw_RarMan_t * p ) +void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p ) { - if ( p->pSml ) Ssw_SmlStop( p->pSml ); - if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); - Vec_PtrFreeP( &p->vSimInfo ); - Vec_IntFreeP( &p->vInits ); - ABC_FREE( p->pGroupValues ); - ABC_FREE( p->pPatCosts ); - ABC_FREE( p->pRarity ); - ABC_FREE( p ); + word * pSim; + Aig_Obj_t * pObj; + int w, i; + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + for ( w = 0; w < p->nWords; w++ ) + pSim[w] = Aig_ManRandom64(0); + pSim[0] <<= 1; + } } +/**Function************************************************************* + + Synopsis [Derives the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal ) +{ + Abc_Cex_t * pCex; + Aig_Obj_t * pObj; + Vec_Int_t * vTrace; + word * pSim; + int i, r, f, iBit, iPatThis; + // compute the pattern sequence + iPatThis = iPatFinal; + vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 ); + Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis ); + for ( r = iFrame / p->nFrames - 1; r >= 0; r-- ) + { + iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 ); + Vec_IntWriteEntry( vTrace, r, iPatThis ); + } + // create counter-example + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 ); + pCex->iFrame = iFrame; + pCex->iPo = iPo; + // insert the bits + iBit = Aig_ManRegNum(p->pAig); + for ( f = 0; f <= iFrame; f++ ) + { + Ssw_RarManAssingRandomPis( p ); + iPatThis = Vec_IntEntry( vTrace, f / p->nFrames ); + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + if ( Aig_InfoHasBit( (unsigned *)pSim, iPatThis ) ) + Aig_InfoSetBit( pCex->pData, iBit ); + iBit++; + } + } + Vec_IntFree( vTrace ); + assert( iBit == pCex->nBits ); + // verify the counter example + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) + { + printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" ); + Abc_CexFree( pCex ); + pCex = NULL; + } + else + { +// printf( "Counter-example verification is successful.\n" ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + } + return pCex; +} + + +/**Function************************************************************* + + Synopsis [Transposing 32-bit matrix.] + + Description [Borrowed from "Hacker's Delight", by Henry Warren.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void transpose32( unsigned A[32] ) +{ + int j, k; + unsigned t, m = 0x0000FFFF; + for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) ) + { + for ( k = 0; k < 32; k = (k + j + 1) & ~j ) + { + t = (A[k] ^ (A[k+j] >> j)) & m; + A[k] = A[k] ^ t; + A[k+j] = A[k+j] ^ (t << j); + } + } +} /**Function************************************************************* - Synopsis [Updates rarity counters.] + Synopsis [Transposing 64-bit matrix.] Description [] @@ -139,39 +231,487 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p ) SeeAlso [] ***********************************************************************/ -static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) +void transpose64( word A[64] ) +{ + int j, k; + word t, m = 0x00000000FFFFFFFF; + for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) + { + for ( k = 0; k < 64; k = (k + j + 1) & ~j ) + { + t = (A[k] ^ (A[k+j] >> j)) & m; + A[k] = A[k] ^ t; + A[k+j] = A[k+j] ^ (t << j); + } + } +} + +/**Function************************************************************* + + Synopsis [Transposing 64-bit matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void transpose64Simple( word A[64], word B[64] ) +{ + int i, k; + for ( i = 0; i < 64; i++ ) + B[i] = 0; + for ( i = 0; i < 64; i++ ) + for ( k = 0; k < 64; k++ ) + if ( (A[i] >> k) & 1 ) + B[k] |= ((word)1 << (63-i)); +} + +/**Function************************************************************* + + Synopsis [Testing the transposing code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void TransposeTest() +{ + word M[64], N[64]; + int i, clk; + Aig_ManRandom64( 1 ); +// for ( i = 0; i < 64; i++ ) +// M[i] = Aig_ManRandom64( 0 ); + for ( i = 0; i < 64; i++ ) + M[i] = i? (word)0 : ~(word)0; +// for ( i = 0; i < 64; i++ ) +// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" ); + + clk = clock(); + for ( i = 0; i < 100001; i++ ) + transpose64Simple( M, N ); + Abc_PrintTime( 1, "Time", clock() - clk ); + + clk = clock(); + for ( i = 0; i < 100001; i++ ) + transpose64( M ); + Abc_PrintTime( 1, "Time", clock() - clk ); + + for ( i = 0; i < 64; i++ ) + if ( M[i] != N[i] ) + printf( "Mismatch\n" ); +/* + printf( "\n" ); + for ( i = 0; i < 64; i++ ) + Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" ); + printf( "\n" ); + for ( i = 0; i < 64; i++ ) + Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_RarTranspose( Ssw_RarMan_t * p ) { Aig_Obj_t * pObj; - unsigned * pData; - int i, k; + word M[64]; + int w, r, i; + for ( w = 0; w < p->nWords; w++ ) + for ( r = 0; r < p->nWordsReg; r++ ) + { + // save input + for ( i = 0; i < 64; i++ ) + { + if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) ) + { + pObj = Saig_ManLi( p->pAig, r*64 + 63-i ); + M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w]; + } + else + M[i] = 0; + } + // transpose + transpose64( M ); + // save output + for ( i = 0; i < 64; i++ ) + Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i]; + } /* Saig_ManForEachLi( p->pAig, pObj, i ) { - pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); - Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" ); + word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" ); } + printf( "\n" ); + for ( i = 0; i < p->nWords*64; i++ ) + { + word * pBitData = Ssw_RarPatSim( p, i ); + Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" ); + } + printf( "\n" ); */ - for ( k = 0; k < p->nWords * 32; k++ ) +} + + + + +/**Function************************************************************* + + Synopsis [Sets random inputs and specialied flop outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) +{ + Aig_Obj_t * pObj, * pObjLi; + word * pSim, * pSimLi; + int w, i; + // constant + pObj = Aig_ManConst1( p->pAig ); + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + for ( w = 0; w < p->nWords; w++ ) + pSim[w] = ~(word)0; + // primary inputs + Ssw_RarManAssingRandomPis( p ); + // flop outputs + if ( vInit ) { - for ( i = 0; i < p->nGroups; i++ ) - p->pGroupValues[i] = 0; - Saig_ManForEachLi( p->pAig, pObj, i ) + assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords ); + Saig_ManForEachLo( p->pAig, pObj, i ) { - pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); - if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) - p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + for ( w = 0; w < p->nWords; w++ ) + pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0; } - for ( i = 0; i < p->nGroups; i++ ) - Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] ); } -/* - for ( i = 0; i < p->nGroups; i++ ) + else { - for ( k = 0; k < (1 << p->nBinSize); k++ ) - printf( "%d ", Ssw_RarGetBinPat(p, i, k) ); - printf( "\n" ); + Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i ) + { + pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) ); + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + for ( w = 0; w < p->nWords; w++ ) + pSim[w] = pSimLi[w]; + } } -*/ +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) +{ + word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + word Flip = pObj->fPhase ? ~0 : 0; + int w; + for ( w = 0; w < p->nWords; w++ ) + if ( pSim[w] ^ Flip ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + word * pSim0 = Ssw_RarObjSim( p, pObj0->Id ); + word * pSim1 = Ssw_RarObjSim( p, pObj1->Id ); + word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0; + int w; + for ( w = 0; w < p->nWords; w++ ) + if ( pSim0[w] ^ pSim1[w] ^ Flip ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) +{ + static int s_SPrimes[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 * pSims; + unsigned uHash; + int i; + uHash = 0; + pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id ); + for ( i = 0; i < 2 * p->nWords; i++ ) + uHash ^= pSims[i] * s_SPrimes[i & 0x7F]; + return uHash; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) +{ + word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + word Flip = pObj->fPhase ? ~0 : 0; + int w, i; + for ( w = 0; w < p->nWords; w++ ) + if ( pSim[w] ^ Flip ) + { + for ( i = 0; i < 64; i++ ) + if ( ((pSim[w] ^ Flip) >> i) & 1 ) + break; + assert( i < 64 ); + return w * 64 + i; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Check if any of the POs becomes non-constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) +{ + Aig_Obj_t * pObj; + int i; + p->iFailPo = -1; + p->iFailPat = -1; + Saig_ManForEachPo( p->pAig, pObj, i ) + { + if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs ) + return 0; + if ( !Ssw_RarManObjIsConst(p, pObj) ) + { + p->iFailPo = i; + p->iFailPat = Ssw_RarManObjWhichOne( p, pObj ); + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs one round of simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst ) +{ + Aig_Obj_t * pObj, * pRepr; + word * pSim, * pSim0, * pSim1; + word Flip, Flip0, Flip1; + int w, i; + // initialize + Ssw_RarManInitialize( p, vInit ); + Vec_PtrClear( p->vUpdConst ); + Vec_PtrClear( p->vUpdClass ); + Aig_ManIncrementTravId( p->pAig ); + // check comb inputs + if ( fUpdate ) + Aig_ManForEachPi( p->pAig, pObj, i ) + { + pRepr = Aig_ObjRepr(p->pAig, pObj); + if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) ) + continue; + if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) ) + continue; + // save for update + if ( pRepr == Aig_ManConst1(p->pAig) ) + Vec_PtrPush( p->vUpdConst, pObj ); + else + { + Vec_PtrPush( p->vUpdClass, pRepr ); + Aig_ObjSetTravIdCurrent( p->pAig, pRepr ); + } + } + // simulate + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); + pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) ); + Flip0 = Aig_ObjFaninC0(pObj) ? ~0 : 0; + Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0; + for ( w = 0; w < p->nWords; w++ ) + pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]); + if ( !fUpdate ) + continue; + // check classes + pRepr = Aig_ObjRepr(p->pAig, pObj); + if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) ) + continue; + if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) ) + continue; + // save for update + if ( pRepr == Aig_ManConst1(p->pAig) ) + Vec_PtrPush( p->vUpdConst, pObj ); + else + { + Vec_PtrPush( p->vUpdClass, pRepr ); + Aig_ObjSetTravIdCurrent( p->pAig, pRepr ); + } + } + // transfer to POs + Aig_ManForEachPo( p->pAig, pObj, i ) + { + pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); + Flip = Aig_ObjFaninC0(pObj) ? ~0 : 0; + for ( w = 0; w < p->nWords; w++ ) + pSim[w] = Flip ^ pSim0[w]; + } + // refine classes + if ( fUpdate ) + { + if ( fFirst ) + { + Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 ); + Aig_ManForEachObj( p->pAig, pObj, i ) + if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) + Vec_PtrPush( vCands, pObj ); + assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) ); + Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 ); + Vec_PtrFree( vCands ); + } + else + { + Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 ); + Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 ); + } + } +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) +{ + Ssw_RarMan_t * p; + if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 ) + return NULL; + p = ABC_CALLOC( Ssw_RarMan_t, 1 ); + p->pAig = pAig; + p->nWords = nWords; + p->nFrames = nFrames; + p->nBinSize = nBinSize; + p->fVerbose = fVerbose; + p->nGroups = Aig_ManRegNum(pAig) / nBinSize; + p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); + p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 ); + p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) ); + p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords ); + p->pPatData = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg ); + p->vUpdConst = Vec_PtrAlloc( 100 ); + p->vUpdClass = Vec_PtrAlloc( 100 ); + p->vPatBests = Vec_IntAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Ssw_RarManStop( Ssw_RarMan_t * p ) +{ + if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); + Vec_IntFreeP( &p->vInits ); + Vec_IntFreeP( &p->vPatBests ); + Vec_PtrFreeP( &p->vUpdConst ); + Vec_PtrFreeP( &p->vUpdClass ); + ABC_FREE( p->pObjData ); + ABC_FREE( p->pPatData ); + ABC_FREE( p->pPatCosts ); + ABC_FREE( p->pRarity ); + ABC_FREE( p ); } /**Function************************************************************* @@ -187,32 +727,36 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) ***********************************************************************/ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) { - Aig_Obj_t * pObj; - unsigned * pData; +// Aig_Obj_t * pObj; + unsigned char * pData; + unsigned * pPattern; int i, k, Value; - // for each pattern - for ( k = 0; k < p->nWords * 32; k++ ) + // more data from regs to pats + Ssw_RarTranspose( p ); + + // update counters + for ( k = 0; k < p->nWords * 64; k++ ) { + pData = (unsigned char *)Ssw_RarPatSim( p, k ); for ( i = 0; i < p->nGroups; i++ ) - p->pGroupValues[i] = 0; - // compute its group values - Saig_ManForEachLi( p->pAig, pObj, i ) - { - pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); - if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) - p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); - } + Ssw_RarAddToBinPat( p, i, pData[i] ); + } + + // for each pattern + for ( k = 0; k < p->nWords * 64; k++ ) + { + pData = (unsigned char *)Ssw_RarPatSim( p, k ); // find the cost of its values p->pPatCosts[k] = 0.0; for ( i = 0; i < p->nGroups; i++ ) { - Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] ); + Value = Ssw_RarGetBinPat( p, i, pData[i] ); assert( Value > 0 ); p->pPatCosts[k] += 1.0/(Value*Value); } // print the result -// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); +//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); } // choose as many as there are words @@ -222,7 +766,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) // select the best int iPatBest = -1; double iCostBest = -ABC_INFINITY; - for ( k = 0; k < p->nWords * 32; k++ ) + for ( k = 0; k < p->nWords * 64; k++ ) if ( iCostBest < p->pPatCosts[k] ) { iCostBest = p->pPatCosts[k]; @@ -232,12 +776,11 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) assert( iPatBest >= 0 ); p->pPatCosts[iPatBest] = -ABC_INFINITY; // set the flops - Saig_ManForEachLi( p->pAig, pObj, k ) - { - pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); - Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) ); - } + pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest ); + for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ ) + Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) ); //printf( "Best pattern %5d\n", iPatBest ); + Vec_IntPush( p->vPatBests, iPatBest ); } assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); } @@ -304,11 +847,11 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex SeeAlso [] ***********************************************************************/ -int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) +int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) { int fMiter = 1; Ssw_RarMan_t * p; - int r, clk, clkTotal = clock(); + int r, f, clk, clkTotal = clock(); int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -316,33 +859,43 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", - nWords, nFrames, nBinSize, nRounds, TimeOut ); + printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", + nWords, nFrames, nRounds, nRandSeed, TimeOut ); // reset random numbers - Aig_ManRandom( 1 ); + Ssw_RarManPrepareRandom( nRandSeed ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); - Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // perform simulation rounds for ( r = 0; r < nRounds; r++ ) { clk = clock(); // simulate - Ssw_SmlSimulateOne( p->pSml ); - if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) + for ( f = 0; f < nFrames; f++ ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - RetValue = 0; - break; + Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); + if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) + { + if ( fVerbose ) printf( "\n" ); +// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + Ssw_RarManPrepareRandom( nRandSeed ); + ABC_FREE( pAig->pSeqModel ); + pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); + RetValue = 0; + goto finish; + } + // check timeout + if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + { + if ( fVerbose ) printf( "\n" ); + printf( "Reached timeout (%d seconds).\n", TimeOut ); + goto finish; + } } // get initialization patterns - Ssw_RarUpdateCounters( p ); Ssw_RarTransferPatterns( p, p->vInits ); - Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // printout if ( fVerbose ) { @@ -350,15 +903,9 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i // Abc_PrintTime( 1, "Time", clock() - clk ); printf( "." ); } - // check timeout - if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) - { - if ( fVerbose ) printf( "\n" ); - printf( "Reached timeout (%d seconds).\n", TimeOut ); - break; - } } - if ( r == nRounds ) +finish: + if ( r == nRounds && f == nFrames ) { if ( fVerbose ) printf( "\n" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); @@ -370,6 +917,30 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i } +/**Function************************************************************* + + Synopsis [Perform sequential simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) +{ + Aig_Man_t * pAig; + int RetValue; + pAig = Gia_ManToAigSimple( p ); + RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); + // save counter-example + Abc_CexFree( p->pCexSeq ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + return RetValue; +} + /**Function************************************************************* Synopsis [Filter equivalence classes of nodes.] @@ -381,11 +952,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { - int fMiter = 0; Ssw_RarMan_t * p; - int r, i, k, clkTotal = clock(); + int r, f, i, k, clkTotal = clock(); int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -393,10 +963,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", - nWords, nFrames, nBinSize, nRounds, TimeOut ); + printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", + nWords, nFrames, nRounds, nRandSeed, TimeOut ); // reset random numbers - Aig_ManRandom( 1 ); + Ssw_RarManPrepareRandom( nRandSeed ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); @@ -411,15 +981,13 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz for ( k = 0; k < Aig_ManRegNum(pAig); k++ ) Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) ); assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords ); - // initialize simulation manager - Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // create trivial equivalence classes with all nodes being candidates for constant 1 if ( pAig->pReprs == NULL ) p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 ); else p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual ); // print the stats if ( fVerbose ) { @@ -436,43 +1004,53 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz break; } // simulate - Ssw_SmlSimulateOne( p->pSml ); - if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) + for ( f = 0; f < nFrames; f++ ) { - if ( fVerbose ) printf( "\n" ); - printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - RetValue = 0; - break; + Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f ); + if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) + { + if ( !fVerbose ) + printf( "\r" ); +// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + Ssw_RarManPrepareRandom( nRandSeed ); + Abc_CexFree( pAig->pSeqModel ); + pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); + RetValue = 0; + goto finish; + } + // check timeout + if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + { + if ( fVerbose ) printf( "\n" ); + printf( "Reached timeout (%d seconds).\n", TimeOut ); + goto finish; + } } - // check equivalence classes - Ssw_ClassesRefineConst1( p->ppClasses, 1 ); - Ssw_ClassesRefine( p->ppClasses, 1 ); + // get initialization patterns + Ssw_RarTransferPatterns( p, p->vInits ); // printout if ( fVerbose ) { printf( "Round %3d: ", r ); Ssw_ClassesPrint( p->ppClasses, 0 ); } - // get initialization patterns - Ssw_RarUpdateCounters( p ); - Ssw_RarTransferPatterns( p, p->vInits ); - Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); - // check timeout - if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + else { - if ( fVerbose ) printf( "\n" ); - printf( "Reached timeout (%d seconds).\n", TimeOut ); - break; + printf( "." ); } } - if ( r == nRounds ) +finish: + // report + if ( r == nRounds && f == nFrames ) { + if ( !fVerbose ) + printf( "\r" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup Ssw_RarManStop( p ); - return -1; + return RetValue; } /**Function************************************************************* @@ -486,7 +1064,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { Aig_Man_t * pAig; int RetValue; @@ -497,15 +1075,16 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz ABC_FREE( p->pReprs ); ABC_FREE( p->pNexts ); } - RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); + RetValue = Ssw_RarSignalFilter( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose ); Gia_ManReprFromAigRepr( pAig, p ); + // save counter-example + Abc_CexFree( p->pCexSeq ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); return RetValue; } - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c index 59f59f93..3026cf6b 100644 --- a/src/aig/ssw/sswRarity2.c +++ b/src/aig/ssw/sswRarity2.c @@ -37,26 +37,18 @@ struct Ssw_RarMan_t_ int nBinSize; // the number of flops in one group int fVerbose; // the verbosiness flag int nGroups; // the number of flop groups - int nWordsReg; // the number of words in the registers // internal data Aig_Man_t * pAig; // AIG with equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes + Ssw_Sml_t * pSml; // simulation manager + Vec_Ptr_t * vSimInfo; // simulation info from pSml manager Vec_Int_t * vInits; // initial state - // simulation data - word * pObjData; // simulation info for each obj - word * pPatData; // pattern data for each reg - // candidates to update - Vec_Ptr_t * vUpdConst; // constant 1 candidates - Vec_Ptr_t * vUpdClass; // class representatives // rarity data int * pRarity; // occur counts for patterns in groups + int * pGroupValues; // occur counts in each group double * pPatCosts; // pattern costs - // best patterns - Vec_Int_t * vPatBests; // best patterns - int iFailPo; // failed primary output - int iFailPat; // failed pattern -}; +}; static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { @@ -77,63 +69,13 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) p->pRarity[iBin * (1 << p->nBinSize) + iPat]++; } -static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); } - -static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id; } -static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; } - - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Prepares random number generator.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_RarManPrepareRandom( int nRandSeed ) -{ - int i; - Aig_ManRandom( 1 ); - for ( i = 0; i < nRandSeed; i++ ) - Aig_ManRandom( 0 ); -} - -/**Function************************************************************* - - Synopsis [Initializes random primary inputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p ) -{ - word * pSim; - Aig_Obj_t * pObj; - int w, i; - Saig_ManForEachPi( p->pAig, pObj, i ) - { - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) - pSim[w] = Aig_ManRandom64(0); - pSim[0] <<= 1; - } -} - -/**Function************************************************************* - - Synopsis [Derives the counter-example.] + Synopsis [] Description [] @@ -142,113 +84,29 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p ) SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal ) +static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) { - Abc_Cex_t * pCex; - Aig_Obj_t * pObj; - Vec_Int_t * vTrace; - word * pSim; - int i, r, f, iBit, iPatThis; - // compute the pattern sequence - iPatThis = iPatFinal; - vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 ); - Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis ); - for ( r = iFrame / p->nFrames - 1; r >= 0; r-- ) - { - iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 ); - Vec_IntWriteEntry( vTrace, r, iPatThis ); - } - // create counter-example - pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 ); - pCex->iFrame = iFrame; - pCex->iPo = iPo; - // insert the bits - iBit = Aig_ManRegNum(p->pAig); - for ( f = 0; f <= iFrame; f++ ) - { - Ssw_RarManAssingRandomPis( p ); - iPatThis = Vec_IntEntry( vTrace, f / p->nFrames ); - Saig_ManForEachPi( p->pAig, pObj, i ) - { - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - if ( Aig_InfoHasBit( (unsigned *)pSim, iPatThis ) ) - Aig_InfoSetBit( pCex->pData, iBit ); - iBit++; - } - } - Vec_IntFree( vTrace ); - assert( iBit == pCex->nBits ); - // verify the counter example - if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) - { - printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" ); - Abc_CexFree( pCex ); - pCex = NULL; - } - else - { -// printf( "Counter-example verification is successful.\n" ); - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); - } - return pCex; + Ssw_RarMan_t * p; + if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 ) + return NULL; + p = ABC_CALLOC( Ssw_RarMan_t, 1 ); + p->pAig = pAig; + p->nWords = nWords; + p->nFrames = nFrames; + p->nBinSize = nBinSize; + p->fVerbose = fVerbose; + p->nGroups = Aig_ManRegNum(pAig) / nBinSize; + p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); + p->pGroupValues = ABC_CALLOC( int, p->nGroups ); + p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 ); + p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords ); + p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml ); + return p; } - -/**Function************************************************************* - - Synopsis [Transposing 32-bit matrix.] - - Description [Borrowed from "Hacker's Delight", by Henry Warren.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void transpose32( unsigned A[32] ) -{ - int j, k; - unsigned t, m = 0x0000FFFF; - for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) ) - { - for ( k = 0; k < 32; k = (k + j + 1) & ~j ) - { - t = (A[k] ^ (A[k+j] >> j)) & m; - A[k] = A[k] ^ t; - A[k+j] = A[k+j] ^ (t << j); - } - } -} - /**Function************************************************************* - Synopsis [Transposing 64-bit matrix.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void transpose64( word A[64] ) -{ - int j, k; - word t, m = 0x00000000FFFFFFFF; - for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) - { - for ( k = 0; k < 64; k = (k + j + 1) & ~j ) - { - t = (A[k] ^ (A[k+j] >> j)) & m; - A[k] = A[k] ^ t; - A[k+j] = A[k+j] ^ (t << j); - } - } -} - -/**Function************************************************************* - - Synopsis [Transposing 64-bit matrix.] + Synopsis [] Description [] @@ -257,66 +115,22 @@ void transpose64( word A[64] ) SeeAlso [] ***********************************************************************/ -void transpose64Simple( word A[64], word B[64] ) +static void Ssw_RarManStop( Ssw_RarMan_t * p ) { - int i, k; - for ( i = 0; i < 64; i++ ) - B[i] = 0; - for ( i = 0; i < 64; i++ ) - for ( k = 0; k < 64; k++ ) - if ( (A[i] >> k) & 1 ) - B[k] |= ((word)1 << (63-i)); + if ( p->pSml ) Ssw_SmlStop( p->pSml ); + if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); + Vec_PtrFreeP( &p->vSimInfo ); + Vec_IntFreeP( &p->vInits ); + ABC_FREE( p->pGroupValues ); + ABC_FREE( p->pPatCosts ); + ABC_FREE( p->pRarity ); + ABC_FREE( p ); } -/**Function************************************************************* - - Synopsis [Testing the transposing code.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void TransposeTest() -{ - word M[64], N[64]; - int i, clk; - Aig_ManRandom64( 1 ); -// for ( i = 0; i < 64; i++ ) -// M[i] = Aig_ManRandom64( 0 ); - for ( i = 0; i < 64; i++ ) - M[i] = i? (word)0 : ~(word)0; -// for ( i = 0; i < 64; i++ ) -// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" ); - - clk = clock(); - for ( i = 0; i < 100001; i++ ) - transpose64Simple( M, N ); - Abc_PrintTime( 1, "Time", clock() - clk ); - - clk = clock(); - for ( i = 0; i < 100001; i++ ) - transpose64( M ); - Abc_PrintTime( 1, "Time", clock() - clk ); - - for ( i = 0; i < 64; i++ ) - if ( M[i] != N[i] ) - printf( "Mismatch\n" ); -/* - printf( "\n" ); - for ( i = 0; i < 64; i++ ) - Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" ); - printf( "\n" ); - for ( i = 0; i < 64; i++ ) - Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" ); -*/ -} /**Function************************************************************* - Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].] + Synopsis [Updates rarity counters.] Description [] @@ -325,393 +139,39 @@ void TransposeTest() SeeAlso [] ***********************************************************************/ -void Ssw_RarTranspose( Ssw_RarMan_t * p ) +static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) { Aig_Obj_t * pObj; - word M[64]; - int w, r, i; - for ( w = 0; w < p->nWords; w++ ) - for ( r = 0; r < p->nWordsReg; r++ ) - { - // save input - for ( i = 0; i < 64; i++ ) - { - if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) ) - { - pObj = Saig_ManLi( p->pAig, r*64 + 63-i ); - M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w]; - } - else - M[i] = 0; - } - // transpose - transpose64( M ); - // save output - for ( i = 0; i < 64; i++ ) - Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i]; - } + unsigned * pData; + int i, k; /* Saig_ManForEachLi( p->pAig, pObj, i ) { - word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" ); + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" ); } - printf( "\n" ); - for ( i = 0; i < p->nWords*64; i++ ) - { - word * pBitData = Ssw_RarPatSim( p, i ); - Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" ); - } - printf( "\n" ); */ -} - - - - -/**Function************************************************************* - - Synopsis [Sets random inputs and specialied flop outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) -{ - Aig_Obj_t * pObj, * pObjLi; - word * pSim, * pSimLi; - int w, i; - // constant - pObj = Aig_ManConst1( p->pAig ); - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) - pSim[w] = ~(word)0; - // primary inputs - Ssw_RarManAssingRandomPis( p ); - // flop outputs - if ( vInit ) - { - assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords ); - Saig_ManForEachLo( p->pAig, pObj, i ) - { - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) - pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0; - } - } - else - { - Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i ) - { - pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) ); - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) - pSim[w] = pSimLi[w]; - } - } -} - -/**Function************************************************************* - - Synopsis [Returns 1 if simulation info is composed of all zeros.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) -{ - word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - word Flip = pObj->fPhase ? ~0 : 0; - int w; - for ( w = 0; w < p->nWords; w++ ) - if ( pSim[w] ^ Flip ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if simulation infos are equal.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) -{ - word * pSim0 = Ssw_RarObjSim( p, pObj0->Id ); - word * pSim1 = Ssw_RarObjSim( p, pObj1->Id ); - word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0; - int w; - for ( w = 0; w < p->nWords; w++ ) - if ( pSim0[w] ^ pSim1[w] ^ Flip ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Computes hash value of the node using its simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) -{ - static int s_SPrimes[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 * pSims; - unsigned uHash; - int i; - uHash = 0; - pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id ); - for ( i = 0; i < 2 * p->nWords; i++ ) - uHash ^= pSims[i] * s_SPrimes[i & 0x7F]; - return uHash; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if simulation info is composed of all zeros.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) -{ - word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - word Flip = pObj->fPhase ? ~0 : 0; - int w, i; - for ( w = 0; w < p->nWords; w++ ) - if ( pSim[w] ^ Flip ) - { - for ( i = 0; i < 64; i++ ) - if ( ((pSim[w] ^ Flip) >> i) & 1 ) - break; - assert( i < 64 ); - return w * 64 + i; - } - return -1; -} - -/**Function************************************************************* - - Synopsis [Check if any of the POs becomes non-constant.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) -{ - Aig_Obj_t * pObj; - int i; - p->iFailPo = -1; - p->iFailPat = -1; - Saig_ManForEachPo( p->pAig, pObj, i ) + for ( k = 0; k < p->nWords * 32; k++ ) { - if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs ) - return 0; - if ( !Ssw_RarManObjIsConst(p, pObj) ) - { - p->iFailPo = i; - p->iFailPat = Ssw_RarManObjWhichOne( p, pObj ); - return 1; - } - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Performs one round of simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst ) -{ - Aig_Obj_t * pObj, * pRepr; - word * pSim, * pSim0, * pSim1; - word Flip, Flip0, Flip1; - int w, i; - // initialize - Ssw_RarManInitialize( p, vInit ); - Vec_PtrClear( p->vUpdConst ); - Vec_PtrClear( p->vUpdClass ); - Aig_ManIncrementTravId( p->pAig ); - // check comb inputs - if ( fUpdate ) - Aig_ManForEachPi( p->pAig, pObj, i ) - { - pRepr = Aig_ObjRepr(p->pAig, pObj); - if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) ) - continue; - if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) ) - continue; - // save for update - if ( pRepr == Aig_ManConst1(p->pAig) ) - Vec_PtrPush( p->vUpdConst, pObj ); - else - { - Vec_PtrPush( p->vUpdClass, pRepr ); - Aig_ObjSetTravIdCurrent( p->pAig, pRepr ); - } - } - // simulate - Aig_ManForEachNode( p->pAig, pObj, i ) - { - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); - pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) ); - Flip0 = Aig_ObjFaninC0(pObj) ? ~0 : 0; - Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0; - for ( w = 0; w < p->nWords; w++ ) - pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]); - if ( !fUpdate ) - continue; - // check classes - pRepr = Aig_ObjRepr(p->pAig, pObj); - if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) ) - continue; - if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) ) - continue; - // save for update - if ( pRepr == Aig_ManConst1(p->pAig) ) - Vec_PtrPush( p->vUpdConst, pObj ); - else + for ( i = 0; i < p->nGroups; i++ ) + p->pGroupValues[i] = 0; + Saig_ManForEachLi( p->pAig, pObj, i ) { - Vec_PtrPush( p->vUpdClass, pRepr ); - Aig_ObjSetTravIdCurrent( p->pAig, pRepr ); + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) + p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); } + for ( i = 0; i < p->nGroups; i++ ) + Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] ); } - // transfer to POs - Aig_ManForEachPo( p->pAig, pObj, i ) +/* + for ( i = 0; i < p->nGroups; i++ ) { - pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); - Flip = Aig_ObjFaninC0(pObj) ? ~0 : 0; - for ( w = 0; w < p->nWords; w++ ) - pSim[w] = Flip ^ pSim0[w]; + for ( k = 0; k < (1 << p->nBinSize); k++ ) + printf( "%d ", Ssw_RarGetBinPat(p, i, k) ); + printf( "\n" ); } - // refine classes - if ( fUpdate ) - { - if ( fFirst ) - { - Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 ); - Aig_ManForEachObj( p->pAig, pObj, i ) - if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) - Vec_PtrPush( vCands, pObj ); - assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) ); - Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 ); - Vec_PtrFree( vCands ); - } - else - { - Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 ); - Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 ); - } - } -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) -{ - Ssw_RarMan_t * p; - if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 ) - return NULL; - p = ABC_CALLOC( Ssw_RarMan_t, 1 ); - p->pAig = pAig; - p->nWords = nWords; - p->nFrames = nFrames; - p->nBinSize = nBinSize; - p->fVerbose = fVerbose; - p->nGroups = Aig_ManRegNum(pAig) / nBinSize; - p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); - p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 ); - p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) ); - p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords ); - p->pPatData = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg ); - p->vUpdConst = Vec_PtrAlloc( 100 ); - p->vUpdClass = Vec_PtrAlloc( 100 ); - p->vPatBests = Vec_IntAlloc( 100 ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ssw_RarManStop( Ssw_RarMan_t * p ) -{ - if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); - Vec_IntFreeP( &p->vInits ); - Vec_IntFreeP( &p->vPatBests ); - Vec_PtrFreeP( &p->vUpdConst ); - Vec_PtrFreeP( &p->vUpdClass ); - ABC_FREE( p->pObjData ); - ABC_FREE( p->pPatData ); - ABC_FREE( p->pPatCosts ); - ABC_FREE( p->pRarity ); - ABC_FREE( p ); +*/ } /**Function************************************************************* @@ -727,36 +187,32 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p ) ***********************************************************************/ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) { -// Aig_Obj_t * pObj; - unsigned char * pData; - unsigned * pPattern; + Aig_Obj_t * pObj; + unsigned * pData; int i, k, Value; - // more data from regs to pats - Ssw_RarTranspose( p ); - - // update counters - for ( k = 0; k < p->nWords * 64; k++ ) - { - pData = (unsigned char *)Ssw_RarPatSim( p, k ); - for ( i = 0; i < p->nGroups; i++ ) - Ssw_RarAddToBinPat( p, i, pData[i] ); - } - // for each pattern - for ( k = 0; k < p->nWords * 64; k++ ) + for ( k = 0; k < p->nWords * 32; k++ ) { - pData = (unsigned char *)Ssw_RarPatSim( p, k ); + for ( i = 0; i < p->nGroups; i++ ) + p->pGroupValues[i] = 0; + // compute its group values + Saig_ManForEachLi( p->pAig, pObj, i ) + { + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) + p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); + } // find the cost of its values p->pPatCosts[k] = 0.0; for ( i = 0; i < p->nGroups; i++ ) { - Value = Ssw_RarGetBinPat( p, i, pData[i] ); + Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] ); assert( Value > 0 ); p->pPatCosts[k] += 1.0/(Value*Value); } // print the result -//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); +// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); } // choose as many as there are words @@ -766,7 +222,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) // select the best int iPatBest = -1; double iCostBest = -ABC_INFINITY; - for ( k = 0; k < p->nWords * 64; k++ ) + for ( k = 0; k < p->nWords * 32; k++ ) if ( iCostBest < p->pPatCosts[k] ) { iCostBest = p->pPatCosts[k]; @@ -776,11 +232,12 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) assert( iPatBest >= 0 ); p->pPatCosts[iPatBest] = -ABC_INFINITY; // set the flops - pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest ); - for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ ) - Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) ); + Saig_ManForEachLi( p->pAig, pObj, k ) + { + pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); + Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) ); + } //printf( "Best pattern %5d\n", iPatBest ); - Vec_IntPush( p->vPatBests, iPatBest ); } assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); } @@ -847,11 +304,11 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex SeeAlso [] ***********************************************************************/ -int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) +int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) { int fMiter = 1; Ssw_RarMan_t * p; - int r, f, clk, clkTotal = clock(); + int r, clk, clkTotal = clock(); int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -859,43 +316,33 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", - nWords, nFrames, nRounds, nRandSeed, TimeOut ); + printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", + nWords, nFrames, nBinSize, nRounds, TimeOut ); // reset random numbers - Ssw_RarManPrepareRandom( nRandSeed ); + Aig_ManRandom( 1 ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); + Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // perform simulation rounds for ( r = 0; r < nRounds; r++ ) { clk = clock(); // simulate - for ( f = 0; f < nFrames; f++ ) + Ssw_SmlSimulateOne( p->pSml ); + if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) { - Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); - if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) - { - if ( fVerbose ) printf( "\n" ); -// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - Ssw_RarManPrepareRandom( nRandSeed ); - ABC_FREE( pAig->pSeqModel ); - pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); - RetValue = 0; - goto finish; - } - // check timeout - if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) - { - if ( fVerbose ) printf( "\n" ); - printf( "Reached timeout (%d seconds).\n", TimeOut ); - goto finish; - } + if ( fVerbose ) printf( "\n" ); + printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + RetValue = 0; + break; } // get initialization patterns + Ssw_RarUpdateCounters( p ); Ssw_RarTransferPatterns( p, p->vInits ); + Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // printout if ( fVerbose ) { @@ -903,9 +350,15 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i // Abc_PrintTime( 1, "Time", clock() - clk ); printf( "." ); } + // check timeout + if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + { + if ( fVerbose ) printf( "\n" ); + printf( "Reached timeout (%d seconds).\n", TimeOut ); + break; + } } -finish: - if ( r == nRounds && f == nFrames ) + if ( r == nRounds ) { if ( fVerbose ) printf( "\n" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); @@ -917,30 +370,6 @@ finish: } -/**Function************************************************************* - - Synopsis [Perform sequential simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) -{ - Aig_Man_t * pAig; - int RetValue; - pAig = Gia_ManToAigSimple( p ); - RetValue = Ssw_RarSimulate2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); - // save counter-example - Abc_CexFree( p->pCexSeq ); - p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; - Aig_ManStop( pAig ); - return RetValue; -} - /**Function************************************************************* Synopsis [Filter equivalence classes of nodes.] @@ -952,10 +381,11 @@ int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, i SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { + int fMiter = 0; Ssw_RarMan_t * p; - int r, f, i, k, clkTotal = clock(); + int r, i, k, clkTotal = clock(); int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -963,10 +393,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz if ( Aig_ManNodeNum(pAig) == 0 ) return -1; if ( fVerbose ) - printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", - nWords, nFrames, nRounds, nRandSeed, TimeOut ); + printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", + nWords, nFrames, nBinSize, nRounds, TimeOut ); // reset random numbers - Ssw_RarManPrepareRandom( nRandSeed ); + Aig_ManRandom( 1 ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); @@ -981,13 +411,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz for ( k = 0; k < Aig_ManRegNum(pAig); k++ ) Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) ); assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords ); + // initialize simulation manager + Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // create trivial equivalence classes with all nodes being candidates for constant 1 if ( pAig->pReprs == NULL ) p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 ); else p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig ); - Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); // print the stats if ( fVerbose ) { @@ -1004,53 +436,43 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz break; } // simulate - for ( f = 0; f < nFrames; f++ ) + Ssw_SmlSimulateOne( p->pSml ); + if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) { - Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f ); - if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) - { - if ( !fVerbose ) - printf( "\r" ); -// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - Ssw_RarManPrepareRandom( nRandSeed ); - Abc_CexFree( pAig->pSeqModel ); - pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); - RetValue = 0; - goto finish; - } - // check timeout - if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) - { - if ( fVerbose ) printf( "\n" ); - printf( "Reached timeout (%d seconds).\n", TimeOut ); - goto finish; - } + if ( fVerbose ) printf( "\n" ); + printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + RetValue = 0; + break; } - // get initialization patterns - Ssw_RarTransferPatterns( p, p->vInits ); + // check equivalence classes + Ssw_ClassesRefineConst1( p->ppClasses, 1 ); + Ssw_ClassesRefine( p->ppClasses, 1 ); // printout if ( fVerbose ) { printf( "Round %3d: ", r ); Ssw_ClassesPrint( p->ppClasses, 0 ); } - else + // get initialization patterns + Ssw_RarUpdateCounters( p ); + Ssw_RarTransferPatterns( p, p->vInits ); + Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); + // check timeout + if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) { - printf( "." ); + if ( fVerbose ) printf( "\n" ); + printf( "Reached timeout (%d seconds).\n", TimeOut ); + break; } } -finish: - // report - if ( r == nRounds && f == nFrames ) + if ( r == nRounds ) { - if ( !fVerbose ) - printf( "\r" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } // cleanup Ssw_RarManStop( p ); - return RetValue; + return -1; } /**Function************************************************************* @@ -1064,7 +486,7 @@ finish: SeeAlso [] ***********************************************************************/ -int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) +int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { Aig_Man_t * pAig; int RetValue; @@ -1075,16 +497,15 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz ABC_FREE( p->pReprs ); ABC_FREE( p->pNexts ); } - RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose ); + RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); Gia_ManReprFromAigRepr( pAig, p ); - // save counter-example - Abc_CexFree( p->pCexSeq ); - p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); return RetValue; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e319c4f8..ee0c98ff 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -24776,7 +24776,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nRandSeed; int TimeOut; int fVerbose; - extern int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); + extern int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); // set defaults nFrames = 20; nWords = 50; @@ -24871,7 +24871,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" ); return 1; } - pAbc->Status = Ssw_RarSimulate2Gia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); + pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; @@ -25310,7 +25310,7 @@ usage: int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) { // extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); - extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); + extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); int c; int nFrames = 20; int nWords = 50; @@ -25435,7 +25435,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) } } // if ( fNewAlgo ) - pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); + pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); // else // pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 4232ab1f..695ae4ef 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3027,53 +3027,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc); } pMan = Abc_NtkToDar( pNtk, 0, 1 ); - if ( Ssw_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 ) - { - if ( pMan->pSeqModel ) - { - printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", - nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame ); - status = Saig_ManVerifyCex( pMan, pMan->pSeqModel ); - if ( status == 0 ) - printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); - } - ABC_FREE( pNtk->pModel ); - ABC_FREE( pNtk->pSeqModel ); - pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - RetValue = 0; - } - else - { - printf( "Simulation of %d frames with %d words did not assert the outputs. ", - nFrames, nWords ); - } - ABC_PRT( "Time", clock() - clk ); - Aig_ManStop( pMan ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Performs random simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) -{ - Aig_Man_t * pMan; - int status, RetValue = -1, clk = clock(); - if ( Abc_NtkGetChoiceNum(pNtk) ) - { - printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) ); - Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc); - } - pMan = Abc_NtkToDar( pNtk, 0, 1 ); - if ( Ssw_RarSignalFilter( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ) == 0 ) + if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 ) { if ( pMan->pSeqModel ) { -- cgit v1.2.3