New MFS package.

7 files changed, 79 insertions, 15 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 07a7207d..ac4a8efa 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4491,7 +4491,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMCZdlaevwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZdlaevwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4539,6 +4539,17 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nWinSizeMax < 0 )
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
+                goto usage;
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -4604,12 +4615,13 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs2 [-WFDMCZ <num>] [-dlaevwh]\n" );
+    Abc_Print( -2, "usage: mfs2 [-WFDMLCZ <num>] [-dlaevwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
     Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
     Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+    Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-Z <num> : treat the first <num> logic nodes as fixed (0 = none) [default = %d]\n", pPars->nFirstFixed );
     Abc_Print( -2, "\t-d       : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 4ca0df00..cf7e2f6e 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -46,7 +46,6 @@ struct Mfs_Par_t_
     int           nWinTfoLevs;   // the maximum fanout levels
     int           nFanoutsMax;   // the maximum number of fanouts
     int           nDepthMax;     // the maximum number of logic levels
-    int           nDivMax;       // the maximum number of divisors
     int           nWinMax;       // the maximum size of the window
     int           nGrowthLevel;  // the maximum allowed growth in level
     int           nBTLimit;      // the maximum number of conflicts in one SAT run
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 18960183..ef04da02 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -46,6 +46,7 @@ struct Sfm_Par_t_
     int             nFanoutMax;    // the maximum number of fanouts
     int             nDepthMax;     // the maximum depth to try
     int             nWinSizeMax;   // the maximum window size
+    int             nGrowthLevel;  // the maximum allowed growth in level
     int             nBTLimit;      // the maximum number of conflicts in one SAT run
     int             nFirstFixed;   // the number of first nodes to be treated as fixed
     int             fFixLevel;     // does not allow level to increase
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index af2cb836..9efb70e2 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -49,6 +49,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
     pPars->nFanoutMax   =   30;  // the maximum number of fanouts
     pPars->nDepthMax    =   20;  // the maximum depth to try  
     pPars->nWinSizeMax  =  300;  // the maximum window size
+    pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
     pPars->nBTLimit     = 5000;  // the maximum number of conflicts in one SAT run
     pPars->fFixLevel    =    1;  // does not allow level to increase
     pPars->fRrOnly      =    0;  // perform redundancy removal
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 60648b44..c9ccbc89 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -58,6 +58,7 @@ struct Sfm_Ntk_t_
     int               nPos;        // PO count (POs should be last objects)
     int               nNodes;      // internal nodes
     int               nObjs;       // total objects
+    int               nLevelMax;   // maximum level
     // user data
     Vec_Str_t *       vFixed;      // persistent objects
     Vec_Wrd_t *       vTruths;     // truth tables
@@ -65,6 +66,7 @@ struct Sfm_Ntk_t_
     // attributes
     Vec_Wec_t         vFanouts;    // fanouts
     Vec_Int_t         vLevels;     // logic level
+    Vec_Int_t         vLevelsR;    // logic level
     Vec_Int_t         vCounts;     // fanin counters
     Vec_Int_t         vId2Var;     // ObjId -> SatVar
     Vec_Int_t         vVar2Id;     // SatVar -> ObjId
@@ -148,6 +150,9 @@ static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p )                    { int i;
 static inline int  Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj )              { return Vec_IntEntry( &p->vLevels, iObj );                         }
 static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev )  { Vec_IntWriteEntry( &p->vLevels, iObj, Lev );                      }
 
+static inline int  Sfm_ObjLevelR( Sfm_Ntk_t * p, int iObj )             { return Vec_IntEntry( &p->vLevelsR, iObj );                        }
+static inline void Sfm_ObjSetLevelR( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevelsR, iObj, Lev );                     }
+
 static inline int  Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj )   { return Vec_IntAddToEntry(&p->vCounts, iObj, -1);                  }
 static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); }
 
