diff options
Diffstat (limited to 'src/aig/cec/cecCore.c')
-rw-r--r-- | src/aig/cec/cecCore.c | 101 |
1 files changed, 76 insertions, 25 deletions
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 9820c05c..10c145ec 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -48,7 +48,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) p->fNonChrono = 0; // use non-chronological backtracling (for circuit SAT only) p->fPolarFlip = 1; // flops polarity of variables p->fCheckMiter = 0; // the circuit is the miter - p->fFirstStop = 0; // stop on the first sat output +// p->fFirstStop = 0; // stop on the first sat output p->fLearnCls = 0; // perform clause learning p->fVerbose = 0; // verbose stats } @@ -67,11 +67,13 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) { memset( p, 0, sizeof(Cec_ParSim_t) ); - p->nWords = 15; // the number of simulation words - p->nRounds = 15; // the number of simulation rounds + p->nWords = 31; // the number of simulation words + p->nFrames = 100; // the number of simulation frames + p->nRounds = 20; // the max number of simulation rounds + p->nNonRefines = 3; // the max number of rounds without refinement p->TimeLimit = 0; // the runtime limit in seconds p->fCheckMiter = 0; // the circuit is the miter - p->fFirstStop = 0; // stop on the first sat output +// p->fFirstStop = 0; // stop on the first sat output p->fDualOut = 0; // miter with separate outputs p->fSeqSimulate = 0; // performs sequential simulation p->fVeryVerbose = 0; // verbose stats @@ -93,13 +95,15 @@ void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p ) { memset( p, 0, sizeof(Cec_ParSmf_t) ); p->nWords = 31; // the number of simulation words - p->nRounds = 1; // the number of simulation rounds - p->nFrames = 2; // the number of time frames + p->nRounds = 200; // the number of simulation rounds + p->nFrames = 200; // the max number of time frames + p->nNonRefines = 3; // the max number of rounds without refinement + p->nMinOutputs = 0; // the min outputs to accumulate p->nBTLimit = 100; // conflict limit at a node p->TimeLimit = 0; // the runtime limit in seconds p->fDualOut = 0; // miter with separate outputs p->fCheckMiter = 0; // the circuit is the miter - p->fFirstStop = 0; // stop on the first sat output +// p->fFirstStop = 0; // stop on the first sat output p->fVerbose = 0; // verbose stats } @@ -126,7 +130,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) p->nDepthMax = 1; // the depth in terms of steps of speculative reduction p->fRewriting = 0; // enables AIG rewriting p->fCheckMiter = 0; // the circuit is the miter - p->fFirstStop = 0; // stop on the first sat output +// p->fFirstStop = 0; // stop on the first sat output p->fDualOut = 0; // miter with separate outputs p->fColorDiff = 0; // miter with separate outputs p->fVeryVerbose = 0; // verbose stats @@ -149,7 +153,7 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ) memset( p, 0, sizeof(Cec_ParCec_t) ); p->nBTLimit = 1000; // conflict limit at a node p->TimeLimit = 0; // the runtime limit in seconds - p->fFirstStop = 0; // stop on the first sat output +// p->fFirstStop = 0; // stop on the first sat output p->fUseSmartCnf = 0; // use smart CNF computation p->fRewriting = 0; // enables AIG rewriting p->fVeryVerbose = 0; // verbose stats @@ -177,7 +181,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ) p->fLatchCorr = 0; // consider only latch outputs p->fUseRings = 1; // combine classes into rings p->fUseCSat = 1; // use circuit-based solver - p->fFirstStop = 0; // stop on the first sat output +// p->fFirstStop = 0; // stop on the first sat output p->fUseSmartCnf = 0; // use smart CNF computation p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats @@ -233,31 +237,79 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) Synopsis [Core procedure for simulation.] - Description [] + Description [Returns 1 if refinement has happened.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) +int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) { Cec_ManSim_t * pSim; - int RetValue, clkTotal = clock(); - if ( pPars->fSeqSimulate ) - printf( "Performing sequential simulation of %d frames with %d words.\n", - pPars->nRounds, pPars->nWords ); - Gia_ManRandom( 1 ); + int RetValue = 0, clkTotal = clock(); pSim = Cec_ManSimStart( pAig, pPars ); - if ( pAig->pReprs == NULL ) - RetValue = Cec_ManSimClassesPrepare( pSim ); - Cec_ManSimClassesRefine( pSim ); - if ( pPars->fCheckMiter ) - printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", - pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds ); + if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim ))) || + (RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) ) + printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n", + pSim->nOuts, pPars->nWords, pPars->nFrames ); if ( pPars->fVerbose ) ABC_PRT( "Time", clock() - clkTotal ); Cec_ManSimStop( pSim ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Core procedure for simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) +{ + int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0; + Gia_ManRandom( 1 ); + if ( pPars->fSeqSimulate ) + printf( "Performing rounds of random simulation of %d frames with %d words.\n", + pPars->nRounds, pPars->nFrames, pPars->nWords ); + nLitsOld = Gia_ManEquivCountLits( pAig ); + for ( r = 0; r < pPars->nRounds; r++ ) + { + if ( Cec_ManSimulationOne( pAig, pPars ) ) + { + fStop = 1; + break; + } + // decide when to stop + nLitsNew = Gia_ManEquivCountLits( pAig ); + if ( nLitsOld == 0 || nLitsOld > nLitsNew ) + { + nLitsOld = nLitsNew; + nCountNoRef = 0; + } + else if ( ++nCountNoRef == pPars->nNonRefines ) + { + r++; + break; + } + assert( nLitsOld == nLitsNew ); + } +// if ( pPars->fVerbose ) + if ( r == pPars->nRounds || fStop ) + printf( "Random simulation is stopped after %d rounds.\n", r ); + else + printf( "Random simulation saturated after %d rounds.\n", r ); + if ( pPars->fCheckMiter ) + { + int nNonConsts = Cec_ManCountNonConstOutputs( pAig ); + if ( nNonConsts ) + printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); + } } /**Function************************************************************* @@ -297,9 +349,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) // simulation Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; - pParsSim->nRounds = pPars->nRounds; + pParsSim->nFrames = pPars->nRounds; pParsSim->fCheckMiter = pPars->fCheckMiter; - pParsSim->fFirstStop = pPars->fFirstStop; pParsSim->fDualOut = pPars->fDualOut; pParsSim->fVerbose = pPars->fVerbose; pSim = Cec_ManSimStart( p->pAig, pParsSim ); |