From fffd733f948622f39bacd2545100dd799f5a3140 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 19 Jan 2012 14:24:56 -0800
Subject: Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to
 control BMC frames and conflicts.

---
 src/base/abci/abc.c    | 34 ++++++++++++++++++++++++++++++----
 src/base/abci/abcDar.c | 28 +++++++++++++++-------------
 2 files changed, 45 insertions(+), 17 deletions(-)

(limited to 'src/base/abci')

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f57d06ca..88d57e40 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17620,14 +17620,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
     char * pLogFileName = NULL;
+    int nBmcFramesMax = 20;
+    int nBmcConfMax = 2000;
 
     extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
-    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar );
+    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax );
     // set defaults
     Fra_SecSetDefaultParams( pSecPar );
 //    pSecPar->TimeLimit = 300;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRTLarmfijkoupwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cbAEFCGDVBRTLarmfijkoupwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -17637,6 +17639,28 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pSecPar->fTryBmc ^= 1;
             break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBmcFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBmcFramesMax < 0 ) 
+                goto usage;
+            break;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBmcConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBmcConfMax < 0 ) 
+                goto usage;
+            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
@@ -17787,7 +17811,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar );
+    pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar, nBmcFramesMax, nBmcConfMax );
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
         Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "dprove" );
@@ -17806,8 +17830,10 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dprove [-FCGDVBRT num] [-L file] [-cbarmfijoupvwh]\n" );
+    Abc_Print( -2, "usage: dprove [-AEFCGDVBRT num] [-L file] [-cbarmfijoupvwh]\n" );
     Abc_Print( -2, "\t         performs SEC on the sequential miter\n" );
+    Abc_Print( -2, "\t-A num : the limit on the depth of BMC [default = %d]\n", nBmcFramesMax );
+    Abc_Print( -2, "\t-E num : the conflict limit during BMC [default = %d]\n", nBmcConfMax );
     Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
     Abc_Print( -2, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
     Abc_Print( -2, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 0bfd515e..4a74ad7e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2204,10 +2204,10 @@ int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax )
 {
     Aig_Man_t * pMan;
-    int RetValue = -1, clkTotal = clock();
+    int iFrame = -1, RetValue = -1, clkTotal = clock();
     if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
     {
         Prove_Params_t Params, * pParams = &Params;
@@ -2250,28 +2250,30 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
             return RetValue;
         }
     }
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+
     if ( pSecPar->fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0, NULL );
+        RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame );
         if ( RetValue == 0 )
         {
             printf( "Networks are not equivalent.\n" );
             if ( pSecPar->fReportSolution )
             {
-            printf( "SOLUTION: FAIL       " );
-            ABC_PRT( "Time", clock() - clkTotal );
+                printf( "SOLUTION: FAIL       " );
+                ABC_PRT( "Time", clock() - clkTotal );
             }
+            Aig_ManStop( pMan );
             return RetValue;
         }
     } 
-    // derive the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( pMan == NULL )
-    {
-        printf( "Converting miter into AIG has failed.\n" );
-        return -1;
-    }
-    assert( pMan->nRegs > 0 );
     // perform verification
     if ( pSecPar->fUseNewProver )
     {
-- 
cgit v1.2.3