Changes for delay-oriented computation.

7 files changed, 133 insertions, 53 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 037a1580..56d8795e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5168,15 +5168,28 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
     extern void Sfm_ParSetDefault3( Sfm_Par_t * pPars );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Sfm_Par_t Pars, * pPars = &Pars;
-    int c;
+    Sfm_Par_t Pars, * pPars = &Pars; int c;
     // set defaults
     Sfm_ParSetDefault3( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFLHDMCNPWdamzospvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IOVFKLHDMCNPWdamzosplvwh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfiLevMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfiLevMax < 1 )
+            {
+                Abc_Print( -1, "The number of TFI levels (switch \"-I\") should be at least 1.\n" );
+                goto usage;
+            }
+            break;
         case 'O':
             if ( globalUtilOptind >= argc )
             {
@@ -5188,19 +5201,16 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTfoLevMax < 0 )
                 goto usage;
             break;
-        case 'I':
+        case 'V':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nTfiLevMax = atoi(argv[globalUtilOptind]);
+            pPars->nTfiLevMax = pPars->nTfoLevMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             if ( pPars->nTfiLevMax < 1 )
-            {
-                Abc_Print( -1, "The number of TFI levels (switch \"-I\") should be at least 1.\n" );
                 goto usage;
-            }
             break;
         case 'F':
             if ( globalUtilOptind >= argc )
@@ -5213,6 +5223,17 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFanoutMax < 0 )
                 goto usage;
             break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nVarMax < 2 || pPars->nVarMax > 6 )
+                goto usage;
+            break;
         case 'L':
             if ( globalUtilOptind >= argc )
             {
@@ -5319,6 +5340,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             pPars->fPrintDecs ^= 1;
             break;
+        case 'l':
+            pPars->fLibVerbose ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -5346,13 +5370,15 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs3 [-OIFLHDMCNPW <num>] [-amzospvwh]\n" );
+    Abc_Print( -2, "usage: mfs3 [-IOVFKLHDMCNPW <num>] [-amzosplvwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of mapped networks\n" );
-    Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
     Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n",             pPars->nTfiLevMax );
+    Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
+    Abc_Print( -2, "\t-V <num> : the number of levels in the TFI/TFO cone (1 <= num) [default = %d]\n",         pPars->nTfiLevMax );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nFanoutMax );
-    Abc_Print( -2, "\t-L <num> : the min size of max fanout-free cone (MFFC) [default = %d]\n",                 pPars->nMffcMin );
-    Abc_Print( -2, "\t-H <num> : the max size of max fanout-free cone (MFFC) [default = %d]\n",                 pPars->nMffcMax );
+    Abc_Print( -2, "\t-K <num> : the max number of variables (2 <= num <= 6 ) [default = %d]\n",                pPars->nVarMax );
+    Abc_Print( -2, "\t-L <num> : the min size of max fanout-free cone (MFFC) (area-only) [default = %d]\n",     pPars->nMffcMin );
+    Abc_Print( -2, "\t-H <num> : the max size of max fanout-free cone (MFFC) (area-only) [default = %d]\n",     pPars->nMffcMax );
     Abc_Print( -2, "\t-D <num> : the max number of decompositions to try (1 <= num <= 4) [default = %d]\n",     pPars->nDecMax );
     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-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
@@ -5365,6 +5391,7 @@ usage:
     Abc_Print( -2, "\t-o       : toggle using old implementation for comparison [default = %s]\n",              pPars->fRrOnly? "yes": "no" );
     Abc_Print( -2, "\t-s       : toggle using simulation [default = %s]\n",                                     pPars->fUseSim? "yes": "no" );
     Abc_Print( -2, "\t-p       : toggle printing decompositions [default = %s]\n",                              pPars->fPrintDecs? "yes": "no" );
