Sequential cleanup with symbolic/ternary simulation.

2 files changed, 57 insertions, 24 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fd8d4e07..ae14d275 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8852,9 +8852,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 }
 */
+
     {
-        void Bdc_SpfdDecomposeTest();
-        Bdc_SpfdDecomposeTest();
+//        void Bdc_SpfdDecomposeTest();
+//        Bdc_SpfdDecomposeTest();
     }
     return 0;
 usage:
@@ -15481,21 +15482,21 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    int fLatchConst;
-    int fLatchEqual;
-    int fSaveNames;
-    int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fVerbose );
+    int fLatchConst  =  1;
+    int fLatchEqual  =  1;
+    int fSaveNames   =  0;
+    int fUseMvSweep  =  0;
+    int nFramesSymb  =  1;
+    int nFramesSatur = 32;
+    int fVerbose     =  0;
+    int fVeryVerbose =  0;
+    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
 
     // set defaults
-    fLatchConst = 1;
-    fLatchEqual = 1;
-    fSaveNames  = 0;
-    fVerbose    = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cenvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cenmFSvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15508,9 +15509,37 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fSaveNames ^= 1;
             break;
+        case 'm':
+            fUseMvSweep ^= 1;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesSymb = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesSymb < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesSatur = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesSatur < 0 ) 
+                goto usage;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -15533,7 +15562,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // modify the current network
-    pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fSaveNames, fVerbose );
+    pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fSaveNames, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Sequential cleanup has failed.\n" );
@@ -15544,13 +15573,17 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: scleanup [-cenvh]\n" );
+    Abc_Print( -2, "usage: scleanup [-cenmFSvwh]\n" );
     Abc_Print( -2, "\t         performs sequential cleanup of the current network\n" );
     Abc_Print( -2, "\t         by removing nodes and latches that do not feed into POs\n" );
     Abc_Print( -2, "\t-c     : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
     Abc_Print( -2, "\t-e     : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
     Abc_Print( -2, "\t-n     : toggle preserving latch names [default = %s]\n", fSaveNames? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle using hybrid ternary/symbolic simulation [default = %s]\n", fUseMvSweep? "yes": "no" );
+    Abc_Print( -2, "\t-F num : the number of first frames simulated symbolically [default = %d]\n", nFramesSymb );
+    Abc_Print( -2, "\t-S num : the number of frames when symbolic saturation begins [default = %d]\n", nFramesSatur );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle very verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -18973,7 +19006,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
     extern int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars );
     Saig_ParBmc_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
@@ -19094,7 +19127,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         {
             extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
             Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose );
-            pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0 );
+            pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 );
             if ( pNtkRes == NULL )
             {
                 Abc_Print( -1, "Removing SAT outputs has failed.\n" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 3b0cbb06..3da01d9f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1892,7 +1892,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
             if ( pPars->fVerbose )
                 printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pMan) );
             pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
-            pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
+            pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
             Aig_ManStop( pAux );
             if ( Aig_ManRegNum(pTemp) == 0 )
             {
@@ -1948,7 +1948,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
         if ( ppNtkRes )
         {
             pTemp = Aig_ManDupUnsolvedOutputs( pMan, 1 );
-            *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0 );
+            *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0, -1, -1, 0, 0 );
             Aig_ManStop( pTemp );
         }
     }
@@ -2591,7 +2591,7 @@ Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, in
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
 {
     extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
     Abc_Ntk_t * pNtkAig;
@@ -2603,7 +2603,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
     {
         Aig_ManSeqCleanup( pMan );
         if ( fLatchConst && pMan->nRegs )
-            pMan = Aig_ManConstReduce( pMan, fVerbose );
+            pMan = Aig_ManConstReduce( pMan, 0, -1, -1, fVerbose, fVeryVerbose );
         if ( fLatchEqual && pMan->nRegs )
             pMan = Aig_ManReduceLaches( pMan, fVerbose );
     }
@@ -2612,7 +2612,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
         if ( pMan->vFlopNums )
             Vec_IntFree( pMan->vFlopNums );
         pMan->vFlopNums = NULL;
-        pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
+        pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
         Aig_ManStop( pTemp );
     }
 
@@ -2649,7 +2649,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
-//    pMan = Aig_ManConstReduce( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1, 0 );
 
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
@@ -2683,7 +2683,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
-//    pMan = Aig_ManConstReduce( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1, 0 );
 
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
@@ -2719,7 +2719,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbo
     Aig_ManStop( pTemp );
 
 //    pMan = Aig_ManReduceLaches( pMan, 1 );
-//    pMan = Aig_ManConstReduce( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1, 0 );
 
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );