Version abc81005

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

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:

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

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. ", 

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");