Changes for delay-oriented computation.

6 files changed, 236 insertions, 136 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 12e911a6..4fe8bc0b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5174,7 +5174,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault3( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "IOVFKLHDMCNPWdamzosplvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IOVFKLHRMCNPWDdamzospdlvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5258,10 +5258,10 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nMffcMax < 0 )
                 goto usage;
             break;
-        case 'D':
+        case 'R':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
                 goto usage;
             }
             pPars->nDecMax = atoi(argv[globalUtilOptind]);
@@ -5324,6 +5324,17 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeWin < 0 || pPars->nTimeWin > 100 )
                 goto usage;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->DeltaCrit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->DeltaCrit < 0 )
+                goto usage;
+            break;
         case 'a':
             pPars->fArea ^= 1;
             break;
@@ -5342,6 +5353,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             pPars->fPrintDecs ^= 1;
             break;
+        case 'd':
+            pPars->fDelayVerbose ^= 1;
+            break;
         case 'l':
             pPars->fLibVerbose ^= 1;
             break;
@@ -5372,7 +5386,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs3 [-IOVFKLHDMCNPW <num>] [-amzosplvwh]\n" );
+    Abc_Print( -2, "usage: mfs3 [-IOVFKLHRMCNPWD <num>] [-amzospdlvwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of mapped networks\n" );
     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 );
