From da65e88e3b346bcd70198b980e918ea9f1e11b4e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 22 Jun 2015 23:04:59 -0700 Subject: Version abc90804 committer: Baruch Sterin --- src/aig/cec/cec.h | 20 ++++--- src/aig/cec/cecCec.c | 1 - src/aig/cec/cecChoice.c | 2 +- src/aig/cec/cecClass.c | 14 ++--- src/aig/cec/cecCore.c | 101 +++++++++++++++++++++++++-------- src/aig/cec/cecCorr.c | 8 +-- src/aig/cec/cecInt.h | 4 +- src/aig/cec/cecMan.c | 6 +- src/aig/cec/cecSeq.c | 148 +++++++++++++++++++++++++++++++++++++++++------- src/aig/cec/cecSolve.c | 6 +- 10 files changed, 237 insertions(+), 73 deletions(-) (limited to 'src/aig/cec') diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index fcadb6ab..7f445970 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -47,21 +47,23 @@ struct Cec_ParSat_t_ int fNonChrono; // use non-chronological backtracling (for circuit SAT only) int fPolarFlip; // flops polarity of variables int fCheckMiter; // the circuit is the miter - int fFirstStop; // stop on the first sat output +// int fFirstStop; // stop on the first sat output int fLearnCls; // perform clause learning int fVerbose; // verbose stats }; // simulation parameters typedef struct Cec_ParSim_t_ Cec_ParSim_t; -struct Cec_ParSim_t_ +struct Cec_ParSim_t_ { int nWords; // the number of simulation words + int nFrames; // the number of simulation frames int nRounds; // the number of simulation rounds + int nNonRefines; // the max number of rounds without refinement int TimeLimit; // the runtime limit in seconds int fDualOut; // miter with separate outputs int fCheckMiter; // the circuit is the miter - int fFirstStop; // stop on the first sat output +// int fFirstStop; // stop on the first sat output int fSeqSimulate; // performs sequential simulation int fLatchCorr; // consider only latch outputs int fVeryVerbose; // verbose stats @@ -74,12 +76,14 @@ struct Cec_ParSmf_t_ { int nWords; // the number of simulation words int nRounds; // the number of simulation rounds - int nFrames; // the number of time frames + int nFrames; // the max number of time frames + int nNonRefines; // the max number of rounds without refinement + int nMinOutputs; // the min outputs to accumulate int nBTLimit; // conflict limit at a node int TimeLimit; // the runtime limit in seconds int fDualOut; // miter with separate outputs int fCheckMiter; // the circuit is the miter - int fFirstStop; // stop on the first sat output +// int fFirstStop; // stop on the first sat output int fVerbose; // verbose stats }; @@ -96,7 +100,7 @@ struct Cec_ParFra_t_ int nDepthMax; // the depth in terms of steps of speculative reduction int fRewriting; // enables AIG rewriting int fCheckMiter; // the circuit is the miter - int fFirstStop; // stop on the first sat output +// int fFirstStop; // stop on the first sat output int fDualOut; // miter with separate outputs int fColorDiff; // miter with separate outputs int fVeryVerbose; // verbose stats @@ -109,7 +113,7 @@ struct Cec_ParCec_t_ { int nBTLimit; // conflict limit at a node int TimeLimit; // the runtime limit in seconds - int fFirstStop; // stop on the first sat output +// int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation int fRewriting; // enables AIG rewriting int fVeryVerbose; // verbose stats @@ -129,7 +133,7 @@ struct Cec_ParCor_t_ int fUseRings; // use rings int fMakeChoices; // use equilvaences as choices int fUseCSat; // use circuit-based solver - int fFirstStop; // stop on the first sat output +// int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation int fVeryVerbose; // verbose stats int fVerbose; // verbose stats diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index a385be3e..1efa9235 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -135,7 +135,6 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) pParsFra->TimeLimit = pPars->TimeLimit; pParsFra->fVerbose = pPars->fVerbose; pParsFra->fCheckMiter = 1; - pParsFra->fFirstStop = 1; pParsFra->fDualOut = 1; pNew = Cec_ManSatSweeping( p, pParsFra ); if ( pNew == NULL ) diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c index f51d138d..fc316f46 100644 --- a/src/aig/cec/cecChoice.c +++ b/src/aig/cec/cecChoice.c @@ -213,7 +213,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; - pParsSim->nRounds = pPars->nRounds; + pParsSim->nFrames = pPars->nRounds; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = 0; pParsSim->fSeqSimulate = 0; diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index fd723f30..749f7f71 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -545,7 +545,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) { unsigned * pInfo; - int i, ScoreBest = 0, iPatBest = 1; + int i, ScoreBest = 0, iPatBest = 1; // set the first pattern // find the best pattern for ( i = 0; i < 32 * p->nWords; i++ ) if ( ScoreBest < p->pScores[i] ) @@ -588,8 +588,8 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) // compare outputs with 0 if ( p->pPars->fDualOut ) { - assert( (Gia_ManCoNum(p->pAig) & 1) == 0 ); - for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ ) + assert( (Gia_ManPoNum(p->pAig) & 1) == 0 ); + for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) { pInfo = Vec_PtrEntry( p->vCoSimInfo, i ); pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i ); @@ -601,7 +601,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) ); } if ( p->pCexes == NULL ) - p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 ); + p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 ); if ( p->pCexes[i/2] == NULL ) { p->nOuts++; @@ -612,7 +612,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) } else { - for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ ) + for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) { pInfo = Vec_PtrEntry( p->vCoSimInfo, i ); if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) ) @@ -623,7 +623,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) ); } if ( p->pCexes == NULL ) - p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) ); + p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) ); if ( p->pCexes[i] == NULL ) { p->nOuts++; @@ -632,7 +632,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) } } } - return p->pCexes != NULL && p->pPars->fFirstStop; + return p->pCexes != NULL; } /**Function************************************************************* 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 ); diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 96af801d..96c45907 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -545,7 +545,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); Gia_ManSetRefs( pSim->pAig ); // pSim->pPars->nWords = 63; - pSim->pPars->nRounds = nFrames; + pSim->pPars->nFrames = nFrames; vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords ); while ( iStart < Vec_IntSize(vCexStore) ) { @@ -580,7 +580,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS Vec_Ptr_t * vSimInfo; int RetValue = 0, iStart = 0; Gia_ManSetRefs( pSim->pAig ); - pSim->pPars->nRounds = 1; + pSim->pPars->nFrames = 1; vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); while ( iStart < Vec_IntSize(vCexStore) ) { @@ -774,7 +774,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; - pParsSim->nRounds = pPars->nRounds; + pParsSim->nFrames = pPars->nRounds; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = pPars->fLatchCorr; pParsSim->fSeqSimulate = 1; @@ -853,7 +853,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; - pParsSim->nRounds = pPars->nRounds; + pParsSim->nFrames = pPars->nFrames; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = pPars->fLatchCorr; pParsSim->fSeqSimulate = 1; diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h index 9c012f73..73f108ba 100644 --- a/src/aig/cec/cecInt.h +++ b/src/aig/cec/cecInt.h @@ -192,8 +192,10 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit ); /*=== cecSeq.c ============================================================*/ extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ); -extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState ); +extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter ); extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex ); +extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ); +extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c index de71ecc9..70396cca 100644 --- a/src/aig/cec/cecMan.c +++ b/src/aig/cec/cecMan.c @@ -76,13 +76,13 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p ) printf( "MinVar = %5d ", p->pPars->nSatVarMax ); printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle ); printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", - p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 ); + p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 ); ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal ); printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ", - p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 ); + p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 ); ABC_PRTP( "Time", p->timeSatSat, p->timeTotal ); printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ", - p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 ); + p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 ); ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal ); ABC_PRT( "Total time", p->timeTotal ); } diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index b19950b3..49f2a018 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -125,9 +125,9 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) { unsigned * pInfo0, * pInfo1; - int f, i, k, w, RetValue = 0; + int f, i, k, w; // assert( Gia_ManRegNum(p->pAig) > 0 ); - assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds ); + assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames ); for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ ) { pInfo0 = Vec_PtrEntry( vInfo, k ); @@ -135,7 +135,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) for ( w = 0; w < p->nWords; w++ ) pInfo1[w] = pInfo0[w]; } - for ( f = 0; f < p->pPars->nRounds; f++ ) + for ( f = 0; f < p->pPars->nFrames; f++ ) { for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) { @@ -152,13 +152,10 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) pInfo1[w] = pInfo0[w]; } if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) - { - printf( "One of the outputs of the miter is asserted.\n" ); - RetValue = 1; - } + return 1; } assert( k == Vec_PtrSize(vInfo) ); - return RetValue; + return 0; } /**Function************************************************************* @@ -172,15 +169,16 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) SeeAlso [] ***********************************************************************/ -int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState ) +int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter ) { Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; Cec_ManSim_t * pSim; int RetValue, clkTotal = clock(); assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 ); Cec_ManSimSetDefaultParams( pParsSim ); - pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig); + pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig); pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo ); + pParsSim->fCheckMiter = fCheckMiter; Gia_ManSetRefs( pAig ); pSim = Cec_ManSimStart( pAig, pParsSim ); if ( pBestState ) @@ -228,23 +226,81 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex return -1; } if ( pPars->fVerbose ) - printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 ); + printf( "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 ); Gia_ManRandom( 1 ); vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + - Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 ); + Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 ); Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex ); if ( pPars->fVerbose ) Gia_ManEquivPrintClasses( pAig, 0, 0 ); - RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL ); + RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter ); if ( pPars->fVerbose ) Gia_ManEquivPrintClasses( pAig, 0, 0 ); Vec_PtrFree( vSimInfo ); if ( pPars->fVerbose ) ABC_PRT( "Time", clock() - clkTotal ); + if ( RetValue ) + printf( "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); return RetValue; } +/**Function************************************************************* + + Synopsis [Returns the number of POs that are not const0 cands.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + if ( pAig->pReprs == NULL ) + return -1; + Gia_ManForEachPo( pAig, pObj, i ) + if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the number of POs that are not const0 cands.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; + int i, RetValue = 0; + if ( pAig->pReprs == NULL ) + return 0; + // label internal nodes driving POs + Gia_ManForEachPo( pAig, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + // check if there are non-labled equivs + Gia_ManForEachObj( pAig, pObj, i ) + if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID ) + { + RetValue = 1; + break; + } + // clean internal nodes driving POs + Gia_ManForEachPo( pAig, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 0; + return RetValue; +} + /**Function************************************************************* Synopsis [Performs semiformal refinement of equivalence classes.] @@ -258,13 +314,15 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex ***********************************************************************/ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) { - int nAddFrames = 10; // additional timeframes to simulate + int nAddFrames = 16; // additional timeframes to simulate + int nCountNoRef = 0; + int nFramesReal; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Vec_Ptr_t * vSimInfo; Vec_Str_t * vStatus; Gia_Cex_t * pState; - Gia_Man_t * pSrm; - int r, nPats, RetValue = -1; + Gia_Man_t * pSrm, * pReduce, * pAux; + int r, nPats, RetValue = 0; if ( pAig->pReprs == NULL ) { printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); @@ -290,22 +348,36 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) Gia_ManEquivPrintClasses( pAig, 0, 0 ); } // perform the given number of BMC rounds + Gia_ManCleanMark0( pAig ); for ( r = 0; r < pPars->nRounds; r++ ) { + if ( !Cec_ManCheckNonTrivialCands(pAig) ) + { + printf( "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); + break; + } // Gia_ManPrintCounterExample( pState ); // derive speculatively reduced model - pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut ); - assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * pPars->nFrames) ); +// pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut ); + pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs ); + if ( pSrm == NULL ) + { + printf( "Quitting refinement because miter could not be unrolled.\n" ); + break; + } + assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) ); + if ( pPars->fVerbose ) + printf( "Unrolled for %d frames.\n", nFramesReal ); // allocate room for simulation info vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + - Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords ); + Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords ); Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState ); // fill in simulation info with counter-examples vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats ); Vec_StrFree( vStatus ); Gia_ManStop( pSrm ); // resimulate and refine the classes - RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState ); + RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter ); Vec_PtrFree( vSimInfo ); assert( pState->iPo >= 0 ); // hit counter pState->iPo = -1; @@ -314,11 +386,47 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) printf( "BMC = %3d ", nPats ); Gia_ManEquivPrintClasses( pAig, 0, 0 ); } + + // write equivalence classes + Gia_WriteAiger( pAig, "gore.aig", 0, 0 ); + // reduce the model + pReduce = Gia_ManSpecReduce( pAig, 0, 0 ); + if ( pReduce ) + { + pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); + Gia_ManStop( pAux ); + Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 ); +// printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); +// Gia_ManPrintStatsShort( pReduce ); + Gia_ManStop( pReduce ); + } + + if ( RetValue ) + { + printf( "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" ); + break; + } + // decide when to stop + if ( nPats > 0 ) + nCountNoRef = 0; + else if ( ++nCountNoRef == pPars->nNonRefines ) + break; } ABC_FREE( pState ); + if ( pPars->fCheckMiter ) + { + int nNonConsts = Cec_ManCountNonConstOutputs( pAig ); + if ( nNonConsts ) + printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); + } return RetValue; } +//&r s13207.aig; &ps; ≡ &ps; &semi -R 2 -vm +//&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v +//r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv +//&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index 1aaf54ff..fa10d222 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -718,7 +718,7 @@ clk2 = clock(); pPat->timeTotalSave += clock() - clk3; } // quit if one of them is solved - if ( pPars->fFirstStop ) + if ( pPars->fCheckMiter ) break; } p->timeTotal = clock() - clk; @@ -810,12 +810,12 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat { if ( Gia_ObjFaninC0(pObj) ) { - printf( "Constant 1 output of SRM!!!\n" ); +// printf( "Constant 1 output of SRM!!!\n" ); Vec_StrPush( vStatus, 0 ); } else { - printf( "Constant 0 output of SRM!!!\n" ); +// printf( "Constant 0 output of SRM!!!\n" ); Vec_StrPush( vStatus, 1 ); } continue; -- cgit v1.2.3