Sequential cleanup with symbolic/ternary simulation.

src/aig/aig/aig.h

@@ -617,7 +617,7 @@ extern int             Aig_ManSeqCleanupBasic( Aig_Man_t * p );
 extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
 extern void            Aig_ManComputeSccs( Aig_Man_t * p ); 
-extern Aig_Man_t *     Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
+extern Aig_Man_t *     Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
 /*=== aigShow.c ========================================================*/
 extern void            Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
 /*=== aigTable.c ========================================================*/
@@ -640,7 +640,7 @@ extern void            Aig_ManVerifyReverseLevel( Aig_Man_t * p );
 /*=== aigTruth.c ========================================================*/
 extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
 /*=== aigTsim.c ========================================================*/
-extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
+extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
 /*=== aigUtil.c =========================================================*/
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );

src/aig/aig/aigScl.c

@@ -619,7 +619,7 @@ Aig_Man_t * Aig_ManSclPart( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual,
         Aig_ManSetRegNum( pTemp, pTemp->nRegs );
         if (nCountPis>0) 
         {
-            pNew = Aig_ManScl( pTemp, fLatchConst, fLatchEqual, fVerbose );
+            pNew = Aig_ManScl( pTemp, fLatchConst, fLatchEqual, 0, -1, -1, fVerbose, 0 );
             nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
             if ( fVerbose )
                 printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d\n",
@@ -646,7 +646,7 @@ Aig_Man_t * Aig_ManSclPart( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual,
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
+Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
 {
     extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
     extern int Saig_ManReportComplements( Aig_Man_t * p );
@@ -667,7 +667,7 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
     pAig->vFlopReprs = Vec_IntAlloc( 100 );
     Aig_ManSeqCleanup( pAig );
     if ( fLatchConst && pAig->nRegs )
-        pAig = Aig_ManConstReduce( pAig, fVerbose );
+        pAig = Aig_ManConstReduce( pAig, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
     if ( fLatchEqual && pAig->nRegs )
         pAig = Aig_ManReduceLaches( pAig, fVerbose );
     // translate pairs into reprs

src/aig/aig/aigTsim.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -344,7 +345,7 @@ void Aig_TsiStateOrAll( Aig_Tsi_t * pTsi, unsigned * pState )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
+Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
 {
     Aig_Tsi_t * pTsi;
     Vec_Ptr_t * vMap;
@@ -374,7 +375,11 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
         }
 
 //        printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
-//Aig_TsiStatePrint( pTsi, pState );
+if ( fVeryVerbose )
+{
+printf( "%3d : ", f );
+Aig_TsiStatePrint( pTsi, pState );
+}
         // check if this state exists
         if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
             break;
@@ -446,6 +451,8 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     }
     if ( fConstants == 0 )
     {
+        if ( fVerbose )
+        printf( "Detected 0 constants after %d iterations of ternary simulation.\n", f );
         Aig_TsiStop( pTsi );
         return NULL;
     }
@@ -488,12 +495,18 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
+Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pTemp;
     Vec_Ptr_t * vMap;
-    while ( (vMap = Aig_ManTernarySimulate( p, fVerbose )) )
+    while ( 1 )
     {
+        if ( fUseMvSweep )
+            vMap = Saig_MvManSimulate( p, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
+        else
+            vMap = Aig_ManTernarySimulate( p, fVerbose, fVeryVerbose );
+        if ( vMap == NULL )
+            break;
         p = Aig_ManRemap( pTemp = p, vMap );
         Vec_PtrFree( vMap );
         Aig_ManSeqCleanup( p );

src/aig/fra/fraSec.c

@@ -126,7 +126,7 @@ clk = clock();
     if ( pNew->nRegs )
     pNew = Aig_ManReduceLaches( pNew, 0 );
     if ( pNew->nRegs )
-    pNew = Aig_ManConstReduce( pNew, 0 );
+    pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
     if ( pParSec->fVerbose )
     {
         printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
@@ -407,7 +407,7 @@ ABC_PRT( "Time", clock() - clk );
         }  
 
         if ( pNew->nRegs )
-            pNew = Aig_ManConstReduce( pNew, 0 );
+            pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
 
         // perform rewriting
 clk = clock();
@@ -498,7 +498,7 @@ clk = clock();
                 if ( pPars->fVerbose )
                     printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pNew) );
                 pTemp = Aig_ManDupOneOutput( pNew, 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 ( Saig_ManRegNum(pTemp) > 0 )
                 {
@@ -537,7 +537,7 @@ clk = clock();
             }
             pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
             Aig_ManStop( pTemp );
-            pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0 );
+            pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0, -1, -1, 0, 0 );
             Aig_ManStop( pTemp );
         }
         else

src/aig/gia/giaAig.c

@@ -548,7 +548,7 @@ void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbo
 {
     Aig_Man_t * pNew, * pTemp;
     pNew  = Gia_ManToAigSimple( p );
-    pTemp = Aig_ManScl( pNew, fConst, fEquiv, fVerbose );
+    pTemp = Aig_ManScl( pNew, fConst, fEquiv, 0, -1, -1, fVerbose, 0 );
     Gia_ManReprFromAigRepr( pNew, p );
     Aig_ManStop( pTemp );
     Aig_ManStop( pNew );

src/aig/ntl/ntlFraig.c

@@ -648,14 +648,14 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     {
         Aig_Man_t * pAigRst;
         pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
-        pTemp = Aig_ManScl( pAigRst, fLatchConst, fLatchEqual, fVerbose );
+        pTemp = Aig_ManScl( pAigRst, fLatchConst, fLatchEqual, 0, -1, -1, fVerbose, 0 );
         Aig_ManStop( pTemp );
         Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
         Aig_ManStop( pAigRst );
     }
     else
     {
-        pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
+        pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, 0, -1, -1, fVerbose, 0 );
         Aig_ManStop( pTemp );
     }
 

src/aig/saig/saig.h

@@ -203,7 +203,7 @@ extern Vec_Int_t *       Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iF
 /*=== saigSimExt.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
 /*=== saigSimMv.c ==========================================================*/
-extern int               Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose );
+extern Vec_Ptr_t *       Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
 /*=== saigStrSim.c ==========================================================*/
 extern Vec_Int_t *       Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
 /*=== saigSwitch.c ==========================================================*/

src/aig/saig/saigSimMv.c

@@ -63,6 +63,7 @@ struct Saig_MvMan_t_
     // compacted AIG
     Saig_MvObj_t *   pAigOld;      // AIG objects
     Vec_Ptr_t *      vFlops;       // collected flops
+    Vec_Int_t *      vXFlops;      // flops that had at least one X-value
     Vec_Ptr_t *      vTired;       // collected flops
     unsigned *       pTStates;     // hash table for states
     int              nTStatesSize; // hash table size
@@ -96,7 +97,7 @@ static inline int    Saig_MvUndef()                            { return SAIG_UND
 static inline int    Saig_MvIsConst0( int iNode )              { return iNode == 1;                }
 static inline int    Saig_MvIsConst1( int iNode )              { return iNode == 0;                }
 static inline int    Saig_MvIsConst( int iNode )               { return iNode  < 2;                }
-static inline int    Saig_MvIsUndef( int iNode )               { return iNode == SAIG_UNDEF_VALUE;}
+static inline int    Saig_MvIsUndef( int iNode )               { return iNode == SAIG_UNDEF_VALUE; }
 
 static inline int    Saig_MvRegular( int iNode )               { return (iNode & ~01);             }
 static inline int    Saig_MvNot( int iNode )                   { return (iNode ^  01);             }
@@ -200,7 +201,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
   SeeAlso     []
 
 ***********************************************************************/
-Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig )
+Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig, int nFramesSatur )
 {
     Saig_MvMan_t * p;
     int i;
@@ -209,7 +210,7 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig )
     memset( p, 0, sizeof(Saig_MvMan_t) );
     // set parameters
     p->pAig         = pAig;
