Extending library handling to 8 inputs.

4 files changed, 116 insertions, 71 deletions

diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c
index ea0779ff..6310cb1a 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -117,8 +117,8 @@ struct Sfm_Dec_t_
     int               nMaxWin;
     word              nAllDivs;
     word              nAllWin;
-    int               nLuckySizes[10];
-    int               nLuckyGates[10];
+    int               nLuckySizes[SFM_SUPP_MAX+1];
+    int               nLuckyGates[SFM_SUPP_MAX+1];
 };
 
 #define SFM_MASK_PI     1  // supp(node) is contained in supp(TFI(pivot))
@@ -274,6 +274,7 @@ static inline word Sfm_ObjSimulate( Abc_Obj_t * pObj )
     Sfm_Dec_t * p = Sfm_DecMan( pObj );
     Vec_Int_t * vExpr = Mio_GateReadExpr( (Mio_Gate_t *)pObj->pData );
     Abc_Obj_t * pFanin; int i; word uFanins[6];
+    assert( Abc_ObjFaninNum(pObj) <= 6 );
     Abc_ObjForEachFanin( pObj, pFanin, i )
         uFanins[i] = Sfm_DecObjSim( p, pFanin );
     return Exp_Truth6( Abc_ObjFaninNum(pObj), vExpr, uFanins );
@@ -778,13 +779,14 @@ int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSup
     {
         memcpy( pSupp,  pSupp0,  sizeof(int)*nSupp0   );
         memcpy( pTruth, pTruth0, sizeof(word)*nWords0 );
+        Abc_TtStretch6( pTruth, nSupp0, p->pPars->nVarMax );
         return nSupp0;
     }
     // merge support variables
     Vec_IntTwoMerge2Int( &vVec0, &vVec1, &vVec );
     Vec_IntPushOrder( &vVec, Var );
     nSupp = Vec_IntSize( &vVec );
-    if ( nSupp > SFM_SUPP_MAX )
+    if ( nSupp > p->pPars->nVarMax )
         return -2;
     // expand truth tables
     Abc_TtStretch6( pTruth0, nSupp0, nSupp );
@@ -794,6 +796,7 @@ int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSup
     // perform operation
     iSuppVar = Vec_IntFind( &vVec, Var );
     Abc_TtMux( pTruth, p->pTtElems[iSuppVar], pTruth1, pTruth0, Abc_TtWordNum(nSupp) );
+    Abc_TtStretch6( pTruth, nSupp, p->pPars->nVarMax );
     return nSupp;
 }
 int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssump, int nAssump, word Masks[2], int fCofactor, int nSuppAdd )
@@ -835,7 +838,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
         {
             p->nSatCallsUnsat++;
             p->timeSatUnsat += Abc_Clock() - clk;
-            pTruth[0] = c ? ~((word)0) : 0;
+            Abc_TtConst( pTruth, Abc_TtWordNum(p->pPars->nVarMax), c );
             if ( p->pPars->fVeryVerbose )
                 printf( "Found constant %d.\n", c );
             return 0;
@@ -907,13 +910,13 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
         }
         assert( Abc_Lit2Var(Impls[0]) == Abc_Lit2Var(Impls[1]) );
         // found buffer/inverter
-        pTruth[0] = Abc_LitIsCompl(Impls[0]) ? ~p->pTtElems[0][0] : p->pTtElems[0][0];
+        Abc_TtUnit( pTruth, Abc_TtWordNum(p->pPars->nVarMax), Abc_LitIsCompl(Impls[0]) );
         pSupp[0] = Abc_Lit2Var(Impls[0]);
         if ( p->pPars->fVeryVerbose )
             printf( "Found variable %s%d.\n", Abc_LitIsCompl(Impls[0]) ? "!":"", pSupp[0] );
         return 1;        
     }
-    if ( nSuppAdd > 4 )
+    if ( nSuppAdd > p->pPars->nVarMax - 2 )
     {
         if ( p->pPars->fVeryVerbose )
             printf( "The number of assumption is more than MFFC size.\n" );
@@ -969,6 +972,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
                     pSupp[i] = Abc_Lit2Var(pSupp[i]);
                 }
             }
