New MFS package.

src/base/abci/abc.c

@@ -4318,7 +4318,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Abc_NtkMfsParsDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdraestpgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdlraestpgvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4391,6 +4391,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fRrOnly ^= 1;
             break;
+        case 'l':
+            pPars->nGrowthLevel = 10000;
+            break;
         case 'r':
             pPars->fResub ^= 1;
             break;
@@ -4445,7 +4448,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-draestpgvh]\n" );
+    Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-dlraestpgvh]\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->nWinTfoLevs );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
@@ -4454,6 +4457,7 @@ usage:
     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-d       : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );
+    Abc_Print( -2, "\t-l       : allow logic level to increase [default = %s]\n", (pPars->nGrowthLevel > 0)? "yes": "no" );
     Abc_Print( -2, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
     Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );

src/misc/vec/vecWec.h

@@ -215,6 +215,14 @@ static inline int Vec_WecSizeUsed( Vec_Wec_t * p )
         Counter += (int)(Vec_IntSize(vVec) > 0);
     return Counter;
 }
+static inline int Vec_WecSizeUsedLimits( Vec_Wec_t * p, int iStart, int iStop )
+{
+    Vec_Int_t * vVec;
+    int i, Counter = 0;
+    Vec_WecForEachLevelStartStop( p, vVec, i, iStart, iStop )
+        Counter += (int)(Vec_IntSize(vVec) > 0);
+    return Counter;
+}
 
 /**Function*************************************************************
 

src/opt/sfm/sfmCnf.c

@@ -150,7 +150,7 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
+void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
 {
     Vec_Int_t * vClause;
     char Entry;
@@ -159,11 +159,14 @@ void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap
     vClause = Vec_WecPushLevel( vRes );
     Vec_StrForEachEntry( vCnf, Entry, i )
     {
-        Lit = (int)Entry;
-        if ( Lit == -1 )
+        if ( (int)Entry == -1 )
+        {
             vClause = Vec_WecPushLevel( vRes );
-        else
-            Vec_IntPush( vClause, Abc_Lit2LitV( Vec_IntArray(vFaninMap), Lit ) );
+            continue;
+        }
+        Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
+        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
+        Vec_IntPush( vClause, Lit );
     }
 }
 

src/opt/sfm/sfmCore.c

@@ -49,7 +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->nBTLimit     =    0;  // the maximum number of conflicts in one SAT run
+    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
     pPars->fArea        =    0;  // performs optimization for area
@@ -255,13 +255,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
     int i, k, Counter = 0;
     p->timeTotal = Abc_Clock();
-    if ( pPars->fVerbose )
+    if ( pPars->fVerbose && Vec_StrSum(p->vFixed) > 0 )
         printf( "Performing MFS with %d fixed objects.\n", Vec_StrSum(p->vFixed) );
     p->pPars = pPars;
     Sfm_NtkPrepare( p );
 //    Sfm_ComputeInterpolantCheck( p );
 //    return 0;
-    p->nTotalNodesBeg = Vec_WecSize(&p->vFanins) - Sfm_NtkPiNum(p) - Sfm_NtkPoNum(p);
+    p->nTotalNodesBeg = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
     p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
     Sfm_NtkForEachNode( p, i )
     {
@@ -278,7 +278,7 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
         }
         Counter += (k > 0);
     }
-    p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
+    p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
     p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
     p->timeTotal = Abc_Clock() - p->timeTotal;
     if ( pPars->fVerbose )

src/opt/sfm/sfmInt.h

@@ -42,7 +42,6 @@
 ABC_NAMESPACE_HEADER_START
 
 #define SFM_FANIN_MAX 6
-
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
@@ -77,9 +76,11 @@ struct Sfm_Ntk_t_
     int               nTravIds;    // traversal IDs
     int               nTravIds2;   // traversal IDs
     // window
-    int               iNode;
+    int               iPivotNode;  // window pivot
     Vec_Int_t *       vLeaves;     // leaves 
+    Vec_Int_t *       vLeaves2;    // leaves 
     Vec_Int_t *       vNodes;      // internal
+    Vec_Int_t *       vNodes2;     // internal
     Vec_Int_t *       vDivs;       // divisors
     Vec_Int_t *       vRoots;      // roots
     Vec_Int_t *       vTfo;        // TFO (excluding iNode)
@@ -145,7 +146,7 @@ static inline int  Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k )         { return
 static inline int  Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj )             { assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); return Vec_IntEntry(&p->vId2Var, iObj);  }
 static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Vec_IntEntry(&p->vId2Var, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num);  Vec_IntWriteEntry(&p->vVar2Id, Num, iObj);  }
 static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num )         { int iObj = Vec_IntEntry(&p->vVar2Id, Num); assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); Vec_IntWriteEntry(&p->vId2Var, iObj, -1);  Vec_IntWriteEntry(&p->vVar2Id, Num, -1); }
-static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p )                    { int i; for ( i = 1; i < p->nSatVars; i++ )  Sfm_ObjCleanSatVar( p, i ); }
+static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p )                    { int i; for ( i = 1; i < p->nSatVars; i++ )  if ( Vec_IntEntry(&p->vVar2Id, i) != -1 ) Sfm_ObjCleanSatVar( p, 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 );                      }
@@ -171,7 +172,7 @@ extern void        Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 extern void         Sfm_PrintCnf( Vec_Str_t * vCnf );
 extern int          Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf );
 extern Vec_Wec_t *  Sfm_CreateCnf( Sfm_Ntk_t * p );
-extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap );
+extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar );
 /*=== sfmCore.c ==========================================================*/
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );

src/opt/sfm/sfmNtk.c

@@ -155,8 +155,8 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     Vec_IntFill( &p->vCounts,   p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds,  p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds2, p->nObjs,  0 );
-    Vec_IntFill( &p->vId2Var,   p->nObjs, -1 );
-    Vec_IntFill( &p->vVar2Id,   p->nObjs, -1 );
+    Vec_IntFill( &p->vId2Var,   2*p->nObjs, -1 );
+    Vec_IntFill( &p->vVar2Id,   2*p->nObjs, -1 );
     p->vCover   = Vec_IntAlloc( 1 << 16 );
     p->vCnfs    = Sfm_CreateCnf( p );
     return p;
@@ -164,7 +164,9 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
 void Sfm_NtkPrepare( Sfm_Ntk_t * p )
 {
     p->vLeaves   = Vec_IntAlloc( 1000 );
+    p->vLeaves2  = Vec_IntAlloc( 1000 );
     p->vNodes    = Vec_IntAlloc( 1000 );
+    p->vNodes2   = Vec_IntAlloc( 1000 );
     p->vDivs     = Vec_IntAlloc( 100 );
     p->vRoots    = Vec_IntAlloc( 1000 );
     p->vTfo      = Vec_IntAlloc( 1000 );
@@ -197,7 +199,9 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_IntFree( p->vCover );
     // other data
     Vec_IntFreeP( &p->vLeaves );
+    Vec_IntFreeP( &p->vLeaves2 );
     Vec_IntFreeP( &p->vNodes );
+    Vec_IntFreeP( &p->vNodes2 );
     Vec_IntFreeP( &p->vDivs  );
     Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vTfo   );

src/opt/sfm/sfmSat.c

@@ -53,13 +53,17 @@ static word s_Truths6[6] = {
 ***********************************************************************/
 void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 {
+    // p->vOrder contains all variables in the window in a good order
+    // p->vDivs is a subset of nodes in p->vOrder used as divisor candidates
+    // p->vTfo contains TFO of the node (does not include node)
+    // p->vRoots contains roots of the TFO of the node (may include node)
     Vec_Int_t * vClause;
     int RetValue, iNode = -1, iFanin, i, k;
     abctime clk = Abc_Clock();
 //    if ( p->pSat )
 //        printf( "%d  ", p->pSat->stats.learnts );
     sat_solver_restart( p->pSat );
-    sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 50 );
+    sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vOrder) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 10 );
     // create SAT variables
     Sfm_NtkCleanVars( p );
     p->nSatVars = 1;
@@ -80,7 +84,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
             Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
         Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
         // generate CNF 
-        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
+        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, -1 );
         // add clauses
         Vec_WecForEachLevel( p->vClauses, vClause, k )
         {
@@ -90,6 +94,51 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
             assert( RetValue );
         }
     }