+    Abc_Print( -2, "\t-l       : toggle printing library usage statistics [default = %s]\n",                    pPars->fLibVerbose? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index b09852ff..e4e92503 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -286,7 +286,7 @@ static inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry )
 {
     if ( p->nSize < Level + 1 )
     {
-        Vec_WecGrow( p, Abc_MaxInt(2*p->nCap, Level + 1) );
+        Vec_WecGrow( p, Abc_MaxInt(2*p->nSize, Level + 1) );
         p->nSize = Level + 1;
     }
     Vec_IntPush( Vec_WecEntry(p, Level), Entry );
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 53cbe8e5..1133b7e8 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -46,6 +46,7 @@ struct Sfm_Par_t_
     int             nTfiLevMax;    // the maximum fanin levels
     int             nFanoutMax;    // the maximum number of fanouts
     int             nDepthMax;     // the maximum depth to try
+    int             nVarMax;       // the maximum variable count
     int             nMffcMin;      // the minimum MFFC size
     int             nMffcMax;      // the maximum MFFC size
     int             nDecMax;       // the maximum number of decompositions
@@ -63,6 +64,7 @@ struct Sfm_Par_t_
     int             fZeroCost;     // enable zero-cost replacement
     int             fUseSim;       // enable simulation
     int             fPrintDecs;    // enable printing decompositions
+    int             fLibVerbose;   // enable library stats
     int             fVerbose;      // enable basic stats
     int             fVeryVerbose;  // enable detailed stats
 };
diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c
index 775b9f4c..ea0779ff 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -58,6 +58,7 @@ struct Sfm_Dec_t_
     int               AreaMffc;    // the area of gates in MFFC
     int               DelayMin;    // temporary min delay
     int               iTarget;     // target node
+    int               DeltaCrit;   // critical delta
     word              uCareSet;    // computed careset
     Vec_Int_t         vObjRoots;   // roots of the window
     Vec_Int_t         vObjGates;   // functionality
@@ -84,11 +85,13 @@ struct Sfm_Dec_t_
     Vec_Int_t         vTemp2;
     Vec_Int_t         vCands;
     // statistics
+    abctime           timeLib;
     abctime           timeWin;
     abctime           timeCnf;
     abctime           timeSat;
     abctime           timeSatSat;
     abctime           timeSatUnsat;
+    abctime           timeTime;
     abctime           timeOther;
     abctime           timeStart;
     abctime           timeTotal;
@@ -150,7 +153,8 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
     pPars->nTfiLevMax   =  100;  // the maximum fanin levels
     pPars->nFanoutMax   =   30;  // the maximum number of fanoutsp
     pPars->nMffcMin     =    1;  // the maximum MFFC size
-    pPars->nMffcMax     =    3;  // the maximum MFFC size
+    pPars->nMffcMax     =    8;  // the maximum MFFC size
+    pPars->nVarMax      =    6;  // the maximum variable count
     pPars->nDecMax      =    1;  // the maximum number of decompositions
     pPars->nWinSizeMax  =    0;  // the maximum window size
     pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
@@ -159,7 +163,7 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
     pPars->fUseAndOr    =    0;  // enable internal detection of AND/OR gates
     pPars->fZeroCost    =    0;  // enable zero-cost replacement
     pPars->fUseSim      =    0;  // enable simulation
-    pPars->fArea        =    1;  // performs optimization for area
+    pPars->fArea        =    0;  // performs optimization for area
     pPars->fVerbose     =    0;  // enable basic stats
     pPars->fVeryVerbose =    0;  // enable detailed stats
 }