@@ -5381,18 +5395,20 @@ usage:
     Abc_Print( -2, "\t-K <num> : the max number of variables (2 <= num <= 8 ) [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-R <num> : the max number of decomposition rounds (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 );
     Abc_Print( -2, "\t-N <num> : the max number of nodes to try (0 = all) [default = %d]\n",                    pPars->nNodesMax );
     Abc_Print( -2, "\t-P <num> : one particular node to try (0 = none) [default = %d]\n",                       pPars->iNodeOne );
     Abc_Print( -2, "\t-W <num> : size of timing window in percents (0 <= num <= 100) [default = %d]\n",         pPars->nTimeWin );
+    Abc_Print( -2, "\t-D <num> : size of critical-timing delay-delta (in picoseconds) [default = %d]\n",        pPars->DeltaCrit );
     Abc_Print( -2, "\t-a       : toggle area minimization [default = %s]\n",                                    pPars->fArea? "yes": "no" );
     Abc_Print( -2, "\t-m       : toggle detecting multi-input AND/OR gates [default = %s]\n",                   pPars->fUseAndOr? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggle zero-cost replacements [default = %s]\n",                               pPars->fZeroCost? "yes": "no" );
     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-d       : toggle printing delay profile statistics [default = %s]\n",                    pPars->fDelayVerbose? "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" );
diff --git a/src/map/scl/sclSize.c b/src/map/scl/sclSize.c
index d323df8b..ab3e3f3e 100644
--- a/src/map/scl/sclSize.c
+++ b/src/map/scl/sclSize.c
@@ -567,7 +567,7 @@ void Abc_SclTimeIncUpdateLevel_rec( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, LevelNew = Abc_ObjLevelNew(pObj);
-    if ( LevelNew == (int)pObj->Level )
+    if ( LevelNew == (int)pObj->Level && Abc_ObjIsNode(pObj) && Abc_ObjFaninNum(pObj) > 0 )
         return;
     pObj->Level = LevelNew;
     Abc_ObjForEachFanout( pObj, pFanout, i )
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 1133b7e8..02d12b3a 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -57,6 +57,7 @@ struct Sfm_Par_t_
     int             iNodeOne;      // one particular node to try
     int             nFirstFixed;   // the number of first nodes to be treated as fixed
     int             nTimeWin;      // the size of timing window in percents
+    int             DeltaCrit;     // delay delta in picoseconds
     int             fRrOnly;       // perform redundance removal
     int             fArea;         // performs optimization for area
     int             fMoreEffort;   // performs high-affort minimization
@@ -65,6 +66,7 @@ struct Sfm_Par_t_
     int             fUseSim;       // enable simulation
     int             fPrintDecs;    // enable printing decompositions
     int             fLibVerbose;   // enable library stats
+    int             fDelayVerbose; // enable delay 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 6310cb1a..3d1e8ce2 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -153,13 +153,14 @@ 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     =    8;  // the maximum MFFC size
+    pPars->nMffcMax     =    3;  // 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
     pPars->nBTLimit     =    0;  // the maximum number of conflicts in one SAT run
     pPars->nTimeWin     =    1;  // the size of timing window in percents
+    pPars->DeltaCrit    =    0;  // delta delay in picoseconds
     pPars->fUseAndOr    =    0;  // enable internal detection of AND/OR gates
     pPars->fZeroCost    =    0;  // enable zero-cost replacement
     pPars->fUseSim      =    0;  // enable simulation
@@ -187,9 +188,10 @@ Sfm_Dec_t * Sfm_DecStart( Sfm_Par_t * pPars, Mio_Library_t * pLib, Abc_Ntk_t * p
     p->pPars     = pPars;
     p->pNtk      = pNtk;
     p->pSat      = sat_solver_new();
-    p->DeltaCrit = 5 * (int)(MIO_NUM*Mio_LibraryReadDelayInvMax(pLib)) / 2;
+    if ( pPars->DeltaCrit == 0 )
+        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->pLib = Sfm_LibPrepare( pPars->nVarMax, 1, !pPars->fArea, pPars->fVerbose, pPars->fLibVerbose );
 p->timeLib = Abc_Clock() - p->timeLib;
     if ( !pPars->fArea )
         p->pTim = Sfm_TimStart( pLib, NULL, pNtk, p->DeltaCrit );
@@ -224,6 +226,11 @@ p->timeLib = Abc_Clock() - p->timeLib;
 void Sfm_DecStop( Sfm_Dec_t * p )
 {
     Abc_Ntk_t * pNtk = p->pNtk;
+    Abc_Obj_t * pObj; int i;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        //assert( (int)pObj->Level == Abc_ObjLevelNew(pObj) );
+        if ( (int)pObj->Level != Abc_ObjLevelNew(pObj) )
+            printf( "Level count mismatch at node %d.\n", i );
     Sfm_LibStop( p->pLib );
     if ( p->pTim ) Sfm_TimStop( p->pTim );
     // library
@@ -767,6 +774,71 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Sfm_DecMffcArea( Abc_Ntk_t * pNtk, Vec_Int_t * vMffc )
+{
+    Abc_Obj_t * pObj; 
+    int i, nAreaMffc = 0;
+    Abc_NtkForEachObjVec( vMffc, pNtk, pObj, i )
+        nAreaMffc += (int)(MIO_NUM * Mio_GateReadArea((Mio_Gate_t *)pObj->pData));
+    return nAreaMffc;
+}
+int Sfm_MffcDeref_rec( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Area = (int)(MIO_NUM*Mio_GateReadArea((Mio_Gate_t *)pObj->pData));
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        assert( pFanin->vFanouts.nSize > 0 );
+        if ( --pFanin->vFanouts.nSize == 0 && !Abc_ObjIsCi(pFanin) )
+            Area += Sfm_MffcDeref_rec( pFanin );
+    }
+    return Area;
+}
+int Sfm_MffcRef_rec( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Area = (int)(MIO_NUM*Mio_GateReadArea((Mio_Gate_t *)pObj->pData));
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( pFanin->vFanouts.nSize++ == 0 && !Abc_ObjIsCi(pFanin) )
+            Area += Sfm_MffcRef_rec( pFanin );
+    }
+    return Area;
+}
+int Sfm_DecMffcAreaReal( Abc_Obj_t * pPivot, Vec_Int_t * vCut )
+{
+    Abc_Ntk_t * pNtk = pPivot->pNtk;
+    Abc_Obj_t * pObj; 
+    int i, Area1, Area2;
+    assert( Abc_ObjIsNode(pPivot) );
+    Abc_NtkForEachObjVec( vCut, pNtk, pObj, i )
+        pObj->vFanouts.nSize++;
+    Area1 = Sfm_MffcDeref_rec( pPivot );
+    Area2 = Sfm_MffcRef_rec( pPivot );
+    Abc_NtkForEachObjVec( vCut, pNtk, pObj, i )
+        pObj->vFanouts.nSize--;
+    assert( Area1 == Area2 );
+    return Area1;
+}
+void Sfm_DecPrepareVec( Vec_Int_t * vMap, int * pNodes, int nNodes, Vec_Int_t * vCut )
+{
+    int i;
+    Vec_IntClear( vCut );
+    for ( i = 0; i < nNodes; i++ )
+        Vec_IntPush( vCut, Vec_IntEntry(vMap, pNodes[i]) );    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSupp0, int * pSupp1, int nSupp0, int nSupp1, word * pTruth, int * pSupp, int Var )
 {
     Vec_Int_t vVec0 = { 2*SFM_SUPP_MAX, nSupp0, pSupp0 };
@@ -1058,7 +1130,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )
     int nSupp[SFM_DEC_MAX], pAssump[SFM_WIN_MAX];
     int fVeryVerbose = p->pPars->fPrintDecs || p->pPars->fVeryVerbose;
     int nDecs = Abc_MaxInt(p->pPars->nDecMax, 1);
-    int i, iBest = -1, RetValue, Prev = 0; 
+    int i, RetValue, Prev = 0, iBest = -1, AreaThis, AreaNew;
+    int GainThis, GainBest = -1, iLibObj, iLibObjBest = -1; 
     assert( p->pPars->fArea == 1 );
     if ( p->pPars->fUseSim )
         Sfm_ObjSetupSimInfo( pObj );
@@ -1093,10 +1166,33 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )
             printf( "Dec  %d: Pat0 = %2d  Pat1 = %2d  Supp = %d  ", i, p->nPats[0], p->nPats[1], nSupp[i] );
         if ( fVeryVerbose )
             Dau_DsdPrintFromTruth( uTruth[i], nSupp[i] );
-        if ( iBest == -1 || nSupp[iBest] > nSupp[i] )
-            iBest = i;
-        if ( nSupp[iBest] < 2 )
-            break;
+        if ( nSupp[i] < 2 )
+        {
+            RetValue = Sfm_LibImplementSimple( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vObjGates, &p->vObjFanins );
+            assert( nSupp[i] <= p->pPars->nVarMax );
+            p->nLuckySizes[nSupp[i]]++;
+            assert( RetValue <= 2 );
+            p->nLuckyGates[RetValue]++;
+            return RetValue;
+        }
+        AreaNew = Sfm_LibFindAreaMatch( p->pLib, uTruth[i], nSupp[i], &iLibObj );
+        if ( AreaNew == -1 )
+            continue;
+        // compute area savings
+        Sfm_DecPrepareVec( &p->vObjMap, pSupp[i], nSupp[i], &p->vTemp );
+        AreaThis = Sfm_DecMffcAreaReal(pObj, &p->vTemp);
+        assert( p->AreaMffc <= AreaThis );
+        if ( p->pPars->fZeroCost ? (AreaNew > AreaThis) : (AreaNew >= AreaThis) )
+            continue;
+        // find the best gain
+        GainThis = AreaThis - AreaNew;
+        assert( GainThis >= 0 );
+        if ( p->pPars->fZeroCost ? (GainBest <= GainThis) : (GainBest < GainThis) )
+        {
+            GainBest    = GainThis;
+            iLibObjBest = iLibObj;
+            iBest       = i;
+        }
     }
     if ( p->pPars->fUseSim )
         Sfm_ObjSetdownSimInfo( pObj );
@@ -1107,28 +1203,18 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )
         p->nNoDecs++;
         return -2;
     }