+            Abc_TtStretch6( pTruth, nFinal, p->pPars->nVarMax );
             p->nNodesAndOr++;
             if ( p->pPars->fVeryVerbose )
                 printf( "Found %d-input AND/OR gate.\n", nFinal );
@@ -1028,7 +1032,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
     if ( Var >= 0 )
     {
         word uTruth[2][SFM_WORD_MAX], MasksNext[2];
-        int Supp[2][2*SFM_SUPP_MAX], nSupp[2] = {0}, nSuppAll;
+        int Supp[2][2*SFM_SUPP_MAX], nSupp[2] = {0};
         Vec_IntPush( &p->vObjDec, Var );
         for ( i = 0; i < 2; i++ )
         {
@@ -1043,10 +1047,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
                 return -2;
         }
         // combine solutions
-        nSuppAll = Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var );
-        if ( nSuppAll > 6 )
-            return -2;
-        return nSuppAll;
+        return Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var );
     }
     return -2;
 }
@@ -1114,13 +1115,19 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )
 //            Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );
     }
 //    return -1;
-    RetValue = Sfm_LibImplement( p->pLib, uTruth[iBest][0], pSupp[iBest], nSupp[iBest], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost );
+    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;
 }
 int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
@@ -1171,8 +1178,10 @@ 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][0], pSupp[i], nSupp[i], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost );
-            p->nLuckySizes[nSupp[i]]++;
+            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]]++;
+            assert( RetValue <= 2 );
             p->nLuckyGates[RetValue]++;
             return RetValue;
         }
@@ -1182,7 +1191,7 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
         //}
 
         // try the delay
-        nMatches = Sfm_LibFindMatches( p->pLib, uTruth[i][0], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans );
+        nMatches = Sfm_LibFindMatches( 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++ )
         {
@@ -1217,7 +1226,9 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
 //    if ( fVeryVerbose )
 //        Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );
     RetValue = Sfm_LibAddNewGates( 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 );
     p->nLuckyGates[RetValue]++;
     p->DelayMin = DelayMin;
     return 1;
@@ -1629,13 +1640,13 @@ void Sfm_DecPrintStats( Sfm_Dec_t * p )
     ABC_PRTP( "ALL   ", p->timeTotal,     p->timeTotal );
 
     printf( "Cone sizes:  " );
-    for ( i = 0; i < 10; i++ )
+    for ( i = 0; i <= SFM_SUPP_MAX; i++ )
         if ( p->nLuckySizes[i] )
             printf( "%d=%d  ", i, p->nLuckySizes[i] );
     printf( "  " );
 
     printf( "Gate sizes:  " );
-    for ( i = 0; i < 10; i++ )
+    for ( i = 0; i <= SFM_SUPP_MAX; i++ )
         if ( p->nLuckyGates[i] )
             printf( "%d=%d  ", i, p->nLuckyGates[i] );
     printf( "\n" );
@@ -1792,7 +1803,7 @@ clk = Abc_Clock();
             Sfm_TimUpdateTiming( p->pTim, &p->vTemp );
 p->timeTime += Abc_Clock() - clk;
             pObjNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk)-1 );
-            assert( p->DelayMin == Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)) );
+            assert( p->DelayMin == 0 || 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", 
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index e5f73e38..fb799582 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -50,7 +50,7 @@ ABC_NAMESPACE_HEADER_START
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
-#define SFM_SUPP_MAX  6
+#define SFM_SUPP_MAX  8
 #define SFM_WORD_MAX ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)
 #define SFM_WIN_MAX   1000
 #define SFM_DEC_MAX   4
@@ -201,9 +201,9 @@ extern int          Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, in
 extern Sfm_Lib_t *  Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose );
 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 uTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans );
+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 uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost );
+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 );
 /*=== 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 00fc92e0..eb3c74c8 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -39,12 +39,13 @@ struct Sfm_Fun_t_
 {
     int             Next;          // next function in the list
     int             Area;          // area of this function
-    char            pFansT[8];     // top gate ID, followed by fanin perm
-    char            pFansB[8];     // bottom gate ID, followed by fanin perm
+    char            pFansT[SFM_SUPP_MAX+1];     // top gate ID, followed by fanin perm
+    char            pFansB[SFM_SUPP_MAX+1];     // bottom gate ID, followed by fanin perm
 };
 struct Sfm_Lib_t_
 {
     int             nVars;         // variable count
+    int             nWords;        // truth table words
     int             fVerbose;      // verbose statistics
     Mio_Cell2_t *   pCells;        // library gates
     int             nCells;        // library gate count
@@ -172,6 +173,7 @@ int Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int i
             if ( uTruth == uTruthSwap )
                 return i;
     }
+    // add checking for complemeting control input of a MUX
     if ( piFaninNew ) *piFaninNew = -1;
     return -1;
 }
@@ -191,6 +193,7 @@ int Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int i
 Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay, int fVerbose )
 {
     Sfm_Lib_t * p = ABC_CALLOC( Sfm_Lib_t, 1 );
+    assert( nVars <= SFM_SUPP_MAX );
     p->vTtMem = Vec_MemAllocForTT( nVars, 0 );   
     Vec_IntGrow( &p->vLists,  (1 << 16) );
     Vec_IntGrow( &p->vCounts, (1 << 16) );
@@ -205,6 +208,7 @@ Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay, int fVerbose )
     if ( fDelay ) Vec_IntGrow( &p->vStore,  (1 << 18) );
     Vec_IntGrow( &p->vTemp, 16 );
     p->nVars = nVars;
+    p->nWords = Abc_TtWordNum( nVars );
     p->fVerbose = fVerbose;
     return p;
 }
@@ -216,7 +220,7 @@ void Sfm_LibStop( Sfm_Lib_t * p )
         int i, nFanins;  word * pTruth;
         Vec_MemForEachEntry( p->vTtMem, pTruth, i )
         {
-            if ( Vec_IntEntry(&p->vHits, i) == 0 )
+            if ( i < 2 || Vec_IntEntry(&p->vHits, i) == 0 )
                 continue;
             nFanins = Abc_TtSupportSize(pTruth, p->nVars);
             printf( "%8d : ", i );
@@ -248,10 +252,10 @@ void Sfm_LibStop( Sfm_Lib_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-word Sfm_LibTruthTwo( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
+word Sfm_LibTruth6Two( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
 {
+    word uFanins[SFM_SUPP_MAX]; int i, k;
     word uTruthBot = Exp_Truth6( pCellBot->nFanins, pCellBot->vExpr, NULL );
-    word uFanins[6]; int i, k;
     assert( InTop >= 0 && InTop < (int)pCellTop->nFanins );
     for ( i = 0, k = pCellBot->nFanins; i < (int)pCellTop->nFanins; i++ )
         if ( i == InTop )
@@ -262,6 +266,19 @@ word Sfm_LibTruthTwo( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop
     uTruthBot = Exp_Truth6( pCellTop->nFanins, pCellTop->vExpr, uFanins );
     return uTruthBot;
 }
+void Sfm_LibTruth8Two( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop, word * pRes )
+{
+    word uTruthBot[4], * puFanins[SFM_SUPP_MAX]; int i, k;
+    Exp_Truth8( pCellBot->nFanins, pCellBot->vExpr, NULL, uTruthBot );
+    assert( InTop >= 0 && InTop < (int)pCellTop->nFanins );
+    for ( i = 0, k = pCellBot->nFanins; i < (int)pCellTop->nFanins; i++ )
+        if ( i == InTop )
+            puFanins[i] = uTruthBot;
+        else
+            puFanins[i] = s_Truth8[k++];
+    assert( (int)pCellBot->nFanins + (int)pCellTop->nFanins == k + 1 );
+    Exp_Truth8( pCellTop->nFanins, pCellTop->vExpr, puFanins, pRes );
+}
 
 /**Function*************************************************************
 
@@ -305,12 +322,12 @@ static inline int Sfm_LibNewContains( Sfm_Fun_t * pObj, int * pProf, int Area, i
             return 0;
     return 1;
 }
-void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word uTruth, int * Perm, int nFanins, Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
+void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word * pTruth, int * Perm, int nFanins, Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
 {
     Sfm_Fun_t * pObj;
-    int InvPerm[6], Profile[6];
+    int InvPerm[SFM_SUPP_MAX], Profile[SFM_SUPP_MAX];
     int Area = (int)pCellBot->Area + (pCellTop ? (int)pCellTop->Area : 0);
-    int i, k, Id, Prev, Offset, * pProf, iFunc = Vec_MemHashInsert( p->vTtMem, &uTruth );
+    int i, k, Id, Prev, Offset, * pProf, iFunc = Vec_MemHashInsert( p->vTtMem, pTruth );
     if ( iFunc == Vec_IntSize(&p->vLists) )
     {
         Vec_IntPush( &p->vLists, -1 );
@@ -413,23 +430,23 @@ 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, fVerbose );
     Mio_Cell2_t * pCell1, * pCell2, * pLimit;
-    int * pPerm[7], * Perm1, * Perm2, Perm[6];
-    int nPerms[7], i, f, n;
-    Vec_Int_t * vUseful;
-    word tTemp1, tCur;
+    int * pPerm[SFM_SUPP_MAX+1], * Perm1, * Perm2, Perm[SFM_SUPP_MAX];
+    int nPerms[SFM_SUPP_MAX+1], i, f, n;
+    word tTemp1[4], tCur[4];
     char pRes[1000];
-    assert( nVars <= 6 );
+    assert( nVars <= SFM_SUPP_MAX );
     // precompute gates
-    p->pCells = Mio_CollectRootsNewDefault2( nVars, &p->nCells, 0 );
+    p->pCells = Mio_CollectRootsNewDefault2( Abc_MinInt(6, nVars), &p->nCells, 0 );
     pLimit = p->pCells + p->nCells;
     // find useful ones
-    vUseful = Vec_IntStart( p->nCells );
-//    vUseful = Vec_IntStartFull( p->nCells );
     for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
     {
         word uTruth = pCell1->uTruth;
-        if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
-            Vec_IntWriteEntry( vUseful, pCell1 - p->pCells, 1 );
+        pCell1->Type = 0;
+        if ( Abc_Tt6IsAndType(uTruth, pCell1->nFanins) || Abc_Tt6IsOrType(uTruth, pCell1->nFanins) )
+            pCell1->Type = 1;
+        else if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
+            pCell1->Type = 2;
         else if ( p->fVerbose )
             printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );
     }
@@ -439,32 +456,33 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
     for ( i = 2; i <= nVars; i++ )
         nPerms[i] = Extra_Factorial( i );
     // add single cells
-    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
-    if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) )
+    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ ) 
     {
         int nFanins = pCell1->nFanins;
-        assert( nFanins >= 2 && nFanins <= 6 );
+        assert( nFanins >= 2 && nFanins <= nVars );
         for ( i = 0; i < nFanins; i++ )
             Perm[i] = i;
         // permute truth table
-        tCur = tTemp1 = pCell1->uTruth;
+        tCur[0] = tTemp1[0] = pCell1->uTruth;
+        if ( p->nVars > 6 )
+            tTemp1[1] = tTemp1[2] = tTemp1[3] = tCur[1] = tCur[2] = tCur[3] = tCur[0];
         for ( n = 0; n < nPerms[nFanins]; n++ )
         {
             Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, NULL, -1 );
             // update
-            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] );
+            Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );
             Perm1 = Perm + pPerm[nFanins][n];
             Perm2 = Perm1 + 1;
             ABC_SWAP( int, *Perm1, *Perm2 );
         }
-        assert( tTemp1 == tCur );
+        assert( Abc_TtEqual(tTemp1, tCur, p->nWords) );
     }
     // add double cells
     if ( fTwo )
     for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
-    if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) )
+    if ( pCell1->Type > 0 )
     for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ )
-    if ( Vec_IntEntry(vUseful, pCell2 - p->pCells) )
+    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++ )
     {
@@ -473,22 +491,27 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )
         for ( i = 0; i < nFanins; i++ )
             Perm[i] = i;
         // permute truth table
-        tCur = tTemp1 = Sfm_LibTruthTwo( pCell1, pCell2, f );
+        if ( p->nVars > 6 )
+        {
+            Sfm_LibTruth8Two( pCell1, pCell2, f, tCur );
+            Abc_TtCopy( tTemp1, tCur, p->nWords, 0 );
+        }
+        else
+            tCur[0] = tTemp1[0] = Sfm_LibTruth6Two( pCell1, pCell2, f );
         for ( n = 0; n < nPerms[nFanins]; n++ )
         {
             Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, pCell2, f );
             // update
-            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] );
+            Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );
             Perm1 = Perm + pPerm[nFanins][n];
             Perm2 = Perm1 + 1;
             ABC_SWAP( int, *Perm1, *Perm2 );
         }
-        assert( tTemp1 == tCur );
+        assert( Abc_TtEqual(tTemp1, tCur, p->nWords) );
     }
     // cleanup
     for ( i = 2; i <= nVars; i++ )
         ABC_FREE( pPerm[i] );
-    Vec_IntFree( vUseful );
     if ( fVerbose )
     {
         printf( "Library processing: Var = %d. Cell = %d.  Fun = %d. Obj = %d. Ave = %.2f.  Skip = %d. Rem = %d.  ", 
@@ -532,20 +555,25 @@ void Sfm_LibPrintObj( Sfm_Lib_t * p, Sfm_Fun_t * pObj )
 }
 void Sfm_LibPrint( Sfm_Lib_t * p )
 {
-    word * pTruth; Sfm_Fun_t * pObj; int iFunc, nSupp; 
+    word * pTruth; Sfm_Fun_t * pObj; int iFunc, nSupp, Count; 
     Vec_MemForEachEntry( p->vTtMem, pTruth, iFunc )
     {
         if ( iFunc < 2 ) 
             continue;
-        nSupp = Abc_TtSupportSize(pTruth, 6);
-        if ( nSupp > 3 )
-            continue;        
+        nSupp = Abc_TtSupportSize(pTruth, p->nVars);
+        //if ( nSupp > 3 )
+        //    continue;        
         //if ( iFunc % 10000 )
         //    continue;
-        printf( "%d : Count = %d   ", iFunc, Vec_IntEntry(&p->vCounts, iFunc) );
+        printf( "%d : Supp = %d   Count = %d   ", iFunc, nSupp, Vec_IntEntry(&p->vCounts, iFunc) );
         Dau_DsdPrintFromTruth( pTruth, nSupp );
+        Count = 0;
         Sfm_LibForEachSuper( p, pObj, iFunc )
+        {
             Sfm_LibPrintObj( p, pObj );
+            if ( Count++ == 5 )
+                break;
+        }
     }
 }
 void Sfm_LibTest()
@@ -557,9 +585,9 @@ void Sfm_LibTest()
         printf( "There is no current library.\n" );
         return;
     }
-    p = Sfm_LibPrepare( 6, 1, 1, fVerbose );
-    //if ( fVerbose )
-    //    Sfm_LibPrint( p );
+    p = Sfm_LibPrepare( 7, 1, 1, fVerbose );
+    if ( fVerbose )
+        Sfm_LibPrint( p );
     Sfm_LibStop( p );
 }
 
@@ -574,20 +602,26 @@ void Sfm_LibTest()
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_LibFindMatches( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans )
+int Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans )
 {
-    Mio_Cell2_t * pCellB, * pCellT;
     Sfm_Fun_t * pObj;
+    Mio_Cell2_t * pCellB, * pCellT;
     int iFunc;
+//    word pCopy[4];
+//    Abc_TtCopy( pCopy, pTruth, 2, 0 );
+//    Dau_DsdPrintFromTruth( pCopy, 7 );
     Vec_PtrClear( vGates );
     Vec_PtrClear( vFans );
     // look for gate
-    assert( uTruth != 0 && uTruth != ~(word)0 && uTruth != s_Truths6[0] && uTruth != ~s_Truths6[0] );
-    iFunc = *Vec_MemHashLookup( p->vTtMem,  &uTruth );
+    assert( !Abc_TtIsConst0(pTruth, p->nWords) && 
+            !Abc_TtIsConst1(pTruth, p->nWords) && 
+            !Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) && 
+            !Abc_TtOpposite(pTruth, s_Truth8[0], p->nWords) );
+    iFunc = *Vec_MemHashLookup( p->vTtMem,  pTruth );
     if ( iFunc == -1 )
     {
         // print functions not found in the library
-        //Dau_DsdPrintFromTruth( &uTruth, nFanins );
+        //Dau_DsdPrintFromTruth( pTruth, nFanins );
         return 0;
     }
     Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
@@ -638,7 +672,7 @@ int Sfm_LibAddNewGates( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_G
             Vec_IntPush( vLevel, pFanins[(int)pFansT[i]] );
     return 2;
 }
-int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost )
+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 )
 {
     Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
     Mio_Gate_t * pGate;
@@ -646,25 +680,25 @@ int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, in
     Vec_Int_t * vLevel;
     Sfm_Fun_t * pObj, * pObjMin = NULL;
     int i, iFunc;
-    if ( uTruth == 0 || uTruth == ~(word)0 )
+    if ( Abc_TtIsConst0(pTruth, p->nWords) || Abc_TtIsConst1(pTruth, p->nWords) )
     {
         assert( nFanins == 0 );
-        pGate = uTruth ? Mio_LibraryReadConst1(pLib) : Mio_LibraryReadConst0(pLib);
+        pGate = Abc_TtIsConst1(pTruth, p->nWords) ? Mio_LibraryReadConst1(pLib) : Mio_LibraryReadConst0(pLib);
         Vec_IntPush( vGates, Mio_GateReadValue(pGate) );
         vLevel = Vec_WecPushLevel( vFanins );
         return 1;
     }
-    if ( uTruth == s_Truths6[0] || uTruth == ~s_Truths6[0] )
+    if ( Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) || Abc_TtOpposite(pTruth, s_Truth8[0], p->nWords) )
     {
         assert( nFanins == 1 );
-        pGate = uTruth == s_Truths6[0] ? Mio_LibraryReadBuf(pLib) : Mio_LibraryReadInv(pLib);
+        pGate = Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) ? Mio_LibraryReadBuf(pLib) : Mio_LibraryReadInv(pLib);
         Vec_IntPush( vGates, Mio_GateReadValue(pGate) );
         vLevel = Vec_WecPushLevel( vFanins );
         Vec_IntPush( vLevel, pFanins[0] );
         return 1;
     }
     // look for gate
-    iFunc = *Vec_MemHashLookup( p->vTtMem,  &uTruth );
+    iFunc = *Vec_MemHashLookup( p->vTtMem, pTruth );
     if ( iFunc == -1 )
         return -1;
     Vec_IntAddToEntry( &p->vHits, iFunc, 1 );
diff --git a/src/opt/sfm/sfmTime.c b/src/opt/sfm/sfmTime.c
index 939bcd85..8334d291 100644
--- a/src/opt/sfm/sfmTime.c
+++ b/src/opt/sfm/sfmTime.c
@@ -253,7 +253,7 @@ 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 );
-    assert( DeltaCrit > 0 && DeltaCrit < 10000 );
+    assert( DeltaCrit > 0 && DeltaCrit < MIO_NUM*1000 );
     p->DeltaCrit = DeltaCrit;
     return p;
 }