+    if ( Vec_IntSize(p->vTfo) > 0 )
+    {
+        assert( p->pPars->nTfoLevMax > 0 );
+        assert( Vec_IntSize(p->vRoots) > 0 );
+        assert( Vec_IntEntry(p->vTfo, 0) != p->iPivotNode );
+        // collect variables of root nodes
+        Vec_IntClear( p->vLits );
+        Vec_IntForEachEntry( p->vRoots, iNode, i )
+            Vec_IntPush( p->vLits, Sfm_ObjSatVar(p, iNode) );
+        // assign new variables to the TFO nodes
+        Vec_IntForEachEntry( p->vTfo, iNode, i )
+        {
+            Sfm_ObjCleanSatVar( p, Sfm_ObjSatVar(p, iNode) );
+            Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+        }
+        // add CNF clauses for the TFO
+        Vec_IntForEachEntry( p->vTfo, iNode, i )
+        {
+            assert( Sfm_ObjIsNode(p, iNode) );
+            // collect fanin variables
+            Vec_IntClear( p->vFaninMap );
+            Sfm_ObjForEachFanin( p, iNode, iFanin, k )
+                Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
+            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
+            // generate CNF 
+            Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, Sfm_ObjSatVar(p, p->iPivotNode) );
+            // add clauses
+            Vec_WecForEachLevel( p->vClauses, vClause, k )
+            {
+                if ( Vec_IntSize(vClause) == 0 )
+                    break;
+                RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+                assert( RetValue );
+            }
+        }
+        // create XOR clauses for the roots
+        Vec_IntForEachEntry( p->vRoots, iNode, i )
+        {
+            sat_solver_add_xor( p->pSat, Vec_IntEntry(p->vLits, i), Sfm_ObjSatVar(p, iNode), p->nSatVars++, 0 );
+            Vec_IntWriteEntry( p->vLits, i, Abc_Var2Lit(p->nSatVars-1, 0) );
+        }
+        // make OR clause for the last nRoots variables
+        RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
+        assert( RetValue );
+    }
     // finalize
     RetValue = sat_solver_simplify( p->pSat );
     assert( RetValue );
@@ -113,7 +162,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
     int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
     int pLits[2], nVars = sat_solver_nvars( p->pSat );
     sat_solver_setnvars( p->pSat, nVars + 1 );
-    pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, Vec_IntEntryLast(p->vNodes)), 0 ); // F = 1
+    pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
     pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
     while ( 1 ) 
     {

src/opt/sfm/sfmWin.c

@@ -114,6 +114,7 @@ int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj )
 static inline void  Sfm_NtkIncrementTravId( Sfm_Ntk_t * p )            { p->nTravIds++;                                            }       
 static inline void  Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id )   { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds );       }
 static inline int   Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id )    { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds);   }   
+static inline int   Sfm_ObjIsTravIdPrevious( Sfm_Ntk_t * p, int Id )   { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds-1); }   
 
 static inline void  Sfm_NtkIncrementTravId2( Sfm_Ntk_t * p )           { p->nTravIds2++;                                           }       
 static inline void  Sfm_ObjSetTravIdCurrent2( Sfm_Ntk_t * p, int Id )  { Vec_IntWriteEntry( &p->vTravIds2, Id, p->nTravIds2 );     }
@@ -136,7 +137,8 @@ int Sfm_NtkCheckOverlap_rec( Sfm_Ntk_t * p, int iThis, int iNode )
     int i, iFanin;
     if ( Sfm_ObjIsTravIdCurrent2(p, iThis) || iThis == iNode )
         return 0;
-    if ( Sfm_ObjIsTravIdCurrent(p, iThis) )
+//    if ( Sfm_ObjIsTravIdCurrent(p, iThis) )
+    if ( Sfm_ObjIsTravIdPrevious(p, iThis) )
         return 1;
     Sfm_ObjSetTravIdCurrent2(p, iThis);
     Sfm_ObjForEachFanin( p, iThis, iFanin, i )