-    else
-    {
-        if ( fVeryVerbose )
-            printf( "Best %d: %d  ", iBest, nSupp[iBest] );
-//        if ( fVeryVerbose )
-//            Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );
-    }
-//    return -1;
-    RetValue = Sfm_LibImplement( p->pLib, uTruth[iBest], pSupp[iBest], nSupp[iBest], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost );
     if ( fVeryVerbose )
-        printf( "Area-reducing implementation %sfound.\n", RetValue < 0 ? "NOT " : "" );
-    if ( RetValue >= 0 )
-    {
-        assert( nSupp[iBest] <= p->pPars->nVarMax );
-        p->nLuckySizes[nSupp[iBest]]++;
-    }
-    if ( RetValue >= 0 )
-    {
-        assert( RetValue <= 2 );
-        p->nLuckyGates[RetValue]++;
-    }
-    return RetValue;
+        printf( "Best %d: %d  ", iBest, nSupp[iBest] );
+    if ( fVeryVerbose )
+      Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );
+    // implement
+    assert( iLibObjBest >= 0 );
+    RetValue = Sfm_LibImplementGatesArea( p->pLib, pSupp[iBest], nSupp[iBest], iLibObjBest, &p->vObjGates, &p->vObjFanins );
+    assert( nSupp[iBest] <= p->pPars->nVarMax );
+    p->nLuckySizes[nSupp[iBest]]++;
+    assert( RetValue <= 2 );
+    p->nLuckyGates[RetValue]++;
+    return 1;
 }
 int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
 {
@@ -1178,9 +1264,9 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
             Dau_DsdPrintFromTruth( uTruth[i], nSupp[i] );
         if ( nSupp[i] < 2 )
         {
-            RetValue = Sfm_LibImplement( p->pLib, uTruth[i], pSupp[i], nSupp[i], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost );
-            assert( nSupp[iBest] <= p->pPars->nVarMax );
-            p->nLuckySizes[nSupp[iBest]]++;
+            RetValue = Sfm_LibImplementSimple( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vObjGates, &p->vObjFanins );
+            assert( nSupp[i] <= p->pPars->nVarMax );
+            p->nLuckySizes[nSupp[i]]++;
             assert( RetValue <= 2 );
             p->nLuckyGates[RetValue]++;
             return RetValue;
@@ -1191,7 +1277,7 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
         //}
 
         // try the delay
-        nMatches = Sfm_LibFindMatches( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans );
+        nMatches = Sfm_LibFindDelayMatches( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans );
         DelayMin = DelayOrig = Sfm_TimReadObjDelay( p->pTim, Abc_ObjId(pObj) );
         for ( k = 0; k < nMatches; k++ )
         {
@@ -1225,7 +1311,7 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
         printf( "Best %d: %d  ", iBest, nSupp[iBest] );
 //    if ( fVeryVerbose )
 //        Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );
-    RetValue = Sfm_LibAddNewGates( p->pLib, pSupp[iBest], pGate1Best, pGate2Best, pFans1Best, pFans2Best, &p->vObjGates, &p->vObjFanins );
+    RetValue = Sfm_LibImplementGatesDelay( p->pLib, pSupp[iBest], pGate1Best, pGate2Best, pFans1Best, pFans2Best, &p->vObjGates, &p->vObjFanins );
     assert( nSupp[iBest] <= p->pPars->nVarMax );
     p->nLuckySizes[nSupp[iBest]]++;
     assert( RetValue <= 2 );
@@ -1249,10 +1335,10 @@ void Abc_NtkUpdateIncLevel_rec( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, LevelNew = Abc_ObjLevelNew(pObj);
-    if ( LevelNew == (int)pObj->Level )
+    if ( LevelNew == Abc_ObjLevel(pObj) && Abc_ObjIsNode(pObj) && Abc_ObjFaninNum(pObj) > 0 )
         return;
     pObj->Level = LevelNew;
-    if ( Abc_ObjIsNode(pObj) )
+    if ( !Abc_ObjIsCo(pObj) )
         Abc_ObjForEachFanout( pObj, pFanout, i )
             Abc_NtkUpdateIncLevel_rec( pFanout );
 }
@@ -1412,14 +1498,6 @@ void Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nLevelMin, int nMffcMax, int fVery
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_DecMffcArea( Abc_Ntk_t * pNtk, Vec_Int_t * vMffc )
-{
-    Abc_Obj_t * pObj; 
-    int i, nAreaMffc = 0;
-    Abc_NtkForEachObjVec( vMffc, pNtk, pObj, i )
-        nAreaMffc += (int)(MIO_NUM * Mio_GateReadArea((Mio_Gate_t *)pObj->pData));
-    return nAreaMffc;
-}
 int Sfm_DecExtract( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars, Abc_Obj_t * pPivot, Vec_Int_t * vRoots, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Int_t * vTfi, Vec_Int_t * vTfo, Vec_Int_t * vMffc, Vec_Int_t * vInMffc, Sfm_Tim_t * pTim )
 {
     int fVeryVerbose = 0;//pPars->fVeryVerbose;
@@ -1805,7 +1883,7 @@ p->timeTime += Abc_Clock() - clk;
             pObjNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk)-1 );
             assert( p->DelayMin == 0 || p->DelayMin == Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)) );
             // report
