diff options
Diffstat (limited to 'src/aig/ssw/sswRarity2.c')
-rw-r--r-- | src/aig/ssw/sswRarity2.c | 835 |
1 files changed, 128 insertions, 707 deletions
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 ); @@ -919,30 +372,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.] Description [] @@ -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 /// //////////////////////////////////////////////////////////////////////// |