@@ -152,24 +154,44 @@ int Sfm_NtkCheckOverlap( Sfm_Ntk_t * p, int iFan, int iNode )
 
 /**Function*************************************************************
 
-  Synopsis    [Check fanouts of the node.]
+  Synopsis    [Recursively collects roots of the window.]
 
-  Description [Returns 1 if they can be used instead of the node.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
+static inline int Sfm_NtkCheckRoot( Sfm_Ntk_t * p, int iNode, int nLevelMax )
 {
     int i, iFanout;
-    if ( Sfm_ObjFanoutNum(p, iNode) >= p->pPars->nFanoutMax )
-        return 0;
+    // the node is the root if one of the following is true:
+    // (1) the node has more than fanouts than the limit
+    if ( Sfm_ObjFanoutNum(p, iNode) > p->pPars->nFanoutMax )
+        return 1;
+    // (2) the node has CO fanouts
+    // (3) the node has fanouts above the cutoff level
     Sfm_ObjForEachFanout( p, iNode, iFanout, i )
-        if ( !Sfm_NtkCheckOverlap( p, iFanout, iNode ) )
-            return 0;
-    return 1;
+        if ( Sfm_ObjIsPo(p, iFanout) || Sfm_ObjLevel(p, iFanout) > nLevelMax )//|| !Sfm_NtkCheckOverlap(p, iFanout, iNode) )
+            return 1;
+    return 0;
+}
+void Sfm_NtkComputeRoots_rec( Sfm_Ntk_t * p, int iNode, int nLevelMax, Vec_Int_t * vRoots, Vec_Int_t * vTfo )
+{
+    int i, iFanout;
+    assert( Sfm_ObjIsNode(p, iNode) );
+    if ( Sfm_ObjIsTravIdCurrent(p, iNode) )
+        return;
+    Sfm_ObjSetTravIdCurrent(p, iNode);
+    if ( iNode != p->iPivotNode )
+        Vec_IntPush( vTfo, iNode );
+    // check if the node should be the root
+    if ( Sfm_NtkCheckRoot( p, iNode, nLevelMax ) )
+        Vec_IntPush( vRoots, iNode );
+    else // if not, explore its fanouts
+        Sfm_ObjForEachFanout( p, iNode, iFanout, i )
+            Sfm_NtkComputeRoots_rec( p, iFanout, nLevelMax, vRoots, vTfo );
 }
 
 /**Function*************************************************************
@@ -244,7 +266,7 @@ static inline int Sfm_ObjIsUseful( Sfm_Ntk_t * p, int iNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax )
+int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
 {
     int i, iFanin;
     if ( Sfm_ObjIsTravIdCurrent( p, iNode ) )
@@ -252,50 +274,41 @@ int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax )
     Sfm_ObjSetTravIdCurrent( p, iNode );
     if ( Sfm_ObjIsPi( p, iNode ) )
     {
-        Vec_IntPush( p->vLeaves, iNode );
+        Vec_IntPush( vLeaves, iNode );
         return 0;
     }
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
-        if ( Sfm_NtkCollectTfi_rec( p, iFanin, nWinSizeMax ) )
+        if ( Sfm_NtkCollectTfi_rec( p, iFanin, vLeaves, vNodes ) )
             return 1;
-    Vec_IntPush( p->vNodes, iNode );
-    return nWinSizeMax && (Vec_IntSize(p->vNodes) > nWinSizeMax);
+    Vec_IntPush( vNodes, iNode );
+    return p->pPars->nWinSizeMax && (Vec_IntSize(vNodes) > p->pPars->nWinSizeMax);
 }
 int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
     int i, k, iTemp, nDivStart;
-    abctime clk = Abc_Clock();
+    abctime clkDiv, clkWin = Abc_Clock();
+
     assert( Sfm_ObjIsNode( p, iNode ) );
+    p->iPivotNode = iNode;
     Vec_IntClear( p->vLeaves ); // leaves 
+    Vec_IntClear( p->vLeaves2 );// leaves 
     Vec_IntClear( p->vNodes );  // internal
+    Vec_IntClear( p->vNodes2 ); // internal
     Vec_IntClear( p->vDivs );   // divisors
     Vec_IntClear( p->vRoots );  // roots
     Vec_IntClear( p->vTfo );    // roots
+
     // collect transitive fanin
     Sfm_NtkIncrementTravId( p );
-    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) )
+    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->vLeaves, p->vNodes ) )
     {
         p->nMaxDivs++;
-        p->timeWin += Abc_Clock() - clk;
+        p->timeWin += Abc_Clock() - clkWin;
         return 0;
     }
-    // collect TFO (currently use only one level of TFO)
-//    if ( Sfm_NtkCheckFanouts(p, iNode) )
-    if ( 0 )
-    {
-        Sfm_ObjForEachFanout( p, iNode, iTemp, i )
-        {
-            if ( Sfm_ObjIsPo(p, iTemp) )
-                continue;
-            Vec_IntPush( p->vRoots, iTemp );
-            Vec_IntPush( p->vTfo, iTemp );
-        }
-    }
-    else
-        Vec_IntPush( p->vRoots, iNode );
-    p->timeWin += Abc_Clock() - clk;
-    clk = Abc_Clock();
+
     // create divisors
+    clkDiv = Abc_Clock();
     Vec_IntClear( p->vDivs );
     Vec_IntForEachEntry( p->vLeaves, iTemp, i )
         Vec_IntPush( p->vDivs, iTemp );
@@ -304,26 +317,26 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     Vec_IntPop( p->vDivs );
     // add non-topological divisors
     nDivStart = Vec_IntSize(p->vDivs);
-    if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax )
+    if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
     {
         Sfm_NtkIncrementTravId2( p );
         Vec_IntForEachEntry( p->vDivs, iTemp, i )
-            if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax )
+            if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
                 Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
     }
     if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
+    {
+/*
+        k = 0;
+        Vec_IntForEachEntryStart( p->vDivs, iTemp, i, Vec_IntSize(p->vDivs) - p->pPars->nWinSizeMax )
+            Vec_IntWriteEntry( p->vDivs, k++, iTemp );
+        assert( k == p->pPars->nWinSizeMax );
+*/
         Vec_IntShrink( p->vDivs, p->pPars->nWinSizeMax );