-            if ( pPars->fVerbose )
+            if ( pPars->fDelayVerbose )
                 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)), 
@@ -1868,6 +1946,8 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     // print stats and quit
     if ( pPars->fVerbose )
     Sfm_DecPrintStats( p );
+    if ( pPars->fLibVerbose )
+        Sfm_LibPrint( p->pLib );
     Sfm_DecStop( p );
 }
 
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index fb799582..dcc8d4fc 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -198,12 +198,14 @@ extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_In
 /*=== sfmCore.c ==========================================================*/
 /*=== sfmLib.c ==========================================================*/
 extern int          Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int iFanin, int * piFaninNew );
-extern Sfm_Lib_t *  Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose );
+extern Sfm_Lib_t *  Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose, int fLibVerbose );
 extern void         Sfm_LibPrint( Sfm_Lib_t * p );
 extern void         Sfm_LibStop( Sfm_Lib_t * p );
-extern int          Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans );
-extern int          Sfm_LibAddNewGates( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_Gate_t * pGateT, char * pFansB, char * pFansT, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
-extern int          Sfm_LibImplement( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost );
+extern int          Sfm_LibFindAreaMatch( Sfm_Lib_t * p, word * pTruth, int nFanins, int * piObj );
+extern int          Sfm_LibFindDelayMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans );
+extern int          Sfm_LibImplementSimple( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
+extern int          Sfm_LibImplementGatesArea( Sfm_Lib_t * p, int * pFanins, int nFanins, int iObj, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
+extern int          Sfm_LibImplementGatesDelay( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_Gate_t * pGateT, char * pFansB, char * pFansT, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
 extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c
index fce20001..8d41f2e3 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -225,20 +225,6 @@ Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay, int fVerbose )
 }
 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 ( i < 2 || 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 );
@@ -302,7 +288,7 @@ void Sfm_LibTruth8Two( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Sfm_LibCellProfile( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop, int nFanins, int * Perm, int * pProf )
+void Sfm_LibCellProfile( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop, int nFanins, int * Perm, int * pProf )
 {
     int i, DelayAdd = (int)(pCellTop ? pCellTop->Delays[InTop] : 0);
     for ( i = 0; i < nFanins; i++ )
@@ -436,10 +422,10 @@ void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word * pTruth, int * Perm, int nFanins, M
         pObj->pFansT[i+1] = (char)(i == InTop ? 16 : InvPerm[k++]);
     assert( k == nFanins );
 }
-Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
+Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose, int fLibVerbose )
 {
     abctime clk = Abc_Clock();
-    Sfm_Lib_t * p = Sfm_LibStart( nVars, fDelay, fVerbose );
+    Sfm_Lib_t * p = Sfm_LibStart( nVars, fDelay, fLibVerbose );
     Mio_Cell2_t * pCell1, * pCell2, * pLimit;
     int * pPerm[SFM_SUPP_MAX+1], * Perm1, * Perm2, Perm[SFM_SUPP_MAX];
     int nPerms[SFM_SUPP_MAX+1], i, f, n;
@@ -458,7 +444,7 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
             pCell1->Type = 1;
         else if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
             pCell1->Type = 2;
-        else if ( p->fVerbose )
+        else if ( fLibVerbose )
             printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );
     }
     // generate permutations
