From 32314347bae6ddcd841a268e797ec4da45726abb Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 10 Mar 2009 08:01:00 -0700 Subject: Version abc90310 --- src/aig/cec/cec.h | 44 ++- src/aig/cec/cecCec.c | 241 +++++++++++++ src/aig/cec/cecClass.c | 887 ++++++++++++++++-------------------------------- src/aig/cec/cecCore.c | 285 ++++++++++++---- src/aig/cec/cecInt.h | 67 ++-- src/aig/cec/cecIso.c | 370 ++++++++++++++++++++ src/aig/cec/cecMan.c | 174 ++++++---- src/aig/cec/cecPat.c | 6 +- src/aig/cec/cecSim.c | 48 +++ src/aig/cec/cecSolve.c | 97 +++++- src/aig/cec/cecSweep.c | 294 ++++++++++++++++ src/aig/cec/module.make | 8 +- 12 files changed, 1741 insertions(+), 780 deletions(-) create mode 100644 src/aig/cec/cecCec.c create mode 100644 src/aig/cec/cecIso.c create mode 100644 src/aig/cec/cecSim.c create mode 100644 src/aig/cec/cecSweep.c (limited to 'src/aig/cec') diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index fa7c5dbc..16748233 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -45,24 +45,42 @@ struct Cec_ParSat_t_ int nSatVarMax; // the max number of SAT variables int nCallsRecycle; // calls to perform before recycling SAT solver int fPolarFlip; // flops polarity of variables + int fCheckMiter; // the circuit is the miter int fFirstStop; // stop on the first sat output int fVerbose; // verbose stats }; +// simulation parameters +typedef struct Cec_ParSim_t_ Cec_ParSim_t; +struct Cec_ParSim_t_ +{ + int nWords; // the number of simulation words + int nRounds; // the number of simulation rounds + int TimeLimit; // the runtime limit in seconds + int fDoubleOuts; // miter with separate outputs + int fCheckMiter; // the circuit is the miter + int fFirstStop; // stop on the first sat output + int fSeqSimulate; // performs sequential simulation + int fVeryVerbose; // verbose stats + int fVerbose; // verbose stats +}; + // combinational SAT sweeping parameters -typedef struct Cec_ParCsw_t_ Cec_ParCsw_t; -struct Cec_ParCsw_t_ +typedef struct Cec_ParFra_t_ Cec_ParFra_t; +struct Cec_ParFra_t_ { int nWords; // the number of simulation words int nRounds; // the number of simulation rounds int nItersMax; // the maximum number of iterations of SAT sweeping int nBTLimit; // conflict limit at a node - int nSatVarMax; // the max number of SAT variables - int nCallsRecycle; // calls to perform before recycling SAT solver + int TimeLimit; // the runtime limit in seconds int nLevelMax; // restriction on the level nodes to be swept int nDepthMax; // the depth in terms of steps of speculative reduction int fRewriting; // enables AIG rewriting + int fCheckMiter; // the circuit is the miter int fFirstStop; // stop on the first sat output + int fDoubleOuts; // miter with separate outputs + int fColorDiff; // miter with separate outputs int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; @@ -71,13 +89,12 @@ struct Cec_ParCsw_t_ typedef struct Cec_ParCec_t_ Cec_ParCec_t; struct Cec_ParCec_t_ { - int nIters; // iterations of SAT solving/sweeping - int nBTLimitBeg; // starting backtrack limit - int nBTlimitMulti; // multiple of backtrack limit + int nBTLimit; // conflict limit at a node + int TimeLimit; // the runtime limit in seconds + int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation int fRewriting; // enables AIG rewriting - int fSatSweeping; // enables SAT sweeping - int fFirstStop; // stop on the first sat output + int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; @@ -89,12 +106,17 @@ struct Cec_ParCec_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== cecCec.c ==========================================================*/ +extern int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ); +extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ); /*=== cecCore.c ==========================================================*/ extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); -extern void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ); +extern void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ); +extern void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ); extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); -extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars ); +extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); +extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); #ifdef __cplusplus } diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c new file mode 100644 index 00000000..ea730693 --- /dev/null +++ b/src/aig/cec/cecCec.c @@ -0,0 +1,241 @@ +/**CFile**************************************************************** + + FileName [cecCec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Integrated combinatinal equivalence checker.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecCec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Saves the input pattern with the given number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) +{ + int i; + assert( p->pCexComb == NULL ); + p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, + sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) ); + p->pCexComb->iPo = iOut; + p->pCexComb->nPis = Gia_ManCiNum(p); + p->pCexComb->nBits = Gia_ManCiNum(p); + for ( i = 0; i < Gia_ManCiNum(p); i++ ) + if ( pValues[i] ) + Aig_InfoSetBit( p->pCexComb->pData, i ); +} + +/**Function************************************************************* + + Synopsis [Interface to the old CEC engine] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose ) +{ + extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); + extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ); + Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); + Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp ); + int RetValue, iOut, nOuts, clkTotal = clock(); + Gia_ManStop( pTemp ); + // run CEC on this miter + RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose ); + // report the miter + if ( RetValue == 1 ) + { + printf( "Networks are equivalent. " ); +ABC_PRT( "Time", clock() - clkTotal ); + } + else if ( RetValue == 0 ) + { + printf( "Networks are NOT EQUIVALENT. " ); +ABC_PRT( "Time", clock() - clkTotal ); + if ( pMiterCec->pData == NULL ) + printf( "Counter-example is not available.\n" ); + else + { + iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts ); + if ( iOut == -1 ) + printf( "Counter-example verification has failed.\n" ); + else + { + printf( "Primary output %d has failed in frame %d.\n", iOut ); + printf( "The counter-example detected %d incorrect outputs.\n", nOuts ); + } + Cec_ManTransformPattern( pMiter, iOut, pMiterCec->pData ); + } + } + else + { + printf( "Networks are UNDECIDED. " ); +ABC_PRT( "Time", clock() - clkTotal ); + } + fflush( stdout ); + Aig_ManStop( pMiterCec ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [New CEC engine.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) +{ + int fDumpUndecided = 1; + Cec_ParFra_t ParsFra, * pParsFra = &ParsFra; + Gia_Man_t * pNew; + int RetValue, clk = clock(); + double clkTotal = clock(); + // sweep for equivalences + Cec_ManFraSetDefaultParams( pParsFra ); + pParsFra->nBTLimit = pPars->nBTLimit; + pParsFra->TimeLimit = pPars->TimeLimit; + pParsFra->fVerbose = pPars->fVerbose; + pParsFra->fCheckMiter = 1; + pParsFra->fFirstStop = 1; + pParsFra->fDoubleOuts = 1; + pNew = Cec_ManSatSweeping( p, pParsFra ); + if ( pNew == NULL ) + { + if ( !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) + printf( "Counter-example simulation has failed.\n" ); + printf( "Networks are NOT EQUIVALENT. " ); + ABC_PRT( "Time", clock() - clk ); + return 0; + } + if ( Gia_ManAndNum(pNew) == 0 ) + { + printf( "Networks are equivalent. " ); + ABC_PRT( "Time", clock() - clk ); + Gia_ManStop( pNew ); + return 1; + } + printf( "Networks are UNDECIDED after the new CEC engine. " ); + ABC_PRT( "Time", clock() - clk ); + if ( fDumpUndecided ) + { + Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 ); + printf( "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); + } + if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) + { + Gia_ManStop( pNew ); + return -1; + } + // call other solver + printf( "Calling the old CEC engine.\n" ); + fflush( stdout ); + RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose ); + p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL; + if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) + printf( "Counter-example simulation has failed.\n" ); + Gia_ManStop( pNew ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [New CEC engine applied to two circuits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ) +{ + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Gia_Man_t * pMiter; + int RetValue; + Cec_ManCecSetDefaultParams( pPars ); + pPars->fVerbose = fVerbose; + pMiter = Gia_ManMiter( p0, p1, 0, 1, pPars->fVerbose ); + if ( pMiter == NULL ) + return -1; + RetValue = Cec_ManVerify( pMiter, pPars ); + p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL; + Gia_ManStop( pMiter ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [New CEC engine applied to two circuits.] + + Description [Returns 1 if equivalent, 0 if counter-example, -1 if undecided. + Counter-example is returned in the first manager as pAig0->pSeqModel. + The format is given in Gia_Cex_t (file "abc\src\aig\gia\gia.h").] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ) +{ + Gia_Man_t * p0, * p1, * pTemp; + int RetValue; + + p0 = Gia_ManFromAig( pAig0 ); + p0 = Gia_ManCleanup( pTemp = p0 ); + Gia_ManStop( pTemp ); + + p1 = Gia_ManFromAig( pAig1 ); + p1 = Gia_ManCleanup( pTemp = p1 ); + Gia_ManStop( pTemp ); + + RetValue = Cec_ManVerifyTwo( p0, p1, fVerbose ); + pAig0->pSeqModel = p0->pCexComb; p0->pCexComb = NULL; + Gia_ManStop( p0 ); + Gia_ManStop( p1 ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 65fa2e9b..aaa85ffa 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -24,39 +24,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Cec_ObjRepr( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iRepr; } -static inline void Cec_ObjSetRepr( Cec_ManCsw_t * p, int Id, int Num ) { p->pObjs[Id].iRepr = Num; } - -static inline int Cec_ObjProved( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iProved; } -static inline void Cec_ObjSetProved( Cec_ManCsw_t * p, int Id ) { p->pObjs[Id].iProved = 1; } - -static inline int Cec_ObjFailed( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iFailed; } -static inline void Cec_ObjSetFailed( Cec_ManCsw_t * p, int Id ) { p->pObjs[Id].iFailed = 1; } - -static inline int Cec_ObjNext( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].iNext; } -static inline void Cec_ObjSetNext( Cec_ManCsw_t * p, int Id, int Num ) { p->pObjs[Id].iNext = Num; } - -static inline unsigned Cec_ObjSim( Cec_ManCsw_t * p, int Id ) { return p->pObjs[Id].SimNum; } -static inline unsigned * Cec_ObjSimP1( Cec_ManCsw_t * p, int Id ) { return &p->pObjs[Id].SimNum; } -static inline unsigned * Cec_ObjSimP( Cec_ManCsw_t * p, int Id ) { return p->pMems + Cec_ObjSim(p, Id) + 1; } -static inline void Cec_ObjSetSim( Cec_ManCsw_t * p, int Id, unsigned n ) { p->pObjs[Id].SimNum = n; } - -static inline int Cec_ObjIsConst( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) == 0; } -static inline int Cec_ObjIsHead( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) > 0; } -static inline int Cec_ObjIsNone( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) == 0; } -static inline int Cec_ObjIsTail( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) > 0 && Cec_ObjNext(p, Id) == 0; } -static inline int Cec_ObjIsClass( Cec_ManCsw_t * p, int Id ) { return Cec_ObjRepr(p, Id) > 0 || Cec_ObjNext(p, Id) > 0; } - -#define Cec_ManForEachObj( p, i ) \ - for ( i = 0; i < Gia_ManObjNum(p->pAig); i++ ) -#define Cec_ManForEachObj1( p, i ) \ - for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) -#define Cec_ManForEachClass( p, i ) \ - for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) if ( !Cec_ObjIsHead(p, i) ) {} else -#define Cec_ClassForEachObj( p, i, iObj ) \ - for ( assert(Cec_ObjIsHead(p, i)), iObj = i; iObj; iObj = Cec_ObjNext(p, iObj) ) -#define Cec_ClassForEachObj1( p, i, iObj ) \ - for ( assert(Cec_ObjIsHead(p, i)), iObj = Cec_ObjNext(p, i); iObj; iObj = Cec_ObjNext(p, iObj) ) +static inline unsigned * Cec_ObjSim( Cec_ManSim_t * p, int Id ) { return p->pMems + p->pSimInfo[Id] + 1; } +static inline void Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n ) { p->pSimInfo[Id] = n; } + +static inline float Cec_MemUsage( Cec_ManSim_t * p ) { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -64,30 +35,7 @@ static inline int Cec_ObjIsClass( Cec_ManCsw_t * p, int Id ) { /**Function************************************************************* - Synopsis [Creates the set of representatives.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p ) -{ - int i, * pReprs = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); - for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) - if ( Cec_ObjProved(p, i) ) - { - assert( Cec_ObjRepr(p, i) >= 0 ); - pReprs[i] = Cec_ObjRepr(p, i); - } - return pReprs; -} - -/**Function************************************************************* - - Synopsis [] + Synopsis [Compares simulation info of one node with constant 0.] Description [] @@ -96,250 +44,28 @@ int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManCswDupWithClasses( Cec_ManCsw_t * p ) +int Cec_ManSimCompareConst( unsigned * p, int nWords ) { - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; - int iRes0, iRes1, iRepr, iNode; - int i, fCompl, * piCopies; - Vec_IntClear( p->vXorNodes ); - Gia_ManLevelNum( p->pAig ); - pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); - Gia_ManHashAlloc( pNew ); - piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); - piCopies[0] = 0; - Gia_ManForEachObj1( p->pAig, pObj, i ) - { - if ( Gia_ObjIsCi(pObj) ) - { - piCopies[i] = Gia_ManAppendCi( pNew ); - continue; - } - iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); - if ( Gia_ObjIsCo(pObj) ) - { - Gia_ManAppendCo( pNew, iRes0 ); - continue; - } - iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); - iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); - if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) ) - continue; - assert( Cec_ObjRepr(p, i) < i ); - iRepr = piCopies[Cec_ObjRepr(p, i)]; - if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) ) - continue; - pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) ); - fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr); - piCopies[i] = Gia_LitNotCond( iRepr, fCompl ); - } - ABC_FREE( piCopies ); - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, 0 ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Cec_ManCswSpecReduction( Cec_ManCsw_t * p ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; - int iRes0, iRes1, iRepr, iNode, iMiter; - int i, fCompl, * piCopies, * pDepths; - Vec_IntClear( p->vXorNodes ); -// Gia_ManLevelNum( p->pAig ); - pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); - Gia_ManHashAlloc( pNew ); - piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); - pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); - piCopies[0] = 0; - Gia_ManForEachObj1( p->pAig, pObj, i ) - { - if ( Gia_ObjIsCi(pObj) ) - { - piCopies[i] = Gia_ManAppendCi( pNew ); - continue; - } - if ( Gia_ObjIsCo(pObj) ) - continue; - if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 || - piCopies[Gia_ObjFaninId1(pObj,i)] == -1 ) - continue; - iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); - iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); - iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); - pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); - if ( Cec_ObjRepr(p, i) < 0 || Cec_ObjFailed(p, i) ) - continue; - assert( Cec_ObjRepr(p, i) < i ); - iRepr = piCopies[Cec_ObjRepr(p, i)]; - if ( iRepr == -1 ) - continue; - if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) ) - continue; - pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) ); - fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr); - piCopies[i] = Gia_LitNotCond( iRepr, fCompl ); - if ( Cec_ObjProved(p, i) ) - continue; -// if ( p->pPars->nLevelMax && -// (Gia_ObjLevel(p->pAig, pObj) > p->pPars->nLevelMax || -// Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) ) -// continue; - // produce speculative miter - iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] ); - Gia_ManAppendCo( pNew, iMiter ); - Vec_IntPush( p->vXorNodes, Cec_ObjRepr(p, i) ); - Vec_IntPush( p->vXorNodes, i ); - // add to the depth of this node - pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Cec_ObjRepr(p, i)] ); - if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax ) - piCopies[i] = -1; - } - ABC_FREE( piCopies ); - ABC_FREE( pDepths ); - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, 0 ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; - int iRes0, iRes1, iRepr, iNode, iMiter; - int i, fCompl, * piCopies; - Vec_IntClear( p->vXorNodes ); - Gia_ManLevelNum( p->pAig ); - pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); - Gia_ManHashAlloc( pNew ); - piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); - piCopies[0] = 0; - Gia_ManForEachObj1( p->pAig, pObj, i ) + int w; + if ( p[0] & 1 ) { - if ( Gia_ObjIsCi(pObj) ) - { - piCopies[i] = Gia_ManAppendCi( pNew ); - continue; - } - if ( Gia_ObjIsCo(pObj) ) - continue; - iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); - iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); - iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); - if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) ) - continue; - assert( Cec_ObjRepr(p, i) < i ); - iRepr = piCopies[Cec_ObjRepr(p, i)]; - if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) ) - continue; - pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) ); - fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr); - piCopies[i] = Gia_LitNotCond( iRepr, fCompl ); - // add speculative miter - iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] ); - Gia_ManAppendCo( pNew, iMiter ); + for ( w = 0; w < nWords; w++ ) + if ( p[w] != ~0 ) + return 0; + return 1; } - ABC_FREE( piCopies ); - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, 0 ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManCswCountOne( Cec_ManCsw_t * p, int i ) -{ - int Ent, nLits = 1; - Cec_ClassForEachObj1( p, i, Ent ) + else { - assert( Cec_ObjRepr(p, Ent) == i ); - nLits++; + for ( w = 0; w < nWords; w++ ) + if ( p[w] != 0 ) + return 0; + return 1; } - return nLits; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManCswCountLitsAll( Cec_ManCsw_t * p ) -{ - int i, nLits = 0; - Cec_ManForEachObj( p, i ) - nLits += (Cec_ObjRepr(p, i) >= 0); - return nLits; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter ) -{ - int Ent; - printf( "Class %4d : Num = %2d {", Counter, Cec_ManCswCountOne(p, i) ); - Cec_ClassForEachObj( p, i, Ent ) - printf(" %d", Ent ); - printf( " }\n" ); } /**Function************************************************************* - Synopsis [] + Synopsis [Compares simulation info of two nodes.] Description [] @@ -348,32 +74,28 @@ void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose ) +int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords ) { - int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits; - Cec_ManForEachObj1( p, i ) + int w; + if ( (p0[0] & 1) == (p1[0] & 1) ) { - if ( Cec_ObjIsHead(p, i) ) - Counter++; - else if ( Cec_ObjIsConst(p, i) ) - Counter1++; - else if ( Cec_ObjIsNone(p, i) ) - CounterX++; + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != p1[w] ) + return 0; + return 1; } - nLits = Cec_ManCswCountLitsAll( p ); - printf( "Class =%7d. Const =%7d. Unsed =%7d. Lits =%8d. All =%8d. Mem = %5.2f Mb\n", - Counter, Counter1, CounterX, nLits-Counter1, nLits, 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20) ); - if ( fVerbose ) + else { - Counter = 0; - Cec_ManForEachClass( p, i ) - Cec_ManCswPrintOne( p, i, ++Counter ); + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != ~p1[w] ) + return 0; + return 1; } } /**Function************************************************************* - Synopsis [] + Synopsis [Returns the number of the first non-equal bit.] Description [] @@ -382,28 +104,28 @@ void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords ) +int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords ) { int w; - if ( (p0[0] & 1) == (p1[0] & 1) ) + if ( p[0] & 1 ) { for ( w = 0; w < nWords; w++ ) - if ( p0[w] != p1[w] ) - return 0; - return 1; + if ( p[w] != ~0 ) + return 32*w + Aig_WordFindFirstBit( ~p[w] ); + return -1; } else { for ( w = 0; w < nWords; w++ ) - if ( p0[w] != ~p1[w] ) - return 0; - return 1; + if ( p[w] != 0 ) + return 32*w + Aig_WordFindFirstBit( p[w] ); + return -1; } } /**Function************************************************************* - Synopsis [] + Synopsis [Compares simulation info of two nodes.] Description [] @@ -412,28 +134,28 @@ int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords ) SeeAlso [] ***********************************************************************/ -int Cec_ManCswCompareConst( unsigned * p, int nWords ) +int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords ) { int w; - if ( p[0] & 1 ) + if ( (p0[0] & 1) == (p1[0] & 1) ) { for ( w = 0; w < nWords; w++ ) - if ( p[w] != ~0 ) - return 0; - return 1; + if ( p0[w] != p1[w] ) + return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] ); + return -1; } else { for ( w = 0; w < nWords; w++ ) - if ( p[w] != 0 ) - return 0; - return 1; + if ( p0[w] != ~p1[w] ) + return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] ); + return -1; } } /**Function************************************************************* - Synopsis [] + Synopsis [Creates equivalence class.] Description [] @@ -442,31 +164,31 @@ int Cec_ManCswCompareConst( unsigned * p, int nWords ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass ) +void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) { - int Repr = -1, EntPrev = -1, Ent, i; + int Repr = GIA_VOID, EntPrev = -1, Ent, i; assert( Vec_IntSize(vClass) > 0 ); Vec_IntForEachEntry( vClass, Ent, i ) { if ( i == 0 ) { Repr = Ent; - Cec_ObjSetRepr( p, Ent, -1 ); + Gia_ObjSetRepr( p, Ent, GIA_VOID ); EntPrev = Ent; } else { - Cec_ObjSetRepr( p, Ent, Repr ); - Cec_ObjSetNext( p, EntPrev, Ent ); + Gia_ObjSetRepr( p, Ent, Repr ); + Gia_ObjSetNext( p, EntPrev, Ent ); EntPrev = Ent; } } - Cec_ObjSetNext( p, EntPrev, 0 ); + Gia_ObjSetNext( p, EntPrev, 0 ); } /**Function************************************************************* - Synopsis [] + Synopsis [Refines one equivalence class.] Description [] @@ -475,34 +197,34 @@ void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass ) SeeAlso [] ***********************************************************************/ -int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst ) +int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i ) { unsigned * pSim0, * pSim1; int Ent; Vec_IntClear( p->vClassOld ); Vec_IntClear( p->vClassNew ); Vec_IntPush( p->vClassOld, i ); - pSim0 = fFirst? Cec_ObjSimP1(p, i) : Cec_ObjSimP(p, i); - Cec_ClassForEachObj1( p, i, Ent ) + pSim0 = Cec_ObjSim(p, i); + Gia_ClassForEachObj1( p->pAig, i, Ent ) { - pSim1 = fFirst? Cec_ObjSimP1(p, Ent) : Cec_ObjSimP(p, Ent); - if ( Cec_ManCswCompareEqual( pSim0, pSim1, p->nWords ) ) + pSim1 = Cec_ObjSim(p, Ent); + if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) ) Vec_IntPush( p->vClassOld, Ent ); else Vec_IntPush( p->vClassNew, Ent ); } if ( Vec_IntSize( p->vClassNew ) == 0 ) return 0; - Cec_ManCswClassCreate( p, p->vClassOld ); - Cec_ManCswClassCreate( p, p->vClassNew ); + Cec_ManSimClassCreate( p->pAig, p->vClassOld ); + Cec_ManSimClassCreate( p->pAig, p->vClassNew ); if ( Vec_IntSize(p->vClassNew) > 1 ) - return 1 + Cec_ManCswClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), fFirst ); + return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) ); return 1; } /**Function************************************************************* - Synopsis [] + Synopsis [Computes hash key of the simuation info.] Description [] @@ -511,7 +233,7 @@ int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst ) SeeAlso [] ***********************************************************************/ -int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize ) +int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize ) { static int s_Primes[16] = { 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, @@ -530,7 +252,7 @@ int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize ) /**Function************************************************************* - Synopsis [] + Synopsis [Resets pointers to the simulation memory.] Description [] @@ -539,90 +261,7 @@ int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswClassesCreate( Cec_ManCsw_t * p ) -{ - int * pTable, nTableSize, i, Key; - p->nWords = 1; - nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p->pAig) / 10 ); - pTable = ABC_CALLOC( int, nTableSize ); - Cec_ObjSetRepr( p, 0, -1 ); - Cec_ManForEachObj1( p, i ) - { - if ( Gia_ObjIsCo(Gia_ManObj(p->pAig, i)) ) - { - Cec_ObjSetRepr( p, i, -1 ); - continue; - } - if ( Cec_ManCswCompareConst( Cec_ObjSimP1(p, i), p->nWords ) ) - { - Cec_ObjSetRepr( p, i, 0 ); - continue; - } - Key = Cec_ManCswHashKey( Cec_ObjSimP1(p, i), p->nWords, nTableSize ); - if ( pTable[Key] == 0 ) - Cec_ObjSetRepr( p, i, -1 ); - else - { - Cec_ObjSetNext( p, pTable[Key], i ); - Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) ); - if ( Cec_ObjRepr(p, i) == -1 ) - Cec_ObjSetRepr( p, i, pTable[Key] ); - } - pTable[Key] = i; - } - ABC_FREE( pTable ); - if ( p->pPars->fVeryVerbose ) - Cec_ManCswPrintClasses( p, 0 ); - // refine classes - Cec_ManForEachClass( p, i ) - Cec_ManCswClassRefineOne( p, i, 1 ); - // clean memory - Cec_ManForEachObj( p, i ) - Cec_ObjSetSim( p, i, 0 ); - if ( p->pPars->fVeryVerbose ) - Cec_ManCswPrintClasses( p, 0 ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCswSimulateSimple( Cec_ManCsw_t * p ) -{ - Gia_Obj_t * pObj; - unsigned Res0, Res1; - int i; - Gia_ManForEachCi( p->pAig, pObj, i ) - Cec_ObjSetSim( p, i, Aig_ManRandom(0) ); - Gia_ManForEachAnd( p->pAig, pObj, i ) - { - Res0 = Cec_ObjSim( p, Gia_ObjFaninId0(pObj, i) ); - Res1 = Cec_ObjSim( p, Gia_ObjFaninId1(pObj, i) ); - Cec_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) & - (Gia_ObjFaninC1(pObj)? ~Res1: Res1) ); - } -} - -/**Function************************************************************* - - Synopsis [References simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p ) +void Cec_ManSimMemRelink( Cec_ManSim_t * p ) { unsigned * pPlace, Ent; pPlace = &p->MemFree; @@ -634,6 +273,7 @@ void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p ) pPlace = p->pMems + Ent; } *pPlace = 0; + p->nWordsOld = p->nWords; } /**Function************************************************************* @@ -647,10 +287,10 @@ void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p ) SeeAlso [] ***********************************************************************/ -unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i ) +unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i ) { unsigned * pSim; - assert( p->pObjs[i].SimNum == 0 ); + assert( p->pSimInfo[i] == 0 ); if ( p->MemFree == 0 ) { if ( p->nWordsAlloc == 0 ) @@ -661,9 +301,9 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i ) } p->nWordsAlloc *= 2; p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc ); - Cec_ManCswSimMemRelink( p ); + Cec_ManSimMemRelink( p ); } - p->pObjs[i].SimNum = p->MemFree; + p->pSimInfo[i] = p->MemFree; pSim = p->pMems + p->MemFree; p->MemFree = pSim[0]; pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) ); @@ -675,7 +315,7 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i ) /**Function************************************************************* - Synopsis [Dereference simulaton info.] + Synopsis [Dereferences simulaton info.] Description [] @@ -684,16 +324,16 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i ) SeeAlso [] ***********************************************************************/ -unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i ) +unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i ) { unsigned * pSim; - assert( p->pObjs[i].SimNum > 0 ); - pSim = p->pMems + p->pObjs[i].SimNum; + assert( p->pSimInfo[i] > 0 ); + pSim = p->pMems + p->pSimInfo[i]; if ( --pSim[0] == 0 ) { pSim[0] = p->MemFree; - p->MemFree = p->pObjs[i].SimNum; - p->pObjs[i].SimNum = 0; + p->MemFree = p->pSimInfo[i]; + p->pSimInfo[i] = 0; p->nMems--; } return pSim; @@ -701,7 +341,7 @@ unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i ) /**Function************************************************************* - Synopsis [] + Synopsis [Refines nodes belonging to candidate constant class.] Description [] @@ -710,50 +350,143 @@ unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined ) +void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined ) { unsigned * pSim; int * pTable, nTableSize, i, k, Key; if ( Vec_IntSize(vRefined) == 0 ) return; - nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); + nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); pTable = ABC_CALLOC( int, nTableSize ); Vec_IntForEachEntry( vRefined, i, k ) { - if ( i == 7720 ) - { - int s = 0; - } - pSim = Cec_ObjSimP( p, i ); - assert( !Cec_ManCswCompareConst( pSim, p->nWords ) ); - Key = Cec_ManCswHashKey( pSim, p->nWords, nTableSize ); + pSim = Cec_ObjSim( p, i ); + assert( !Cec_ManSimCompareConst( pSim, p->nWords ) ); + Key = Cec_ManSimHashKey( pSim, p->nWords, nTableSize ); if ( pTable[Key] == 0 ) { - assert( Cec_ObjRepr(p, i) == 0 ); - assert( Cec_ObjNext(p, i) == 0 ); - Cec_ObjSetRepr( p, i, -1 ); + assert( Gia_ObjRepr(p->pAig, i) == 0 ); + assert( Gia_ObjNext(p->pAig, i) == 0 ); + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); } else { - Cec_ObjSetNext( p, pTable[Key], i ); - Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) ); - if ( Cec_ObjRepr(p, i) == -1 ) - Cec_ObjSetRepr( p, i, pTable[Key] ); - assert( Cec_ObjRepr(p, i) > 0 ); + Gia_ObjSetNext( p->pAig, pTable[Key], i ); + Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) ); + if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID ) + Gia_ObjSetRepr( p->pAig, i, pTable[Key] ); + assert( Gia_ObjRepr(p->pAig, i) > 0 ); } pTable[Key] = i; } Vec_IntForEachEntry( vRefined, i, k ) { - if ( Cec_ObjIsHead( p, i ) ) - Cec_ManCswClassRefineOne( p, i, 0 ); + if ( Gia_ObjIsHead( p->pAig, i ) ) + Cec_ManSimClassRefineOne( p, i ); } Vec_IntForEachEntry( vRefined, i, k ) - Cec_ManCswSimDeref( p, i ); + Cec_ManSimSimDeref( p, i ); ABC_FREE( pTable ); } +/**Function************************************************************* + + Synopsis [Saves the input pattern with the given number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) +{ + unsigned * pInfo; + int i; + assert( p->pCexComb == NULL ); + assert( iPat >= 0 && iPat < 32 * p->nWords ); + p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, + sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) ); + p->pCexComb->iPo = p->iOut; + p->pCexComb->nPis = Gia_ManCiNum(p->pAig); + p->pCexComb->nBits = Gia_ManCiNum(p->pAig); + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + { + pInfo = Vec_PtrEntry( p->vCiSimInfo, i ); + if ( Aig_InfoHasBit( pInfo, iPat ) ) + Aig_InfoSetBit( p->pCexComb->pData, i ); + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if computation should stop.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) +{ + unsigned * pInfo, * pInfo2; + int i; + if ( p->vCoSimInfo == NULL ) + return 0; + // compare outputs with 0 + if ( p->pPars->fDoubleOuts ) + { + assert( (Gia_ManCoNum(p->pAig) & 1) == 0 ); + for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ ) + { + pInfo = Vec_PtrEntry( p->vCoSimInfo, i ); + pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i ); + if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) ) + { + if ( p->iOut == -1 ) + { + p->iOut = i/2; + Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) ); + } + if ( p->pCexes == NULL ) + p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 ); + if ( p->pCexes[i/2] == NULL ) + { + p->nOuts++; + p->pCexes[i/2] = (void *)1; + } + } + } + } + else + { + for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ ) + { + pInfo = Vec_PtrEntry( p->vCoSimInfo, i ); + if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) ) + { + if ( p->iOut == -1 ) + { + p->iOut = i; + Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) ); + } + if ( p->pCexes == NULL ) + p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) ); + if ( p->pCexes[i] == NULL ) + { + p->nOuts++; + p->pCexes[i] = (void *)1; + } + } + } + } + return p->pCexes != NULL && p->pPars->fFirstStop; +} + /**Function************************************************************* Synopsis [Simulates one round.] @@ -765,17 +498,20 @@ void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, int iSeries, int fRandomize ) +int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) { - static int nCountRand = 0; Gia_Obj_t * pObj; unsigned * pRes0, * pRes1, * pRes; int i, k, w, Ent, iCiId = 0, iCoId = 0; + // prepare internal storage + if ( p->nWordsOld != p->nWords ) + Cec_ManSimMemRelink( p ); p->nMemsMax = 0; + // simulate nodes Vec_IntClear( p->vRefinedC ); if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) ) { - pRes = Cec_ManCswSimRef( p, 0 ); + pRes = Cec_ManSimSimRef( p, 0 ); for ( w = 1; w <= p->nWords; w++ ) pRes[w] = 0; } @@ -788,16 +524,12 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t iCiId++; continue; } - pRes = Cec_ManCswSimRef( p, i ); + pRes = Cec_ManSimSimRef( p, i ); if ( vInfoCis ) { pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ ); for ( w = 1; w <= p->nWords; w++ ) - { - pRes[w] = pRes0[iSeries*p->nWords+w-1]; - if ( fRandomize ) - pRes[w] ^= (1 << (nCountRand++ & 0x1f)); - } + pRes[w] = pRes0[w-1]; } else { @@ -810,7 +542,7 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t } if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin { - pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) ); + pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); if ( vInfoCos ) { pRes = Vec_PtrEntry( vInfoCos, iCoId++ ); @@ -824,9 +556,9 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t continue; } assert( Gia_ObjValue(pObj) ); - pRes = Cec_ManCswSimRef( p, i ); - pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) ); - pRes1 = Cec_ManCswSimDeref( p, Gia_ObjFaninId1(pObj,i) ); + pRes = Cec_ManSimSimRef( p, i ); + pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); + pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) ); if ( Gia_ObjFaninC0(pObj) ) { if ( Gia_ObjFaninC1(pObj) ) @@ -847,47 +579,50 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t } references: // if this node is candidate constant, collect it - if ( Cec_ObjIsConst(p, i) && !Cec_ManCswCompareConst(pRes + 1, p->nWords) ) + if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) ) { pRes[0]++; Vec_IntPush( p->vRefinedC, i ); } // if the node belongs to a class, save it - if ( Cec_ObjIsClass(p, i) ) + if ( Gia_ObjIsClass(p->pAig, i) ) pRes[0]++; // if this is the last node of the class, process it - if ( Cec_ObjIsTail(p, i) ) + if ( Gia_ObjIsTail(p->pAig, i) ) { Vec_IntClear( p->vClassTemp ); - Cec_ClassForEachObj( p, Cec_ObjRepr(p, i), Ent ) + Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent ) Vec_IntPush( p->vClassTemp, Ent ); - Cec_ManCswClassRefineOne( p, Cec_ObjRepr(p, i), 0 ); + Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) ); Vec_IntForEachEntry( p->vClassTemp, Ent, k ) - Cec_ManCswSimDeref( p, Ent ); + Cec_ManSimSimDeref( p, Ent ); } } if ( Vec_IntSize(p->vRefinedC) > 0 ) - Cec_ManCswProcessRefined( p, p->vRefinedC ); + Cec_ManSimProcessRefined( p, p->vRefinedC ); assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) ); assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) ); assert( p->nMems == 1 ); + if ( p->nMems != 1 ) + printf( "Cec_ManSimSimulateRound(): Memory management error!\n" ); if ( p->pPars->fVeryVerbose ) - Cec_ManCswPrintClasses( p, 0 ); + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); /* - if ( p->nMems > 1 ) - { + if ( p->nMems > 1 ) { for ( i = 1; i < p->nObjs; i++ ) - if ( p->pSims[i] ) - { + if ( p->pSims[i] ) { int x = 0; } } */ + return Cec_ManSimAnalyzeOutputs( p ); } + + /**Function************************************************************* - Synopsis [] + Synopsis [Creates simulation info for this round.] Description [] @@ -896,28 +631,41 @@ references: SeeAlso [] ***********************************************************************/ -int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p ) +void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) { - int i; - Gia_ManSetRefs( p->pAig ); - Cec_ManCswSimulateSimple( p ); - Cec_ManCswClassesCreate( p ); - for ( i = 0; i < p->pPars->nRounds; i++ ) + unsigned * pRes0, * pRes1; + int i, w; + if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 ) { - p->nWords = i + 1; - Cec_ManCswSimMemRelink( p ); - Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 ); + assert( vInfoCis && vInfoCos ); + for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) + { + pRes0 = Vec_PtrEntry( vInfoCis, i ); + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = Aig_ManRandom( 0 ); + } + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + pRes0 = Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i ); + pRes1 = Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i ); + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = pRes1[w]; + } + } + else + { + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + { + pRes0 = Vec_PtrEntry( vInfoCis, i ); + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = Aig_ManRandom( 0 ); + } } - p->nWords = p->pPars->nWords; - Cec_ManCswSimMemRelink( p ); - for ( i = 0; i < p->pPars->nRounds; i++ ) - Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 ); - return 1; } /**Function************************************************************* - Synopsis [] + Synopsis [Returns 1 if the bug is found.] Description [] @@ -926,21 +674,37 @@ int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p ) SeeAlso [] ***********************************************************************/ -int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj ) +int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ) { - int Result; - if ( pObj->fMark0 ) - return 1; - if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) ) - return 0; - Result = (Cec_ManCswClassesUpdate_rec( Gia_ObjFanin0(pObj) ) | - Cec_ManCswClassesUpdate_rec( Gia_ObjFanin1(pObj) )); - return pObj->fMark0 = Result; + Gia_Obj_t * pObj; + int i; + assert( p->pAig->pReprs == NULL ); + // allocate representation + p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) ); + p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); + Gia_ManForEachObj( p->pAig, pObj, i ) + Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj)) ? 0 : GIA_VOID ); + // perform simulation + Gia_ManSetRefs( p->pAig ); + p->nWords = 1; + do { + if ( p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + for ( i = 0; i < 4; i++ ) + { + Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; + } + p->nWords = 2 * p->nWords + 1; + } + while ( p->nWords <= p->pPars->nWords ); + return 0; } /**Function************************************************************* - Synopsis [] + Synopsis [Returns 1 if the bug is found.] Description [] @@ -949,100 +713,23 @@ int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew ) +int Cec_ManSimClassesRefine( Cec_ManSim_t * p ) { - Vec_Ptr_t * vInfo; - Gia_Obj_t * pObj, * pObjOld, * pReprOld; - int i, k, iRepr, iNode; - vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), p->pPars->nWords ); - if ( vInfo != NULL ) - { - for ( i = 0; i < pPat->nSeries; i++ ) - Cec_ManCswSimulateRound( p, vInfo, NULL, i, 0 ); - Vec_PtrFree( vInfo ); - } - assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) ); - // mark the transitive fanout of failed nodes - if ( p->pPars->nDepthMax != 1 ) + int i; + Gia_ManSetRefs( p->pAig ); + p->nWords = p->pPars->nWords; + for ( i = 0; i < p->pPars->nRounds; i++ ) { - Gia_ManCleanMark0( p->pAig ); - Gia_ManCleanMark1( p->pAig ); - Gia_ManForEachCo( pNew, pObj, k ) - { - iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); - iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); - if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved - continue; -// Gia_ManObj(p->pAig, iRepr)->fMark0 = 1; - Gia_ManObj(p->pAig, iNode)->fMark0 = 1; - } - // mark the nodes reachable through the failed nodes - Gia_ManForEachAnd( p->pAig, pObjOld, k ) - pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0); - // unmark the disproved nodes - Gia_ManForEachCo( pNew, pObj, k ) - { - iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); - iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); - if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved - continue; - pObjOld = Gia_ManObj(p->pAig, iNode); - assert( pObjOld->fMark0 == 1 ); - if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 ) - pObjOld->fMark1 = 1; - } - // clean marks - Gia_ManForEachAnd( p->pAig, pObjOld, k ) - if ( pObjOld->fMark1 ) - { - pObjOld->fMark0 = 0; - pObjOld->fMark1 = 0; - } + if ( (i % 4) == 0 && p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; } - // set the results - Gia_ManForEachCo( pNew, pObj, k ) - { - iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); - iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); - pReprOld = Gia_ManObj(p->pAig, iRepr); - pObjOld = Gia_ManObj(p->pAig, iNode); - if ( pObj->fMark1 ) - { // proved - assert( pObj->fMark0 == 0 ); - assert( !Cec_ObjProved(p, iNode) ); - if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 ) -// if ( pObjOld->fMark0 == 0 ) - { - assert( iRepr == Cec_ObjRepr(p, iNode) ); - Cec_ObjSetProved( p, iNode ); - p->nAllProved++; - } - } - else if ( pObj->fMark0 ) - { // disproved - assert( pObj->fMark1 == 0 ); - if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 ) -// if ( pObjOld->fMark0 == 0 ) - { - if ( iRepr == Cec_ObjRepr(p, iNode) ) - printf( "Cec_ManCswClassesUpdate(): Error! Node is not refined!\n" ); - p->nAllDisproved++; - } - } - else - { // failed - assert( pObj->fMark0 == 0 ); - assert( pObj->fMark1 == 0 ); - assert( !Cec_ObjFailed(p, iNode) ); - assert( !Cec_ObjProved(p, iNode) ); - Cec_ObjSetFailed( p, iNode ); - p->nAllFailed++; - } - } + if ( p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); return 0; } - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index ab8fd5cf..e25ddc90 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -44,11 +44,37 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) memset( p, 0, sizeof(Cec_ParSat_t) ); p->nBTLimit = 10; // conflict limit at a node p->nSatVarMax = 2000; // the max number of SAT variables - p->nCallsRecycle = 100; // calls to perform before recycling SAT solver + p->nCallsRecycle = 200; // calls to perform before recycling SAT solver p->fPolarFlip = 1; // flops polarity of variables + p->fCheckMiter = 0; // the circuit is the miter p->fFirstStop = 0; // stop on the first sat output - p->fVerbose = 1; // verbose stats + p->fVerbose = 0; // verbose stats } + +/**Function************ ************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) +{ + memset( p, 0, sizeof(Cec_ParSim_t) ); + p->nWords = 15; // the number of simulation words + p->nRounds = 15; // the number of simulation rounds + p->TimeLimit = 0; // the runtime limit in seconds + p->fCheckMiter = 0; // the circuit is the miter + p->fFirstStop = 0; // stop on the first sat output + p->fDoubleOuts = 0; // miter with separate outputs + p->fSeqSimulate = 0; // performs sequential simulation + p->fVeryVerbose = 0; // verbose stats + p->fVerbose = 0; // verbose stats +} /**Function************ ************************************************* @@ -61,19 +87,21 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ) +void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) { - memset( p, 0, sizeof(Cec_ParCsw_t) ); - p->nWords = 20; // the number of simulation words - p->nRounds = 20; // the number of simulation rounds - p->nItersMax = 20; // the maximum number of iterations of SAT sweeping - p->nBTLimit = 10000; // conflict limit at a node - p->nSatVarMax = 2000; // the max number of SAT variables - p->nCallsRecycle = 100; // calls to perform before recycling SAT solver + memset( p, 0, sizeof(Cec_ParFra_t) ); + p->nWords = 15; // the number of simulation words + p->nRounds = 15; // the number of simulation rounds + p->TimeLimit = 0; // the runtime limit in seconds + p->nItersMax = 1000; // the maximum number of iterations of SAT sweeping + p->nBTLimit = 1000; // conflict limit at a node p->nLevelMax = 0; // restriction on the level of nodes to be swept p->nDepthMax = 1; // the depth in terms of steps of speculative reduction p->fRewriting = 0; // enables AIG rewriting + p->fCheckMiter = 0; // the circuit is the miter p->fFirstStop = 0; // stop on the first sat output + p->fDoubleOuts = 0; // miter with separate outputs + p->fColorDiff = 0; // miter with separate outputs p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } @@ -92,14 +120,13 @@ void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ) void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ) { memset( p, 0, sizeof(Cec_ParCec_t) ); - p->nIters = 1; // iterations of SAT solving/sweeping - p->nBTLimitBeg = 2; // starting backtrack limit - p->nBTlimitMulti = 8; // multiple of backtrack limiter + p->nBTLimit = 1000; // conflict limit at a node + p->TimeLimit = 0; // the runtime limit in seconds + p->fFirstStop = 0; // stop on the first sat output p->fUseSmartCnf = 0; // use smart CNF computation p->fRewriting = 0; // enables AIG rewriting - p->fSatSweeping = 0; // enables SAT sweeping - p->fFirstStop = 0; // stop on the first sat output - p->fVerbose = 1; // verbose stats + p->fVeryVerbose = 0; // verbose stats + p->fVerbose = 0; // verbose stats } /**Function************************************************************* @@ -124,6 +151,35 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) return pNew; } +/**Function************************************************************* + + Synopsis [Core procedure for simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) +{ + Cec_ManSim_t * pSim; + int RetValue, clkTotal = clock(); + if ( pPars->fSeqSimulate ) + printf( "Performing sequential simulation of %d frames with %d words.\n", + pPars->nWords, pPars->nRounds ); + Aig_ManRandom( 1 ); + pSim = Cec_ManSimStart( pAig, pPars ); + if ( pAig->pReprs == NULL ) + RetValue = Cec_ManSimClassesPrepare( pSim ); + Cec_ManSimClassesRefine( pSim ); + if ( pPars->fCheckMiter ) + printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", + pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds ); + ABC_PRT( "Time", clock() - clkTotal ); + Cec_ManSimStop( pSim ); +} /**Function************************************************************* @@ -136,96 +192,185 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars ) +Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) { + int fOutputResult = 0; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; - Gia_Man_t * pNew; - Cec_ManCsw_t * p; + Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; + Gia_Man_t * pIni, * pSrm, * pTemp; + Cec_ManFra_t * p; + Cec_ManSim_t * pSim; Cec_ManPat_t * pPat; - int i, RetValue, clk, clk2, clkTotal = clock(); + int i, fTimeOut = 0, nMatches = 0, clk, clk2; + double clkTotal = clock(); + + // duplicate AIG and transfer equivalence classes Aig_ManRandom( 1 ); - Gia_ManSetPhase( pAig ); - Gia_ManCleanMark0( pAig ); - Gia_ManCleanMark1( pAig ); - p = Cec_ManCswStart( pAig, pPars ); -clk = clock(); - RetValue = Cec_ManCswClassesPrepare( p ); -p->timeSim += clock() - clk; + pIni = Gia_ManDup(pAig); + pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL; + pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL; + + // prepare the managers + // SAT sweeping + p = Cec_ManFraStart( pIni, pPars ); + if ( pPars->fDoubleOuts ) + pPars->fColorDiff = 1; + // simulation + Cec_ManSimSetDefaultParams( pParsSim ); + pParsSim->nWords = pPars->nWords; + pParsSim->nRounds = pPars->nRounds; + pParsSim->fCheckMiter = pPars->fCheckMiter; + pParsSim->fFirstStop = pPars->fFirstStop; + pParsSim->fDoubleOuts = pPars->fDoubleOuts; + pParsSim->fVerbose = pPars->fVerbose; + pSim = Cec_ManSimStart( p->pAig, pParsSim ); + pSim->nWords = p->pPars->nWords; + // SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->fVerbose = pPars->fVeryVerbose; + // simulation patterns pPat = Cec_ManPatStart(); pPat->fVerbose = pPars->fVeryVerbose; + + // start equivalence classes +clk = clock(); + if ( p->pAig->pReprs == NULL ) + { + if ( Cec_ManSimClassesPrepare(pSim) || Cec_ManSimClassesRefine(pSim) ) + { + Gia_ManStop( p->pAig ); + p->pAig = NULL; + goto finalize; + } + } +p->timeSim += clock() - clk; + // perform solving for ( i = 1; i <= pPars->nItersMax; i++ ) { clk2 = clock(); - pNew = Cec_ManCswSpecReduction( p ); - if ( pPars->fVeryVerbose ) + nMatches = 0; + if ( pPars->fDoubleOuts ) { - Gia_ManPrintStats( p->pAig ); - Gia_ManPrintStats( pNew ); + nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose ); +// p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig ); +// Gia_ManEquivTransform( p->pAig, 1 ); } - if ( Gia_ManCoNum(pNew) == 0 ) + pSrm = Cec_ManFraSpecReduction( p ); + if ( pPars->fVeryVerbose ) + Gia_ManPrintStats( pSrm ); + if ( Gia_ManCoNum(pSrm) == 0 ) { - Gia_ManStop( pNew ); + Gia_ManStop( pSrm ); + if ( p->pPars->fVerbose ) + printf( "Considered all available candidate equivalences.\n" ); + if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) > 0 ) + { + if ( pPars->fColorDiff ) + { + if ( p->pPars->fVerbose ) + printf( "Switching into reduced mode.\n" ); + pPars->fColorDiff = 0; + } + else + { + if ( p->pPars->fVerbose ) + printf( "Switching into normal mode.\n" ); + pPars->fDoubleOuts = 0; + } + continue; + } break; } clk = clock(); - Cec_ManSatSolve( pPat, pNew, pParsSat ); + Cec_ManSatSolve( pPat, pSrm, pParsSat ); p->timeSat += clock() - clk; -clk = clock(); - Cec_ManCswClassesUpdate( p, pPat, pNew ); -p->timeSim += clock() - clk; - Gia_ManStop( pNew ); - pNew = Cec_ManCswDupWithClasses( p ); - Gia_WriteAiger( pNew, "gia_temp_new.aig", 0, 1 ); + if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) ) + { + Gia_ManStop( pSrm ); + Gia_ManStop( p->pAig ); + p->pAig = NULL; + goto finalize; + } + Gia_ManStop( pSrm ); + + // update the manager + pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDoubleOuts ); + Gia_ManStop( pTemp ); if ( p->pPars->fVerbose ) { - printf( "%3d : P =%7d. D =%7d. F =%6d. Lit =%8d. And =%8d. ", - i, p->nAllProved, p->nAllDisproved, p->nAllFailed, - Cec_ManCswCountLitsAll(p), Gia_ManAndNum(pNew) ); + printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", + i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) ); ABC_PRT( "Time", clock() - clk2 ); } - if ( p->pPars->fVeryVerbose ) + if ( Gia_ManAndNum(p->pAig) == 0 ) { - ABC_PRTP( "Sim ", p->timeSim, clock() - clkTotal ); - ABC_PRTP( "Sat ", p->timeSat, clock() - clkTotal ); - ABC_PRT( "Time", clock() - clkTotal ); - printf( "****** Intermedate result %3d ******\n", i ); - Gia_ManPrintStats( p->pAig ); - Gia_ManPrintStats( pNew ); - printf("The result is written into file \"%s\".\n", "gia_temp.aig" ); - printf( "************************************\n" ); + if ( p->pPars->fVerbose ) + printf( "Network after reduction is empty.\n" ); + break; } - if ( Gia_ManAndNum(pNew) == 0 ) + // check resource limits + if ( p->pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit ) { - Gia_ManStop( pNew ); + fTimeOut = 1; break; } - Gia_ManStop( pNew ); +// if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved ) + if ( p->nAllFailed > p->nAllProved + p->nAllDisproved ) + { + if ( pParsSat->nBTLimit >= 10000 ) + break; + pParsSat->nBTLimit *= 10; + if ( p->pPars->fVerbose ) + { + if ( p->pPars->fVerbose ) + printf( "Increasing conflict limit to %d.\n", pParsSat->nBTLimit ); + if ( fOutputResult ) + { + Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 ); + printf("The result is written into file \"%s\".\n", "gia_cec_temp.aig" ); + } + } + } + if ( pPars->fDoubleOuts && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 ) + { + if ( p->pPars->fVerbose ) + printf( "Switching into reduced mode.\n" ); + pPars->fColorDiff = 0; + } + if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) < 20000 ) + { + if ( p->pPars->fVerbose ) + printf( "Switching into normal mode.\n" ); + pPars->fColorDiff = 0; + pPars->fDoubleOuts = 0; + } } - Gia_ManCleanMark0( pAig ); - Gia_ManCleanMark1( pAig ); - - // verify the result +finalize: if ( p->pPars->fVerbose ) { - printf( "Verifying the result:\n" ); - pNew = Cec_ManCswSpecReductionProved( p ); - pParsSat->nBTLimit = 1000000; - pParsSat->fVerbose = 1; - Cec_ManSatSolve( NULL, pNew, pParsSat ); - Gia_ManStop( pNew ); + ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal ); + ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal ); + ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal ); + ABC_PRT( "Time", clock() - clkTotal ); } - // create the resulting miter - pAig->pReprs = Cec_ManCswDeriveReprs( p ); - pNew = Gia_ManDupDfsClasses( pAig ); - Cec_ManCswStop( p ); + pTemp = p->pAig; p->pAig = NULL; + if ( pTemp == NULL ) + printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut ); + else if ( pSim->pCexes ) + printf( "Disproved %d outputs of the miter.\n", pSim->nOuts ); + if ( fTimeOut ) + printf( "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC ); + + pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL; + Cec_ManSimStop( pSim ); Cec_ManPatStop( pPat ); - return pNew; + Cec_ManFraStop( p ); + return pTemp; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h index 309f4292..1898b07c 100644 --- a/src/aig/cec/cecInt.h +++ b/src/aig/cec/cecInt.h @@ -65,6 +65,7 @@ struct Cec_ManPat_t_ int timeSort; // sorting literals int timePack; // packing into sim info structures int timeTotal; // total runtime + int timeTotalSave; // total runtime for saving }; // SAT solving manager @@ -100,38 +101,43 @@ struct Cec_ManSat_t_ int timeTotal; // total runtime }; -// combinational sweeping object -typedef struct Cec_ObjCsw_t_ Cec_ObjCsw_t; -struct Cec_ObjCsw_t_ -{ - int iRepr; // representative node - unsigned iNext : 30; // next node in the class - unsigned iProved : 1; // this node is proved - unsigned iFailed : 1; // this node is failed - unsigned SimNum; // simulation info number -}; - // combinational simulation manager -typedef struct Cec_ManCsw_t_ Cec_ManCsw_t; -struct Cec_ManCsw_t_ +typedef struct Cec_ManSim_t_ Cec_ManSim_t; +struct Cec_ManSim_t_ { // parameters Gia_Man_t * pAig; // the AIG to be used for simulation - Cec_ParCsw_t * pPars; // SAT sweeping parameters + Cec_ParSim_t * pPars; // simulation parameters int nWords; // the number of simulation words - // equivalence classes - Cec_ObjCsw_t * pObjs; // objects used for SAT sweeping // recycable memory + int * pSimInfo; // simulation information offsets unsigned * pMems; // allocated simulaton memory int nWordsAlloc; // the number of allocated entries int nMems; // the number of used entries int nMemsMax; // the max number of used entries int MemFree; // next free entry + int nWordsOld; // the number of simulation words after previous relink + // bug catcher + Vec_Ptr_t * vCiSimInfo; // CI simulation info + Vec_Ptr_t * vCoSimInfo; // CO simulation info + void ** pCexes; // counter-examples for each output + int iOut; // first failed output + int nOuts; // the number of failed outputs + Gia_Cex_t * pCexComb; // counter-example for the first failed output // temporaries Vec_Int_t * vClassOld; // old class numbers Vec_Int_t * vClassNew; // new class numbers Vec_Int_t * vClassTemp; // temporary storage Vec_Int_t * vRefinedC; // refined const reprs +}; + +// combinational simulation manager +typedef struct Cec_ManFra_t_ Cec_ManFra_t; +struct Cec_ManFra_t_ +{ + // parameters + Gia_Man_t * pAig; // the AIG to be used for simulation + Cec_ParFra_t * pPars; // SAT sweeping parameters // simulation patterns Vec_Int_t * vXorNodes; // nodes used in speculative reduction int nAllProved; // total number of proved nodes @@ -139,6 +145,7 @@ struct Cec_ManCsw_t_ int nAllFailed; // total number of failed nodes // runtime stats int timeSim; // unsat + int timePat; // unsat int timeSat; // sat int timeTotal; // total runtime }; @@ -153,29 +160,31 @@ struct Cec_ManCsw_t_ /*=== cecCore.c ============================================================*/ /*=== cecClass.c ============================================================*/ -extern int Cec_ManCswCountLitsAll( Cec_ManCsw_t * p ); -extern int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p ); -extern Gia_Man_t * Cec_ManCswSpecReduction( Cec_ManCsw_t * p ); -extern Gia_Man_t * Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p ); -extern Gia_Man_t * Cec_ManCswDupWithClasses( Cec_ManCsw_t * p ); -extern int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p ); -extern int Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew ); +extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ); +extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p ); +extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ); +/*=== cecIso.c ============================================================*/ +extern int * Cec_ManDetectIsomorphism( Gia_Man_t * p ); /*=== cecMan.c ============================================================*/ -extern Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t * pPars ); -extern void Cec_ManCswStop( Cec_ManCsw_t * p ); -extern Cec_ManPat_t * Cec_ManPatStart(); -extern void Cec_ManPatPrintStats( Cec_ManPat_t * p ); -extern void Cec_ManPatStop( Cec_ManPat_t * p ); extern Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern void Cec_ManSatPrintStats( Cec_ManSat_t * p ); extern void Cec_ManSatStop( Cec_ManSat_t * p ); +extern Cec_ManPat_t * Cec_ManPatStart(); +extern void Cec_ManPatPrintStats( Cec_ManPat_t * p ); +extern void Cec_ManPatStop( Cec_ManPat_t * p ); +extern Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); +extern void Cec_ManSimStop( Cec_ManSim_t * p ); +extern Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * pPars ); +extern void Cec_ManFraStop( Cec_ManFra_t * p ); /*=== cecPat.c ============================================================*/ extern void Cec_ManPatSavePattern( Cec_ManPat_t * pPat, Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWords ); /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); -/*=== cecUtil.c ============================================================*/ +/*=== ceFraeep.c ============================================================*/ +extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ); +extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ); #ifdef __cplusplus } diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c new file mode 100644 index 00000000..08d4b7ec --- /dev/null +++ b/src/aig/cec/cecIso.c @@ -0,0 +1,370 @@ +/**CFile**************************************************************** + + FileName [cecIso.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Detection of structural isomorphism.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline unsigned * Cec_ManIsoInfo( unsigned * pStore, int nWords, int Id ) { return pStore + nWords * Id; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes simulation info for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManIsoSimulate( Gia_Obj_t * pObj, int Id, unsigned * pStore, int nWords ) +{ + unsigned * pInfo = Cec_ManIsoInfo( pStore, nWords, Id ); + unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Gia_ObjFaninId0(pObj, Id) ); + unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, Gia_ObjFaninId1(pObj, Id) ); + int w; + if ( Gia_ObjFaninC0(pObj) ) + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < nWords; w++ ) + pInfo[w] = ~(pInfo0[w] | pInfo1[w]); + else + for ( w = 0; w < nWords; w++ ) + pInfo[w] = ~pInfo0[w] & pInfo1[w]; + } + else + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < nWords; w++ ) + pInfo[w] = pInfo0[w] & ~pInfo1[w]; + else + for ( w = 0; w < nWords; w++ ) + pInfo[w] = pInfo0[w] & pInfo1[w]; + } +} + +/**Function************************************************************* + + Synopsis [Copies simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManIsoCopy( int IdDest, int IdSour, unsigned * pStore, int nWords ) +{ + unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, IdDest ); + unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, IdSour ); + int w; + for ( w = 0; w < nWords; w++ ) + pInfo0[w] = pInfo1[w]; +} + +/**Function************************************************************* + + Synopsis [Compares simulation info of two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManIsoEqual( int Id0, int Id1, unsigned * pStore, int nWords ) +{ + unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id0 ); + unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, Id1 ); + int w; + for ( w = 0; w < nWords; w++ ) + if ( pInfo0[w] != pInfo1[w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Generates random simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords ) +{ + unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id ); + int w; + for ( w = 0; w < nWords; w++ ) + pInfo0[w] = Aig_ManRandom( 0 ); +} + +/**Function************************************************************* + + Synopsis [Computes hash key of the simuation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManIsoHashKey( int Id, unsigned * pStore, int nWords, int nTableSize ) +{ + static int s_Primes[16] = { + 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, + 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; + unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id ); + unsigned uHash = 0; + int i; + for ( i = 0; i < nWords; i++ ) + uHash ^= pInfo0[i] * s_Primes[i & 0xf]; + return (int)(uHash % nTableSize); + +} + +/**Function************************************************************* + + Synopsis [Adds node to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManIsoTableAdd( Gia_Man_t * p, int Id, unsigned * pStore, int nWords, int * pTable, int nTableSize ) +{ + Gia_Obj_t * pTemp; + int Key, Ent, Counter = 0, Color = Gia_ObjColors( p, Id ); + assert( Color == 1 || Color == 2 ); + Key = Gia_ManIsoHashKey( Id, pStore, nWords, nTableSize ); + for ( Ent = pTable[Key], pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL); pTemp; + Ent = pTemp->Value, pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL) ) + { + if ( Gia_ObjColors( p, Ent ) != Color ) + continue; + if ( !Gia_ManIsoEqual( Id, Ent, pStore, nWords ) ) + continue; + // found node with the same color and signature - mark it and do not add new node + pTemp->fMark0 = 1; + return; + } + // did not find the node with the same color and signature - add new node + pTemp = Gia_ManObj( p, Id ); + assert( pTemp->Value == 0 ); + assert( pTemp->fMark0 == 0 ); + pTemp->Value = pTable[Key]; + pTable[Key] = Id; +} + +/**Function************************************************************* + + Synopsis [Extracts equivalence class candidates from one bin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManIsoExtractClasses( Gia_Man_t * p, int Bin, unsigned * pStore, int nWords, Vec_Int_t * vNodesA, Vec_Int_t * vNodesB ) +{ + Gia_Obj_t * pTemp; + int Ent; + Vec_IntClear( vNodesA ); + Vec_IntClear( vNodesB ); + for ( Ent = Bin, pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL); pTemp; + Ent = pTemp->Value, pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL) ) + { + if ( pTemp->fMark0 ) + { + pTemp->fMark0 = 0; + continue; + } + if ( Gia_ObjColors( p, Ent ) == 1 ) + Vec_IntPush( vNodesA, Ent ); + else + Vec_IntPush( vNodesB, Ent ); + } + return Vec_IntSize(vNodesA) > 0 && Vec_IntSize(vNodesB) > 0; +} + +/**Function************************************************************* + + Synopsis [Matches nodes in the extacted classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ManIsoMatchNodes( int * pIso, unsigned * pStore, int nWords, Vec_Int_t * vNodesA, Vec_Int_t * vNodesB ) +{ + int k0, k1, IdA, IdB; + Vec_IntForEachEntry( vNodesA, IdA, k0 ) + Vec_IntForEachEntry( vNodesB, IdB, k1 ) + { + if ( Gia_ManIsoEqual( IdA, IdB, pStore, nWords ) ) + { + assert( pIso[IdA] == 0 ); + assert( pIso[IdB] == 0 ); + assert( IdA != IdB ); + pIso[IdA] = IdB; + pIso[IdB] = IdA; + continue; + } + } +} + +/**Function************************************************************* + + Synopsis [Transforms iso into equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManTransformClasses( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + assert( p->pReprs && p->pNexts && p->pIso ); + memset( p->pReprs, 0, sizeof(int) * Gia_ManObjNum(p) ); + memset( p->pNexts, 0, sizeof(int) * Gia_ManObjNum(p) ); + Gia_ManForEachObj( p, pObj, i ) + { + p->pReprs[i].iRepr = GIA_VOID; + if ( p->pIso[i] && p->pIso[i] < i ) + { + p->pReprs[i].iRepr = p->pIso[i]; + p->pNexts[p->pIso[i]] = i; + } + } +} + +/**Function************************************************************* + + Synopsis [Finds node correspondences in the miter.] + + Description [Assumes that the colors are assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Cec_ManDetectIsomorphism( Gia_Man_t * p ) +{ + int nWords = 2; + Gia_Obj_t * pObj; + Vec_Int_t * vNodesA, * vNodesB; + unsigned * pStore, Counter; + int i, * pIso, * pTable, nTableSize; + // start equivalence classes + pIso = ABC_CALLOC( int, Gia_ManObjNum(p) ); + Gia_ManForEachObj( p, pObj, i ) + { + if ( Gia_ObjIsCo(pObj) ) + { + assert( Gia_ObjColors(p, i) == 0 ); + continue; + } + assert( Gia_ObjColors(p, i) ); + if ( Gia_ObjColors(p, i) == 3 ) + pIso[i] = i; + } + // start simulation info + pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords ); + // simulate and create table + nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 ); + pTable = ABC_CALLOC( int, nTableSize ); + Gia_ManCleanValue( p ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsCo(pObj) ) + continue; + if ( pIso[i] == 0 ) // simulate + Gia_ManIsoSimulate( pObj, i, pStore, nWords ); + else if ( pIso[i] < i ) // copy + Gia_ManIsoCopy( i, pIso[i], pStore, nWords ); + else // generate + Gia_ManIsoRandom( i, pStore, nWords ); + if ( pIso[i] == 0 ) + Gia_ManIsoTableAdd( p, i, pStore, nWords, pTable, nTableSize ); + } + // create equivalence classes + vNodesA = Vec_IntAlloc( 100 ); + vNodesB = Vec_IntAlloc( 100 ); + for ( i = 0; i < nTableSize; i++ ) + if ( Gia_ManIsoExtractClasses( p, pTable[i], pStore, nWords, vNodesA, vNodesB ) ) + Gia_ManIsoMatchNodes( pIso, pStore, nWords, vNodesA, vNodesB ); + Vec_IntFree( vNodesA ); + Vec_IntFree( vNodesB ); + // collect info + Counter = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + Counter += (pIso[i] && pIso[i] < i); +/* + if ( pIso[i] && pIso[i] < i ) + { + if ( (Gia_ObjIsHead(p,pIso[i]) && Gia_ObjRepr(p,i)==pIso[i]) || + (Gia_ObjIsClass(p,pIso[i]) && Gia_ObjRepr(p,i)==Gia_ObjRepr(p,pIso[i])) ) + printf( "1" ); + else + printf( "0" ); + } +*/ + } + printf( "Computed %d pairs of structurally equivalent nodes.\n", Counter ); +// p->pIso = pIso; +// Cec_ManTransformClasses( p ); + + ABC_FREE( pTable ); + ABC_FREE( pStore ); + return pIso; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c index b8ee75b2..1a94409f 100644 --- a/src/aig/cec/cecMan.c +++ b/src/aig/cec/cecMan.c @@ -30,7 +30,7 @@ /**Function************************************************************* - Synopsis [Creates AIG.] + Synopsis [Creates the manager.] Description [] @@ -39,26 +39,25 @@ SeeAlso [] ***********************************************************************/ -Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t * pPars ) -{ - Cec_ManCsw_t * p; - p = ABC_ALLOC( Cec_ManCsw_t, 1 ); - memset( p, 0, sizeof(Cec_ManCsw_t) ); - p->pAig = pAig; - p->pPars = pPars; - p->pObjs = ABC_CALLOC( Cec_ObjCsw_t, Gia_ManObjNum(pAig) ); - // temporaries - p->vClassOld = Vec_IntAlloc( 1000 ); - p->vClassNew = Vec_IntAlloc( 1000 ); - p->vClassTemp = Vec_IntAlloc( 1000 ); - p->vRefinedC = Vec_IntAlloc( 10000 ); - p->vXorNodes = Vec_IntAlloc( 1000 ); +Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +{ + Cec_ManSat_t * p; + // create interpolation manager + p = ABC_ALLOC( Cec_ManSat_t, 1 ); + memset( p, 0, sizeof(Cec_ManSat_t) ); + p->pPars = pPars; + p->pAig = pAig; + // SAT solving + p->nSatVars = 1; + p->pSatVars = ABC_CALLOC( int, Gia_ManObjNum(pAig) ); + p->vUsedNodes = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); return p; } /**Function************************************************************* - Synopsis [Deletes AIG.] + Synopsis [Prints statistics of the manager.] Description [] @@ -67,19 +66,46 @@ Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t * pPars ) SeeAlso [] ***********************************************************************/ -void Cec_ManCswStop( Cec_ManCsw_t * p ) +void Cec_ManSatPrintStats( Cec_ManSat_t * p ) { - Vec_IntFree( p->vXorNodes ); - Vec_IntFree( p->vClassOld ); - Vec_IntFree( p->vClassNew ); - Vec_IntFree( p->vClassTemp ); - Vec_IntFree( p->vRefinedC ); - ABC_FREE( p->pMems ); - ABC_FREE( p->pObjs ); + printf( "CO = %6d ", Gia_ManCoNum(p->pAig) ); + printf( "Conf = %5d ", p->pPars->nBTLimit ); + printf( "MinVar = %5d ", p->pPars->nSatVarMax ); + printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle ); + printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", + p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 ); + ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal ); + printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ", + p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 ); + ABC_PRTP( "Time", p->timeSatSat, p->timeTotal ); + printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ", + p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 ); + ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatStop( Cec_ManSat_t * p ) +{ + if ( p->pSat ) + sat_solver_delete( p->pSat ); + Vec_PtrFree( p->vUsedNodes ); + Vec_PtrFree( p->vFanins ); + ABC_FREE( p->pSatVars ); ABC_FREE( p ); } + /**Function************************************************************* Synopsis [Creates AIG.] @@ -147,9 +173,11 @@ void Cec_ManPatStop( Cec_ManPat_t * p ) ABC_FREE( p ); } + + /**Function************************************************************* - Synopsis [Creates the manager.] + Synopsis [Creates AIG.] Description [] @@ -158,25 +186,31 @@ void Cec_ManPatStop( Cec_ManPat_t * p ) SeeAlso [] ***********************************************************************/ -Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) -{ - Cec_ManSat_t * p; - // create interpolation manager - p = ABC_ALLOC( Cec_ManSat_t, 1 ); - memset( p, 0, sizeof(Cec_ManSat_t) ); - p->pPars = pPars; - p->pAig = pAig; - // SAT solving - p->nSatVars = 1; - p->pSatVars = ABC_CALLOC( int, Gia_ManObjNum(pAig) ); - p->vUsedNodes = Vec_PtrAlloc( 1000 ); - p->vFanins = Vec_PtrAlloc( 100 ); +Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) +{ + Cec_ManSim_t * p; + p = ABC_ALLOC( Cec_ManSim_t, 1 ); + memset( p, 0, sizeof(Cec_ManSim_t) ); + p->pAig = pAig; + p->pPars = pPars; + p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) ); + p->vClassOld = Vec_IntAlloc( 1000 ); + p->vClassNew = Vec_IntAlloc( 1000 ); + p->vClassTemp = Vec_IntAlloc( 1000 ); + p->vRefinedC = Vec_IntAlloc( 10000 ); + p->vCiSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(p->pAig), pPars->nWords ); + if ( pPars->fCheckMiter || Gia_ManRegNum(p->pAig) ) + { + p->vCoSimInfo = Vec_PtrAllocSimInfo( Gia_ManCoNum(p->pAig), pPars->nWords ); + Vec_PtrCleanSimInfo( p->vCoSimInfo, 0, pPars->nWords ); + } + p->iOut = -1; return p; } /**Function************************************************************* - Synopsis [Prints statistics of the manager.] + Synopsis [Deletes AIG.] Description [] @@ -185,26 +219,27 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) SeeAlso [] ***********************************************************************/ -void Cec_ManSatPrintStats( Cec_ManSat_t * p ) +void Cec_ManSimStop( Cec_ManSim_t * p ) { - printf( "CO = %6d ", Gia_ManCoNum(p->pAig) ); - printf( "Conf = %5d ", p->pPars->nBTLimit ); - printf( "MinVar = %5d ", p->pPars->nSatVarMax ); - printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle ); - printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", - p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 ); - ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal ); - printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ", - p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 ); - ABC_PRTP( "Time", p->timeSatSat, p->timeTotal ); - printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ", - p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 ); - ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal ); + Vec_IntFree( p->vClassOld ); + Vec_IntFree( p->vClassNew ); + Vec_IntFree( p->vClassTemp ); + Vec_IntFree( p->vRefinedC ); + if ( p->vCiSimInfo ) + Vec_PtrFree( p->vCiSimInfo ); + if ( p->vCoSimInfo ) + Vec_PtrFree( p->vCoSimInfo ); + ABC_FREE( p->pCexComb ); + ABC_FREE( p->pCexes ); + ABC_FREE( p->pMems ); + ABC_FREE( p->pSimInfo ); + ABC_FREE( p ); } + /**Function************************************************************* - Synopsis [Frees the manager.] + Synopsis [Creates AIG.] Description [] @@ -213,16 +248,35 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p ) SeeAlso [] ***********************************************************************/ -void Cec_ManSatStop( Cec_ManSat_t * p ) +Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) +{ + Cec_ManFra_t * p; + p = ABC_ALLOC( Cec_ManFra_t, 1 ); + memset( p, 0, sizeof(Cec_ManFra_t) ); + p->pAig = pAig; + p->pPars = pPars; + p->vXorNodes = Vec_IntAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deletes AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManFraStop( Cec_ManFra_t * p ) { - if ( p->pSat ) - sat_solver_delete( p->pSat ); - Vec_PtrFree( p->vUsedNodes ); - Vec_PtrFree( p->vFanins ); - ABC_FREE( p->pSatVars ); + Vec_IntFree( p->vXorNodes ); ABC_FREE( p ); } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c index 1af4f333..b80f1e44 100644 --- a/src/aig/cec/cecPat.c +++ b/src/aig/cec/cecPat.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [cec.c] + FileName [cecPat.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Combinatinoal equivalence checking.] - Synopsis [] + Synopsis [Simulation pattern manager.] Author [Alan Mishchenko] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: cec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: cecPat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c new file mode 100644 index 00000000..dbd3bd5e --- /dev/null +++ b/src/aig/cec/cecSim.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [cecSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Simulation manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index e4daf719..ba4b0477 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -388,6 +388,70 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) p->nCallsSince = 0; } +/**Function************************************************************* + + Synopsis [Sets variable activities in the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMin, int LevelMax ) +{ + float dActConeBumpMax = 20.0; + int iVar; + // skip visited variables + if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p->pAig, pObj); + // add the PI to the list + if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) ) + return; + // set the factor of this variable + // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump + if ( (iVar = Cec_ObjSatNum(p,pObj)) ) + { + p->pSat->factors[iVar] = dActConeBumpMax * (Gia_ObjLevel(p->pAig, pObj) - LevelMin)/(LevelMax - LevelMin); + veci_push(&p->pSat->act_vars, iVar); + } + // explore the fanins + Cec_SetActivityFactors_rec( p, Gia_ObjFanin0(pObj), LevelMin, LevelMax ); + Cec_SetActivityFactors_rec( p, Gia_ObjFanin1(pObj), LevelMin, LevelMax ); +} + +/**Function************************************************************* + + Synopsis [Sets variable activities in the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj ) +{ + float dActConeRatio = 0.5; + int LevelMin, LevelMax; + // reset the active variables + veci_resize(&p->pSat->act_vars, 0); + // prepare for traversal + Gia_ManIncrementTravId( p->pAig ); + // determine the min and max level to visit + assert( dActConeRatio > 0 && dActConeRatio < 1 ); + LevelMax = Gia_ObjLevel(p->pAig,pObj); + LevelMin = (int)(LevelMax * (1.0 - dActConeRatio)); + // traverse + Cec_SetActivityFactors_rec( p, pObj, LevelMin, LevelMax ); +//Cec_PrintActivity( p ); + return 1; +} + + /**Function************************************************************* Synopsis [Runs equivalence test for the two nodes.] @@ -402,7 +466,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { int nBTLimit = p->pPars->nBTLimit; - int Lit, RetValue, status, clk, nConflicts; + int Lit, RetValue, status, clk, clk2, nConflicts; p->nCallsSince++; // experiment with this!!! p->nSatTotal++; @@ -415,7 +479,14 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) Cec_ManSatSolverRecycle( p ); // if the nodes do not have SAT variables, allocate them +clk2 = clock(); Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) ); +//ABC_PRT( "cnf", clock() - clk2 ); +//printf( "%d \n", p->pSat->size ); + +clk2 = clock(); +// Cec_SetActivityFactors( p, Gia_ObjFanin0(pObj) ); +//ABC_PRT( "act", clock() - clk2 ); // propage unit clauses if ( p->pSat->qtail != p->pSat->qhead ) @@ -435,8 +506,12 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); clk = clock(); nConflicts = p->pSat->stats.conflicts; + +clk2 = clock(); RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +//ABC_PRT( "sat", clock() - clk2 ); + if ( RetValue == l_False ) { p->timeSatUnsat += clock() - clk; @@ -466,6 +541,7 @@ p->timeSatUndec += clock() - clk; } } + /**Function************************************************************* Synopsis [Performs one round of solving for the POs of the AIG.] @@ -486,7 +562,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; Gia_Obj_t * pObj; - int i, status, clk = clock(); + int i, status, clk = clock(), clk2; // sprintf( Buffer, "gia%03d.aig", Counter++ ); //Gia_WriteAiger( pAig, Buffer, 0, 0 ); @@ -499,8 +575,9 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar pPat->nPats = 0; pPat->nPatLits = 0; pPat->nPatLitsMin = 0; - } + } Gia_ManSetPhase( pAig ); + Gia_ManLevelNum( pAig ); Gia_ManResetTravId( pAig ); p = Cec_ManSatCreate( pAig, pPars ); pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); @@ -512,12 +589,18 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar pObj->fMark1 = 1; continue; } -//printf( "Output %6d : ", i ); - Bar_ProgressUpdate( pProgress, i, "SAT..." ); +clk2 = clock(); status = Cec_ManSatCheckNode( p, pObj ); pObj->fMark0 = (status == 0); pObj->fMark1 = (status == 1); +/* +printf( "Output %6d : ", i ); +printf( "conf = %6d ", p->pSat->stats.conflicts ); +printf( "prop = %6d ", p->pSat->stats.propagations ); +ABC_PRT( "time", clock() - clk2 ); +*/ + /* if ( status == -1 ) { @@ -531,7 +614,11 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar continue; // save the pattern if ( pPat ) + { + int clk3 = clock(); Cec_ManPatSavePattern( pPat, p, pObj ); + pPat->timeTotalSave += clock() - clk3; + } // quit if one of them is solved if ( pPars->fFirstStop ) break; diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c new file mode 100644 index 00000000..20a668bd --- /dev/null +++ b/src/aig/cec/cecSweep.c @@ -0,0 +1,294 @@ +/**CFile**************************************************************** + + FileName [ceFraeep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [SAT sweeping manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ceFraeep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs limited speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + int iRes0, iRes1, iRepr, iNode, iMiter; + int i, fCompl, * piCopies, * pDepths; + Gia_ManSetPhase( p->pAig ); + Vec_IntClear( p->vXorNodes ); + if ( p->pPars->nLevelMax ) + Gia_ManLevelNum( p->pAig ); + pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); + pNew->pName = Aig_UtilStrsav( p->pAig->pName ); + Gia_ManHashAlloc( pNew ); + piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); + pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); + piCopies[0] = 0; + Gia_ManForEachObj1( p->pAig, pObj, i ) + { + if ( Gia_ObjIsCi(pObj) ) + { + piCopies[i] = Gia_ManAppendCi( pNew ); + continue; + } + if ( Gia_ObjIsCo(pObj) ) + continue; + if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 || + piCopies[Gia_ObjFaninId1(pObj,i)] == -1 ) + continue; + iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); + iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); + iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); + pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); + if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) ) + continue; + assert( Gia_ObjRepr(p->pAig, i) < i ); + iRepr = piCopies[Gia_ObjRepr(p->pAig, i)]; + if ( iRepr == -1 ) + continue; + if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) ) + continue; + if ( p->pPars->nLevelMax && + (Gia_ObjLevel(p->pAig, pObj) > p->pPars->nLevelMax || + Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) ) + continue; + if ( p->pPars->fDoubleOuts ) + { +// if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) ) +// Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 ); + if ( p->pPars->fColorDiff ) + { + if ( !Gia_ObjDiffColors( p->pAig, Gia_ObjRepr(p->pAig, i), i ) ) + continue; + } + else + { + if ( !Gia_ObjDiffColors2( p->pAig, Gia_ObjRepr(p->pAig, i), i ) ) + continue; + } + } + pRepr = Gia_ManObj( p->pAig, Gia_ObjRepr(p->pAig, i) ); + fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr); + piCopies[i] = Gia_LitNotCond( iRepr, fCompl ); + if ( Gia_ObjProved(p->pAig, i) ) + continue; + // produce speculative miter + iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] ); + Gia_ManAppendCo( pNew, iMiter ); + Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) ); + Vec_IntPush( p->vXorNodes, i ); + // add to the depth of this node + pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] ); + if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax ) + piCopies[i] = -1; + } + ABC_FREE( piCopies ); + ABC_FREE( pDepths ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, 0 ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManFraClassesUpdate_rec( Gia_Obj_t * pObj ) +{ + int Result; + if ( pObj->fMark0 ) + return 1; + if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) ) + return 0; + Result = (Cec_ManFraClassesUpdate_rec( Gia_ObjFanin0(pObj) ) | + Cec_ManFraClassesUpdate_rec( Gia_ObjFanin1(pObj) )); + return pObj->fMark0 = Result; +} + +/**Function************************************************************* + + Synopsis [Creates simulation info for this round.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManFraCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vCiInfo, Vec_Ptr_t * vInfo, int nSeries ) +{ + unsigned * pRes0, * pRes1; + int i, w; + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + { + pRes0 = Vec_PtrEntry( vCiInfo, i ); + pRes1 = Vec_PtrEntry( vInfo, i ); + pRes1 += p->nWords * nSeries; + for ( w = 0; w < p->nWords; w++ ) + pRes0[w] = pRes1[w]; + } +} + +/**Function************************************************************* + + Synopsis [Updates equivalence classes using the patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ) +{ + Vec_Ptr_t * vInfo; + Gia_Obj_t * pObj, * pObjOld, * pReprOld; + int i, k, iRepr, iNode, clk; +clk = clock(); + vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords ); +p->timePat += clock() - clk; +clk = clock(); + if ( vInfo != NULL ) + { + Gia_ManSetRefs( p->pAig ); + for ( i = 0; i < pPat->nSeries; i++ ) + { + Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i ); + if ( Cec_ManSimSimulateRound( pSim, pSim->vCiSimInfo, pSim->vCoSimInfo ) ) + { + Vec_PtrFree( vInfo ); + return 1; + } + } + Vec_PtrFree( vInfo ); + } +p->timeSim += clock() - clk; + assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) ); + // mark the transitive fanout of failed nodes + if ( p->pPars->nDepthMax != 1 ) + { + Gia_ManCleanMark0( p->pAig ); + Gia_ManCleanMark1( p->pAig ); + Gia_ManForEachCo( pNew, pObj, k ) + { + iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); + iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); + if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved + continue; +// Gia_ManObj(p->pAig, iRepr)->fMark0 = 1; + Gia_ManObj(p->pAig, iNode)->fMark0 = 1; + } + // mark the nodes reachable through the failed nodes + Gia_ManForEachAnd( p->pAig, pObjOld, k ) + pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0); + // unmark the disproved nodes + Gia_ManForEachCo( pNew, pObj, k ) + { + iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); + iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); + if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved + continue; + pObjOld = Gia_ManObj(p->pAig, iNode); + assert( pObjOld->fMark0 == 1 ); + if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 ) + pObjOld->fMark1 = 1; + } + // clean marks + Gia_ManForEachAnd( p->pAig, pObjOld, k ) + if ( pObjOld->fMark1 ) + { + pObjOld->fMark0 = 0; + pObjOld->fMark1 = 0; + } + } + // set the results + p->nAllProved = p->nAllDisproved = p->nAllFailed = 0; + Gia_ManForEachCo( pNew, pObj, k ) + { + iRepr = Vec_IntEntry( p->vXorNodes, 2*k ); + iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 ); + pReprOld = Gia_ManObj(p->pAig, iRepr); + pObjOld = Gia_ManObj(p->pAig, iNode); + if ( pObj->fMark1 ) + { // proved + assert( pObj->fMark0 == 0 ); + assert( !Gia_ObjProved(p->pAig, iNode) ); + if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 ) +// if ( pObjOld->fMark0 == 0 ) + { + assert( iRepr == Gia_ObjRepr(p->pAig, iNode) ); + Gia_ObjSetProved( p->pAig, iNode ); + p->nAllProved++; + } + } + else if ( pObj->fMark0 ) + { // disproved + assert( pObj->fMark1 == 0 ); + if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 ) +// if ( pObjOld->fMark0 == 0 ) + { + if ( iRepr == Gia_ObjRepr(p->pAig, iNode) ) + printf( "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" ); + p->nAllDisproved++; + } + } + else + { // failed + assert( pObj->fMark0 == 0 ); + assert( pObj->fMark1 == 0 ); + assert( !Gia_ObjFailed(p->pAig, iNode) ); + assert( !Gia_ObjProved(p->pAig, iNode) ); + Gia_ObjSetFailed( p->pAig, iNode ); + p->nAllFailed++; + } + } + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make index f8e2602a..4618c424 100644 --- a/src/aig/cec/module.make +++ b/src/aig/cec/module.make @@ -1,5 +1,9 @@ -SRC += src/aig/cec/cecClass.c \ +SRC += src/aig/cec/cecCec.c \ + src/aig/cec/cecClass.c \ src/aig/cec/cecCore.c \ + src/aig/cec/cecIso.c \ src/aig/cec/cecMan.c \ src/aig/cec/cecPat.c \ - src/aig/cec/cecSolve.c + src/aig/cec/cecSim.c \ + src/aig/cec/cecSolve.c \ + src/aig/cec/cecSweep.c -- cgit v1.2.3