/**CFile**************************************************************** FileName [ivyFraig.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [And-Inverter Graph package.] Synopsis [Functional reduction of AIGs] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - May 11, 2006.] Revision [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] ***********************************************************************/ #include #include "sat/bsat/satSolver.h" #include "misc/extra/extra.h" #include "ivy.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t; typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t; typedef struct Ivy_FraigList_t_ Ivy_FraigList_t; struct Ivy_FraigList_t_ { Ivy_Obj_t * pHead; Ivy_Obj_t * pTail; int nItems; }; struct Ivy_FraigSim_t_ { int Type; Ivy_FraigSim_t * pNext; Ivy_FraigSim_t * pFanin0; Ivy_FraigSim_t * pFanin1; unsigned pData[0]; }; struct Ivy_FraigMan_t_ { // general info Ivy_FraigParams_t * pParams; // various parameters // temporary backtrack limits because "ABC_INT64_T" cannot be defined in Ivy_FraigParams_t ... ABC_INT64_T nBTLimitGlobal; // global limit on the number of backtracks ABC_INT64_T nInsLimitGlobal;// global limit on the number of clause inspects // AIG manager Ivy_Man_t * pManAig; // the starting AIG manager Ivy_Man_t * pManFraig; // the final AIG manager // simulation information int nSimWords; // the number of words char * pSimWords; // the simulation info Ivy_FraigSim_t * pSimStart; // the list of simulation info for internal nodes // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example int * pPatScores; // the scores of each pattern // equivalence classes Ivy_FraigList_t lClasses; // equivalence classes Ivy_FraigList_t lCand; // candidatates int nPairs; // the number of pairs of nodes // equivalence checking sat_solver * pSat; // SAT solver int nSatVars; // the number of variables currently used Vec_Ptr_t * vPiVars; // the PIs of the cone used // other ProgressBar * pProgress; // statistics int nSimRounds; int nNodesMiter; int nClassesZero; int nClassesBeg; int nClassesEnd; int nPairsBeg; int nPairsEnd; int nSatCalls; int nSatCallsSat; int nSatCallsUnsat; int nSatProof; int nSatFails; int nSatFailsReal; // runtime abctime timeSim; abctime timeTrav; abctime timeSat; abctime timeSatUnsat; abctime timeSatSat; abctime timeSatFail; abctime timeRef; abctime timeTotal; abctime time1; abctime time2; }; typedef struct Prove_ParamsStruct_t_ Prove_Params_t; struct Prove_ParamsStruct_t_ { // general parameters int fUseFraiging; // enables fraiging int fUseRewriting; // enables rewriting int fUseBdds; // enables BDD construction when other methods fail int fVerbose; // prints verbose stats // iterations int nItersMax; // the number of iterations // mitering int nMiteringLimitStart; // starting mitering limit float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration // rewriting int nRewritingLimitStart; // the number of rewriting iterations float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration // fraiging int nFraigingLimitStart; // starting backtrack(conflict) limit float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration // last-gasp BDD construction int nBddSizeLimit; // the number of BDD nodes when construction is aborted int fBddReorder; // enables dynamic BDD variable reordering // last-gasp mitering int nMiteringLimitLast; // final mitering limit // global SAT solver limits ABC_INT64_T nTotalBacktrackLimit; // global limit on the number of backtracks ABC_INT64_T nTotalInspectLimit; // global limit on the number of clause inspects // global resources applied ABC_INT64_T nTotalBacktracksMade; // the total number of backtracks made ABC_INT64_T nTotalInspectsMade; // the total number of inspects made }; static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; } static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; } static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; } static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; } static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; } static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; } static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj ) { return pObj->pPrevFan1; } static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj ) { return pObj->pEquiv; } static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)(ABC_PTRUINT_T)pObj->pNextFan0; } static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; } static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; } static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; } static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; } static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; } static inline void Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; } static inline void Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; } static inline void Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; } static inline void Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode ) { pObj->pEquiv = pNode; } static inline void Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num ) { pObj->pNextFan0 = (Ivy_Obj_t *)(ABC_PTRUINT_T)Num; } static inline void Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins ) { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; } static inline unsigned Ivy_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } // iterate through equivalence classes #define Ivy_FraigForEachEquivClass( pList, pEnt ) \ for ( pEnt = pList; \ pEnt; \ pEnt = Ivy_ObjEquivListNext(pEnt) ) #define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 ) \ for ( pEnt = pList, \ pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL; \ pEnt; \ pEnt = pEnt2, \ pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL ) // iterate through nodes in one class #define Ivy_FraigForEachClassNode( pClass, pEnt ) \ for ( pEnt = pClass; \ pEnt; \ pEnt = Ivy_ObjClassNodeNext(pEnt) ) // iterate through nodes in the hash table #define Ivy_FraigForEachBinNode( pBin, pEnt ) \ for ( pEnt = pBin; \ pEnt; \ pEnt = Ivy_ObjNodeHashNext(pEnt) ) static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); static Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T * pnSatConfs, ABC_INT64_T * pnSatInspects ); static void Ivy_FraigPrint( Ivy_FraigMan_t * p ); static void Ivy_FraigStop( Ivy_FraigMan_t * p ); static void Ivy_FraigSimulate( Ivy_FraigMan_t * p ); static void Ivy_FraigSweep( Ivy_FraigMan_t * p ); static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ); static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ); static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ); static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ); static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ); static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew ); static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan ); static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ); static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose ); static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p ); static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 ); static int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit ); static ABC_INT64_T s_nBTLimitGlobal = 0; static ABC_INT64_T s_nInsLimitGlobal = 0; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Sets the default solving parameters.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ) { memset( pParams, 0, sizeof(Ivy_FraigParams_t) ); pParams->nSimWords = 32; // the number of words in the simulation info pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached pParams->fPatScores = 0; // enables simulation pattern scoring pParams->MaxScore = 25; // max score after which resimulation is used pParams->fDoSparse = 1; // skips sparse functions // pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped // pParams->dActConeBumpMax = 5.0; // the largest bump of activity pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped pParams->dActConeBumpMax = 10.0; // the largest bump of activity pParams->nBTLimitNode = 100; // conflict limit at a node pParams->nBTLimitMiter = 500000; // conflict limit at an output // pParams->nBTLimitGlobal = 0; // conflict limit global // pParams->nInsLimitGlobal = 0; // inspection limit global } /**Function************************************************************* Synopsis [Performs combinational equivalence checking for the miter.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) { Prove_Params_t * pParams = (Prove_Params_t *)pPars; Ivy_FraigParams_t Params, * pIvyParams = &Params; Ivy_Man_t * pManAig, * pManTemp; int RetValue, nIter; abctime clk;//, Counter; ABC_INT64_T nSatConfs = 0, nSatInspects = 0; // start the network and parameters pManAig = *ppManAig; Ivy_FraigParamsDefault( pIvyParams ); pIvyParams->fVerbose = pParams->fVerbose; pIvyParams->fProve = 1; if ( pParams->fVerbose ) { printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n", pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" ); printf( "Miter = %d (%3.1f). Rwr = %d (%3.1f). Fraig = %d (%3.1f). Last = %d.\n", pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti, pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti, pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti, pParams->nMiteringLimitLast ); } // if SAT only, solve without iteration if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) { clk = Abc_Clock(); pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig); pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); *ppManAig = pManAig; return RetValue; } if ( Ivy_ManNodeNum(pManAig) < 500 ) { // run the first mitering clk = Abc_Clock(); pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig); pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); if ( RetValue >= 0 ) { *ppManAig = pManAig; return RetValue; } } // check the current resource limits RetValue = -1; for ( nIter = 0; nIter < pParams->nItersMax; nIter++ ) { if ( pParams->fVerbose ) { printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) ); fflush( stdout ); } // try rewriting if ( pParams->fUseRewriting ) { // bug in Ivy_NodeFindCutsAll() when leaves are identical! /* clk = Abc_Clock(); Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); pManAig = Ivy_ManRwsat( pManAig, 0 ); RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose ); */ } if ( RetValue >= 0 ) break; // catch the situation when ref pattern detects the bug RetValue = Ivy_FraigMiterStatus( pManAig ); if ( RetValue >= 0 ) break; // try fraiging followed by mitering if ( pParams->fUseFraiging ) { clk = Abc_Clock(); pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)); pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig); pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp ); RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose ); } if ( RetValue >= 0 ) break; // add to the number of backtracks and inspects pParams->nTotalBacktracksMade += nSatConfs; pParams->nTotalInspectsMade += nSatInspects; // check if global resource limit is reached if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) || (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) ) { printf( "Reached global limit on conflicts/inspects. Quitting.\n" ); *ppManAig = pManAig; return -1; } } /* if ( RetValue < 0 ) { if ( pParams->fVerbose ) { printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast ); fflush( stdout ); } clk = Abc_Clock(); pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig); if ( pParams->nTotalBacktrackLimit ) s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade; if ( pParams->nTotalInspectLimit ) s_nInsLimitGlobal = pParams->nTotalInspectLimit - pParams->nTotalInspectsMade; pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); s_nBTLimitGlobal = 0; s_nInsLimitGlobal = 0; RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); // make sure that the sover never returns "undecided" when infinite resource limits are set if( RetValue == -1 && pParams->nTotalInspectLimit == 0 && pParams->nTotalBacktrackLimit == 0 ) { extern void Prove_ParamsPrint( Prove_Params_t * pParams ); Prove_ParamsPrint( pParams ); printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n"); exit(1); } } */ // assign the model if it was proved by rewriting (const 1 miter) if ( RetValue == 0 && pManAig->pData == NULL ) { pManAig->pData = ABC_ALLOC( int, Ivy_ManPiNum(pManAig) ); memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) ); } *ppManAig = pManAig; return RetValue; } /**Function************************************************************* Synopsis [Performs fraiging of the AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T * pnSatConfs, ABC_INT64_T * pnSatInspects ) { Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; abctime clk; if ( Ivy_ManNodeNum(pManAig) == 0 ) return Ivy_ManDup(pManAig); clk = Abc_Clock(); assert( Ivy_ManLatchNum(pManAig) == 0 ); p = Ivy_FraigStart( pManAig, pParams ); // set global limits p->nBTLimitGlobal = nBTLimitGlobal; p->nInsLimitGlobal = nInsLimitGlobal; Ivy_FraigSimulate( p ); Ivy_FraigSweep( p ); pManAigNew = p->pManFraig; p->timeTotal = Abc_Clock() - clk; if ( pnSatConfs ) *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0; if ( pnSatInspects ) *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0; Ivy_FraigStop( p ); return pManAigNew; } /**Function************************************************************* Synopsis [Performs fraiging of the AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; abctime clk; if ( Ivy_ManNodeNum(pManAig) == 0 ) return Ivy_ManDup(pManAig); clk = Abc_Clock(); assert( Ivy_ManLatchNum(pManAig) == 0 ); p = Ivy_FraigStart( pManAig, pParams ); Ivy_FraigSimulate( p ); Ivy_FraigSweep( p ); pManAigNew = p->pManFraig; p->timeTotal = Abc_Clock() - clk; Ivy_FraigStop( p ); return pManAigNew; } /**Function************************************************************* Synopsis [Applies brute-force SAT to the miter.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; Ivy_Obj_t * pObj; int i; abctime clk; clk = Abc_Clock(); assert( Ivy_ManLatchNum(pManAig) == 0 ); p = Ivy_FraigStartSimple( pManAig, pParams ); // set global limits p->nBTLimitGlobal = s_nBTLimitGlobal; p->nInsLimitGlobal = s_nInsLimitGlobal; // duplicate internal nodes Ivy_ManForEachNode( p->pManAig, pObj, i ) pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); // try to prove each output of the miter Ivy_FraigMiterProve( p ); // add the POs Ivy_ManForEachPo( p->pManAig, pObj, i ) Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); // clean the new manager Ivy_ManForEachObj( p->pManFraig, pObj, i ) { if ( Ivy_ObjFaninVec(pObj) ) Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); pObj->pNextFan0 = pObj->pNextFan1 = NULL; } // remove dangling nodes Ivy_ManCleanup( p->pManFraig ); pManAigNew = p->pManFraig; p->timeTotal = Abc_Clock() - clk; //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) ); //ABC_PRT( "Time", p->timeTotal ); Ivy_FraigStop( p ); return pManAigNew; } /**Function************************************************************* Synopsis [Starts the fraiging manager without simulation info.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { Ivy_FraigMan_t * p; // allocat the fraiging manager p = ABC_ALLOC( Ivy_FraigMan_t, 1 ); memset( p, 0, sizeof(Ivy_FraigMan_t) ); p->pParams = pParams; p->pManAig = pManAig; p->pManFraig = Ivy_ManStartFrom( pManAig ); p->vPiVars = Vec_PtrAlloc( 100 ); return p; } /**Function************************************************************* Synopsis [Starts the fraiging manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { Ivy_FraigMan_t * p; Ivy_FraigSim_t * pSims; Ivy_Obj_t * pObj; int i, k, EntrySize; // clean the fanout representation Ivy_ManForEachObj( pManAig, pObj, i ) // pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; assert( !pObj->pEquiv && !pObj->pFanout ); // allocat the fraiging manager p = ABC_ALLOC( Ivy_FraigMan_t, 1 ); memset( p, 0, sizeof(Ivy_FraigMan_t) ); p->pParams = pParams; p->pManAig = pManAig; p->pManFraig = Ivy_ManStartFrom( pManAig ); // allocate simulation info p->nSimWords = pParams->nSimWords; // p->pSimWords = ABC_ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords; p->pSimWords = (char *)ABC_ALLOC( char, Ivy_ManObjNum(pManAig) * EntrySize ); memset( p->pSimWords, 0, EntrySize ); k = 0; Ivy_ManForEachObj( pManAig, pObj, i ) { pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++); pSims->pNext = NULL; if ( Ivy_ObjIsNode(pObj) ) { if ( p->pSimStart == NULL ) p->pSimStart = pSims; else ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims; pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) ); pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) ); pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase; } else { pSims->pFanin0 = NULL; pSims->pFanin1 = NULL; pSims->Type = 0; } Ivy_ObjSetSim( pObj, pSims ); } assert( k == Ivy_ManObjNum(pManAig) ); // allocate storage for sim pattern p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) ); p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords ); p->vPiVars = Vec_PtrAlloc( 100 ); // set random number generator srand( 0xABCABC ); return p; } /**Function************************************************************* Synopsis [Stops the fraiging manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigStop( Ivy_FraigMan_t * p ) { if ( p->pParams->fVerbose ) Ivy_FraigPrint( p ); if ( p->vPiVars ) Vec_PtrFree( p->vPiVars ); if ( p->pSat ) sat_solver_delete( p->pSat ); ABC_FREE( p->pPatScores ); ABC_FREE( p->pPatWords ); ABC_FREE( p->pSimWords ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Prints stats for the fraiging manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigPrint( Ivy_FraigMan_t * p ) { double nMemory; nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20); printf( "SimWords = %d. Rounds = %d. Mem = %0.2f MB. ", p->nSimWords, p->nSimRounds, nMemory ); printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd ); // printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter ); printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero ); printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); ABC_PRT( "AIG simulation ", p->timeSim ); ABC_PRT( "AIG traversal ", p->timeTrav ); ABC_PRT( "SAT solving ", p->timeSat ); ABC_PRT( " Unsat ", p->timeSatUnsat ); ABC_PRT( " Sat ", p->timeSatSat ); ABC_PRT( " Fail ", p->timeSatFail ); ABC_PRT( "Class refining ", p->timeRef ); ABC_PRT( "TOTAL RUNTIME ", p->timeTotal ); if ( p->time1 ) { ABC_PRT( "time1 ", p->time1 ); } } /**Function************************************************************* Synopsis [Assigns random patterns to the PI node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { Ivy_FraigSim_t * pSims; int i; assert( Ivy_ObjIsPi(pObj) ); pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = Ivy_ObjRandomSim(); } /**Function************************************************************* Synopsis [Assigns constant patterns to the PI node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 ) { Ivy_FraigSim_t * pSims; int i; assert( Ivy_ObjIsPi(pObj) ); pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = fConst1? ~(unsigned)0 : 0; } /**Function************************************************************* Synopsis [Assings random simulation info for the PIs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i; Ivy_ManForEachPi( p->pManAig, pObj, i ) Ivy_NodeAssignRandom( p, pObj ); } /**Function************************************************************* Synopsis [Assings distance-1 simulation info for the PIs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat ) { Ivy_Obj_t * pObj; int i, Limit; Ivy_ManForEachPi( p->pManAig, pObj, i ) { Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) ); // printf( "%d", Ivy_InfoHasBit(pPat, i) ); } // printf( "\n" ); Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 ); } /**Function************************************************************* Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { Ivy_FraigSim_t * pSims; int i; pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) if ( pSims->pData[i] ) return 0; return 1; } /**Function************************************************************* Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { Ivy_FraigSim_t * pSims; int i; pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = ~pSims->pData[i]; } /**Function************************************************************* Synopsis [Returns 1 if simulation infos are equal.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) { Ivy_FraigSim_t * pSims0, * pSims1; int i; pSims0 = Ivy_ObjSim(pObj0); pSims1 = Ivy_ObjSim(pObj1); for ( i = 0; i < p->nSimWords; i++ ) if ( pSims0->pData[i] != pSims1->pData[i] ) return 0; return 1; } /**Function************************************************************* Synopsis [Simulates one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims ) { unsigned * pData, * pData0, * pData1; int i; pData = pSims->pData; pData0 = pSims->pFanin0->pData; pData1 = pSims->pFanin1->pData; switch( pSims->Type ) { case 0: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = (pData0[i] & pData1[i]); break; case 1: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = ~(pData0[i] & pData1[i]); break; case 2: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = (pData0[i] & ~pData1[i]); break; case 3: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = (~pData0[i] | pData1[i]); break; case 4: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = (~pData0[i] & pData1[i]); break; case 5: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = (pData0[i] | ~pData1[i]); break; case 6: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = ~(pData0[i] | pData1[i]); break; case 7: for ( i = 0; i < p->nSimWords; i++ ) pData[i] = (pData0[i] | pData1[i]); break; } } /**Function************************************************************* Synopsis [Simulates one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { Ivy_FraigSim_t * pSims, * pSims0, * pSims1; int fCompl, fCompl0, fCompl1, i; assert( !Ivy_IsComplement(pObj) ); // get hold of the simulation information pSims = Ivy_ObjSim(pObj); pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj)); pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj)); // get complemented attributes of the children using their random info fCompl = pObj->fPhase; fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)); fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)); // simulate if ( fCompl0 && fCompl1 ) { if ( fCompl ) for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]); else for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]); } else if ( fCompl0 && !fCompl1 ) { if ( fCompl ) for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]); else for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]); } else if ( !fCompl0 && fCompl1 ) { if ( fCompl ) for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]); else for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]); } else // if ( !fCompl0 && !fCompl1 ) { if ( fCompl ) for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]); else for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]); } } /**Function************************************************************* Synopsis [Computes hash value using simulation info.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { static int s_FPrimes[128] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 }; Ivy_FraigSim_t * pSims; unsigned uHash; int i; assert( p->nSimWords <= 128 ); uHash = 0; pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) uHash ^= pSims->pData[i] * s_FPrimes[i]; return uHash; } /**Function************************************************************* Synopsis [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i; abctime clk; clk = Abc_Clock(); Ivy_ManForEachNode( p->pManAig, pObj, i ) { Ivy_NodeSimulate( p, pObj ); /* if ( Ivy_ObjFraig(pObj) == NULL ) printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase ); else printf( "%3d %3d %2d %d : ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase ); Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 ); printf( "\n" ); */ } p->timeSim += Abc_Clock() - clk; p->nSimRounds++; } /**Function************************************************************* Synopsis [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p ) { Ivy_FraigSim_t * pSims; abctime clk; clk = Abc_Clock(); for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext ) Ivy_NodeSimulateSim( p, pSims ); p->timeSim += Abc_Clock() - clk; p->nSimRounds++; } /**Function************************************************************* Synopsis [Adds one node to the equivalence class.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj ) { if ( Ivy_ObjClassNodeNext(pClass) == NULL ) Ivy_ObjSetClassNodeNext( pClass, pObj ); else Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj ); Ivy_ObjSetClassNodeLast( pClass, pObj ); Ivy_ObjSetClassNodeRepr( pObj, pClass ); Ivy_ObjSetClassNodeNext( pObj, NULL ); } /**Function************************************************************* Synopsis [Adds equivalence class to the list of classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass ) { if ( pList->pHead == NULL ) { pList->pHead = pClass; pList->pTail = pClass; Ivy_ObjSetEquivListPrev( pClass, NULL ); Ivy_ObjSetEquivListNext( pClass, NULL ); } else { Ivy_ObjSetEquivListNext( pList->pTail, pClass ); Ivy_ObjSetEquivListPrev( pClass, pList->pTail ); Ivy_ObjSetEquivListNext( pClass, NULL ); pList->pTail = pClass; } pList->nItems++; } /**Function************************************************************* Synopsis [Updates the list of classes after base class has split.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass ) { Ivy_ObjSetEquivListPrev( pClass, pBase ); Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); if ( Ivy_ObjEquivListNext(pBase) ) Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass ); Ivy_ObjSetEquivListNext( pBase, pClass ); if ( pList->pTail == pBase ) pList->pTail = pClass; pList->nItems++; } /**Function************************************************************* Synopsis [Removes equivalence class from the list of classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass ) { if ( pList->pHead == pClass ) pList->pHead = Ivy_ObjEquivListNext(pClass); if ( pList->pTail == pClass ) pList->pTail = Ivy_ObjEquivListPrev(pClass); if ( Ivy_ObjEquivListPrev(pClass) ) Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); if ( Ivy_ObjEquivListNext(pClass) ) Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) ); Ivy_ObjSetEquivListNext( pClass, NULL ); Ivy_ObjSetEquivListPrev( pClass, NULL ); pClass->fMarkA = 0; pList->nItems--; } /**Function************************************************************* Synopsis [Count the number of pairs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass, * pNode; int nPairs = 0, nNodes; return nPairs; Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass ) { nNodes = 0; Ivy_FraigForEachClassNode( pClass, pNode ) nNodes++; nPairs += nNodes * (nNodes - 1) / 2; } return nPairs; } /**Function************************************************************* Synopsis [Creates initial simulation classes.] Description [Assumes that simulation info is assigned.] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t ** pTable; Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry; int i, nTableSize; unsigned Hash; pConst1 = Ivy_ManConst1(p->pManAig); // allocate the table nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13; pTable = ABC_ALLOC( Ivy_Obj_t *, nTableSize ); memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize ); // collect nodes into the table Ivy_ManForEachObj( p->pManAig, pObj, i ) { if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) ) continue; Hash = Ivy_NodeHash( p, pObj ); if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) ) { Ivy_NodeAddToClass( pConst1, pObj ); continue; } // add the node to the table pBin = pTable[Hash % nTableSize]; Ivy_FraigForEachBinNode( pBin, pEntry ) if ( Ivy_NodeCompareSims( p, pEntry, pObj ) ) { Ivy_NodeAddToClass( pEntry, pObj ); break; } // check if the entry was added if ( pEntry ) continue; Ivy_ObjSetNodeHashNext( pObj, pBin ); pTable[Hash % nTableSize] = pObj; } // collect non-trivial classes assert( p->lClasses.pHead == NULL ); Ivy_ManForEachObj( p->pManAig, pObj, i ) { if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) ) continue; Ivy_ObjSetNodeHashNext( pObj, NULL ); if ( Ivy_ObjClassNodeRepr(pObj) == NULL ) { assert( Ivy_ObjClassNodeNext(pObj) == NULL ); continue; } // recognize the head of the class if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL ) continue; // clean the class representative and add it to the list Ivy_ObjSetClassNodeRepr( pObj, NULL ); Ivy_FraigAddClass( &p->lClasses, pObj ); } // free the table ABC_FREE( pTable ); } /**Function************************************************************* Synopsis [Recursively refines the class after simulation.] Description [Returns 1 if the class has changed.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass ) { Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode; int RetValue = 0; // check if there is refinement pListOld = pClass; Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew ) { if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) ) { if ( p->pParams->fPatScores ) Ivy_FraigAddToPatScores( p, pClass, pClassNew ); break; } pListOld = pClassNew; } if ( pClassNew == NULL ) return 0; // set representative of the new class Ivy_ObjSetClassNodeRepr( pClassNew, NULL ); // start the new list pListNew = pClassNew; // go through the remaining nodes and sort them into two groups: // (1) matches of the old node; (2) non-matches of the old node Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode ) if ( Ivy_NodeCompareSims( p, pClass, pNode ) ) { Ivy_ObjSetClassNodeNext( pListOld, pNode ); pListOld = pNode; } else { Ivy_ObjSetClassNodeNext( pListNew, pNode ); Ivy_ObjSetClassNodeRepr( pNode, pClassNew ); pListNew = pNode; } // finish both lists Ivy_ObjSetClassNodeNext( pListNew, NULL ); Ivy_ObjSetClassNodeNext( pListOld, NULL ); // update the list of classes Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew ); // if the old class is trivial, remove it if ( Ivy_ObjClassNodeNext(pClass) == NULL ) Ivy_FraigRemoveClass( &p->lClasses, pClass ); // if the new class is trivial, remove it; otherwise, try to refine it if ( Ivy_ObjClassNodeNext(pClassNew) == NULL ) Ivy_FraigRemoveClass( &p->lClasses, pClassNew ); else RetValue = Ivy_FraigRefineClass_rec( p, pClassNew ); return RetValue + 1; } /**Function************************************************************* Synopsis [Creates the counter-example from the successful pattern.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { Ivy_FraigSim_t * pSims; int i, k, BestPat, * pModel; // find the word of the pattern pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) if ( pSims->pData[i] ) break; assert( i < p->nSimWords ); // find the bit of the pattern for ( k = 0; k < 32; k++ ) if ( pSims->pData[i] & (1 << k) ) break; assert( k < 32 ); // determine the best pattern BestPat = i * 32 + k; // fill in the counter-example data pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); Ivy_ManForEachPi( p->pManAig, pObj, i ) { pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat); // printf( "%d", pModel[i] ); } // printf( "\n" ); // set the model assert( p->pManFraig->pData == NULL ); p->pManFraig->pData = pModel; return; } /**Function************************************************************* Synopsis [Returns 1 if the one of the output is already non-constant 0.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i; // make sure the reference simulation pattern does not detect the bug // pObj = Ivy_ManPo( p->pManAig, 0 ); Ivy_ManForEachPo( p->pManAig, pObj, i ) { assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0 // complement simulation info // if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) // Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) ); // check if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) ) { // create the counter-example from this pattern Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) ); return 1; } // complement simulation info // if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) ); } return 0; } /**Function************************************************************* Synopsis [Refines the classes after simulation.] Description [Assumes that simulation info is assigned. Returns the number of classes refined.] SideEffects [Large equivalence class of constant 0 may cause problems.] SeeAlso [] ***********************************************************************/ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass, * pClass2; int RetValue, Counter = 0; abctime clk; // check if some outputs already became non-constant // this is a special case when computation can be stopped!!! if ( p->pParams->fProve ) Ivy_FraigCheckOutputSims( p ); if ( p->pManFraig->pData ) return 0; // refine the classed clk = Abc_Clock(); Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 ) { if ( pClass->fMarkA ) continue; RetValue = Ivy_FraigRefineClass_rec( p, pClass ); Counter += ( RetValue > 0 ); //if ( Ivy_ObjIsConst1(pClass) ) //printf( "%d ", RetValue ); //if ( Ivy_ObjIsConst1(pClass) ) // p->time1 += Abc_Clock() - clk; } p->timeRef += Abc_Clock() - clk; return Counter; } /**Function************************************************************* Synopsis [Print the class.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigPrintClass( Ivy_Obj_t * pClass ) { Ivy_Obj_t * pObj; printf( "Class {" ); Ivy_FraigForEachClassNode( pClass, pObj ) printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' ); printf( " }\n" ); } /**Function************************************************************* Synopsis [Count the number of elements in the class.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass ) { Ivy_Obj_t * pObj; int Counter = 0; Ivy_FraigForEachClassNode( pClass, pObj ) Counter++; return Counter; } /**Function************************************************************* Synopsis [Prints simulation classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass; Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass ) { // Ivy_FraigPrintClass( pClass ); printf( "%d ", Ivy_FraigCountClassNodes( pClass ) ); } // printf( "\n" ); } /**Function************************************************************* Synopsis [Generated const 0 pattern.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p ) { memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); } /**Function************************************************************* Synopsis [[Generated const 1 pattern.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p ) { memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords ); } /**Function************************************************************* Synopsis [Generates the counter-example satisfying the miter.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p ) { int * pModel; Ivy_Obj_t * pObj; int i; pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); Ivy_ManForEachPi( p->pManFraig, pObj, i ) // pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ); pModel[i] = ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True ); return pModel; } /**Function************************************************************* Synopsis [Copy pattern from the solver into the internal storage.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); Ivy_ManForEachPi( p->pManFraig, pObj, i ) // Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i ) // if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True ) Ivy_InfoSetBit( p->pPatWords, i ); // Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); } /**Function************************************************************* Synopsis [Copy pattern from the solver into the internal storage.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); // Ivy_ManForEachPi( p->pManFraig, pObj, i ) Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i ) // if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True ) // Ivy_InfoSetBit( p->pPatWords, i ); Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); } /**Function************************************************************* Synopsis [Copy pattern from the solver into the internal storage.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i; for ( i = 0; i < p->nPatWords; i++ ) p->pPatWords[i] = Ivy_ObjRandomSim(); Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i ) // if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) ) if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ sat_solver_var_value(p->pSat, Ivy_ObjSatNum(pObj)) ) Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 ); } /**Function************************************************************* Synopsis [Performs simulation of the manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSimulate( Ivy_FraigMan_t * p ) { int nChanges, nClasses; // start the classes Ivy_FraigAssignRandom( p ); Ivy_FraigSimulateOne( p ); Ivy_FraigCreateClasses( p ); //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) ); // refine classes by walking 0/1 patterns Ivy_FraigSavePattern0( p ); Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); nChanges = Ivy_FraigRefineClasses( p ); if ( p->pManFraig->pData ) return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); Ivy_FraigSavePattern1( p ); Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); nChanges = Ivy_FraigRefineClasses( p ); if ( p->pManFraig->pData ) return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); // refine classes by random simulation do { Ivy_FraigAssignRandom( p ); Ivy_FraigSimulateOne( p ); nClasses = p->lClasses.nItems; nChanges = Ivy_FraigRefineClasses( p ); if ( p->pManFraig->pData ) return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); } while ( (double)nChanges / nClasses > p->pParams->dSimSatur ); // Ivy_FraigPrintSimClasses( p ); } /**Function************************************************************* Synopsis [Cleans pattern scores.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p ) { int i, nLimit = p->nSimWords * 32; for ( i = 0; i < nLimit; i++ ) p->pPatScores[i] = 0; } /**Function************************************************************* Synopsis [Adds to pattern scores.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew ) { Ivy_FraigSim_t * pSims0, * pSims1; unsigned uDiff; int i, w; // get hold of the simulation information pSims0 = Ivy_ObjSim(pClass); pSims1 = Ivy_ObjSim(pClassNew); // iterate through the differences and record the score for ( w = 0; w < p->nSimWords; w++ ) { uDiff = pSims0->pData[w] ^ pSims1->pData[w]; if ( uDiff == 0 ) continue; for ( i = 0; i < 32; i++ ) if ( uDiff & ( 1 << i ) ) p->pPatScores[w*32+i]++; } } /**Function************************************************************* Synopsis [Selects the best pattern.] Description [Returns 1 if such pattern is found.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p ) { Ivy_FraigSim_t * pSims; Ivy_Obj_t * pObj; int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1; for ( i = 1; i < nLimit; i++ ) { if ( MaxScore < p->pPatScores[i] ) { MaxScore = p->pPatScores[i]; BestPat = i; } } if ( MaxScore == 0 ) return 0; // if ( MaxScore > p->pParams->MaxScore ) // printf( "Max score is %3d. ", MaxScore ); // copy the best pattern into the selected pattern memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); Ivy_ManForEachPi( p->pManAig, pObj, i ) { pSims = Ivy_ObjSim(pObj); if ( Ivy_InfoHasBit(pSims->pData, BestPat) ) Ivy_InfoSetBit(p->pPatWords, i); } return MaxScore; } /**Function************************************************************* Synopsis [Resimulates fraiging manager after finding a counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigResimulate( Ivy_FraigMan_t * p ) { int nChanges; Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); if ( p->pParams->fPatScores ) Ivy_FraigCleanPatScores( p ); nChanges = Ivy_FraigRefineClasses( p ); if ( p->pManFraig->pData ) return; if ( nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); assert( nChanges >= 1 ); //printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges ); if ( !p->pParams->fPatScores ) return; // perform additional simulation using dist1 patterns derived from successful patterns while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore ) { Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); Ivy_FraigCleanPatScores( p ); nChanges = Ivy_FraigRefineClasses( p ); if ( p->pManFraig->pData ) return; //printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); if ( nChanges == 0 ) break; } } /**Function************************************************************* Synopsis [Prints the status of the miter.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose ) { if ( !fVerbose ) return; printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) ); ABC_PRT( pString, Abc_Clock() - clk ); } /**Function************************************************************* Synopsis [Reports the status of the miter.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigMiterStatus( Ivy_Man_t * pMan ) { Ivy_Obj_t * pObj, * pObjNew; int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; if ( pMan->pData ) return 0; Ivy_ManForEachPo( pMan, pObj, i ) { pObjNew = Ivy_ObjChild0(pObj); // check if the output is constant 1 if ( pObjNew == pMan->pConst1 ) { CountNonConst0++; continue; } // check if the output is constant 0 if ( pObjNew == Ivy_Not(pMan->pConst1) ) { CountConst0++; continue; } /* // check if the output is a primary input if ( Ivy_ObjIsPi(Ivy_Regular(pObjNew)) ) { CountNonConst0++; continue; } */ // check if the output can be constant 0 if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) ) { CountNonConst0++; continue; } CountUndecided++; } /* if ( p->pParams->fVerbose ) { printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) ); printf( "Const0 = %d. ", CountConst0 ); printf( "NonConst0 = %d. ", CountNonConst0 ); printf( "Undecided = %d. ", CountUndecided ); printf( "\n" ); } */ if ( CountNonConst0 ) return 0; if ( CountUndecided ) return -1; return 1; } /**Function************************************************************* Synopsis [Tries to prove each output of the miter until encountering a sat output.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj, * pObjNew; int i, RetValue; abctime clk = Abc_Clock(); int fVerbose = 0; Ivy_ManForEachPo( p->pManAig, pObj, i ) { if ( i && fVerbose ) { ABC_PRT( "Time", Abc_Clock() -clk ); } pObjNew = Ivy_ObjChild0Equiv(pObj); // check if the output is constant 1 if ( pObjNew == p->pManFraig->pConst1 ) { if ( fVerbose ) printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) ); // assing constant 0 model p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) ); break; } // check if the output is constant 0 if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) ) { if ( fVerbose ) printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); continue; } // check if the output can be constant 0 if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) ) { if ( fVerbose ) printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); // assing constant 0 model p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) ); break; } /* // check the representative of this node pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj)); if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 ) printf( "Representative is not constant 1.\n" ); else printf( "Representative is constant 1.\n" ); */ // try to prove the output constant 0 RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) ); if ( RetValue == 1 ) // proved equivalent { if ( fVerbose ) printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); // set the constant miter Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) ); continue; } if ( RetValue == -1 ) // failed { if ( fVerbose ) printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter ); continue; } // proved satisfiable if ( fVerbose ) printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); // create the model p->pManFraig->pData = Ivy_FraigCreateModel(p); break; } if ( fVerbose ) { ABC_PRT( "Time", Abc_Clock() -clk ); } } /**Function************************************************************* Synopsis [Performs fraiging for the internal nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSweep( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj;//, * pTemp; int i, k = 0; p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0; p->nClassesBeg = p->lClasses.nItems; // duplicate internal nodes p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) ); Ivy_ManForEachNode( p->pManAig, pObj, i ) { Extra_ProgressBarUpdate( p->pProgress, k++, NULL ); // default to simple strashing if simulation detected a counter-example for a PO if ( p->pManFraig->pData ) pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); else pObj->pEquiv = Ivy_FraigAnd( p, pObj ); assert( pObj->pEquiv != NULL ); // pTemp = Ivy_Regular(pObj->pEquiv); // assert( Ivy_Regular(pObj->pEquiv)->Type ); } Extra_ProgressBarStop( p->pProgress ); p->nClassesEnd = p->lClasses.nItems; // try to prove the outputs of the miter p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig); // Ivy_FraigMiterStatus( p->pManFraig ); if ( p->pParams->fProve && p->pManFraig->pData == NULL ) Ivy_FraigMiterProve( p ); // add the POs Ivy_ManForEachPo( p->pManAig, pObj, i ) Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); // clean the old manager Ivy_ManForEachObj( p->pManAig, pObj, i ) pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; // clean the new manager Ivy_ManForEachObj( p->pManFraig, pObj, i ) { if ( Ivy_ObjFaninVec(pObj) ) Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); pObj->pNextFan0 = pObj->pNextFan1 = NULL; pObj->pEquiv = NULL; } // remove dangling nodes Ivy_ManCleanup( p->pManFraig ); // clean up the class marks Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj ) pObj->fMarkA = 0; } /**Function************************************************************* Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ) { Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew; int RetValue; // get the fraiged fanins pFanin0New = Ivy_ObjChild0Equiv(pObjOld); pFanin1New = Ivy_ObjChild1Equiv(pObjOld); // get the candidate fraig node pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New ); // get representative of this class if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node { // assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) ); // assert( pObjNew != Ivy_Regular(pFanin0New) ); // assert( pObjNew != Ivy_Regular(pFanin1New) ); return pObjNew; } // get the fraiged representative pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld)); // if the fraiged nodes are the same return if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) ) return pObjNew; assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) ); // printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id ); // they are different (the counter-example is in p->pPatWords) RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) ); if ( RetValue == 1 ) // proved equivalent { // mark the class as proved if ( Ivy_ObjClassNodeNext(pObjOld) == NULL ) Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1; return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase ); } if ( RetValue == -1 ) // failed return pObjNew; // simulate the counter-example and return the new node Ivy_FraigResimulate( p ); return pObjNew; } /**Function************************************************************* Synopsis [Prints variable activity.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p ) { int i; for ( i = 0; i < p->nSatVars; i++ ) printf( "%d %d ", i, p->pSat->activity[i] ); printf( "\n" ); } /**Function************************************************************* Synopsis [Runs equivalence test for the two nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { int pLits[4], RetValue, RetValue1, nBTLimit; abctime clk; //, clk2 = Abc_Clock(); // make sure the nodes are not complemented assert( !Ivy_IsComplement(pNew) ); assert( !Ivy_IsComplement(pOld) ); assert( pNew != pOld ); // if at least one of the nodes is a failed node, perform adjustments: // if the backtrack limit is small, simply skip this node // if the backtrack limit is > 10, take the quare root of the limit nBTLimit = p->pParams->nBTLimitNode; if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) { p->nSatFails++; // fail immediately // return -1; if ( nBTLimit <= 10 ) return -1; nBTLimit = (int)pow(nBTLimit, 0.7); } p->nSatCalls++; // make sure the solver is allocated and has enough variables if ( p->pSat == NULL ) { p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 1000 ); p->pSat->factors = ABC_CALLOC( double, p->pSat->cap ); p->nSatVars = 1; // var 0 is reserved for const1 node - add the clause // pLits[0] = toLit( 0 ); // sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them Ivy_FraigNodeAddToSolver( p, pOld, pNew ); // prepare variable activity Ivy_FraigSetActivityFactors( p, pOld, pNew ); // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 clk = Abc_Clock(); pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 ); pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, p->nBTLimitGlobal, p->nInsLimitGlobal ); p->timeSat += Abc_Clock() - clk; if ( RetValue1 == l_False ) { p->timeSatUnsat += Abc_Clock() - clk; pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); assert( RetValue ); // continue solving the other implication p->nSatCallsUnsat++; } else if ( RetValue1 == l_True ) { p->timeSatSat += Abc_Clock() - clk; Ivy_FraigSavePattern( p ); p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { p->timeSatFail += Abc_Clock() - clk; /* if ( nBTLimit > 1000 ) { RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit ); if ( RetValue != -1 ) return RetValue; } */ // mark the node as the failed node if ( pOld != p->pManFraig->pConst1 ) pOld->fFailTfo = 1; pNew->fFailTfo = 1; p->nSatFailsReal++; return -1; } // if the old node was constant 0, we already know the answer if ( pOld == p->pManFraig->pConst1 ) { p->nSatProof++; return 1; } // solve under assumptions // A = 0; B = 1 OR A = 0; B = 0 clk = Abc_Clock(); pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 ); pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase ); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, p->nBTLimitGlobal, p->nInsLimitGlobal ); p->timeSat += Abc_Clock() - clk; if ( RetValue1 == l_False ) { p->timeSatUnsat += Abc_Clock() - clk; pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); assert( RetValue ); p->nSatCallsUnsat++; } else if ( RetValue1 == l_True ) { p->timeSatSat += Abc_Clock() - clk; Ivy_FraigSavePattern( p ); p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { p->timeSatFail += Abc_Clock() - clk; /* if ( nBTLimit > 1000 ) { RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit ); if ( RetValue != -1 ) return RetValue; } */ // mark the node as the failed node pOld->fFailTfo = 1; pNew->fFailTfo = 1; p->nSatFailsReal++; return -1; } /* // check BDD proof { int RetVal; ABC_PRT( "Sat", Abc_Clock() - clk2 ); clk2 = Abc_Clock(); RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew ); // printf( "%d ", RetVal ); assert( RetVal ); ABC_PRT( "Bdd", Abc_Clock() - clk2 ); printf( "\n" ); } */ // return SAT proof p->nSatProof++; return 1; } /**Function************************************************************* Synopsis [Runs equivalence test for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) { int pLits[2], RetValue1; abctime clk; int RetValue; // make sure the nodes are not complemented assert( !Ivy_IsComplement(pNew) ); assert( pNew != p->pManFraig->pConst1 ); p->nSatCalls++; // make sure the solver is allocated and has enough variables if ( p->pSat == NULL ) { p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 1000 ); p->pSat->factors = ABC_CALLOC( double, p->pSat->cap ); p->nSatVars = 1; // var 0 is reserved for const1 node - add the clause // pLits[0] = toLit( 0 ); // sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them Ivy_FraigNodeAddToSolver( p, NULL, pNew ); // prepare variable activity Ivy_FraigSetActivityFactors( p, NULL, pNew ); // solve under assumptions clk = Abc_Clock(); pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase ); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, (ABC_INT64_T)p->pParams->nBTLimitMiter, (ABC_INT64_T)0, p->nBTLimitGlobal, p->nInsLimitGlobal ); p->timeSat += Abc_Clock() - clk; if ( RetValue1 == l_False ) { p->timeSatUnsat += Abc_Clock() - clk; pLits[0] = lit_neg( pLits[0] ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); assert( RetValue ); // continue solving the other implication p->nSatCallsUnsat++; } else if ( RetValue1 == l_True ) { p->timeSatSat += Abc_Clock() - clk; if ( p->pPatWords ) Ivy_FraigSavePattern( p ); p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { p->timeSatFail += Abc_Clock() - clk; /* if ( p->pParams->nBTLimitMiter > 1000 ) { RetValue = Ivy_FraigCheckCone( p, p->pManFraig, p->pManFraig->pConst1, pNew, p->pParams->nBTLimitMiter ); if ( RetValue != -1 ) return RetValue; } */ // mark the node as the failed node pNew->fFailTfo = 1; p->nSatFailsReal++; return -1; } // return SAT proof p->nSatProof++; return 1; } /**Function************************************************************* Synopsis [Addes clauses to the solver.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode ) { Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE; int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; assert( !Ivy_IsComplement( pNode ) ); assert( Ivy_ObjIsMuxType( pNode ) ); // get nodes (I = if, T = then, E = else) pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); // get the variable numbers VarF = Ivy_ObjSatNum(pNode); VarI = Ivy_ObjSatNum(pNodeI); VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT)); VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE)); // get the complementation flags fCompT = Ivy_IsComplement(pNodeT); fCompE = Ivy_IsComplement(pNodeE); // f = ITE(i, t, e) // i' + t' + f // i' + t + f' // i + e' + f // i + e + f' // create four clauses pLits[0] = toLitCond(VarI, 1); pLits[1] = toLitCond(VarT, 1^fCompT); pLits[2] = toLitCond(VarF, 0); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); assert( RetValue ); pLits[0] = toLitCond(VarI, 1); pLits[1] = toLitCond(VarT, 0^fCompT); pLits[2] = toLitCond(VarF, 1); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); assert( RetValue ); pLits[0] = toLitCond(VarI, 0); pLits[1] = toLitCond(VarE, 1^fCompE); pLits[2] = toLitCond(VarF, 0); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); assert( RetValue ); pLits[0] = toLitCond(VarI, 0); pLits[1] = toLitCond(VarE, 0^fCompE); pLits[2] = toLitCond(VarF, 1); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); assert( RetValue ); // two additional clauses // t' & e' -> f' // t & e -> f // t + e + f' // t' + e' + f if ( VarT == VarE ) { // assert( fCompT == !fCompE ); return; } pLits[0] = toLitCond(VarT, 0^fCompT); pLits[1] = toLitCond(VarE, 0^fCompE); pLits[2] = toLitCond(VarF, 1); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); assert( RetValue ); pLits[0] = toLitCond(VarT, 1^fCompT); pLits[1] = toLitCond(VarE, 1^fCompE); pLits[2] = toLitCond(VarF, 0); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); assert( RetValue ); } /**Function************************************************************* Synopsis [Addes clauses to the solver.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper ) { Ivy_Obj_t * pFanin; int * pLits, nLits, RetValue, i; assert( !Ivy_IsComplement(pNode) ); assert( Ivy_ObjIsNode( pNode ) ); // create storage for literals nLits = Vec_PtrSize(vSuper) + 1; pLits = ABC_ALLOC( int, nLits ); // suppose AND-gate is A & B = C // add !A => !C or A + !C Vec_PtrForEachEntry( Ivy_Obj_t *, vSuper, pFanin, i ) { pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin)); pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); assert( RetValue ); } // add A & B => C or !A + !B + C Vec_PtrForEachEntry( Ivy_Obj_t *, vSuper, pFanin, i ) pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin)); pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); assert( RetValue ); ABC_FREE( pLits ); } /**Function************************************************************* Synopsis [Collects the supergate.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) { // if the new node is complemented or a PI, another gate begins if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || (fUseMuxes && Ivy_ObjIsMuxType(pObj)) ) { Vec_PtrPushUnique( vSuper, pObj ); return; } // go through the branches Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes ); Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes ); } /**Function************************************************************* Synopsis [Collects the supergate.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes ) { Vec_Ptr_t * vSuper; assert( !Ivy_IsComplement(pObj) ); assert( !Ivy_ObjIsPi(pObj) ); vSuper = Vec_PtrAlloc( 4 ); Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); return vSuper; } /**Function************************************************************* Synopsis [Updates the solver clause database.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier ) { assert( !Ivy_IsComplement(pObj) ); if ( Ivy_ObjSatNum(pObj) ) return; assert( Ivy_ObjSatNum(pObj) == 0 ); assert( Ivy_ObjFaninVec(pObj) == NULL ); if ( Ivy_ObjIsConst1(pObj) ) return; //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars ); Ivy_ObjSetSatNum( pObj, p->nSatVars++ ); if ( Ivy_ObjIsNode(pObj) ) Vec_PtrPush( vFrontier, pObj ); } /**Function************************************************************* Synopsis [Updates the solver clause database.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { Vec_Ptr_t * vFrontier, * vFanins; Ivy_Obj_t * pNode, * pFanin; int i, k, fUseMuxes = 1; assert( pOld || pNew ); // quit if CNF is ready if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) ) return; // start the frontier vFrontier = Vec_PtrAlloc( 100 ); if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier ); if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier ); // explore nodes in the frontier Vec_PtrForEachEntry( Ivy_Obj_t *, vFrontier, pNode, i ) { // create the supergate assert( Ivy_ObjSatNum(pNode) ); assert( Ivy_ObjFaninVec(pNode) == NULL ); if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) ) { vFanins = Vec_PtrAlloc( 4 ); Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) ); Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) ); Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) ); Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) ); Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, k ) Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier ); Ivy_FraigAddClausesMux( p, pNode ); } else { vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes ); Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, k ) Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier ); Ivy_FraigAddClausesSuper( p, pNode, vFanins ); } assert( Vec_PtrSize(vFanins) > 1 ); Ivy_ObjSetFaninVec( pNode, vFanins ); } Vec_PtrFree( vFrontier ); sat_solver_simplify( p->pSat ); } /**Function************************************************************* Synopsis [Sets variable activities in the cone.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax ) { Vec_Ptr_t * vFanins; Ivy_Obj_t * pFanin; int i, Counter = 0; assert( !Ivy_IsComplement(pObj) ); assert( Ivy_ObjSatNum(pObj) ); // skip visited variables if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) ) return 0; Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj); // add the PI to the list if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) ) return 0; // set the factor of this variable // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin); veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj)); // explore the fanins vFanins = Ivy_ObjFaninVec( pObj ); Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, i ) Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax ); return 1 + Counter; } /**Function************************************************************* Synopsis [Sets variable activities in the cone.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { int LevelMin, LevelMax; abctime clk; assert( pOld || pNew ); clk = Abc_Clock(); // reset the active variables veci_resize(&p->pSat->act_vars, 0); // prepare for traversal Ivy_ManIncrementTravId( p->pManFraig ); // determine the min and max level to visit assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 ); LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) ); LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio)); // traverse if ( pOld && !Ivy_ObjIsConst1(pOld) ) Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax ); if ( pNew && !Ivy_ObjIsConst1(pNew) ) Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax ); //Ivy_FraigPrintActivity( p ); p->timeTrav += Abc_Clock() - clk; return 1; } ABC_NAMESPACE_IMPL_END #include "bdd/cudd/cuddInt.h" ABC_NAMESPACE_IMPL_START /**Function************************************************************* Synopsis [Checks equivalence using BDDs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_t * vFront, int Level ) { DdNode ** pFuncs; DdNode * bFuncNew; Vec_Ptr_t * vTemp; Ivy_Obj_t * pObj, * pFanin; int i, NewSize; // create new frontier vTemp = Vec_PtrAlloc( 100 ); Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i ) { if ( (int)pObj->Level != Level ) { pObj->fMarkB = 1; pObj->TravId = Vec_PtrSize(vTemp); Vec_PtrPush( vTemp, pObj ); continue; } pFanin = Ivy_ObjFanin0(pObj); if ( pFanin->fMarkB == 0 ) { pFanin->fMarkB = 1; pFanin->TravId = Vec_PtrSize(vTemp); Vec_PtrPush( vTemp, pFanin ); } pFanin = Ivy_ObjFanin1(pObj); if ( pFanin->fMarkB == 0 ) { pFanin->fMarkB = 1; pFanin->TravId = Vec_PtrSize(vTemp); Vec_PtrPush( vTemp, pFanin ); } } // collect the permutation NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp)); pFuncs = ABC_ALLOC( DdNode *, NewSize ); Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i ) { if ( (int)pObj->Level != Level ) pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId ); else pFuncs[i] = Cudd_bddAnd( dd, Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ), Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) ); Cudd_Ref( pFuncs[i] ); } // add the remaining vars assert( NewSize == dd->size ); for ( i = Vec_PtrSize(vFront); i < dd->size; i++ ) { pFuncs[i] = Cudd_bddIthVar( dd, i ); Cudd_Ref( pFuncs[i] ); } // create new bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew ); // clean trav Id Vec_PtrForEachEntry( Ivy_Obj_t *, vTemp, pObj, i ) { pObj->fMarkB = 0; pObj->TravId = 0; } // deref for ( i = 0; i < dd->size; i++ ) Cudd_RecursiveDeref( dd, pFuncs[i] ); ABC_FREE( pFuncs ); ABC_FREE( vFront->pArray ); *vFront = *vTemp; vTemp->nCap = vTemp->nSize = 0; vTemp->pArray = NULL; Vec_PtrFree( vTemp ); Cudd_Deref( bFuncNew ); return bFuncNew; } /**Function************************************************************* Synopsis [Checks equivalence using BDDs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 ) { static DdManager * dd = NULL; DdNode * bFunc, * bTemp; Vec_Ptr_t * vFront; Ivy_Obj_t * pObj; int i, RetValue, Iter, Level; // start the manager if ( dd == NULL ) dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); // create front vFront = Vec_PtrAlloc( 100 ); Vec_PtrPush( vFront, pObj1 ); Vec_PtrPush( vFront, pObj2 ); // get the function bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) ); Cudd_Ref( bFunc ); bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase ); // try running BDDs for ( Iter = 0; ; Iter++ ) { // find max level Level = 0; Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i ) if ( Level < (int)pObj->Level ) Level = (int)pObj->Level; if ( Level == 0 ) break; bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc ); Cudd_RecursiveDeref( dd, bTemp ); if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved {printf( "%d", Iter ); break;} if ( Cudd_DagSize(bFunc) > 1000 ) {printf( "b" ); break;} if ( dd->size > 120 ) {printf( "s" ); break;} if ( Iter > 50 ) {printf( "i" ); break;} } if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat RetValue = 1; else if ( Level == 0 ) // sat RetValue = 0; else RetValue = -1; // spaceout/timeout Cudd_RecursiveDeref( dd, bFunc ); Vec_PtrFree( vFront ); return RetValue; } ABC_NAMESPACE_IMPL_END #include "aig/aig/aig.h" ABC_NAMESPACE_IMPL_START /**Function************************************************************* Synopsis [Computes truth table of the cut.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigExtractCone_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) { if ( pNode->fMarkB ) return; pNode->fMarkB = 1; if ( Ivy_ObjIsPi(pNode) ) { Vec_IntPush( vLeaves, pNode->Id ); return; } assert( Ivy_ObjIsAnd(pNode) ); Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin0(pNode), vLeaves, vNodes ); Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin1(pNode), vLeaves, vNodes ); Vec_IntPush( vNodes, pNode->Id ); } /**Function************************************************************* Synopsis [Checks equivalence using BDDs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Ivy_FraigExtractCone( Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, Vec_Int_t * vLeaves ) { Aig_Man_t * pMan; Aig_Obj_t * pMiter; Vec_Int_t * vNodes; Ivy_Obj_t * pObjIvy; int i; // collect nodes vNodes = Vec_IntAlloc( 100 ); Ivy_ManConst1(p)->fMarkB = 1; Ivy_FraigExtractCone_rec( p, pObj1, vLeaves, vNodes ); Ivy_FraigExtractCone_rec( p, pObj2, vLeaves, vNodes ); Ivy_ManConst1(p)->fMarkB = 0; // create new manager pMan = Aig_ManStart( 1000 ); Ivy_ManConst1(p)->pEquiv = (Ivy_Obj_t *)Aig_ManConst1(pMan); Ivy_ManForEachNodeVec( p, vLeaves, pObjIvy, i ) { pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_ObjCreateCi( pMan ); pObjIvy->fMarkB = 0; } // duplicate internal nodes Ivy_ManForEachNodeVec( p, vNodes, pObjIvy, i ) { pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pObjIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pObjIvy) ); pObjIvy->fMarkB = 0; pMiter = (Aig_Obj_t *)pObjIvy->pEquiv; assert( pMiter->fPhase == pObjIvy->fPhase ); } // create the PO pMiter = Aig_Exor( pMan, (Aig_Obj_t *)pObj1->pEquiv, (Aig_Obj_t *)pObj2->pEquiv ); pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); /* printf( "Polarity = %d\n", pMiter->fPhase ); if ( Ivy_ObjIsConst1(pObj1) || Ivy_ObjIsConst1(pObj2) ) { pMiter = Aig_NotCond( pMiter, 1 ); printf( "***************\n" ); } */ pMiter = Aig_ObjCreateCo( pMan, pMiter ); //printf( "Polarity = %d\n", pMiter->fPhase ); Aig_ManCleanup( pMan ); Vec_IntFree( vNodes ); return pMan; } /**Function************************************************************* Synopsis [Checks equivalence using BDDs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit ) { extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ); Vec_Int_t * vLeaves; Aig_Man_t * pMan; Aig_Obj_t * pObj; int i, RetValue; vLeaves = Vec_IntAlloc( 100 ); pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves ); RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 0, 0, 0, 1 ); if ( RetValue == 0 ) { int Counter = 0; memset( pGlo->pPatWords, 0, sizeof(unsigned) * pGlo->nPatWords ); Aig_ManForEachCi( pMan, pObj, i ) if ( ((int *)pMan->pData)[i] ) { int iObjIvy = Vec_IntEntry( vLeaves, i ); assert( iObjIvy > 0 && iObjIvy <= Ivy_ManPiNum(p) ); Ivy_InfoSetBit( pGlo->pPatWords, iObjIvy-1 ); //printf( "%d ", iObjIvy ); Counter++; } assert( Counter > 0 ); } Vec_IntFree( vLeaves ); if ( RetValue == 1 ) printf( "UNSAT\n" ); else if ( RetValue == 0 ) printf( "SAT\n" ); else if ( RetValue == -1 ) printf( "UNDEC\n" ); // p->pModel = (int *)pMan->pData, pMan2->pData = NULL; Aig_ManStop( pMan ); return RetValue; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END