@@ -490,10 +476,10 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
     }
     // add double cells
     if ( fTwo )
-    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
+    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ ) // Bot
     if ( pCell1->Type > 0 )
-    for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ )
-    if ( pCell2->Type > 0 && pCell1->Type + pCell2->Type <= 2 )
+    for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ ) // Top
+    if ( pCell2->Type > 0 )//&& pCell1->Type + pCell2->Type <= 2 )
     if ( (int)pCell1->nFanins + (int)pCell2->nFanins <= nVars + 1 )
     for ( f = 0; f < (int)pCell2->nFanins; f++ )
     {
@@ -512,6 +498,8 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
         for ( n = 0; n < nPerms[nFanins]; n++ )
         {
             Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, pCell2, f );
+            if ( nFanins > 5 )
+                break;
             // update
             Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );
             Perm1 = Perm + pPerm[nFanins][n];
@@ -536,7 +524,7 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
 void Sfm_LibPrintGate( Mio_Cell2_t * pCell, char * pFanins, Mio_Cell2_t * pCell2, char * pFanins2 )
 {
     int k;
-    printf( " %s(", pCell->pName );
+    printf( " %-20s(", pCell->pName );
     for ( k = 0; k < (int)pCell->nFanins; k++ )
         if ( pFanins[k] == (char)16 )
             Sfm_LibPrintGate( pCell2, pFanins2, NULL, NULL );
@@ -549,7 +537,7 @@ void Sfm_LibPrintObj( Sfm_Lib_t * p, Sfm_Fun_t * pObj )
     Mio_Cell2_t * pCellB = p->pCells + (int)pObj->pFansB[0];
     Mio_Cell2_t * pCellT = p->pCells + (int)pObj->pFansT[0];
     int i, nFanins = pCellB->nFanins + (pCellT == p->pCells ? 0 : pCellT->nFanins - 1);
-    printf( "     Area = %6.2f  Fanins = %d  ", MIO_NUMINV*pObj->Area, nFanins );
+    printf( "F = %d  A =%6.2f  ", nFanins, MIO_NUMINV*pObj->Area );
     if ( pCellT == p->pCells )
         Sfm_LibPrintGate( pCellB, pObj->pFansB + 1, NULL, NULL );
     else
@@ -562,29 +550,25 @@ void Sfm_LibPrintObj( Sfm_Lib_t * p, Sfm_Fun_t * pObj )
         for ( i = 0; i < nFanins; i++ )
             printf( "%6.2f ", MIO_NUMINV*pProf[i] );
     }
