/**CFile**************************************************************** FileName [sswCore.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Inductive prover with constraints.] Synopsis [The core procedures.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - September 1, 2008.] Revision [$Id: sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] ***********************************************************************/ #include "sswInt.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [This procedure sets default parameters.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) { memset( p, 0, sizeof(Ssw_Pars_t) ); p->nPartSize = 0; // size of the partition p->nOverSize = 0; // size of the overlap between partitions p->nFramesK = 1; // the induction depth p->nFramesAddSim = 2; // additional frames to simulate p->fConstrs = 0; // treat the last nConstrs POs as seq constraints p->fMergeFull = 0; // enables full merge when constraints are used p->nBTLimit = 1000; // conflict limit at a node p->nBTLimitGlobal = 5000000; // conflict limit for all runs p->nMinDomSize = 100; // min clock domain considered for optimization p->nItersStop = -1; // stop after the given number of iterations p->nResimDelta = 1000; // the internal of nodes to resimulate p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fPolarFlip = 0; // uses polarity adjustment p->fLatchCorr = 0; // performs register correspondence p->fConstCorr = 0; // performs constant correspondence p->fOutputCorr = 0; // perform 'PO correspondence' p->fSemiFormal = 0; // enable semiformal filtering p->fDynamic = 0; // dynamic partitioning p->fLocalSim = 0; // local simulation p->fVerbose = 0; // verbose stats p->fEquivDump = 0; // enables dumping equivalences // latch correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence p->nSatVarMax = 1000; // the max number of SAT variables p->nRecycleCalls = 50; // calls to perform before recycling SAT solver // signal correspondence p->nSatVarMax2 = 5000; // the max number of SAT variables p->nRecycleCalls2 = 250; // calls to perform before recycling SAT solver // return values p->nIters = 0; // the number of iterations performed } /**Function************************************************************* Synopsis [This procedure sets default parameters.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ) { Ssw_ManSetDefaultParams( p ); p->fLatchCorrOpt = 1; p->nBTLimit = 10000; } /**Function************************************************************* Synopsis [Reports improvements for property cones.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop ) { Aig_Man_t * pAig1, * pAig2, * pAux; pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 ); pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0, -1, -1, 0, 0 ); Aig_ManStop( pAux ); pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 ); pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0, -1, -1, 0, 0 ); Aig_ManStop( pAux ); p->nNodesBegC = Aig_ManNodeNum(pAig1); p->nNodesEndC = Aig_ManNodeNum(pAig2); p->nRegsBegC = Aig_ManRegNum(pAig1); p->nRegsEndC = Aig_ManRegNum(pAig2); Aig_ManStop( pAig1 ); Aig_ManStop( pAig2 ); } /**Function************************************************************* Synopsis [Reports one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( pObj == Aig_ManConst1(p) ) Abc_Print( 1, "1" ); else if ( pObj == Aig_ManConst0(p) ) Abc_Print( 1, "0" ); else Abc_Print( 1, "X" ); } /**Function************************************************************* Synopsis [Reports improvements for property cones.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ReportOutputs( Aig_Man_t * pAig ) { Aig_Obj_t * pObj; int i; Saig_ManForEachPo( pAig, pObj, i ) { if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) ) Abc_Print( 1, "o" ); else Abc_Print( 1, "c" ); Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) ); } Abc_Print( 1, "\n" ); } /**Function************************************************************* Synopsis [Remove from-equivs that are in the cone of constraints.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose ) { Vec_Ptr_t * vCones; Aig_Obj_t ** pArray; Aig_Obj_t * pObj; int i, nTotal = 0, nRemoved = 0; // collect the nodes in the cone of constraints pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vCos); pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig); vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) ); // remove all the node that are equiv to something and are in the cones Aig_ManForEachObj( pAig, pObj, i ) { if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; if ( pAig->pReprs[i] != NULL ) nTotal++; if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) ) continue; if ( pAig->pReprs[i] ) { if ( p->pPars->fConstrs && !p->pPars->fMergeFull ) { pAig->pReprs[i] = NULL; nRemoved++; } } } // collect statistics p->nConesTotal = Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig); p->nConesConstr = Vec_PtrSize(vCones); p->nEquivsTotal = nTotal; p->nEquivsConstr = nRemoved; Vec_PtrFree( vCones ); } /**Function************************************************************* Synopsis [Performs computation of signal correspondence with constraints.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) { int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques; Aig_Man_t * pAigNew; int RetValue, nIter = -1; abctime clk, clkTotal = Abc_Clock(); // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesBeg = Aig_ManNodeNum(p->pAig); p->nRegsBeg = Aig_ManRegNum(p->pAig); // refine classes using BMC if ( p->pPars->fVerbose ) { Abc_Print( 1, "Before BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } if ( !p->pPars->fLatchCorr ) { p->pMSat = Ssw_SatStart( 0 ); if ( p->pPars->fConstrs ) Ssw_ManSweepBmcConstr( p ); else Ssw_ManSweepBmc( p ); Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); } if ( p->pPars->fVerbose ) { Abc_Print( 1, "After BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } // apply semi-formal filtering /* if ( p->pPars->fSemiFormal ) { Aig_Man_t * pSRed; Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose ); // Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose ); pSRed = Ssw_SpeculativeReduction( p ); Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); Aig_ManStop( pSRed ); } */ if ( p->pPars->pFunc ) { ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); } if ( p->pPars->nStepsMax == 0 ) { Abc_Print( 1, "Stopped signal correspondence after BMC.\n" ); goto finalize; } // refine classes using induction nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { if ( p->pPars->nStepsMax == nIter ) { Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter ); goto finalize; } if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) { Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); Aig_ManStop( pSRed ); Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter ); Abc_Print( 1, "The network is reduced using candidate equivalences.\n" ); Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" ); Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" ); break; } clk = Abc_Clock(); p->pMSat = Ssw_SatStart( 0 ); if ( p->pPars->fLatchCorrOpt ) { RetValue = Ssw_ManSweepLatch( p ); if ( p->pPars->fVerbose ) { Abc_Print( 1, "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal ); ABC_PRT( "T", Abc_Clock() - clk ); } } else { if ( p->pPars->fConstrs ) RetValue = Ssw_ManSweepConstr( p ); else if ( p->pPars->fDynamic ) RetValue = Ssw_ManSweepDyn( p ); else RetValue = Ssw_ManSweep( p ); p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts; if ( p->pPars->fVerbose ) { Abc_Print( 1, "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nConstrReduced, Aig_ManNodeNum(p->pFrames) ); if ( p->pPars->fDynamic ) { Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat ); Abc_Print( 1, "R =%4d. ", p->nRecycles-nRecycles ); } Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal, (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" ); ABC_PRT( "T", Abc_Clock() - clk ); } // if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 ) // p->pPars->nBTLimit = 10000; if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) ) { printf( "Iterative refinement is stopped after iteration %d\n", nIter ); printf( "because the property output is no longer a candidate constant.\n" ); // prepare to quite p->nLitsEnd = p->nLitsBeg; p->nNodesEnd = p->nNodesBeg; p->nRegsEnd = p->nRegsBeg; // cleanup Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); // cleanup Aig_ManSetPhase( p->pAig ); Aig_ManCleanMarkB( p->pAig ); return Aig_ManDupSimple( p->pAig ); } } nSatProof = p->nSatProof; nSatCallsSat = p->nSatCallsSat; nRecycles = p->nRecycles; nSatFailsReal = p->nSatFailsReal; nUniques = p->nUniques; p->nVarsMax = Abc_MaxInt( p->nVarsMax, p->pMSat->nSatVars ); p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls ); Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); if ( !RetValue ) break; if ( p->pPars->pFunc ) ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); } finalize: p->pPars->nIters = nIter + 1; p->timeTotal = Abc_Clock() - clkTotal; Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose ); pAigNew = Aig_ManDupRepr( p->pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); //Ssw_ClassesPrint( p->ppClasses, 1 ); // get the final stats p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); // cleanup Aig_ManSetPhase( p->pAig ); Aig_ManCleanMarkB( p->pAig ); return pAigNew; } /**Function************************************************************* Synopsis [Performs computation of signal correspondence with constraints.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { Ssw_Pars_t Pars; Aig_Man_t * pAigNew; Ssw_Man_t * p; assert( Aig_ManRegNum(pAig) > 0 ); // reset random numbers Aig_ManRandom( 1 ); // if parameters are not given, create them if ( pPars == NULL ) Ssw_ManSetDefaultParams( pPars = &Pars ); // consider the case of empty AIG if ( Aig_ManNodeNum(pAig) == 0 ) { pPars->nIters = 0; // Ntl_ManFinalize() needs the following to satisfy an assertion Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) ); return Aig_ManDupOrdered(pAig); } // check and update parameters if ( pPars->fLatchCorrOpt ) { pPars->fLatchCorr = 1; pPars->nFramesAddSim = 0; if ( (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) return Ssw_SignalCorrespondencePart( pAig, pPars ); } else { assert( pPars->nFramesK > 0 ); // perform partitioning if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) return Ssw_SignalCorrespondencePart( pAig, pPars ); } if ( pPars->fScorrGia ) { if ( pPars->fLatchCorrOpt ) { extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ); return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); } else { extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ); return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); } } // start the induction manager p = Ssw_ManCreate( pAig, pPars ); // compute candidate equivalence classes // p->pPars->nConstrs = 1; if ( p->pPars->fConstrs ) { // create trivial equivalence classes with all nodes being candidates for constant 1 p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); // derive phase bits to satisfy the constraints if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 ) { Abc_Print( 1, "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" ); p->pPars->fVerbose = 0; Ssw_ManStop( p ); return NULL; } // perform simulation of the first timeframes Ssw_ManRefineByConstrSim( p ); } else { // perform one round of seq simulation and generate candidate equivalence classes p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); // p->ppClasses = Ssw_ClassesPrepareTargets( pAig ); if ( pPars->fLatchCorrOpt ) p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 ); else if ( pPars->fDynamic ) p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); else p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 ); Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); } // allocate storage if ( p->pPars->fLocalSim ) p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); // Ssw_ReportOutputs( pAigNew ); if ( pPars->fConstrs && pPars->fVerbose ) Ssw_ReportConeReductions( p, pAig, pAigNew ); // cleanup Ssw_ManStop( p ); return pAigNew; } /**Function************************************************************* Synopsis [Performs computation of latch correspondence.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { Aig_Man_t * pRes; Ssw_Pars_t Pars; if ( pPars == NULL ) Ssw_ManSetDefaultParamsLcorr( pPars = &Pars ); pRes = Ssw_SignalCorrespondence( pAig, pPars ); // if ( pPars->fConstrs && pPars->fVerbose ) // Ssw_ReportConeReductions( pAig, pRes ); return pRes; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END