Cumulative changes in the last few weeks.

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 )