diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 12:38:59 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 12:38:59 -0800 |
commit | ae4b51351c93983a1285ce1028e3bbd90a6d5721 (patch) | |
tree | b06797a1771bb1c79124f2ac7d57f1a54c9afc34 /src/aig/fra | |
parent | f4066b5be3b5473f5c64ab71d1983df6ca7aec76 (diff) | |
download | abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.tar.gz abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.tar.bz2 abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.zip |
Cumulative changes in the last few weeks.
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 23 |
2 files changed, 24 insertions, 1 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index b046cc47..aee38d08 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -123,6 +123,7 @@ struct Fra_Sec_t_ int nBddVarsMax; // the state space limit for BDD reachability int nBddMax; // the max number of BDD nodes int nBddIterMax; // the limit on the number of BDD iterations + int nPdrTimeout; // the timeout for PDR in the end int fPhaseAbstract; // enables phase abstraction int fRetimeFirst; // enables most-forward retiming at the beginning int fRetimeRegs; // enables min-register retiming at the beginning @@ -134,6 +135,7 @@ struct Fra_Sec_t_ int fReorderImage; // enables BDD reordering during image computation int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove int fUseNewProver; // the new prover + int fUsePdr; // the PDR int fSilent; // disables all output int fVerbose; // enables verbose reporting of statistics int fVeryVerbose; // enables very verbose reporting diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 1576a70a..7608791f 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -24,6 +24,7 @@ #include "ssw.h" #include "saig.h" #include "bbr.h" +#include "pdr.h" ABC_NAMESPACE_IMPL_START @@ -70,6 +71,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) p->fReorderImage = 1; // enables variable reordering during image computation p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove p->fUseNewProver = 0; // enables new prover + p->fUsePdr = 1; // enables PDR + p->nPdrTimeout = 60; // enabled PDR timeout p->fSilent = 0; // disables all output p->fVerbose = 0; // enables verbose reporting of statistics p->fVeryVerbose = 0; // enables very verbose reporting @@ -539,7 +542,7 @@ clk = clock(); } else { - Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew ); + Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew ); RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth ); if ( pNewOrpos->pSeqModel ) { @@ -582,6 +585,24 @@ ABC_PRT( "Time", clock() - clk ); RetValue = Aig_ManVerifyUsingBdds( pNew, pPars ); } + // try PDR + if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 ) + { + Abc_Cex_t * pCex = NULL; + Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew ); + Pdr_Par_t Pars, * pPars = &Pars; + Pdr_ManSetDefaultParams( pPars ); + pPars->nTimeOut = pParSec->nPdrTimeout; + pPars->fVerbose = pParSec->fVerbose; + if ( pParSec->fVerbose ) + printf( "Running property directed reachability...\n" ); + RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex ); + if ( pCex ) + pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex ); + Aig_ManStop( pNewOrpos ); + pNew->pSeqModel = pCex; + } + finish: // report the miter if ( RetValue == 1 ) |