| /**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 "aig/gia/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 |
| // 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 |
| // rarity data |
| int * pRarity; // occur counts for patterns in groups |
| int * pGroupValues; // occur counts in each group |
| double * pPatCosts; // pattern costs |
| |
| }; |
| |
| 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]++; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**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->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 [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static void Ssw_RarManStop( 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 ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Updates rarity counters.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| unsigned * pData; |
| int i, k; |
| /* |
| 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 ); Abc_Print( 1, "\n" ); |
| } |
| */ |
| for ( k = 0; k < p->nWords * 32; k++ ) |
| { |
| for ( i = 0; i < p->nGroups; i++ ) |
| p->pGroupValues[i] = 0; |
| Saig_ManForEachLi( p->pAig, pObj, i ) |
| { |
| pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); |
| if ( Abc_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] ); |
| } |
| /* |
| for ( i = 0; i < p->nGroups; i++ ) |
| { |
| for ( k = 0; k < (1 << p->nBinSize); k++ ) |
| Abc_Print( 1, "%d ", Ssw_RarGetBinPat(p, i, k) ); |
| Abc_Print( 1, "\n" ); |
| } |
| */ |
| } |
| |
| /**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 * pData; |
| int i, k, Value; |
| |
| // for each pattern |
| for ( k = 0; k < p->nWords * 32; 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 ( Abc_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, p->pGroupValues[i] ); |
| assert( Value > 0 ); |
| p->pPatCosts[k] += 1.0/(Value*Value); |
| } |
| // print the result |
| // Abc_Print( 1, "%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 * 32; 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 |
| Saig_ManForEachLi( p->pAig, pObj, k ) |
| { |
| pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); |
| Vec_IntPush( vInits, Abc_InfoHasBit(pData, iPatBest) ); |
| } |
| //Abc_Print( 1, "Best pattern %5d\n", 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 = Abc_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 = Abc_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_ManForEachCo( 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_ManCo( pAig, pCex->iPo ); |
| // if ( pObj->fMarkB != 1 ) |
| // Abc_Print( 1, "The counter-example does not refine the output.\n" ); |
| // record the new pattern |
| vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) ); |
| Saig_ManForEachLo( pAig, pObj, i ) |
| Vec_IntPush( vInit, pObj->fMarkB ); |
| return vInit; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Perform sequential simulation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| 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; |
| abctime clk, clkTotal = Abc_Clock(); |
| abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; |
| 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; |
| if ( fVerbose ) |
| Abc_Print( 1, "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", |
| nWords, nFrames, nBinSize, nRounds, TimeOut ); |
| // reset random numbers |
| 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 = Abc_Clock(); |
| // simulate |
| Ssw_SmlSimulateOne( p->pSml ); |
| if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) |
| { |
| if ( fVerbose ) Abc_Print( 1, "\n" ); |
| Abc_Print( 1, "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 ) |
| { |
| // Abc_Print( 1, "Round %3d: ", r ); |
| // Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| Abc_Print( 1, "." ); |
| } |
| // check timeout |
| if ( TimeOut && Abc_Clock() > nTimeToStop ) |
| { |
| if ( fVerbose ) Abc_Print( 1, "\n" ); |
| Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut ); |
| break; |
| } |
| } |
| if ( r == nRounds ) |
| { |
| if ( fVerbose ) Abc_Print( 1, "\n" ); |
| Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); |
| } |
| // cleanup |
| Ssw_RarManStop( p ); |
| return RetValue; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Filter equivalence classes of nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| 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 fMiter = 0; |
| Ssw_RarMan_t * p; |
| int r, i, k; |
| abctime clkTotal = Abc_Clock(); |
| abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; |
| 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; |
| if ( fVerbose ) |
| Abc_Print( 1, "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 |
| Aig_ManRandom( 1 ); |
| |
| // 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 ); |
| 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 ); |
| // 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, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); |
| // print the stats |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "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 ) |
| { |
| Abc_Print( 1, "All equivalences are refined away.\n" ); |
| break; |
| } |
| // simulate |
| Ssw_SmlSimulateOne( p->pSml ); |
| if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) |
| { |
| if ( fVerbose ) Abc_Print( 1, "\n" ); |
| Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); |
| RetValue = 0; |
| break; |
| } |
| // check equivalence classes |
| Ssw_ClassesRefineConst1( p->ppClasses, 1 ); |
| Ssw_ClassesRefine( p->ppClasses, 1 ); |
| // printout |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "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 && Abc_Clock() > nTimeToStop ) |
| { |
| if ( fVerbose ) Abc_Print( 1, "\n" ); |
| Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut ); |
| break; |
| } |
| } |
| if ( r == nRounds ) |
| { |
| Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); |
| } |
| // cleanup |
| Ssw_RarManStop( p ); |
| return -1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Filter equivalence classes of nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| 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 ) |
| { |
| 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_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); |
| Gia_ManReprFromAigRepr( pAig, p ); |
| Aig_ManStop( pAig ); |
| return RetValue; |
| } |
| |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
