From a2535d49a0dac5bad8d27567ad674adc78edf74b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 5 Oct 2008 08:01:00 -0700 Subject: Version abc81005 --- src/aig/fra/fra.h | 5 ++++ src/aig/fra/fraSec.c | 73 +++++++++++++++++++++++++++++++++------------------ src/aig/ssw/ssw.h | 2 ++ src/aig/ssw/sswCore.c | 36 +++++++++++++------------ src/base/abci/abc.c | 71 ++++++++++++++++++++++++++++++++++++++----------- 5 files changed, 130 insertions(+), 57 deletions(-) (limited to 'src') diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index eceda480..dc98adc9 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -116,10 +116,15 @@ struct Fra_Sec_t_ int fTryComb; // try CEC call as a preprocessing step int fTryBmc; // try BMC call as a preprocessing step int nFramesMax; // the max number of frames used for induction + int nBTLimit; // the conflict limit at a node + int nBTLimitGlobal; // the global conflict limit + int nBddMax; // the max number of BDD nodes + int nBddIterMax; // the limit on the number of BDD iterations int fPhaseAbstract; // enables phase abstraction int fRetimeFirst; // enables most-forward retiming at the beginning int fRetimeRegs; // enables min-register retiming at the beginning int fFraiging; // enables fraiging at the beginning + int fInduction; // enable the use of induction int fInterpolation; // enables interpolation int fReachability; // enables BDD based reachability int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index dce34600..216ed8df 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -46,23 +46,28 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) { memset( p, 0, sizeof(Fra_Sec_t) ); - p->fTryComb = 1; // try CEC call as a preprocessing step - p->fTryBmc = 1; // try BMC call as a preprocessing step - p->nFramesMax = 4; // the max number of frames used for induction - p->fPhaseAbstract = 1; // enables phase abstraction - p->fRetimeFirst = 1; // enables most-forward retiming at the beginning - p->fRetimeRegs = 1; // enables min-register retiming at the beginning - p->fFraiging = 1; // enables fraiging at the beginning - p->fInterpolation = 1; // enables interpolation - p->fReachability = 1; // enables BDD based reachability - p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove - p->fUseNewProver = 0; // enables new prover - p->fSilent = 0; // disables all output - p->fVerbose = 0; // enables verbose reporting of statistics - p->fVeryVerbose = 0; // enables very verbose reporting - p->TimeLimit = 0; // enables the timeout + p->fTryComb = 1; // try CEC call as a preprocessing step + p->fTryBmc = 1; // try BMC call as a preprocessing step + p->nFramesMax = 4; // the max number of frames used for induction + p->nBTLimit = 1000; // conflict limit at a node during induction + p->nBTLimitGlobal = 5000000; // global conflict limit during induction + p->nBddMax = 50000; // the limit on the number of BDD nodes + p->nBddIterMax = 1000000; // the limit on the number of BDD iterations + p->fPhaseAbstract = 0; // enables phase abstraction + p->fRetimeFirst = 1; // enables most-forward retiming at the beginning + p->fRetimeRegs = 1; // enables min-register retiming at the beginning + p->fFraiging = 1; // enables fraiging at the beginning + p->fInduction = 1; // enables the use of induction (signal correspondence) + p->fInterpolation = 1; // enables interpolation + p->fReachability = 1; // enables BDD based reachability + p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove + p->fUseNewProver = 0; // enables new prover + p->fSilent = 0; // disables all output + p->fVerbose = 0; // enables verbose reporting of statistics + p->fVeryVerbose = 0; // enables very verbose reporting + p->TimeLimit = 0; // enables the timeout // internal parameters - p->fReportSolution = 0; // enables specialized format for reporting solution + p->fReportSolution = 0; // enables specialized format for reporting solution } /**Function************************************************************* @@ -159,6 +164,7 @@ clk = clock(); pNew = Aig_ManDupOrdered( pTemp = pNew ); // pNew = Aig_ManDupDfs( pTemp = pNew ); Aig_ManStop( pTemp ); +/* if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); @@ -172,7 +178,7 @@ clk = clock(); goto finish; } } - +*/ // pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); //Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL ); @@ -228,7 +234,7 @@ PRT( "Time", clock() - clkTotal ); PRT( "Time", clock() - clk ); } } - +/* if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); @@ -242,7 +248,7 @@ PRT( "Time", clock() - clk ); goto finish; } } - +*/ // perform fraiging if ( pParSec->fFraiging ) { @@ -263,7 +269,7 @@ PRT( "Time", clock() - clk ); RetValue = Fra_FraigMiterStatus( pNew ); if ( RetValue >= 0 ) goto finish; - +/* if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); @@ -277,7 +283,7 @@ PRT( "Time", clock() - clk ); goto finish; } } - +*/ // perform min-area retiming if ( pParSec->fRetimeRegs && pNew->nRegs ) { @@ -300,9 +306,10 @@ PRT( "Time", clock() - clk ); // perform seq sweeping while increasing the number of frames RetValue = Fra_FraigMiterStatus( pNew ); - if ( RetValue == -1 ) + if ( RetValue == -1 && pParSec->fInduction ) for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 ) { +/* if ( RetValue == -1 && pParSec->TimeLimit ) { TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); @@ -316,7 +323,8 @@ PRT( "Time", clock() - clk ); goto finish; } } - +*/ + clk = clock(); pPars->nFramesK = nFrames; pPars->TimeLimit = TimeLeft; @@ -324,7 +332,19 @@ clk = clock(); // pNew = Fra_FraigInduction( pTemp = pNew, pPars ); pPars2->nFramesK = nFrames; - pPars2->nBTLimit = 1000 * nFrames; + pPars2->nBTLimit = pParSec->nBTLimit; + pPars2->nBTLimitGlobal = pParSec->nBTLimitGlobal; +// pPars2->nBTLimit = 1000 * nFrames; + + if ( RetValue == -1 && pPars2->nConflicts > pPars2->nBTLimitGlobal ) + { + if ( !pParSec->fSilent ) + printf( "Global conflict limit (%d) exceeded.\n", pPars2->nBTLimitGlobal ); + RetValue = -1; + TimeOut = 1; + goto finish; + } + Aig_ManSetRegNum( pNew, pNew->nRegs ); pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); if ( pNew == NULL ) @@ -334,6 +354,9 @@ clk = clock(); TimeOut = 1; goto finish; } + +// printf( "Total conflicts = %d.\n", pPars2->nConflicts ); + Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( pParSec->fVerbose ) @@ -477,7 +500,7 @@ PRT( "Time", clock() - clk ); extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent ); + RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, 0, pParSec->fSilent ); } finish: diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index e6e3a1b4..2785bca6 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -48,6 +48,7 @@ struct Ssw_Pars_t_ int nConstrs; // treat the last nConstrs POs as seq constraints int nMaxLevs; // the max number of levels of nodes to consider int nBTLimit; // conflict limit at a node + int nBTLimitGlobal;// conflict limit for multiple runs int nMinDomSize; // min clock domain considered for optimization int fPolarFlip; // uses polarity adjustment int fSkipCheck; // do not run equivalence check for unaffected cones @@ -62,6 +63,7 @@ struct Ssw_Pars_t_ int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only) // internal parameters int nIters; // the number of iterations performed + int nConflicts; // the total number of conflicts performed }; // sequential counter-example diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 8052ffcd..2af9e900 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -42,25 +42,26 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) { memset( p, 0, sizeof(Ssw_Pars_t) ); - p->nPartSize = 0; // size of the partition - p->nOverSize = 0; // size of the overlap between partitions - p->nFramesK = 1; // the induction depth - p->nFramesAddSim = 0; // additional frames to simulate - p->nConstrs = 0; // treat the last nConstrs POs as seq constraints - p->nBTLimit = 1000; // conflict limit at a node - p->nMinDomSize = 100; // min clock domain considered for optimization - p->fPolarFlip = 0; // uses polarity adjustment - p->fSkipCheck = 0; // do not run equivalence check for unaffected cones - p->fLatchCorr = 0; // performs register correspondence - p->fSemiFormal = 0; // enable semiformal filtering - p->fUniqueness = 0; // enable uniqueness constraints - p->fVerbose = 0; // verbose stats + p->nPartSize = 0; // size of the partition + p->nOverSize = 0; // size of the overlap between partitions + p->nFramesK = 1; // the induction depth + p->nFramesAddSim = 0; // additional frames to simulate + p->nConstrs = 0; // treat the last nConstrs POs as seq constraints + p->nBTLimit = 1000; // conflict limit at a node + p->nBTLimitGlobal = 5000000; // conflict limit for all runs + p->nMinDomSize = 100; // min clock domain considered for optimization + p->fPolarFlip = 0; // uses polarity adjustment + p->fSkipCheck = 0; // do not run equivalence check for unaffected cones + p->fLatchCorr = 0; // performs register correspondence + p->fSemiFormal = 0; // enable semiformal filtering + p->fUniqueness = 0; // enable uniqueness constraints + p->fVerbose = 0; // verbose stats // latch correspondence - p->fLatchCorrOpt = 0; // performs optimized register correspondence - p->nSatVarMax = 1000; // the max number of SAT variables - p->nRecycleCalls = 50; // calls to perform before recycling SAT solver + p->fLatchCorrOpt = 0; // performs optimized register correspondence + p->nSatVarMax = 1000; // the max number of SAT variables + p->nRecycleCalls = 50; // calls to perform before recycling SAT solver // return values - p->nIters = 0; // the number of iterations performed + p->nIters = 0; // the number of iterations performed } /**Function************************************************************* @@ -152,6 +153,7 @@ clk = clock(); else { RetValue = Ssw_ManSweep( p ); + p->pPars->nConflicts += p->pSat->stats.conflicts; if ( p->pPars->fVerbose ) { printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 50fb11ac..d6bbd5e6 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15203,9 +15203,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Fra_SecSetDefaultParams( pSecPar ); - pSecPar->TimeLimit = 300; +// pSecPar->TimeLimit = 300; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfnwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGBRarmfijwvh" ) ) != EOF ) { switch ( c ) { @@ -15215,26 +15215,59 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': pSecPar->fTryBmc ^= 1; break; - case 'T': + case 'F': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - pSecPar->TimeLimit = atoi(argv[globalUtilOptind]); + pSecPar->nFramesMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pSecPar->TimeLimit < 0 ) + if ( pSecPar->nFramesMax < 0 ) goto usage; break; - case 'F': + case 'C': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - pSecPar->nFramesMax = atoi(argv[globalUtilOptind]); + pSecPar->nBTLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pSecPar->nFramesMax < 0 ) + if ( pSecPar->nBTLimit < 0 ) + goto usage; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBTLimitGlobal = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBTLimitGlobal < 0 ) + goto usage; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBddMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBddMax < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBddIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBddIterMax < 0 ) goto usage; break; case 'a': @@ -15249,8 +15282,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': pSecPar->fFraiging ^= 1; break; - case 'n': - pSecPar->fUseNewProver ^= 1; + case 'i': + pSecPar->fInduction ^= 1; + break; + case 'j': + pSecPar->fInterpolation ^= 1; break; case 'w': pSecPar->fVeryVerbose ^= 1; @@ -15277,17 +15313,22 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfnwvh]\n" ); + fprintf( pErr, "usage: dprove [-FCGBR num] [-cbarmfijwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); - fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit ); + fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit ); + fprintf( pErr, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal ); + fprintf( pErr, "\t-B num : the BDD size limit in BDD-based reachablity [default = %d]\n", pSecPar->nBddMax ); + fprintf( pErr, "\t-R num : the max number of reachability iterations [default = %d]\n", pSecPar->nBddIterMax ); fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" ); fprintf( pErr, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", pSecPar->fTryBmc? "yes": "no" ); fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); - fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" ); + fprintf( pErr, "\t-i : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" ); + fprintf( pErr, "\t-j : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" ); +// fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); -- cgit v1.2.3