@@ -179,16 +183,16 @@ Sfm_Dec_t * Sfm_DecStart( Sfm_Par_t * pPars, Mio_Library_t * pLib, Abc_Ntk_t * p
 {
     extern void Sfm_LibPreprocess( Mio_Library_t * pLib, Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t * vGateCnfs, Vec_Ptr_t * vGateHands );
     Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 ); int i;
-    p->pPars = pPars;
-    p->pNtk = pNtk;
-    p->pSat = sat_solver_new();
     p->timeStart = Abc_Clock();
-    for ( i = 0; i < SFM_SUPP_MAX; i++ )
-        p->pTtElems[i] = p->TtElems[i];
-    Abc_TtElemInit( p->pTtElems, SFM_SUPP_MAX );
-    p->pLib = Sfm_LibPrepare( pPars->nMffcMax + 1, 1, !pPars->fArea, pPars->fVerbose );
+    p->pPars     = pPars;
+    p->pNtk      = pNtk;
+    p->pSat      = sat_solver_new();
+    p->DeltaCrit = 5 * (int)(MIO_NUM*Mio_LibraryReadDelayInvMax(pLib)) / 2;
+p->timeLib = Abc_Clock();
+    p->pLib = Sfm_LibPrepare( pPars->nVarMax, 1, !pPars->fArea, pPars->fLibVerbose );
+p->timeLib = Abc_Clock() - p->timeLib;
     if ( !pPars->fArea )
-        p->pTim = Sfm_TimStart( pLib, NULL, pNtk );
+        p->pTim = Sfm_TimStart( pLib, NULL, pNtk, p->DeltaCrit );
     if ( pPars->fVeryVerbose )
 //    if ( pPars->fVerbose )
         Sfm_LibPrint( p->pLib );
@@ -211,6 +215,10 @@ Sfm_Dec_t * Sfm_DecStart( Sfm_Par_t * pPars, Mio_Library_t * pLib, Abc_Ntk_t * p
         p->GateOr[2] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "or10", NULL) );
         p->GateOr[3] = Mio_GateReadValue( Mio_LibraryReadGateByName(pLib, "or11", NULL) );
     }
+    // elementary truth tables
+    for ( i = 0; i < SFM_SUPP_MAX; i++ )
+        p->pTtElems[i] = p->TtElems[i];
+    Abc_TtElemInit( p->pTtElems, SFM_SUPP_MAX );
     return p;
 }
 void Sfm_DecStop( Sfm_Dec_t * p )
@@ -1608,13 +1616,15 @@ void Sfm_DecPrintStats( Sfm_Dec_t * p )
         p->nMaxDivs, p->nMaxWin, (int)(p->nAllDivs/Abc_MaxInt(1, p->nNodesTried)), (int)(p->nAllWin/Abc_MaxInt(1, p->nNodesTried)), p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsOver, p->nTimeOuts );
 
     p->timeTotal = Abc_Clock() - p->timeStart;
-    p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat;
+    p->timeOther = p->timeTotal - p->timeLib - p->timeWin - p->timeCnf - p->timeSat - p->timeTime;
 
+    ABC_PRTP( "Lib   ", p->timeLib  ,     p->timeTotal );
     ABC_PRTP( "Win   ", p->timeWin  ,     p->timeTotal );
     ABC_PRTP( "Cnf   ", p->timeCnf  ,     p->timeTotal );
     ABC_PRTP( "Sat   ", p->timeSat  ,     p->timeTotal );
     ABC_PRTP( " Sat  ", p->timeSatSat,    p->timeTotal );
     ABC_PRTP( " Unsat", p->timeSatUnsat,  p->timeTotal );
+    ABC_PRTP( "Timing", p->timeTime ,     p->timeTotal );
     ABC_PRTP( "Other ", p->timeOther,     p->timeTotal );
     ABC_PRTP( "ALL   ", p->timeTotal,     p->timeTotal );
 
