diff options
Diffstat (limited to 'src')
36 files changed, 1190 insertions, 489 deletions
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,25 +226,83 @@ 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.] Description [] @@ -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; diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index 38978164..7271d256 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -68,7 +68,7 @@ struct Dch_Pars_t_ /*=== dchCore.c ==========================================================*/ extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); - +extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ); #ifdef __cplusplus } diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index 4a8d8b53..d38d5668 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -90,7 +90,7 @@ p->timeTotal = clock() - clkTotal; ABC_FREE( pAig->pTable ); pResult = Dch_DeriveChoiceAig( pAig ); // count the number of representatives - if ( pPars->fVerbose ) + if ( pPars->fVerbose ) printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", Dch_DeriveChoiceCountReprs( pAig ), Dch_DeriveChoiceCountEquivs( pResult ), @@ -98,6 +98,38 @@ p->timeTotal = clock() - clkTotal; return pResult; } +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + Dch_Man_t * p; + int clk, clkTotal = clock(); + // reset random numbers + Aig_ManRandom(1); + // start the choicing manager + p = Dch_ManCreate( pAig, pPars ); + // compute candidate equivalence classes +clk = clock(); + p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose ); +p->timeSimInit = clock() - clk; +// Dch_ClassesPrint( p->ppClasses, 0 ); + p->nLits = Dch_ClassesLitNum( p->ppClasses ); + // perform SAT sweeping + Dch_ManSweep( p ); + // free memory ahead of time +p->timeTotal = clock() - clkTotal; + Dch_ManStop( p ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 72af2466..ccb3e7b1 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -480,6 +480,7 @@ clk = clock(); } else if ( pParSec->fInterSeparate ) { + Ssw_Cex_t * pCex = NULL; Aig_Man_t * pTemp, * pAux; Aig_Obj_t * pObjPo; int i, Counter = 0; @@ -495,8 +496,7 @@ clk = clock(); RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth ); if ( pTemp->pSeqModel ) { - Ssw_Cex_t * pCex; - pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; + pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) ); pCex->iPo = i; Aig_ManStop( pTemp ); break; @@ -520,7 +520,7 @@ clk = clock(); printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) ); } Aig_ManCleanup( pNew ); - if ( pNew->pSeqModel == NULL ) + if ( pCex == NULL ) { printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pNew) ); if ( Counter ) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index af92acc9..9dad2742 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -557,6 +557,7 @@ extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p ); extern int Gia_ManCheckTopoOrder( Gia_Man_t * p ); extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); extern void Gia_ManDeriveReprs( Gia_Man_t * p ); +extern int Gia_ManEquivCountLits( Gia_Man_t * p ); extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); @@ -565,6 +566,7 @@ extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ); +extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); extern void Gia_ManEquivImprove( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ); @@ -663,6 +665,7 @@ extern void Tas_ManStop( Tas_Man_t * p ); extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p ); extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); +extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); #ifdef __cplusplus diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index afe9164f..6c8ace8a 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -841,7 +841,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int // create normalized AIG if ( !Gia_ManIsNormalized(pInit) ) { - printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" ); +// printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" ); p = Gia_ManDupNormalized( pInit ); } else diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 644ccda5..e3aca7df 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -969,13 +969,13 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p ) printf( "JustMax = %5d ", p->Pars.nJustLimit ); printf( "\n" ); 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/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c index a0d97693..bd8f061b 100644 --- a/src/aig/gia/giaCSatOld.c +++ b/src/aig/gia/giaCSatOld.c @@ -680,13 +680,13 @@ void Cbs0_ManSatPrintStats( Cbs0_Man_t * p ) printf( "JustMax = %5d ", p->Pars.nJustLimit ); printf( "\n" ); 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/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 8458268c..0f680e31 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -256,6 +256,69 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits ) SeeAlso [] ***********************************************************************/ +void Gia_ManPrintStatsClasses( Gia_Man_t * p ) +{ + int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits; + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + { + if ( Gia_ObjIsHead(p, i) ) + Counter++; + else if ( Gia_ObjIsConst(p, i) ) + Counter0++; + else if ( Gia_ObjIsNone(p, i) ) + CounterX++; + if ( Gia_ObjProved(p, i) ) + Proved++; + } + CounterX -= Gia_ManCoNum(p); + nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; + +// printf( "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) ); +// printf( "and =%5d ", Gia_ManAndNum(p) ); +// printf( "lev =%3d ", Gia_ManLevelNum(p) ); + printf( "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManEquivCountLits( Gia_Man_t * p ) +{ + int i, Counter = 0, Counter0 = 0, CounterX = 0; + if ( p->pReprs == NULL || p->pNexts == NULL ) + return 0; + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + { + if ( Gia_ObjIsHead(p, i) ) + Counter++; + else if ( Gia_ObjIsConst(p, i) ) + Counter0++; + else if ( Gia_ObjIsNone(p, i) ) + CounterX++; + } + CounterX -= Gia_ManCoNum(p); + return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) { int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits; @@ -274,6 +337,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n", Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); +// printf( "cst =%8d cls =%7d lit =%8d\n", +// Counter0, Counter, nLits ); assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { @@ -696,6 +761,29 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t /**Function************************************************************* + Synopsis [Returns 1 if AIG has dangling nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHasNoEquivs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + if ( p->pReprs == NULL ) + return 1; + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + return i == Gia_ManObjNum(p); +} + +/**Function************************************************************* + Synopsis [Duplicates the AIG in the DFS order.] Description [] @@ -743,16 +831,11 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } - // check if there are any equivalences defined - Gia_ManForEachObj( p, pObj, i ) - if ( Gia_ObjReprObj(p, i) != NULL ) - break; - if ( i == Gia_ManObjNum(p) ) + if ( Gia_ManHasNoEquivs(p) ) { printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" ); return NULL; } - /* if ( !Gia_ManCheckTopoOrder( p ) ) { @@ -792,7 +875,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) return pNew; } - /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] @@ -879,6 +961,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" ); return NULL; } + /* if ( !Gia_ManCheckTopoOrder( p ) ) { @@ -918,7 +1001,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames Gia_ManAppendCo( pNew, iLitNew ); if ( Vec_IntSize(vXorLits) == 0 ) { - printf( "Speculatively reduced model has no primary outputs.\n" ); +// printf( "Speculatively reduced model has no primary outputs.\n" ); Gia_ManAppendCo( pNew, 0 ); } ABC_FREE( p->pCopies ); @@ -931,6 +1014,41 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames /**Function************************************************************* + Synopsis [Creates initialized SRM with the given number of frames.] + + Description [Uses as many frames as needed to create the number of + output not less than the number of equivalence literals.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs ) +{ + Gia_Man_t * pFrames; + int f, nLits; + nLits = Gia_ManEquivCountLits( p ); + for ( f = 1; ; f++ ) + { + pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut ); + if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) || + (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) ) + break; + if ( f == nFramesMax ) + break; + Gia_ManStop( pFrames ); + pFrames = NULL; + } + if ( f == nFramesMax ) + printf( "Stopped unrolling after %d frames.\n", nFramesMax ); + if ( pnFrames ) + *pnFrames = f; + return pFrames; +} + +/**Function************************************************************* + Synopsis [Transforms equiv classes by removing the AB nodes.] Description [] @@ -1292,6 +1410,107 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) return pNew; } +#include "aig.h" +#include "saig.h" +#include "cec.h" +#include "giaAig.h" + +/**Function************************************************************* + + Synopsis [Implements iteration during speculation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose ) +{ + extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); + Aig_Man_t * pTemp; + Gia_Man_t * pSrm, * pReduce, * pAux; + int nIter, nStart = 0; + if ( pGia->pReprs == NULL || pGia->pNexts == NULL ) + { + printf( "Gia_CommandSpecI(): Equivalence classes are not defined.\n" ); + return 0; + } + // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim + Gia_ManCleanMark0( pGia ); + Gia_ManPrintStats( pGia, 0 ); + for ( nIter = 0; ; nIter++ ) + { + if ( Gia_ManHasNoEquivs(pGia) ) + { + printf( "Gia_CommandSpecI: No equivalences left.\n" ); + break; + } + printf( "ITER %3d : ", nIter ); +// if ( fVerbose ) +// printf( "Starting BMC from frame %d.\n", nStart ); +// if ( fVerbose ) +// Gia_ManPrintStats( pGia, 0 ); + Gia_ManPrintStatsClasses( pGia ); + // perform speculative reduction +// if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) ) + if ( !Cec_ManCheckNonTrivialCands(pGia) ) + { + printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); + break; + } + pSrm = Gia_ManSpecReduce( pGia, 0, 0 ); + // bmc2 -F 100 -C 25000 + { + Gia_Cex_t * pCex; + int nFrames = nFramesInit; // different from default + int nNodeDelta = 2000; + int nBTLimit = nBTLimitInit; // different from default + int nBTLimitAll = 2000000; + pTemp = Gia_ManToAig( pSrm, 0 ); +// Aig_ManPrintStats( pTemp ); + Gia_ManStop( pSrm ); + Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 20, nBTLimit, nBTLimitAll, fVerbose, 0 ); + pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL; + Aig_ManStop( pTemp ); + if ( pCex == NULL ) + { + printf( "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" ); + break; + } + if ( fStart ) + nStart = pCex->iFrame; + // perform simulation + { + Cec_ParSim_t Pars, * pPars = &Pars; + Cec_ManSimSetDefaultParams( pPars ); + pPars->fCheckMiter = fCheckMiter; + if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) ) + { + ABC_FREE( pCex ); + break; + } + ABC_FREE( pCex ); + } + } + // write equivalence classes + Gia_WriteAiger( pGia, "gore.aig", 0, 0 ); + // reduce the model + pReduce = Gia_ManSpecReduce( pGia, 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 ); + } + } + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c index 6d29dfb9..d1f89c07 100644 --- a/src/aig/int/intCore.c +++ b/src/aig/int/intCore.c @@ -193,7 +193,7 @@ p->timeCnf += clock() - clk; } // likely spurious counter-example p->nFrames += i; - Inter_ManClean( p ); + Inter_ManClean( p ); break; } else if ( RetValue == -1 ) // timed out diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c index b81414a5..6aaa6c64 100644 --- a/src/aig/ioa/ioaReadAig.c +++ b/src/aig/ioa/ioaReadAig.c @@ -88,34 +88,27 @@ Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries ) /**Function************************************************************* - Synopsis [Reads the AIG in the binary AIGER format.] + Synopsis [Reads the AIG in from the memory buffer.] - Description [] + Description [The buffer constains the AIG in AIGER format. The size gives + the number of types in the buffer. The buffer is allocated by the user + and not deallocated by this procedure.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) +Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ) { -// Bar_Progress_t * pProgress; - FILE * pFile; Vec_Int_t * vLits = NULL; Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms; Aig_Obj_t * pObj, * pNode0, * pNode1; Aig_Man_t * pNew; - int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits; - char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType; + int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits; + char * pDrivers, * pSymbols, * pCur;//, * pType; unsigned uLit0, uLit1, uLit; - // read the file into the buffer - nFileSize = Ioa_FileSize( pFileName ); - pFile = fopen( pFileName, "rb" ); - pContents = ABC_ALLOC( char, nFileSize ); - fread( pContents, nFileSize, 1, pFile ); - fclose( pFile ); - // check if the input file format is correct if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') ) { @@ -145,10 +138,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) // allocate the empty AIG pNew = Aig_ManStart( nAnds ); - pName = Ioa_FileNameGeneric( pFileName ); - pNew->pName = Aig_UtilStrsav( pName ); -// pNew->pSpec = Ioa_UtilStrsav( pFileName ); - ABC_FREE( pName ); // prepare the array of nodes vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); @@ -355,7 +344,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) } // skipping the comments - ABC_FREE( pContents ); Vec_PtrFree( vNodes ); // remove the extra nodes @@ -372,6 +360,43 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) return pNew; } +/**Function************************************************************* + + Synopsis [Reads the AIG in the binary AIGER format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) +{ + FILE * pFile; + Aig_Man_t * pNew; + char * pName, * pContents; + int nFileSize; + + // read the file into the buffer + nFileSize = Ioa_FileSize( pFileName ); + pFile = fopen( pFileName, "rb" ); + pContents = ABC_ALLOC( char, nFileSize ); + fread( pContents, nFileSize, 1, pFile ); + fclose( pFile ); + + pNew = Ioa_ReadAigerFromMemory( pContents, nFileSize, fCheck ); + ABC_FREE( pContents ); + if ( pNew ) + { + pName = Ioa_FileNameGeneric( pFileName ); + pNew->pName = Aig_UtilStrsav( pName ); +// pNew->pSpec = Ioa_UtilStrsav( pFileName ); + ABC_FREE( pName ); + } + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 3ca8dfd7..1d7ac393 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -21,6 +21,7 @@ #include "ntl.h" #include "fra.h" #include "ssw.h" +#include "dch.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -400,12 +401,17 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev } // perform fraiging for the given design -// if ( fUseCSat ) - if ( 0 ) + if ( fUseCSat ) { - extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ); - pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose ); - Aig_ManStop( pTemp ); +// extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ); +// pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose ); +// Aig_ManStop( pTemp ); + extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ); + Dch_Pars_t Pars, * pPars = &Pars; + Dch_ManSetDefaultParams( pPars ); + pPars->nBTLimit = nConfLimit; + pPars->fVerbose = fVerbose; + Dch_ComputeEquivalences( pAigCol, pPars ); } else { diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 85d2d191..b77a4292 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -90,10 +90,10 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ); +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); -extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); +extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite ); /*=== saigCone.c ==========================================================*/ extern void Saig_ManPrintCones( Aig_Man_t * p ); /*=== saigDup.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 3da92fc0..844d6f24 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -25,6 +25,7 @@ #include "satStore.h" #include "ssw.h" #include "ioa.h" +#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -694,17 +695,38 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose ) +Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int * pnUseStart, int fVerbose ) { - extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); + extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite ); extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose ); + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); Vec_Int_t * vFlopsNew, * vPiToReg; Aig_Obj_t * pObj; int i, Entry, iFlop; - Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose ); + if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 ) + { + Fra_Sec_t SecPar, * pSecPar = &SecPar; + int RetValue; + Fra_SecSetDefaultParams( pSecPar ); + pSecPar->fVerbose = fVerbose; + RetValue = Fra_FraigSec( pAbs, pSecPar, NULL ); + } + else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) ) + { + int nBddMax = 1000000; + int nIterMax = nFrames; + int fPartition = 1; + int fReorder = 1; + int fReorderImage = 1; + Aig_ManVerifyUsingBdds( pAbs, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 ); + } + else + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 20, nConfMaxOne, 1000000, fVerbose, 0 ); if ( pAbs->pSeqModel == NULL ) return NULL; + if ( pnUseStart ) + *pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame; // Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel ); vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); if ( Vec_IntSize(vFlopsNew) == 0 ) @@ -766,7 +788,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ) +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -845,13 +867,14 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, Saig_AbsExtendOneStep( p, vFlops ); if ( fVerbose ) printf( " %d flops.\n", Vec_IntSize(vFlops) ); - } + } */ // create the resulting AIG pResult = Saig_ManAbstraction( p, vFlops ); if ( fExtend ) { + int nUseStart = 0; if ( !fVerbose ) { printf( "Init : " ); @@ -860,21 +883,19 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, printf( "Refining abstraction...\n" ); for ( Iter = 0; ; Iter++ ) { - char FileName[100]; - pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose ); + pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose ); if ( pTemp == NULL ) break; Aig_ManStop( pResult ); pResult = pTemp; - printf( "%4d : ", Iter ); + printf( "ITER %4d : ", Iter ); if ( !fVerbose ) Aig_ManPrintStats( pResult ); - else - printf( " -----------------------------------------------------\n" ); +// else +// printf( " -----------------------------------------------------\n" ); // output the intermediate result of abstraction - sprintf( FileName, "gabs%02d.aig", Iter ); - Ioa_WriteAiger( pResult, FileName, 0, 0 ); - printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName ); + Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); +// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); // check if the ratio is reached if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio ) { @@ -886,6 +907,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, } } Vec_IntFree( vFlops ); + // write the final result + if ( pResult ) + { + Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); + printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); + } return pResult; } diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 57759594..a37be3ad 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -508,7 +508,7 @@ Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_BmcSolveTargets( Saig_Bmc_t * p ) +int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved ) { Aig_Obj_t * pObj; int i, VarNum, Lit, RetValue; @@ -520,6 +520,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p ) } Vec_PtrForEachEntry( p->vTargets, pObj, i ) { + if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart ) + continue; if ( p->pSat->stats.conflicts > p->nConfMaxAll ) return l_Undef; VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) ); @@ -575,11 +577,12 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ) +void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite ) { Saig_Bmc_t * p; Aig_Man_t * pNew; Cnf_Dat_t * pCnf; + int nOutsSolved = 0; int Iter, RetValue, clk = clock(), clk2; p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); if ( fVerbose ) @@ -609,7 +612,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf Cnf_DataFree( pCnf ); Aig_ManStop( pNew ); // solve the targets - RetValue = Saig_BmcSolveTargets( p ); + RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved ); if ( fVerbose ) { printf( "%3d : F = %3d. O =%4d. And = %7d. Var = %7d. Conf = %7d. ", @@ -620,11 +623,21 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf break; } if ( RetValue == l_True ) + { + assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved ); printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->iOutputFail, p->iFrameFail ); + } else // if ( RetValue == l_False || RetValue == l_Undef ) printf( "No output was asserted in %d frames. ", p->iFramePrev-1 ); - ABC_PRT( "Time", clock() - clk ); + if ( fVerbOverwrite ) + { + ABC_PRTr( "Time", clock() - clk ); + } + else + { + ABC_PRT( "Time", clock() - clk ); + } if ( RetValue != l_True ) { if ( p->iFrameLast >= p->nFramesMax ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e1cdadac..b73fdf9a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -45,275 +45,279 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintXCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintDsd ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPrintMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMulti ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandLutmin ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTopAnd ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCareSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCover ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandInter ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSenseInput ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDC2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDProve2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSimSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandMatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -//static int Abc_CommandHaigStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandHaigStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandHaigUse ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -//static int Abc_CommandRecStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandRecStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandRecAdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandRecPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandRecUse ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFpgaFast ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIf ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandFlowRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeqSweep2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeqSweepTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandExtWin ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBmc2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPBAbstraction ( Abc_Frame_t * pAbc, int argc, char ** argv ); - - -static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); - - -static int Abc_CommandAbc8Read ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8ReadLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Write ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8ReadLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8PrintLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Check ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandAbc8Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Pfan ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8If ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8DChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8DC2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Bidec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Strash ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Lutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Lutmin ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Insert ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Ssw ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8Zero ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandAbc8Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc8DSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static int Abc_CommandAbc9Get ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Put ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Read ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Write ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Semi ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Times ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Frames ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Retime ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Enable ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintXCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintDsd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMulti ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandLutmin ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTopAnd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCareSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCover ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInter ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSenseInput ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDC2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDProve2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSimSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +//static int Abc_CommandHaigStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandHaigStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandHaigUse ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +//static int Abc_CommandRecStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandRecStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandRecAdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandRecPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandRecUse ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFpgaFast ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIf ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFlowRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqSweep2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqSweepTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExtWin ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmc2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPBAbstraction ( Abc_Frame_t * pAbc, int argc, char ** argv ); + + +static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); + + +static int Abc_CommandAbc8Read ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8ReadLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Write ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8ReadLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8PrintLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Check ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandAbc8Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Pfan ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8If ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8DChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8DC2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Bidec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Strash ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Lutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Lutmin ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Insert ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Ssw ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Zero ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandAbc8Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8DSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandAbc9Get ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Put ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Read ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Write ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Semi ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Times ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Frames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Retime ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Enable ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +extern int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, char ** argv ); +extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -370,6 +374,14 @@ void Abc_FrameClearDesign() ***********************************************************************/ void Abc_Init( Abc_Frame_t * pAbc ) { +/* + { + Aig_Man_t * pAig; + pAig = Ioa_ReadAiger( "i10.aig", 1 ); + Aig_ManStop( pAig ); + } +*/ + // Amap_LibParseTest( "at\\syn\\libraries\\LIBS\\BRDCM\\tsmc13_5.ff.genlib" ); // Amap_LibParseTest( "at\\syn\\libraries\\LIBS\\GS60\\GS60_W_30_1.7_CORE.genlib" ); // Amap_LibParseTest( "at\\syn\\libraries\\LIBS\\TYPICAL\\typical.genlib" ); @@ -614,6 +626,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "AIG", "&dfs", Abc_CommandAbc9Dfs, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&sim", Abc_CommandAbc9Sim, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&resim", Abc_CommandAbc9Resim, 0 ); + Cmd_CommandAdd( pAbc, "AIG", "&speci", Abc_CommandAbc9SpecI, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&equiv", Abc_CommandAbc9Equiv, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&semi", Abc_CommandAbc9Semi, 0 ); Cmd_CommandAdd( pAbc, "AIG", "×", Abc_CommandAbc9Times, 0 ); @@ -637,7 +650,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "AIG", "&dch", Abc_CommandAbc9Dch, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&test", Abc_CommandAbc9Test, 0 ); - Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "l2s", Abc_CommandAbcLivenessToSafety, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "l2ssim", Abc_CommandAbcLivenessToSafetySim, 0 ); + + Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); @@ -6637,6 +6653,7 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv ) */ // Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose ); + pAbc->pCex = pNtk->pSeqModel; // temporary ??? return 0; usage: @@ -15339,7 +15356,7 @@ usage: fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut ); fprintf( pErr, "\t-n : toggle new vs. old implementation [default = %s]\n", fNew? "new": "old" ); fprintf( pErr, "\t-c : toggle comb vs. seq simulaton [default = %s]\n", fComb? "comb": "seq" ); - fprintf( pErr, "\t-m : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "not miter" ); + fprintf( pErr, "\t-m : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "circuit" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -17908,7 +17925,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) int nCofFanLit; int fVerbose; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -18025,7 +18042,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Does not work for combinational networks.\n" ); return 0; } - Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, nCofFanLit, fVerbose ); + Abc_NtkDarBmc( pNtk, 0, nFrames, nSizeMax, nNodeDelta, 0, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, nCofFanLit, fVerbose ); pAbc->pCex = pNtk->pSeqModel; // temporary ??? return 0; @@ -18062,35 +18079,50 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + int nStart; int nFrames; int nSizeMax; int nBTLimit; int nBTLimitAll; int nNodeDelta; + int nTimeOut; int fRewrite; int fNewAlgo; int fVerbose; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + nStart = 0; nFrames = 2000; nSizeMax = 200000; nBTLimit = 2000; nBTLimitAll = 2000000; nNodeDelta = 2000; + nTimeOut = 0; fRewrite = 0; fNewAlgo = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFNTCGDrvh" ) ) != EOF ) { switch ( c ) { + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStart < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { @@ -18113,6 +18145,17 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nSizeMax < 0 ) goto usage; break; + case 'T': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -18176,16 +18219,18 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Does not work for combinational networks.\n" ); return 0; } - Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, fVerbose ); + Abc_NtkDarBmc( pNtk, nStart, nFrames, nSizeMax, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, fVerbose ); pAbc->pCex = pNtk->pSeqModel; // temporary ??? return 0; usage: // fprintf( pErr, "usage: bmc2 [-FNCGD num] [-ravh]\n" ); - fprintf( pErr, "usage: bmc2 [-FCGD num] [-vh]\n" ); + fprintf( pErr, "usage: bmc2 [-SFTCGD num] [-vh]\n" ); fprintf( pErr, "\t performs bounded model checking with dynamic unrolling\n" ); + fprintf( pErr, "\t-S num : the starting time frame [default = %d]\n", nStart ); fprintf( pErr, "\t-F num : the max number of time frames [default = %d]\n", nFrames ); // fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax ); + fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeOut ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll ); fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta ); @@ -18337,6 +18382,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_NtkDarBmcInter( pNtk, pPars ); } + pAbc->pCex = pNtk->pSeqModel; // temporary ??? return 0; usage: @@ -18765,9 +18811,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) int nFramesBmc; int nConfMaxBmc; int nRatio; + int fUseBdds; + int fUseDprove; + int fUseStart; int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -18782,9 +18831,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) nFramesBmc = 2000; nConfMaxBmc = 5000; nRatio = 10; + fUseBdds = 0; + fUseDprove = 0; + fUseStart = 1; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesrpfvh" ) ) != EOF ) { switch ( c ) { @@ -18852,6 +18904,15 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSkipProof ^= 1; break; + case 'r': + fUseBdds ^= 1; + break; + case 'p': + fUseDprove ^= 1; + break; + case 'f': + fUseStart ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -18883,7 +18944,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose ); + pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose ); if ( pNtkRes == NULL ) { if ( pNtk->pSeqModel == NULL ) @@ -18894,7 +18955,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: abs [-FCGDR num] [-desvh]\n" ); + fprintf( pErr, "usage: abs [-FCGDR num] [-desrpfvh]\n" ); fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" ); fprintf( pErr, "\t followed by counter-example-based abstraction\n" ); fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax ); @@ -18905,6 +18966,9 @@ usage: fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" ); fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" ); fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" ); + fprintf( pErr, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", fUseBdds? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", fUseDprove? "yes": "no" ); + fprintf( pErr, "\t-f : toggle starting BMC from a later frame [default = %s]\n", fUseStart? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -20958,7 +21022,7 @@ usage: SideEffects [] - SeeAlso [] + SeeAlso [] ***********************************************************************/ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) @@ -23049,7 +23113,7 @@ usage: fprintf( stdout, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); fprintf( stdout, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters ); fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); - fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "not miter" ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -23082,9 +23146,9 @@ int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - pPars->nRounds = atoi(argv[globalUtilOptind]); + pPars->nFrames = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRounds < 0 ) + if ( pPars->nFrames < 0 ) goto usage; break; case 'm': @@ -23110,13 +23174,96 @@ int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( stdout, "usage: &resim [-F <num>] [-mvh]\n" ); fprintf( stdout, "\t resimulates equivalence classes using counter-example\n" ); - fprintf( stdout, "\t-F num : the number of additinal frames to simulate [default = %d]\n", pPars->nRounds ); - fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "not miter" ); + fprintf( stdout, "\t-F num : the number of additinal frames to simulate [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9SpecI( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Gia_CommandSpecI( Gia_Man_t * pGia, int nFrames, int nBTLimit, int fUseStart, int fCheckMiter, int fVerbose ); + int nFrames = 100; + int nBTLimit = 25000; + int fUseStart = 1; + int fCheckMiter = 1; + int fVerbose = 0; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FCfmvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBTLimit < 0 ) + goto usage; + break; + case 'f': + fUseStart ^= 1; + break; + case 'm': + fCheckMiter ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pAig == NULL ) + { + printf( "Abc_CommandAbc9SpecI(): There is no AIG.\n" ); + return 1; + } + Gia_CommandSpecI( pAbc->pAig, nFrames, nBTLimit, fUseStart, fCheckMiter, fVerbose ); + return 0; + +usage: + fprintf( stdout, "usage: &speci [-FC <num>] [-fmvh]\n" ); + fprintf( stdout, "\t refines equivalence classes using speculative reduction\n" ); + fprintf( stdout, "\t-F num : the max number of time frames [default = %d]\n", nFrames ); + fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); + fprintf( stdout, "\t-f : toggle starting BMC from a later frame [default = %s]\n", fUseStart? "yes": "no" ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", fCheckMiter? "miter": "circuit" ); + fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + + /**Function************************************************************* @@ -23135,7 +23282,7 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManSimSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRTsmfdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFRSTsmdvh" ) ) != EOF ) { switch ( c ) { @@ -23150,6 +23297,17 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nWords < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFrames < 0 ) + goto usage; + break; case 'R': if ( globalUtilOptind >= argc ) { @@ -23161,6 +23319,17 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nRounds < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nNonRefines = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nNonRefines < 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -23178,9 +23347,6 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fCheckMiter ^= 1; break; - case 'f': - pPars->fFirstStop ^= 1; - break; case 'd': pPars->fDualOut ^= 1; break; @@ -23202,14 +23368,15 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &equiv [-WRT <num>] [-smfdvh]\n" ); + fprintf( stdout, "usage: &equiv [-WFRST <num>] [-smdvh]\n" ); fprintf( stdout, "\t computes candidate equivalence classes\n" ); fprintf( stdout, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); - fprintf( stdout, "\t-R num : the number of rounds to simulate [default = %d]\n", pPars->nRounds ); + fprintf( stdout, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-R num : the max number of simulation rounds [default = %d]\n", pPars->nRounds ); + fprintf( stdout, "\t-S num : the max number of rounds w/o refinement to stop [default = %d]\n", pPars->nNonRefines ); fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); fprintf( stdout, "\t-s : toggle seq vs. comb simulation [default = %s]\n", pPars->fSeqSimulate? "yes": "no" ); - fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" ); - fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); fprintf( stdout, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -23233,7 +23400,7 @@ int Abc_CommandAbc9Semi( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManSmfSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRFCTmfdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WRFSMCTmdvh" ) ) != EOF ) { switch ( c ) { @@ -23270,6 +23437,28 @@ int Abc_CommandAbc9Semi( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nFrames < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nNonRefines = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nNonRefines < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMinOutputs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMinOutputs < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -23295,9 +23484,6 @@ int Abc_CommandAbc9Semi( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fCheckMiter ^= 1; break; - case 'f': - pPars->fFirstStop ^= 1; - break; case 'd': pPars->fDualOut ^= 1; break; @@ -23319,15 +23505,16 @@ int Abc_CommandAbc9Semi( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &semi [-WRFCT <num>] [-mfdvh]\n" ); + fprintf( stdout, "usage: &semi [-WRFSMCT <num>] [-mdvh]\n" ); fprintf( stdout, "\t performs semiformal refinement of equivalence classes\n" ); fprintf( stdout, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); - fprintf( stdout, "\t-R num : the number of rounds to simulate [default = %d]\n", pPars->nRounds ); - fprintf( stdout, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-R num : the max number of rounds to simulate [default = %d]\n", pPars->nRounds ); + fprintf( stdout, "\t-F num : the max number of frames to unroll [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-S num : the max number of rounds w/o refinement to stop [default = %d]\n", pPars->nNonRefines ); + fprintf( stdout, "\t-M num : the min number of outputs of bounded SRM [default = %d]\n", pPars->nMinOutputs ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); - fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" ); - fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); fprintf( stdout, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -23775,7 +23962,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ManCorSetDefaultParams( pPars ); pPars->fLatchCorr = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrcvh" ) ) != EOF ) { switch ( c ) { @@ -23812,9 +23999,6 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nPrefix < 0 ) goto usage; break; - case 'f': - pPars->fFirstStop ^= 1; - break; case 'r': pPars->fUseRings ^= 1; break; @@ -23844,12 +24028,11 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &lcorr [-FCP num] [-frcvh]\n" ); + fprintf( stdout, "usage: &lcorr [-FCP num] [-rcvh]\n" ); fprintf( stdout, "\t performs latch correpondence computation\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); - fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -23875,7 +24058,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManCorSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrecvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecvh" ) ) != EOF ) { switch ( c ) { @@ -23912,9 +24095,6 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nPrefix < 0 ) goto usage; break; - case 'f': - pPars->fFirstStop ^= 1; - break; case 'r': pPars->fUseRings ^= 1; break; @@ -23947,12 +24127,11 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &scorr [-FCP num] [-frecvh]\n" ); + fprintf( stdout, "usage: &scorr [-FCP num] [-recvh]\n" ); fprintf( stdout, "\t performs signal correpondence computation\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); - fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); @@ -24048,7 +24227,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCSat = 0; Cec_ManSatSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmftcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmtcvh" ) ) != EOF ) { switch ( c ) { @@ -24091,9 +24270,6 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fCheckMiter ^= 1; break; - case 'f': - pPars->fFirstStop ^= 1; - break; case 't': pPars->fLearnCls ^= 1; break; @@ -24133,14 +24309,13 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfctvh]\n" ); + fprintf( stdout, "usage: &sat [-CSN <num>] [-nmctvh]\n" ); fprintf( stdout, "\t performs SAT solving for the combinational outputs\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax ); fprintf( stdout, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle ); fprintf( stdout, "\t-n : toggle using non-chronological backtracking [default = %s]\n", pPars->fNonChrono? "yes": "no" ); - fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" ); - fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" ); fprintf( stdout, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -24166,7 +24341,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManFraSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmfdwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdwvh" ) ) != EOF ) { switch ( c ) { @@ -24242,9 +24417,6 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fCheckMiter ^= 1; break; - case 'f': - pPars->fFirstStop ^= 1; - break; case 'd': pPars->fDualOut ^= 1; break; @@ -24272,7 +24444,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &fraig [-WRILDC <num>] [-rmfdwvh]\n" ); + fprintf( stdout, "usage: &fraig [-WRILDC <num>] [-rmdwvh]\n" ); fprintf( stdout, "\t performs combinational SAT sweeping\n" ); fprintf( stdout, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); fprintf( stdout, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds ); @@ -24281,8 +24453,7 @@ usage: fprintf( stdout, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" ); - fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" ); - fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); + fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); fprintf( stdout, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" ); fprintf( stdout, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 1220cb40..e30c6a93 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1550,7 +1550,7 @@ static void sigfunc( int signo ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ) +int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ) { Aig_Man_t * pMan; int status, RetValue = -1, clk = clock(); @@ -1632,7 +1632,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); } */ - Saig_BmcPerform( pMan, nFrames, nNodeDelta, nBTLimit, nBTLimitAll, fVerbose ); + Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0 ); ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; @@ -1676,11 +1676,6 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars ) pTemp = Aig_ManDupOneOutput( pMan, i, 1 ); pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 ); Aig_ManStop( pAux ); - if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) ) - { - Aig_ManStop( pTemp ); - continue; - } RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame ); if ( pTemp->pSeqModel ) { @@ -1864,7 +1859,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) } if ( pSecPar->fTryBmc ) { - RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0, 0 ); + RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0 ); if ( RetValue == 0 ) { printf( "Networks are not equivalent.\n" ); @@ -2675,7 +2670,7 @@ ABC_PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; @@ -2685,7 +2680,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf return NULL; Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose ); if ( pTemp->pSeqModel ) { ABC_FREE( pNtk->pModel ); @@ -3498,7 +3493,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) return NULL; /* Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, 1 ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 ); Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 9e0347d5..904d612b 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -504,7 +504,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 ); Abc_NtkDelete( pNtkTemp ); } - + // check the case when the 0000 simulation pattern detect the bug pObj = Abc_NtkPo(pNtk,0); pFanin = Abc_ObjFanin0(pObj); diff --git a/src/map/amap/amapGraph.c b/src/map/amap/amapGraph.c index 0e9fd85c..6f269301 100644 --- a/src/map/amap/amapGraph.c +++ b/src/map/amap/amapGraph.c @@ -115,6 +115,7 @@ Amap_Obj_t * Amap_ManCreatePo( Amap_Man_t * p, Amap_Obj_t * pFan0 ) pObj->Level = Amap_Regular(pFan0)->Level; if ( p->nLevelMax < (int)pObj->Level ) p->nLevelMax = (int)pObj->Level; + assert( p->nLevelMax < 4094 ); // 2^12-2 p->nObjs[AMAP_OBJ_PO]++; return pObj; } @@ -142,6 +143,7 @@ Amap_Obj_t * Amap_ManCreateAnd( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pObj->Level = 1 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level ); if ( p->nLevelMax < (int)pObj->Level ) p->nLevelMax = (int)pObj->Level; + assert( p->nLevelMax < 4094 ); // 2^12-2 p->nObjs[AMAP_OBJ_AND]++; return pObj; } @@ -168,6 +170,7 @@ Amap_Obj_t * Amap_ManCreateXor( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pObj->Level = 2 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level ); if ( p->nLevelMax < (int)pObj->Level ) p->nLevelMax = (int)pObj->Level; + assert( p->nLevelMax < 4094 ); // 2^12-2 p->nObjs[AMAP_OBJ_XOR]++; return pObj; } @@ -197,6 +200,7 @@ Amap_Obj_t * Amap_ManCreateMux( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pObj->Level = 2 + ABC_MAX( pObj->Level, Amap_Regular(pFanC)->Level ); if ( p->nLevelMax < (int)pObj->Level ) p->nLevelMax = (int)pObj->Level; + assert( p->nLevelMax < 4094 ); // 2^12-2 p->nObjs[AMAP_OBJ_MUX]++; return pObj; } @@ -227,6 +231,7 @@ void Amap_ManCreateChoice( Amap_Man_t * p, Amap_Obj_t * pObj ) // mark the largest level if ( p->nLevelMax < (int)pObj->Level ) p->nLevelMax = (int)pObj->Level; + assert( p->nLevelMax < 4094 ); // 2^12-2 } /**Function************************************************************* diff --git a/src/map/amap/amapInt.h b/src/map/amap/amapInt.h index dec7e799..d6d5d68b 100644 --- a/src/map/amap/amapInt.h +++ b/src/map/amap/amapInt.h @@ -200,8 +200,8 @@ struct Amap_Obj_t_ unsigned fPhase : 1; unsigned fRepr : 1; unsigned fPolar : 1; // pCutBest->fInv ^ pSetBest->fInv - unsigned Level : 20; - unsigned nCuts : 12; + unsigned Level : 12; // 20 (July 16, 2009) + unsigned nCuts : 20; // 12 (July 16, 2009) int nRefs; int Equiv; int Fan[3]; diff --git a/src/map/amap/amapMerge.c b/src/map/amap/amapMerge.c index 1a6e3804..23d8384b 100644 --- a/src/map/amap/amapMerge.c +++ b/src/map/amap/amapMerge.c @@ -170,9 +170,10 @@ Amap_Cut_t * Amap_ManCutCreate3( Amap_Man_t * p, ***********************************************************************/ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode ) { + int nMaxCuts = 500; int * pBuffer; Amap_Cut_t * pNext, * pCut; - int i, nWords, Entry, nCuts; + int i, nWords, Entry, nCuts, nCuts2; assert( pNode->pData == NULL ); // count memory needed nCuts = 1; @@ -182,7 +183,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode ) for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) ) { nCuts++; - nWords += pCut->nFans + 1; + if ( nCuts < nMaxCuts ) + nWords += pCut->nFans + 1; } } p->nBytesUsed += 4*nWords; @@ -194,17 +196,23 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode ) pNext->fInv = 0; pNext->nFans = 1; pNext->Fans[0] = Amap_Var2Lit(pNode->Id, 0); - pNext = (Amap_Cut_t *)(pBuffer + 2); + pNext = (Amap_Cut_t *)(pBuffer + 2); // add other cuts + nCuts2 = 1; Vec_IntForEachEntry( p->vTemp, Entry, i ) { for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) ) { - memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) ); - pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1); + nCuts2++; + if ( nCuts2 < nMaxCuts ) + { + memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) ); + pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1); + } } p->ppCutsTemp[Entry] = NULL; } + assert( nCuts == nCuts2 ); assert( (int *)pNext - pBuffer == nWords ); // restore the storage Vec_IntClear( p->vTemp ); @@ -213,7 +221,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode ) if ( p->ppCutsTemp[i] != NULL ) printf( "Amap_ManCutSaveStored(): Error!\n" ); pNode->pData = (Amap_Cut_t *)pBuffer; - pNode->nCuts = nCuts; + pNode->nCuts = ABC_MIN( nCuts, nMaxCuts-1 ); + assert( nCuts < (1<<20) ); // printf("%d ", nCuts ); // verify cuts pCut = NULL; @@ -221,6 +230,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode ) // for ( i = 0, pNext = (Amap_Cut_t *)pNode->pData; i < (int)pNode->nCuts; // i++, pNext = Amap_ManCutNext(pNext) ) { + if ( i == nMaxCuts ) + break; assert( pCut == NULL || pCut->iMat <= pNext->iMat ); pCut = pNext; } @@ -311,8 +322,11 @@ void Amap_ManMergeNodeChoice( Amap_Man_t * p, Amap_Obj_t * pNode ) for ( pTemp = pNode; pTemp; pTemp = Amap_ObjChoice(p, pTemp) ) { Amap_NodeForEachCut( pTemp, pCut, c ) + { + if (!pCut) break; // mikelee added; abort when pCut is NULL if ( pCut->iMat ) Amap_ManCutStore( p, pCut, pNode->fPhase ^ pTemp->fPhase ); + } pTemp->pData = NULL; } Amap_ManCutSaveStored( p, pNode ); diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index f58e3ddf..3c6ca9aa 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -154,6 +154,7 @@ typedef unsigned __int64 ABC_UINT64_T; #define ABC_INFINITY (100000000) #define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))) +#define ABC_PRTr(a,t) (printf("%s = ", (a)), printf("%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC))) #define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC))) #define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)) #define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.2f Mb ", 1.0*(f)/(1<<20))) diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 20d3799c..78d45b14 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -265,6 +265,9 @@ clk = clock(); p->nNodesBad++; return 1; } +clk = clock(); + Abc_NtkMfsConstructGia( p ); +p->timeGia += clock() - clk; // solve the SAT problem if ( p->pPars->fPower ) Abc_NtkMfsEdgePower( p, pNode ); @@ -277,6 +280,7 @@ clk = clock(); Abc_NtkMfsResubNode2( p, pNode ); } p->timeSat += clock() - clk; + Abc_NtkMfsDeconstructGia( p ); return 1; } diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 13f0bce2..6a1d9688 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -32,6 +32,7 @@ #include "satSolver.h" #include "satStore.h" #include "bdc.h" +#include "gia.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -65,6 +66,12 @@ struct Mfs_Man_t_ int nCexes; // the numbe rof current counter-examples int nSatCalls; int nSatCexes; + // intermediate AIG data + Gia_Man_t * pGia; // replica of the AIG in the new package + Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes + Tas_Man_t * pTas; // the SAT solver + Vec_Int_t * vCex; // the counter-example + Vec_Ptr_t * vGiaLits; // literals given as assumptions // used for bidecomposition Vec_Int_t * vTruth; Bdc_Man_t * pManDec; @@ -110,6 +117,7 @@ struct Mfs_Man_t_ int timeWin; int timeDiv; int timeAig; + int timeGia; int timeCnf; int timeSat; int timeInt; @@ -155,6 +163,10 @@ extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode /*=== mfsWin.c ==========================================================*/ extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ); +/*=== mfsGia.c ==========================================================*/ +extern void Abc_NtkMfsConstructGia( Mfs_Man_t * p ); +extern void Abc_NtkMfsDeconstructGia( Mfs_Man_t * p ); +extern int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands ); #ifdef __cplusplus } diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index e947bd52..71595f6c 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -157,15 +157,16 @@ void Mfs_ManPrint( Mfs_Man_t * p ) printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n", p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); } -/* + ABC_PRTP( "Win", p->timeWin , p->timeTotal ); ABC_PRTP( "Div", p->timeDiv , p->timeTotal ); ABC_PRTP( "Aig", p->timeAig , p->timeTotal ); + ABC_PRTP( "Gia", p->timeGia , p->timeTotal ); ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal ); ABC_PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); ABC_PRTP( "Int", p->timeInt , p->timeTotal ); ABC_PRTP( "ALL", p->timeTotal , p->timeTotal ); -*/ + } /**Function************************************************************* diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 008b6863..8cd70dbf 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -99,9 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) { unsigned * pData; int RetValue, iVar, i; + int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands ); +p->timeGia += clock() - clk; + p->nSatCalls++; RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); // assert( RetValue == l_False || RetValue == l_True ); + if ( RetValue != l_Undef && RetValue2 != -1 ) + { + assert( (RetValue == l_False) == (RetValue2 == 1) ); + } + if ( RetValue == l_False ) return 1; if ( RetValue != l_True ) diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make index 544accec..bafc1ce5 100644 --- a/src/opt/mfs/module.make +++ b/src/opt/mfs/module.make @@ -1,5 +1,6 @@ SRC += src/opt/mfs/mfsCore.c \ src/opt/mfs/mfsDiv.c \ + src/opt/mfs/mfsGia.c \ src/opt/mfs/mfsInter.c \ src/opt/mfs/mfsMan.c \ src/opt/mfs/mfsResub.c \ |