/**CFile**************************************************************** FileName [sswRarity.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Inductive prover with constraints.] Synopsis [Rarity-driven refinement of equivalence classes.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - September 1, 2008.] Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] ***********************************************************************/ #include "sswInt.h" #include "giaAig.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Ssw_RarMan_t_ Ssw_RarMan_t; struct Ssw_RarMan_t_ { // parameters int nWords; // the number of words to simulate int nFrames; // the number of frames to simulate 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 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 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 ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); return p->pRarity[iBin * (1 << p->nBinSize) + iPat]; } static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value; } static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); 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; // pSim[0] = (pSim[0] << 2) | 2; pSim[0] = (pSim[0] << 4) | ((i & 1) ? 0xA : 0xC); } } /**Function************************************************************* Synopsis [Derives the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal, 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" ); if ( fVerbose ) 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 [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.] 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; 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 ) { 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" ); */ } /**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( void * pMan, Aig_Obj_t * pObj ) { Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; 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( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; 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( void * pMan, Aig_Obj_t * pObj ) { Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; 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************************************************************* Synopsis [Select best patterns.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) { // Aig_Obj_t * pObj; unsigned char * pData; unsigned * pPattern; 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++ ) { 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, pData[i] ); assert( Value > 0 ); p->pPatCosts[k] += 1.0/(Value*Value); } // print the result //printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); } // choose as many as there are words Vec_IntClear( vInits ); for ( i = 0; i < p->nWords; i++ ) { // select the best int iPatBest = -1; double iCostBest = -ABC_INFINITY; for ( k = 0; k < p->nWords * 64; k++ ) if ( iCostBest < p->pPatCosts[k] ) { iCostBest = p->pPatCosts[k]; iPatBest = k; } // remove from costs 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) ); //printf( "Best pattern %5d\n", iPatBest ); Vec_IntPush( p->vPatBests, iPatBest ); } assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); } /**Function************************************************************* Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) { Vec_Int_t * vInit; Aig_Obj_t * pObj, * pObjLi; int f, i, iBit; // assign register outputs Saig_ManForEachLi( pAig, pObj, i ) pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i ); // simulate the timeframes iBit = pCex->nRegs; for ( f = 0; f <= pCex->iFrame; f++ ) { // set the PI simulation information Aig_ManConst1(pAig)->fMarkB = 1; Saig_ManForEachPi( pAig, pObj, i ) pObj->fMarkB = Aig_InfoHasBit( pCex->pData, iBit++ ); Saig_ManForEachLiLo( pAig, pObjLi, pObj, i ) pObj->fMarkB = pObjLi->fMarkB; // simulate internal nodes Aig_ManForEachNode( pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs Aig_ManForEachPo( pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); } assert( iBit == pCex->nBits ); // check that the output failed as expected -- cannot check because it is not an SRM! // pObj = Aig_ManPo( pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) // printf( "The counter-example does not refine the output.\n" ); // record the new pattern vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) ); Saig_ManForEachLo( pAig, pObj, i ) { //printf( "%d", pObj->fMarkB ); Vec_IntPush( vInit, pObj->fMarkB ); } //printf( "\n" ); Aig_ManCleanMarkB( pAig ); return vInit; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose ) { Aig_Obj_t * pObj; int i; Saig_ManForEachPo( pAig, pObj, i ) { if ( pAig->nConstrs && i >= Saig_ManPoNum(pAig) - pAig->nConstrs ) return 0; if ( pObj->fPhase ) { ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 ); pAig->pSeqModel->iPo = i; if ( fVerbose ) printf( "Output %d is trivally SAT in frame 0. \n", i ); return 1; } } return 0; } /**Function************************************************************* Synopsis [Perform sequential simulation.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ) { int fTryBmc = 0; int fMiter = 1; Ssw_RarMan_t * p; int r, f, clk, clkTotal = clock(); int nTimeToStop = time(NULL) + TimeOut; int RetValue = -1; int iFrameFail = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); // consider the case of empty AIG if ( Aig_ManNodeNum(pAig) == 0 ) return -1; // check trivially SAT miters if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) return 0; if ( fVerbose ) 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 Ssw_RarManPrepareRandom( nRandSeed ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); // perform simulation rounds for ( r = 0; r < nRounds; r++ ) { clk = clock(); if ( fTryBmc ) { Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits ); Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail ); // if ( pNewAig->pSeqModel != NULL ) // printf( "BMC has found a counter-example in frame %d.\n", iFrameFail ); Aig_ManStop( pNewAig ); } // simulate for ( f = 0; f < nFrames; f++ ) { 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, fVerbose ); RetValue = 0; goto finish; } // check timeout if ( TimeOut && time(NULL) > nTimeToStop ) { if ( fVerbose ) printf( "\n" ); printf( "Reached timeout (%d seconds).\n", TimeOut ); goto finish; } } // get initialization patterns Ssw_RarTransferPatterns( p, p->vInits ); // printout if ( fVerbose ) { // printf( "Round %3d: ", r ); // Abc_PrintTime( 1, "Time", clock() - clk ); printf( "." ); } } finish: if ( r == nRounds && f == nFrames ) { if ( fVerbose ) printf( "\n" ); 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; } /**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.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ 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 ) { Ssw_RarMan_t * p; int r, f, i, k, clkTotal = clock(); int nTimeToStop = time(NULL) + TimeOut; int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); // consider the case of empty AIG if ( Aig_ManNodeNum(pAig) == 0 ) return -1; // check trivially SAT miters if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) ) return 0; 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 ); // reset random numbers Ssw_RarManPrepareRandom( nRandSeed ); // create manager p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); // compute starting state if needed assert( p->vInits == NULL ); if ( pCex ) { p->vInits = Ssw_RarFindStartingState( pAig, pCex ); printf( "Beginning simulation from the state derived using the counter-example.\n" ); } else p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) ); // duplicate the array for ( i = 1; i < nWords; i++ ) 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 ); // 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 ); // print the stats if ( fVerbose ) { printf( "Initial : " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } // refine classes using BMC for ( r = 0; r < nRounds; r++ ) { // start filtering equivalence classes if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 ) { printf( "All equivalences are refined away.\n" ); break; } // simulate for ( f = 0; f < nFrames; f++ ) { 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, 1 ); RetValue = 0; goto finish; } // check timeout if ( TimeOut && time(NULL) > nTimeToStop ) { if ( fVerbose ) printf( "\n" ); printf( "Reached timeout (%d seconds).\n", TimeOut ); goto finish; } } // get initialization patterns Ssw_RarTransferPatterns( p, p->vInits ); // printout if ( fVerbose ) { printf( "Round %3d: ", r ); Ssw_ClassesPrint( p->ppClasses, 0 ); } else { printf( "." ); } } 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 RetValue; } /**Function************************************************************* Synopsis [Filter equivalence classes of nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ 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; pAig = Gia_ManToAigSimple( p ); if ( p->pReprs != NULL ) { Gia_ManReprToAigRepr2( pAig, p ); ABC_FREE( p->pReprs ); ABC_FREE( p->pNexts ); } 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 /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END