@@ -1720,11 +1730,9 @@ p->timeSat += Abc_Clock() - clk;
 void Abc_NtkDelayOpt( Sfm_Dec_t * p )
 {
     Abc_Ntk_t * pNtk = p->pNtk;
-    Sfm_Par_t * pPars = p->pPars;
-
-    printf( "Initial    delay = %8.2f.\n", MIO_NUMINV*Sfm_TimReadNtkDelay(p->pTim) );
+    Sfm_Par_t * pPars = p->pPars; int n;
     Abc_NtkCleanMarkABC( pNtk );
-    while ( 1 )
+    for ( n = 0; pPars->nNodesMax == 0 || n < pPars->nNodesMax; n++ )
     {
         Abc_Obj_t * pObj, * pObjNew; abctime clk;
         int i = 0, Limit, RetValue;
@@ -1738,6 +1746,7 @@ void Abc_NtkDelayOpt( Sfm_Dec_t * p )
         {
             int OldId = Abc_ObjId(pObj);
             int DelayOld = Sfm_TimReadObjDelay(p->pTim, OldId);
+            assert( pObj->fMarkA == 0 );
 
             p->nNodesTried++;
 clk = Abc_Clock();
@@ -1745,7 +1754,6 @@ clk = Abc_Clock();
 p->timeWin += Abc_Clock() - clk;
             if ( p->nDivs < 2 || (pPars->nWinSizeMax && pPars->nWinSizeMax < Vec_IntSize(&p->vObjGates)) )
             {
-                assert( pObj->fMarkA == 0 );
                 pObj->fMarkA = 1;
                 continue;
             }
@@ -1762,7 +1770,6 @@ clk = Abc_Clock();
 p->timeCnf += Abc_Clock() - clk;
             if ( !RetValue )
             {
-                assert( pObj->fMarkA == 0 );
                 pObj->fMarkA = 1;
                 continue;
             }
@@ -1773,7 +1780,6 @@ clk = Abc_Clock();
 p->timeSat += Abc_Clock() - clk;
             if ( RetValue < 0 )
             {
-                assert( pObj->fMarkA == 0 );
                 pObj->fMarkA = 1;
                 continue;
             }
@@ -1781,14 +1787,18 @@ p->timeSat += Abc_Clock() - clk;
             assert( Vec_IntSize(&p->vObjGates) - Limit <= 2 );
             p->nNodesChanged++;
             Abc_NtkCountStats( p, Limit );
-            Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands, p->GateBuffer, p->GateInvert, &p->vGateFuncs, &p->vCands );
-            Sfm_TimUpdateTiming( p->pTim, &p->vCands );
-
+            Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands, p->GateBuffer, p->GateInvert, &p->vGateFuncs, &p->vTemp );
+clk = Abc_Clock();
+            Sfm_TimUpdateTiming( p->pTim, &p->vTemp );
+p->timeTime += Abc_Clock() - clk;
             pObjNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk)-1 );
-            printf( "Node %5d : Old =%8.2f.  Predicted =%8.2f.  New =%8.2f.  Final =%8.2f\n", 
-                OldId, MIO_NUMINV*DelayOld, MIO_NUMINV*p->DelayMin, 
-                MIO_NUMINV*Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)), 
-                MIO_NUMINV*Sfm_TimReadNtkDelay(p->pTim) );
+            assert( p->DelayMin == Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)) );
+            // report
+            if ( pPars->fVerbose )
+                printf( "Node %5d :  I =%3d.  Cand = %5d (%6.2f %%)   Old =%8.2f.  New =%8.2f.  Final =%8.2f\n", 
+                    OldId, i, Vec_IntSize(&p->vCands), 100.0 * Vec_IntSize(&p->vCands) / Abc_NtkNodeNum(p->pNtk),
+                    MIO_NUMINV*DelayOld, MIO_NUMINV*Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)), 
+                    MIO_NUMINV*Sfm_TimReadNtkDelay(p->pTim) );
             break;
         }
         if ( pPars->iNodeOne )
@@ -1812,9 +1822,9 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
             printf( "WinMax = %d. ",  pPars->nWinSizeMax );
         if ( pPars->nBTLimit )
             printf( "Confl = %d. ",   pPars->nBTLimit );
-        if ( pPars->nMffcMin )
+        if ( pPars->nMffcMin && pPars->fArea )
             printf( "MffcMin = %d. ", pPars->nMffcMin );
-        if ( pPars->nMffcMax )
+        if ( pPars->nMffcMax && pPars->fArea )
             printf( "MffcMax = %d. ", pPars->nMffcMax );
         if ( pPars->nDecMax )
             printf( "DecMax = %d. ",  pPars->nDecMax );
