From a4bca405978e500b7ef2b987d159e3b11b95905f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 14 Oct 2008 08:01:00 -0700 Subject: Version abc81014 --- src/aig/ssw/sswCore.c | 50 ++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 36 insertions(+), 14 deletions(-) (limited to 'src/aig/ssw/sswCore.c') diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 39f4c736..6db8cc3a 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -60,6 +60,9 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) 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 } @@ -95,7 +98,7 @@ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ) ***********************************************************************/ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) { - int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal; + int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques; Aig_Man_t * pAigNew; int RetValue, nIter; int clk, clkTotal = clock(); @@ -137,7 +140,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) } */ // refine classes using induction - nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0; + nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { clk = clock(); @@ -147,29 +150,44 @@ clk = clock(); RetValue = Ssw_ManSweepLatch( p ); if ( p->pPars->fVerbose ) { - printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ", + printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. Rcl = %3d. F = %3d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal ); PRT( "T", clock() - clk ); - nSatProof = p->nSatProof; - nSatCallsSat = p->nSatCallsSat; - nRecycles = p->nRecycles; - nSatFailsReal = p->nSatFailsReal; } } else { - RetValue = Ssw_ManSweep( p ); + 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 ) { - printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", + printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), - p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal ); + p->nConstrReduced, Aig_ManNodeNum(p->pFrames) ); + if ( p->pPars->fUniqueness ) + printf( "U =%4d. ", p->nUniques-nUniques ); + else if ( p->pPars->fDynamic ) + { + printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat ); + printf( "R =%3d. ", p->nRecycles-nRecycles ); + } + printf( "F =%3d. ", p->nSatFailsReal-nSatFailsReal ); PRT( "T", clock() - clk ); } } + nSatProof = p->nSatProof; + nSatCallsSat = p->nSatCallsSat; + nRecycles = p->nRecycles; + nSatFailsReal = p->nSatFailsReal; + nUniques = p->nUniques; + + p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars ); + p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls ); Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); @@ -234,13 +252,12 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { pPars->nFramesAddSim = 0; if ( pPars->nFramesK != 2 ) - printf( "Setting K = 2 for uniqueness constaints to work.\n" ); + printf( "Setting K = 2 for uniqueness constraints to work.\n" ); pPars->nFramesK = 2; } if ( pPars->fLatchCorrOpt ) { pPars->fLatchCorr = 1; - pPars->nFramesAddSim = 0; } else { @@ -259,7 +276,12 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // perform one round of seq simulation and generate candidate equivalence classes p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); // p->ppClasses = Ssw_ClassesPrepareTargets( pAig ); - p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); + 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, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); } else @@ -271,7 +293,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); if ( pPars->fUniqueness ) - printf( "Uniqueness constaint = %3d. Prevented counter-examples = %3d.\n", + printf( "Uniqueness constraints = %3d. Prevented counter-examples = %3d.\n", p->nUniquesAdded, p->nUniquesUseful ); // cleanup Ssw_ManStop( p ); -- cgit v1.2.3