From 581daaeade7e3b7bfef4bf90b5f3ace0e7fb4a5e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jul 2011 14:20:41 +0700 Subject: Changes to enable smarter simulation. --- src/aig/ssw/ssw.h | 3 + src/aig/ssw/sswClass.c | 20 ++ src/aig/ssw/sswInt.h | 1 + src/aig/ssw/sswRarity.c | 168 ++++----- src/aig/ssw/sswRarity2.c | 871 +++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 980 insertions(+), 83 deletions(-) create mode 100644 src/aig/ssw/sswRarity2.c (limited to 'src/aig/ssw') diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 3870d4ff..7632d923 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -118,6 +118,9 @@ 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 TimeOut, 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 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/sswClass.c b/src/aig/ssw/sswClass.c index a0e64cc0..51514f47 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -1039,6 +1039,26 @@ int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ) return nRefis; } +/**Function************************************************************* + + Synopsis [Refines the classes after simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive ) +{ + Aig_Obj_t * pObj; + int i, nRefis = 0; + Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i ) + nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive ); + return nRefis; +} + /**Function************************************************************* Synopsis [Refine the group of constant 1 nodes.] diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 32959e85..93e828a1 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -226,6 +226,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ); extern Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs ); extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ); +extern int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ); diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c index 5b262d91..5657908e 100644 --- a/src/aig/ssw/sswRarity.c +++ b/src/aig/ssw/sswRarity.c @@ -84,7 +84,7 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) SeeAlso [] ***********************************************************************/ -Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) +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 ) @@ -115,7 +115,7 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n SeeAlso [] ***********************************************************************/ -void Ssw_RarManStop( Ssw_RarMan_t * p ) +static void Ssw_RarManStop( Ssw_RarMan_t * p ) { if ( p->pSml ) Ssw_SmlStop( p->pSml ); if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); @@ -139,7 +139,7 @@ void Ssw_RarManStop( Ssw_RarMan_t * p ) SeeAlso [] ***********************************************************************/ -void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) +static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) { Aig_Obj_t * pObj; unsigned * pData; @@ -185,7 +185,7 @@ void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) SeeAlso [] ***********************************************************************/ -void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) +static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) { Aig_Obj_t * pObj; unsigned * pData; @@ -214,7 +214,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) } // printf( "\n" ); // 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 @@ -239,8 +239,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) 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 ); - +printf( "Best pattern %5d\n", iPatBest ); } assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); } @@ -257,7 +256,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) +static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) { Vec_Int_t * vInit; Aig_Obj_t * pObj, * pObjLi; @@ -295,6 +294,84 @@ Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ) return vInit; } + +/**Function************************************************************* + + Synopsis [Perform sequential simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_RarSimulate( 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, clk, clkTotal = clock(); + 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 ) + 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 + 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 + Ssw_SmlSimulateOne( p->pSml ); + if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) + { + 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 ) + { +// printf( "Round %3d: ", r ); +// 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 ) + { + 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 [Filter equivalence classes of nodes.] @@ -430,81 +507,6 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize -/**Function************************************************************* - - Synopsis [Perform sequential simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_RarSimulate( 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, clk, clkTotal = clock(); - 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 ) - 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 - 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 - Ssw_SmlSimulateOne( p->pSml ); - if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) - { - 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 ) - { -// printf( "Round %3d: ", r ); -// 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 ) - { - 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; -} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c new file mode 100644 index 00000000..b8fefe65 --- /dev/null +++ b/src/aig/ssw/sswRarity2.c @@ -0,0 +1,871 @@ +/**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 +}; + + +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 [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 + 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); + } + // 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 ); + } + } + 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 [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; + 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) ) + 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 ) +{ + 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 ) + { + 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); +// printf( "%d ", Value ); + } +// printf( "\n" ); + // 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 = 0; + // 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 ) + 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, f, clk, clkTotal = clock(); + 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 ) + 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 + Aig_ManRandom( 1 ); + + // 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(); + // simulate + for ( f = 0; f < nFrames; f++ ) + { + Ssw_RarManSimulate( p, f ? NULL : p->vInits, 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 ); + 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_RarTransferPatterns( p, p->vInits ); + // printout + if ( fVerbose ) + { +// printf( "Round %3d: ", r ); +// Abc_PrintTime( 1, "Time", clock() - clk ); + printf( "." ); + } + } +finish: + if ( r == nRounds ) + { + 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 [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, f, i, k, clkTotal = clock(); + 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 ) + 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 + 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 ); + + // 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, NULL, 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 ); + 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 ); + 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; + } + } + // printout + if ( fVerbose ) + { + printf( "Round %3d: ", r ); + Ssw_ClassesPrint( p->ppClasses, 0 ); + } + // get initialization patterns + Ssw_RarTransferPatterns( p, p->vInits ); + } +finish: + // report + if ( r == nRounds ) + { + 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; +} + +/**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 + -- cgit v1.2.3