-    printf( "\n" );
 }
 void Sfm_LibPrint( Sfm_Lib_t * p )
 {
-    word * pTruth; Sfm_Fun_t * pObj; int iFunc, nSupp, Count; 
-    Vec_MemForEachEntry( p->vTtMem, pTruth, iFunc )
+    Sfm_Fun_t * pObj; word * pTruth; int i, nFanins;   
+    Vec_MemForEachEntry( p->vTtMem, pTruth, i )
     {
-        if ( iFunc < 2 ) 
+        if ( i < 2 || Vec_IntEntry(&p->vHits, i) == 0 )
             continue;
-        nSupp = Abc_TtSupportSize(pTruth, p->nVars);
-        //if ( nSupp > 3 )
-        //    continue;        
-        //if ( iFunc % 10000 )
-        //    continue;
-        printf( "%d : Supp = %d   Count = %d   ", iFunc, nSupp, Vec_IntEntry(&p->vCounts, iFunc) );
-        Dau_DsdPrintFromTruth( pTruth, nSupp );
-        Count = 0;
-        Sfm_LibForEachSuper( p, pObj, iFunc )
+        nFanins = Abc_TtSupportSize(pTruth, p->nVars);
+        printf( "%8d : ", i );
+        printf( "Num =%5d  ", Vec_IntEntry(&p->vCounts, i) );
+        printf( "Hit =%4d  ", Vec_IntEntry(&p->vHits, i) );
+        Sfm_LibForEachSuper( p, pObj, i )
         {
             Sfm_LibPrintObj( p, pObj );
-            if ( Count++ == 5 )
-                break;
+            break;
         }
+        printf( "    " );
+        Dau_DsdPrintFromTruth( pTruth, nFanins );
     }
 }
 void Sfm_LibTest()