-    p->nStatesMax   = 200;
+    p->nStatesMax   = 2 * nFramesSatur + 100;
     p->nLevelsMax   = 4;
     p->nValuesMax   = SAIG_DIFF_VALUES;
     p->nFlops       = Aig_ManRegNum(pAig);
@@ -252,6 +253,7 @@ void Saig_MvManStop( Saig_MvMan_t * p )
 {
     Aig_MmFixedStop( p->pMemStates, 0 );
     Vec_PtrFree( p->vStates );
+    Vec_IntFreeP( &p->vXFlops );
     Vec_PtrFree( p->vFlops );
     Vec_PtrFree( p->vTired );
     ABC_FREE( p->pRegsValues[0] );
@@ -321,7 +323,7 @@ static inline int * Saig_MvTableFind( Saig_MvMan_t * p, int iFan0, int iFan1 )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Saig_MvAnd( Saig_MvMan_t * p, int iFan0, int iFan1 )
+static inline int Saig_MvAnd( Saig_MvMan_t * p, int iFan0, int iFan1, int fFirst )
 {
     if ( iFan0 == iFan1 )
         return iFan0;
@@ -333,11 +335,13 @@ static inline int Saig_MvAnd( Saig_MvMan_t * p, int iFan0, int iFan1 )
         return Saig_MvIsConst1(iFan1) ? iFan0 : Saig_MvConst0();
     if ( Saig_MvIsUndef(iFan0) || Saig_MvIsUndef(iFan1) )
         return Saig_MvUndef();
-    if ( Saig_MvLev(p, iFan0) >= p->nLevelsMax || Saig_MvLev(p, iFan1) >= p->nLevelsMax )
-        return Saig_MvUndef();
-
+//    if ( Saig_MvLev(p, iFan0) >= p->nLevelsMax || Saig_MvLev(p, iFan1) >= p->nLevelsMax )
 //        return Saig_MvUndef();
 
+    // go undef after the first frame
+    if ( !fFirst )
+        return Saig_MvUndef();
+
     if ( iFan0 > iFan1 )
     {
         int Temp = iFan0;
@@ -381,6 +385,32 @@ static inline int Saig_MvSimulateValue1( Saig_MvObj_t * pAig, Saig_MvObj_t * pOb
 
 /**Function*************************************************************
 
+  Synopsis    [Prints MV state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_MvPrintState( int Iter, Saig_MvMan_t * p )
+{
+    Saig_MvObj_t * pEntry;
+    int i;
+    printf( "%3d : ", Iter );
+    Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
+    {
+        if ( pEntry->Value == SAIG_UNDEF_VALUE )
+            printf( "    *" );
+        else
+            printf( "%5d", pEntry->Value );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs one iteration of simulation.]
 
   Description []
@@ -390,30 +420,29 @@ static inline int Saig_MvSimulateValue1( Saig_MvObj_t * pAig, Saig_MvObj_t * pOb
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_MvSimulateFrame( Saig_MvMan_t * p, int fFirst )
+void Saig_MvSimulateFrame( Saig_MvMan_t * p, int fFirst, int fVerbose )
 {
-    int fPrintState = 0;
     Saig_MvObj_t * pEntry;
-    int i, NewValue;
+    int i;
     Saig_MvManForEachObj( p->pAigOld, pEntry )
     {
         if ( pEntry->Type == AIG_OBJ_AND )
         {
             pEntry->Value = Saig_MvAnd( p, 
                 Saig_MvSimulateValue0(p->pAigOld, pEntry),
-                Saig_MvSimulateValue1(p->pAigOld, pEntry) );
-/*
-printf( "%d = %d%s * %d%s  --> %d\n", pEntry - p->pAigOld,
-       Saig_MvObjFanin0(pEntry), Saig_MvObjFaninC0(pEntry)? "-":"+",
-       Saig_MvObjFanin1(pEntry), Saig_MvObjFaninC1(pEntry)? "-":"+", pEntry->Value );
-*/
+                Saig_MvSimulateValue1(p->pAigOld, pEntry), fFirst );
         }
         else if ( pEntry->Type == AIG_OBJ_PO )
             pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
         else if ( pEntry->Type == AIG_OBJ_PI )
         {
             if ( pEntry->iFan1 == 0 ) // true PI
+            {
+                if ( fFirst )
                     pEntry->Value = Saig_MvVar2Lit( Saig_MvCreateObj( p, 0, 0 ) );
+                else
+                    pEntry->Value = SAIG_UNDEF_VALUE;
+            }
 //            else if ( fFirst ) // register output
 //                pEntry->Value = Saig_MvConst0();
 //            else
@@ -424,22 +453,9 @@ printf( "%d = %d%s * %d%s  --> %d\n", pEntry - p->pAigOld,
         else if ( pEntry->Type != AIG_OBJ_NONE )
             assert( 0 );
     }
-    Vec_PtrClear( p->vTired );
+    // transfer to registers
     Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
-    {
-        NewValue = Saig_MvSimulateValue0(p->pAigOld, pEntry);
-        if ( NewValue != (int)pEntry->Value )
-            Vec_PtrPush( p->vTired, pEntry );
-        pEntry->Value = NewValue;
-        if ( !fPrintState )
-            continue;
-        if ( pEntry->Value == 536870910 )
-            printf( "* " );
-        else
-            printf( "%d ", pEntry->Value );
-    }
-if ( fPrintState )
-printf( "\n" );
+        pEntry->Value = Saig_MvSimulateValue0( p->pAigOld, pEntry );
 }
 
 
@@ -456,25 +472,28 @@ printf( "\n" );
 ***********************************************************************/
 int Saig_MvSimHash( unsigned * pState, int nFlops, int TableSize )
 {
-    static int s_SPrimes[128] = { 
-        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
-        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
-        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
-        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
-        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
-        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
-        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
-        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
-        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
-        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
-        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
-        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
-        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    static int s_SPrimes[16] = { 
+     1610612741,
+     805306457,
+     402653189,
+     201326611,
+     100663319,
+     50331653,
+     25165843,
+     12582917,
+     6291469,
+     3145739,
+     1572869,
+     786433,
+     393241,
+     196613,
+     98317,
+     49157
     };
     unsigned uHash = 0;
     int i;
     for ( i = 0; i < nFlops; i++ )
-        uHash ^= pState[i] * s_SPrimes[i & 0x7F];
+        uHash ^= pState[i] * s_SPrimes[i & 0xF];
     return (int)(uHash % TableSize);
 }
 
@@ -511,62 +530,15 @@ static inline unsigned * Saig_MvSimTableFind( Saig_MvMan_t * p, unsigned * pStat
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_MvSaveState( Saig_MvMan_t * p, int * piReg )
+int Saig_MvSaveState( Saig_MvMan_t * p )
 {
     Saig_MvObj_t * pEntry;
     unsigned * pState, * pPlace;
-    int i, k, nMaxUndefs = 0;
-    int iTimesOld, iTimesNew;
-    *piReg = -1;
+    int i;
     pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMemStates );
     pState[0] = 0;
     Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
-    {
-        iTimesOld = p->nRegsValues[i];
-        // count the number of different def values
-        if ( !Saig_MvIsUndef( pEntry->Value ) && p->nRegsValues[i] < p->nValuesMax )
-        {
-            for ( k = 0; k < p->nRegsValues[i]; k++ )
-                if ( p->pRegsValues[i][k] == (int)pEntry->Value )
-                    break;
-            if ( k == p->nRegsValues[i] )
-                p->pRegsValues[i][ p->nRegsValues[i]++ ] = pEntry->Value;
-        }
-        else // retire this register (consider moving this up!)
-        {
-            pEntry->Value = Saig_MvUndef();
-            p->nRegsValues[i] = SAIG_DIFF_VALUES+1;
-        }
-        iTimesNew = p->nRegsValues[i];
-        // count the number of times
-        if ( iTimesOld != iTimesNew )
-        {
-            if ( iTimesOld > 0 )
-                p->nRValues[iTimesOld]--;
-            if ( iTimesNew <= SAIG_DIFF_VALUES )
-                p->nRValues[iTimesNew]++;
-        }
-        // count the number of undef values
-        if ( Saig_MvIsUndef( pEntry->Value ) )
-        {
-            if ( p->pRegsUndef[i]++ == 0 )
-                p->nRUndefs++;
-        }
-        // find def reg with the max number of undef values
-        if ( nMaxUndefs < p->pRegsUndef[i] )
-        {
-             nMaxUndefs = p->pRegsUndef[i];
-            *piReg = i;
-        }
-        // remember state
         pState[i+1] = pEntry->Value;
-
-//        if ( pEntry->Value == 536870910 )
-//            printf( "* " );
-//        else
-//            printf( "%d ", pEntry->Value );
-    }
-//printf( "\n" );
     pPlace = Saig_MvSimTableFind( p, pState );
     if ( *pPlace )
         return *pPlace;
@@ -624,7 +596,7 @@ void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
         printf( "FLOP %5d : (%3d) ", iFlop, Vec_IntEntry(vCounter,i) );
 /*
         for ( k = 0; k < p->nRegsValues[iFlop]; k++ )
-            if ( p->pRegsValues[iFlop][k] == 536870910 )
+            if ( p->pRegsValues[iFlop][k] == SAIG_UNDEF_VALUE )
                 printf( "* " );
             else
                 printf( "%d ", p->pRegsValues[iFlop][k] );
@@ -634,7 +606,7 @@ void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
         {
             if ( k == iState+1 )
                 printf( " # " );
-            if ( pState[iFlop+1] == 536870910 )
+            if ( pState[iFlop+1] == SAIG_UNDEF_VALUE )
                 printf( "*" );
             else
                 printf( "%d", pState[iFlop+1] );
@@ -659,71 +631,153 @@ void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose )
+Vec_Int_t * Saig_MvManFindXFlops( Saig_MvMan_t * p )
+{
+    Vec_Int_t * vXFlops;
+    unsigned * pState;
+    int i, k;
+    vXFlops = Vec_IntStart( p->nFlops );
+    Vec_PtrForEachEntry( unsigned *, p->vStates, pState, i )
+    {
+        for ( k = 1; k <= p->nFlops; k++ )
+            if ( Saig_MvIsUndef(pState[k]) )
+                Vec_IntWriteEntry( vXFlops, k-1, 1 );
+    }
+    return vXFlops;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds equivalent flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p )
+{
+    Vec_Int_t * vBinValued;
+    Vec_Ptr_t * vMap = NULL;
+    Aig_Obj_t * pObj;
+    unsigned * pState;
+    int i, k, j, fConst0, Counter1 = 0, Counter2 = 0;
+    // prepare CI map
+    vMap = Vec_PtrAlloc( Aig_ManPiNum(p->pAig) );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        Vec_PtrPush( vMap, pObj );
+    // detect constant flops
+    vBinValued = Vec_IntStart( p->nFlops );
+    for ( k = 0; k < p->nFlops; k++ )
+    {
+        // check if this flop is constant 0 in all states
+        fConst0 = 1;
+        Vec_PtrForEachEntry( unsigned *, p->vStates, pState, i )
+        {
+            if ( !Saig_MvIsConst0(pState[k+1]) )
+                fConst0 = 0;
+            if ( Saig_MvIsUndef(pState[k+1]) )
+                break;
+        }
+        if ( i < Vec_PtrSize(p->vStates) )
+            continue;
+        // mark binary values
+        Vec_IntWriteEntry( vBinValued, k, 1 );
+        // set the constant
+        if ( fConst0 )
+            Vec_PtrWriteEntry( vMap, k, Aig_ManConst0(p->pAig) );
+        Counter1++;
+    }
+    // detect equivalent (non-ternary flops)
+    for ( k = 0; k < p->nFlops; k++ )
+    if ( Vec_IntEntry(vBinValued, k) )
+    for ( j = k+1; j < p->nFlops; j++ )
+    if ( Vec_IntEntry(vBinValued, j) )
+    {
+        // check if they are equal
+        Vec_PtrForEachEntry( unsigned *, p->vStates, pState, i )
+            if ( pState[k+1] != pState[j+1] )
+                break;
+        if ( i < Vec_PtrSize(p->vStates) )
+            continue;
+        // set the equivalence
+        Vec_PtrWriteEntry( vMap, j, Aig_ManPi(p->pAig, k) );
+    }
+    printf( "Detected %d const0 flop and %d equivalent non-ternary flops.\n", Counter1, Counter2 );
+    Vec_IntFree( vBinValued );
+    return vMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs multi-valued simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
 {
+    Vec_Ptr_t * vMap;
     Saig_MvMan_t * p;
     Saig_MvObj_t * pEntry;
-    int f, i, k, iRegMax, iState, clk = clock();
-    // start the manager
-    p = Saig_MvManStart( pAig );
+    int f, i, iState, clk = clock();
+    assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );
+
+    // start manager
+    p = Saig_MvManStart( pAig, nFramesSatur );
+if ( fVerbose )
 ABC_PRT( "Constructing the problem", clock() - clk );
-    clk = clock();
-    // initiliaze registers
+
+    // initialize registers
     Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
-    {
         pEntry->Value = Saig_MvConst0();
-        if ( pEntry->iFan0 == 1 )
-            printf( "Constant value %d\n", i );
-    }
-
-    Saig_MvSaveState( p, &iRegMax );
+    Saig_MvSaveState( p );
+    if ( fVeryVerbose )
+        Saig_MvPrintState( 0, p );
     // simulate until convergence
+    clk = clock();
     for ( f = 0; ; f++ )
     {
-/*
-        if ( fVerbose )
-        {
-            printf( "%3d :  ", f+1 );
-            printf( "*=%6d  ", p->nRUndefs );
-            for ( k = 1; k < SAIG_DIFF_VALUES; k++ )
-                if ( p->nRValues[k] == 0 )
-                    printf( "          " );
-                else
-                    printf( "%d=%6d  ", k, p->nRValues[k] );
-            printf( "aig=%6d", p->nObjs );
-            printf( "\n" );
-        }
-*/
-        Saig_MvSimulateFrame( p, f==0 );
-        iState = Saig_MvSaveState( p, &iRegMax );
+        // retired some flops
+        if ( p->vXFlops )
+            Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
+                pEntry->Value = SAIG_UNDEF_VALUE;
+        // simulate timeframe
+        Saig_MvSimulateFrame( p, (int)(f < nFramesSymb), fVerbose );
+        // save and print state
+        iState = Saig_MvSaveState( p );
+        if ( fVeryVerbose )
+            Saig_MvPrintState( f+1, p );
         if ( iState >= 0 )
         {
             printf( "Converged after %d frames with lasso in state %d. Cycle = %d.\n", f+1, iState-1, f+2-iState );
             printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis );
             break;
         }
-        if ( f >= p->nStatesMax && iRegMax >= 0 )
+        if ( f == nFramesSatur )
         {
-/*
-            pEntry = Vec_PtrEntry( p->vFlops, iRegMax );
-            assert( pEntry->Value != (unsigned)Saig_MvUndef() );
-            pEntry->Value = Saig_MvUndef();
-            printf( "Retiring flop %d.\n", iRegMax );
-*/
-//            printf( "Retiring %d flops.\n", Vec_PtrSize(p->vTired) );
-            Vec_PtrForEachEntry( Saig_MvObj_t *, p->vTired, pEntry, k )
-                pEntry->Value = Saig_MvUndef();
+            printf( "Begining to saturate simulation after %d frames\n", f+1 );
+            // find all flops that have at least one X value in the past and set them to X forever
+            p->vXFlops = Saig_MvManFindXFlops( p );            
         }
     }
-ABC_PRT( "Multi-value simulation", clock() - clk );
+if ( fVerbose )
+ABC_PRT( "Multi-valued simulation", clock() - clk );
     // implement equivalences
-    Saig_MvManPostProcess( p, iState-1 );
+//    Saig_MvManPostProcess( p, iState-1 );
+    vMap = Saig_MvManDeriveMap( p );
     Saig_MvManStop( p );
-    return 1;
+//    return Aig_ManDupSimple( pAig );
+    return vMap;
 }
 
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/ssw/sswCore.c

@@ -111,10 +111,10 @@ void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t *
 {
     Aig_Man_t * pAig1, * pAig2, * pAux;
     pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 );
-    pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0 );
+    pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0, -1, -1, 0, 0 );
     Aig_ManStop( pAux );
     pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 );
-    pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0 );
+    pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0, -1, -1, 0, 0 );
     Aig_ManStop( pAux );
    
     p->nNodesBegC = Aig_ManNodeNum(pAig1);

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

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