@@ -1822,8 +1832,11 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
             printf( "Pivot = %d. ",   pPars->iNodeOne );
         if ( !pPars->fArea )
             printf( "Win = %d. ",     pPars->nTimeWin );
+        if ( !pPars->fArea )
+            printf( "Delta = %.2f ps. ", MIO_NUMINV*p->DeltaCrit );
+        if ( pPars->fArea )
+            printf( "0-cost = %s. ",  pPars->fZeroCost ? "yes" : "no" );
         printf( "Sim = %s. ",         pPars->fUseSim ? "yes" : "no" );
-        printf( "0-cost = %s. ",      pPars->fZeroCost ? "yes" : "no" );
         printf( "\n" );
     }
     // preparation steps
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 1b84a6fb..e5f73e38 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -212,7 +212,7 @@ extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNe
 extern int          Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
 extern word         Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
 /*=== sfmTime.c ==========================================================*/
-extern Sfm_Tim_t *  Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk );
+extern Sfm_Tim_t *  Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit );
 extern void         Sfm_TimStop( Sfm_Tim_t * p );
 extern int          Sfm_TimReadNtkDelay( Sfm_Tim_t * p );
 extern int          Sfm_TimReadObjDelay( Sfm_Tim_t * p, int iObj );
diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c
index bf4f636a..00fc92e0 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -44,6 +44,8 @@ struct Sfm_Fun_t_
 };
 struct Sfm_Lib_t_
 {
+    int             nVars;         // variable count
+    int             fVerbose;      // verbose statistics
     Mio_Cell2_t *   pCells;        // library gates
     int             nCells;        // library gate count
     int             fDelay;        // uses delay profile
@@ -53,6 +55,7 @@ struct Sfm_Lib_t_
     Vec_Mem_t *     vTtMem;        // truth tables
     Vec_Int_t       vLists;        // lists of funcs for each truth table
     Vec_Int_t       vCounts;       // counters of functions for each truth table
+    Vec_Int_t       vHits;         // the number of times this function was used
     Vec_Int_t       vProfs;        // area/delay profiles
     Vec_Int_t       vStore;        // storage for area/delay profiles
     Vec_Int_t       vTemp;         // temporary storage for candidates
@@ -185,28 +188,47 @@ int Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int i
   SeeAlso     []
 
 ***********************************************************************/
-Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay )
+Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay, int fVerbose )
 {
     Sfm_Lib_t * p = ABC_CALLOC( Sfm_Lib_t, 1 );
     p->vTtMem = Vec_MemAllocForTT( nVars, 0 );   
     Vec_IntGrow( &p->vLists,  (1 << 16) );
     Vec_IntGrow( &p->vCounts, (1 << 16) );
+    Vec_IntGrow( &p->vHits,   (1 << 16) );
     Vec_IntFill( &p->vLists,  2, -1 );
     Vec_IntFill( &p->vCounts, 2, -1 );
+    Vec_IntFill( &p->vHits,   2, -1 );
     p->nObjsAlloc = (1 << 16);
     p->pObjs = ABC_CALLOC( Sfm_Fun_t, p->nObjsAlloc );
     p->fDelay = fDelay;
     if ( fDelay ) Vec_IntGrow( &p->vProfs,  (1 << 16) );
     if ( fDelay ) Vec_IntGrow( &p->vStore,  (1 << 18) );
     Vec_IntGrow( &p->vTemp, 16 );
+    p->nVars = nVars;
+    p->fVerbose = fVerbose;
     return p;
 }
 void Sfm_LibStop( Sfm_Lib_t * p )
 {
+    if ( p->fVerbose )
+    {
+        // print usage stats
+        int i, nFanins;  word * pTruth;
+        Vec_MemForEachEntry( p->vTtMem, pTruth, i )
+        {
+            if ( Vec_IntEntry(&p->vHits, i) == 0 )
+                continue;
+            nFanins = Abc_TtSupportSize(pTruth, p->nVars);
+            printf( "%8d : ", i );
+            printf( "%8d   ", Vec_IntEntry(&p->vHits, i) );
+            Dau_DsdPrintFromTruth( pTruth, nFanins );
+        }
+    }
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFree( p->vTtMem );
     Vec_IntErase( &p->vLists );
     Vec_IntErase( &p->vCounts );
+    Vec_IntErase( &p->vHits );
     Vec_IntErase( &p->vProfs );
     Vec_IntErase( &p->vStore );
     Vec_IntErase( &p->vTemp );
@@ -293,6 +315,7 @@ void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word uTruth, int * Perm, int nFanins, Mio
     {
         Vec_IntPush( &p->vLists, -1 );
         Vec_IntPush( &p->vCounts, 0 );
+        Vec_IntPush( &p->vHits,   0 );
     }
     assert( pCellBot != NULL );
     // iterate through the supergates of this truth table
@@ -388,7 +411,7 @@ void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word uTruth, int * Perm, int nFanins, Mio
 Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
 {
     abctime clk = Abc_Clock();
-    Sfm_Lib_t * p = Sfm_LibStart( nVars, fDelay );
+    Sfm_Lib_t * p = Sfm_LibStart( nVars, fDelay, fVerbose );
     Mio_Cell2_t * pCell1, * pCell2, * pLimit;
     int * pPerm[7], * Perm1, * Perm2, Perm[6];
     int nPerms[7], i, f, n;
@@ -407,7 +430,7 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
         word uTruth = pCell1->uTruth;
         if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
             Vec_IntWriteEntry( vUseful, pCell1 - p->pCells, 1 );
-        else
+        else if ( p->fVerbose )
             printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );
     }
     // generate permutations