@@ -157,7 +162,8 @@ extern void        Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#define Sfm_NtkForEachNode( p, i )                for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NtkForEachNode( p, i )               for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NtkForEachNodeReverse( p, i )        for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- )
 #define Sfm_ObjForEachFanin( p, Node, Fan, i )   for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )
 #define Sfm_ObjForEachFanout( p, Node, Fan, i )  for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
 
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index e66e6e8e..1e650454 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -107,21 +107,49 @@ void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sfm_ObjCreateLevel( Vec_Int_t * vArray, Vec_Int_t * vLevels )
+static inline int Sfm_ObjLevelNew( Vec_Int_t * vArray, Vec_Int_t * vLevels )
 {
     int k, Fanin, Level = 0;
     Vec_IntForEachEntry( vArray, Fanin, k )
-        Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) + 1 );
-    return Level;
+        Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) );
+    return Level + 1;
 }
 void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
 {
     Vec_Int_t * vArray;
     int i;
     assert( Vec_IntSize(vLevels) == 0 );
-    Vec_IntGrow( vLevels, Vec_WecSize(vFanins) );
+    Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
     Vec_WecForEachLevel( vFanins, vArray, i )
-        Vec_IntPush( vLevels, Sfm_ObjCreateLevel(vArray, vLevels) );
+        Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sfm_ObjLevelNewR( Vec_Int_t * vArray, Vec_Int_t * vLevelsR )
+{
+    int k, Fanout, LevelR = 0;
+    Vec_IntForEachEntry( vArray, Fanout, k )
+        LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) );
+    return LevelR + 1;
+}
+void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR )
+{
+    Vec_Int_t * vArray;
+    int i;
+    assert( Vec_IntSize(vLevelsR) == 0 );
+    Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 );
+    Vec_WecForEachLevelReverse( vFanouts, vArray, i )
+        Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR) );
 }
 
 /**Function*************************************************************
@@ -152,6 +180,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     // attributes
     Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
     Sfm_CreateLevel( &p->vFanins, &p->vLevels );
+    Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR );
     Vec_IntFill( &p->vCounts,   p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds,  p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds2, p->nObjs,  0 );
@@ -163,6 +192,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
 }
 void Sfm_NtkPrepare( Sfm_Ntk_t * p )
 {
+    p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
     p->vNodes    = Vec_IntAlloc( 1000 );
     p->vDivs     = Vec_IntAlloc( 100 );
     p->vRoots    = Vec_IntAlloc( 1000 );
@@ -187,6 +217,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     // attributes
     Vec_WecErase( &p->vFanouts );
     ABC_FREE( p->vLevels.pArray );
+    ABC_FREE( p->vLevelsR.pArray );
     ABC_FREE( p->vCounts.pArray );
     ABC_FREE( p->vTravIds.pArray );
     ABC_FREE( p->vTravIds2.pArray );
@@ -260,13 +291,22 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
 void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanout;
-    int LevelNew = Sfm_ObjCreateLevel( Sfm_ObjFiArray(p, iNode), &p->vLevels );
+    int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels );
     if ( LevelNew == Sfm_ObjLevel(p, iNode) )
         return;
     Sfm_ObjSetLevel( p, iNode, LevelNew );
-    if ( Sfm_ObjIsNode(p, iNode) )
-        Sfm_ObjForEachFanout( p, iNode, iFanout, i )
-            Sfm_NtkUpdateLevel_rec( p, iFanout );
+    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
+        Sfm_NtkUpdateLevel_rec( p, iFanout );
+}
+void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanin;
+    int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR );
+    if ( LevelNew == Sfm_ObjLevelR(p, iNode) )
+        return;
+    Sfm_ObjSetLevelR( p, iNode, LevelNew );
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        Sfm_NtkUpdateLevelR_rec( p, iFanin );
 }
 void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
 {
@@ -292,6 +332,10 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
     }
     // update logic level
     Sfm_NtkUpdateLevel_rec( p, iNode );
+    if ( iFaninNew != -1 )
+        Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
+    if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
+        Sfm_NtkUpdateLevelR_rec( p, iFanin );
     // update truth table
     Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
     Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index db6bd0ea..f12474c9 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -215,7 +215,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
             return;
         // skip TFI nodes, PO nodes, or nodes with high logic level
         if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
-            (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
+            (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) > nLevelMax) )
             continue;
         // handle single-input nodes
         if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
@@ -311,7 +311,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
         Sfm_NtkIncrementTravId2( p );
         Vec_IntForEachEntry( p->vDivs, iTemp, i )
             if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
-                Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
+//                Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) - 1 );
+                Sfm_NtkAddDivisors( p, iTemp, p->nLevelMax - Sfm_ObjLevelR(p, iNode) ); 
     }
     if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
     {