summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/fra/fra.h5
-rw-r--r--src/aig/fra/fraSec.c73
-rw-r--r--src/aig/ssw/ssw.h2
-rw-r--r--src/aig/ssw/sswCore.c36
4 files changed, 74 insertions, 42 deletions
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. ",
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-19 15:04:41 +0000