+    }
     assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
-    p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax);
-    // create ordering of the nodes
-    Vec_IntClear( p->vOrder );
-    Vec_IntForEachEntryReverse( p->vNodes, iTemp, i )
-        Vec_IntPush( p->vOrder, iTemp );
-    Vec_IntForEachEntry( p->vLeaves, iTemp, i )
-        Vec_IntPush( p->vOrder, iTemp );
-    Vec_IntForEachEntryStart( p->vDivs, iTemp, i, nDivStart )
-        Vec_IntPush( p->vOrder, iTemp );
-    // remove fanins from divisors
+    p->nMaxDivs += (int)(Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax);
+    // remove node/fanins from divisors
     // mark fanins
     Sfm_NtkIncrementTravId2( p );
     Sfm_ObjSetTravIdCurrent2( p, iNode );
@@ -336,9 +349,57 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
             Vec_IntWriteEntry( p->vDivs, k++, iTemp );
     Vec_IntShrink( p->vDivs, k );
     assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
-    // statistics
+    clkDiv = Abc_Clock() - clkDiv;
+    p->timeDiv += clkDiv;
     p->nTotalDivs += Vec_IntSize(p->vDivs);
-    p->timeDiv += Abc_Clock() - clk;
+
+    // collect TFO and window roots
+    if ( p->pPars->nTfoLevMax > 0 && !Sfm_NtkCheckRoot(p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax) )
+    {
+        // explore transitive fanout
+        Sfm_NtkIncrementTravId( p );
+        Sfm_NtkComputeRoots_rec( p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax, p->vRoots, p->vTfo );
+        assert( Vec_IntSize(p->vRoots) > 0 );
+        assert( Vec_IntSize(p->vTfo) > 0 );
+        // compute new leaves and nodes
+        Sfm_NtkIncrementTravId( p );
+        Vec_IntForEachEntry( p->vRoots, iTemp, i )
+            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vLeaves2, p->vNodes2 ) )
+                break;
+        if ( i == Vec_IntSize(p->vRoots) )
+        {
+//        printf( "%d -> %d   %d -> %d\n", Vec_IntSize(p->vLeaves), Vec_IntSize(p->vLeaves2), Vec_IntSize(p->vNodes), Vec_IntSize(p->vNodes2) );
+            // swap leaves and nodes
+            ABC_SWAP( Vec_Int_t *, p->vLeaves, p->vLeaves2 );
+            ABC_SWAP( Vec_Int_t *, p->vNodes,  p->vNodes2 );
+        }
+        else
+        {
+            Vec_IntClear( p->vRoots );
+            Vec_IntClear( p->vTfo );
+        }
+//        printf( "Roots = %d.  TFO = %d.\n", Vec_IntSize(p->vRoots), Vec_IntSize(p->vTfo) );
+    }
+
+    // create ordering of the nodes, leaves and divisors that are not among nodes/leaves
+    Vec_IntClear( p->vOrder );
+    Sfm_NtkIncrementTravId2( p );
+    Vec_IntForEachEntryReverse( p->vNodes, iTemp, i )
+    {
+        Sfm_ObjSetTravIdCurrent2( p, iTemp );
+        Vec_IntPush( p->vOrder, iTemp );
+    }
+    Vec_IntForEachEntry( p->vLeaves, iTemp, i )
+    {
+        Sfm_ObjSetTravIdCurrent2( p, iTemp );
+        Vec_IntPush( p->vOrder, iTemp );
+    }
+    Vec_IntForEachEntry( p->vDivs, iTemp, i )
+        if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) )
+            Vec_IntPush( p->vOrder, iTemp );
+
+    // statistics
+    p->timeWin += Abc_Clock() - clkWin - clkDiv;
     if ( !fVerbose )
         return 1;