@@ -562,7 +585,12 @@ int Sfm_LibFindMatches( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins,
     assert( uTruth != 0 && uTruth != ~(word)0 && uTruth != s_Truths6[0] && uTruth != ~s_Truths6[0] );
     iFunc = *Vec_MemHashLookup( p->vTtMem,  &uTruth );
     if ( iFunc == -1 )
+    {
+        // print functions not found in the library
+        //Dau_DsdPrintFromTruth( &uTruth, nFanins );
         return 0;
+    }
+    Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
     // collect matches
     Sfm_LibForEachSuper( p, pObj, iFunc )
     {
@@ -639,6 +667,7 @@ int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, in
     iFunc = *Vec_MemHashLookup( p->vTtMem,  &uTruth );
     if ( iFunc == -1 )
         return -1;
+    Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
     Sfm_LibForEachSuper( p, pObj, iFunc )
         if ( !pObjMin || pObjMin->Area > pObj->Area )
             pObjMin = pObj;
diff --git a/src/opt/sfm/sfmTime.c b/src/opt/sfm/sfmTime.c
index b58a4bf2..939bcd85 100644
--- a/src/opt/sfm/sfmTime.c
+++ b/src/opt/sfm/sfmTime.c
@@ -34,7 +34,7 @@ struct Sfm_Tim_t_
     Scl_Con_t *       pExt;        // external timing
     Abc_Ntk_t *       pNtk;        // mapped network
     int               Delay;       // the largest delay
-    int               CritDelta;   // critical delay delta
+    int               DeltaCrit;   // critical delay delta
     // timing info
     Vec_Int_t         vTimArrs;    // arrivals (rise/fall)
     Vec_Int_t         vTimReqs;    // required (rise/fall)
@@ -235,7 +235,7 @@ int Sfm_TimTrace( Sfm_Tim_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Sfm_Tim_t * Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk )
+Sfm_Tim_t * Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit )
 {
 //    Abc_Obj_t * pObj; int i;
     Sfm_Tim_t * p = ABC_CALLOC( Sfm_Tim_t, 1 );
@@ -253,7 +253,8 @@ Sfm_Tim_t * Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pN
 //        Vec_IntFillExtra( &p->vTimEdges, Vec_IntSize(Vec_IntSize(&p->vTimEdges)) + Abc_ObjFaninNum(pObj), 0 );
 //    }
     p->Delay = Sfm_TimTrace( p );
-    p->CritDelta = 3 * (int)(MIO_NUM*Mio_LibraryReadDelayInvMax(pLib));
+    assert( DeltaCrit > 0 && DeltaCrit < 10000 );
+    p->DeltaCrit = DeltaCrit;
     return p;
 }
 void Sfm_TimStop( Sfm_Tim_t * p )
@@ -292,7 +293,7 @@ int Sfm_TimReadObjDelay( Sfm_Tim_t * p, int iObj )
 void Sfm_TimTest( Abc_Ntk_t * pNtk )
 {
     Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
-    Sfm_Tim_t * p = Sfm_TimStart( pLib, NULL, pNtk );
+    Sfm_Tim_t * p = Sfm_TimStart( pLib, NULL, pNtk, 100 );
     printf( "Max delay = %.2f.  Path = %d (%d).\n", MIO_NUMINV*p->Delay, Sfm_TimCriticalPath(p, 1), Abc_NtkNodeNum(p->pNtk) );
     Sfm_TimStop( p );
 }
@@ -357,7 +358,7 @@ int Sfm_TimSortArrayByArrival( Sfm_Tim_t * p, Vec_Int_t * vNodes, int iPivot )
     word Entry; 
     int i, Id, nDivNew = -1; 
     int MaxDelay = Sfm_TimArrMaxId(p, iPivot);
-    assert( p->CritDelta > 0 );
+    assert( p->DeltaCrit > 0 );
     // collect nodes
     Vec_WrdClear( &p->vSortData );
     Vec_IntForEachEntry( vNodes, Id, i )
@@ -369,7 +370,7 @@ int Sfm_TimSortArrayByArrival( Sfm_Tim_t * p, Vec_Int_t * vNodes, int iPivot )
     Vec_WrdForEachEntry( &p->vSortData, Entry, i )
     {
         Vec_IntPush( vNodes, (int)(Entry >> 32) );
-        if ( nDivNew == -1 && ((int)Entry) + p->CritDelta > MaxDelay )
+        if ( nDivNew == -1 && ((int)Entry) + p->DeltaCrit > MaxDelay )
             nDivNew = i;
     }
     return nDivNew;
@@ -406,9 +407,17 @@ int Sfm_TimPriorityNodes( Sfm_Tim_t * p, Vec_Int_t * vCands, int Window )
     Vec_WecSort( &p->vLevels, 0 );
     Vec_IntClear( vCands );
     Vec_WecForEachLevel( &p->vLevels, vLevel, i )
+    {
+//        printf( "%d ", Vec_IntSize(vLevel) );
         Abc_NtkForEachObjVec( vLevel, p->pNtk, pObj, k )
             if ( !pObj->fMarkA )
                 Vec_IntPush( vCands, Abc_ObjId(pObj) );
+//        if ( Vec_IntSize(vCands) > 10 )
+//            break;
+    }
+//    printf( "\n" );
+//    printf( "Path = %5d   ", Vec_IntSize(&p->vPath) );
+//    printf( "Cand = %5d   ", Vec_IntSize(vCands) );
     return Vec_IntSize(vCands) > 0;
 }
 
@@ -425,7 +434,7 @@ int Sfm_TimPriorityNodes( Sfm_Tim_t * p, Vec_Int_t * vCands, int Window )
 ***********************************************************************/
 int Sfm_TimNodeIsNonCritical( Sfm_Tim_t * p, Abc_Obj_t * pPivot, Abc_Obj_t * pNode )
 {
-    return Sfm_TimArrMax(p, pNode) + p->CritDelta <= Sfm_TimArrMax(p, pPivot);
+    return Sfm_TimArrMax(p, pNode) + p->DeltaCrit <= Sfm_TimArrMax(p, pPivot);
 }
 
 /**Function*************************************************************