@@ -596,7 +580,7 @@ void Sfm_LibTest()
         printf( "There is no current library.\n" );
         return;
     }
-    p = Sfm_LibPrepare( 7, 1, 1, fVerbose );
+    p = Sfm_LibPrepare( 7, 1, 1, 1, fVerbose );
     if ( fVerbose )
         Sfm_LibPrint( p );
     Sfm_LibStop( p );
@@ -613,14 +597,28 @@ void Sfm_LibTest()
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans )
+int Sfm_LibFindAreaMatch( Sfm_Lib_t * p, word * pTruth, int nFanins, int * piObj )
+{
+    Sfm_Fun_t * pObj = NULL;
+    int iFunc = *Vec_MemHashLookup( p->vTtMem,  pTruth );
+    if ( iFunc == -1 )
+        return -1;
+    Sfm_LibForEachSuper( p, pObj, iFunc )
+        break;
+    *piObj = pObj - p->pObjs;
+    return pObj->Area;
+}
+int Sfm_LibFindDelayMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans )
 {
     Sfm_Fun_t * pObj;
     Mio_Cell2_t * pCellB, * pCellT;
     int iFunc;
-//    word pCopy[4];
-//    Abc_TtCopy( pCopy, pTruth, 2, 0 );
-//    Dau_DsdPrintFromTruth( pCopy, 7 );
+    if ( nFanins > 6 )
+    {
+        word pCopy[4];
+        Abc_TtCopy( pCopy, pTruth, 4, 0 );
+        Dau_DsdPrintFromTruth( pCopy, p->nVars );
+    }
     Vec_PtrClear( vGates );
     Vec_PtrClear( vFans );
     // look for gate
@@ -632,7 +630,11 @@ int Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins
     if ( iFunc == -1 )
     {
         // print functions not found in the library
-        //Dau_DsdPrintFromTruth( pTruth, nFanins );
+        if ( p->fVerbose || nFanins > 6 )
+        {
+            printf( "Not found in the precomputed library: " );
+            Dau_DsdPrintFromTruth( pTruth, nFanins );
+        }
         return 0;
     }
     Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
@@ -660,37 +662,11 @@ int Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_LibAddNewGates( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_Gate_t * pGateT, char * pFansB, char * pFansT, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
-{
-    Vec_Int_t * vLevel;
-    int i, nFanins;
-    // create bottom gate
-    Vec_IntPush( vGates, Mio_GateReadValue(pGateB) );
-    vLevel  = Vec_WecPushLevel( vFanins );
-    nFanins = Mio_GateReadPinNum( pGateB );
-    for ( i = 0; i < nFanins; i++ )
-        Vec_IntPush( vLevel, pFanins[(int)pFansB[i]] );
-    if ( pGateT == NULL )
-        return 1;
-    // create top gate
-    Vec_IntPush( vGates, Mio_GateReadValue(pGateT) );
-    vLevel  = Vec_WecPushLevel( vFanins );
-    nFanins = Mio_GateReadPinNum( pGateT );
-    for ( i = 0; i < nFanins; i++ )
-        if ( pFansT[i] == (char)16 )
-            Vec_IntPush( vLevel, Vec_WecSize(vFanins)-2 );
-        else
-            Vec_IntPush( vLevel, pFanins[(int)pFansT[i]] );
-    return 2;
-}
-int Sfm_LibImplement( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost )
+int Sfm_LibImplementSimple( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
 {
     Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
     Mio_Gate_t * pGate;
-    Mio_Cell2_t * pCellB, * pCellT;
     Vec_Int_t * vLevel;
-    Sfm_Fun_t * pObj, * pObjMin = NULL;
-    int i, iFunc;
     if ( Abc_TtIsConst0(pTruth, p->nWords) || Abc_TtIsConst1(pTruth, p->nWords) )
     {
         assert( nFanins == 0 );
@@ -708,16 +684,17 @@ int Sfm_LibImplement( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins,
         Vec_IntPush( vLevel, pFanins[0] );
         return 1;
     }
-    // look for gate
-    iFunc = *Vec_MemHashLookup( p->vTtMem, pTruth );
-    if ( iFunc == -1 )
-        return -1;
-    Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
-    Sfm_LibForEachSuper( p, pObj, iFunc )
-        if ( !pObjMin || pObjMin->Area > pObj->Area )
-            pObjMin = pObj;
-    if ( pObjMin == NULL || (fZeroCost ? pObjMin->Area > AreaMffc : pObjMin->Area >= AreaMffc) )
-        return -1;
+    assert( 0 );
+    return -1;
+}
+int Sfm_LibImplementGatesArea( Sfm_Lib_t * p, int * pFanins, int nFanins, int iObj, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
+{
+    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
+    Sfm_Fun_t * pObjMin = p->pObjs + iObj;
+    Mio_Cell2_t * pCellB, * pCellT;
+    Mio_Gate_t * pGate;
+    Vec_Int_t * vLevel;
+    int i;
     // get the gates
     pCellB = p->pCells + (int)pObjMin->pFansB[0];
     pCellT = p->pCells + (int)pObjMin->pFansT[0];
@@ -742,6 +719,29 @@ int Sfm_LibImplement( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins,
             Vec_IntPush( vLevel, pFanins[(int)pObjMin->pFansT[i+1]] );
     return 2;
 }
+int Sfm_LibImplementGatesDelay( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_Gate_t * pGateT, char * pFansB, char * pFansT, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
+{
+    Vec_Int_t * vLevel;
+    int i, nFanins;
+    // create bottom gate
+    Vec_IntPush( vGates, Mio_GateReadValue(pGateB) );
+    vLevel  = Vec_WecPushLevel( vFanins );
+    nFanins = Mio_GateReadPinNum( pGateB );
+    for ( i = 0; i < nFanins; i++ )
+        Vec_IntPush( vLevel, pFanins[(int)pFansB[i]] );
+    if ( pGateT == NULL )
+        return 1;
+    // create top gate
+    Vec_IntPush( vGates, Mio_GateReadValue(pGateT) );
+    vLevel  = Vec_WecPushLevel( vFanins );
+    nFanins = Mio_GateReadPinNum( pGateT );
+    for ( i = 0; i < nFanins; i++ )
+        if ( pFansT[i] == (char)16 )
+            Vec_IntPush( vLevel, Vec_WecSize(vFanins)-2 );
+        else
+            Vec_IntPush( vLevel, pFanins[(int)pFansT[i]] );
+    return 2;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///