Allowing nodes and boxes to have more than 6 inputs in mfs2 and &mfs.

11 files changed, 270 insertions, 57 deletions

diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
index 2d9d09e8..69f6ee7a 100644
--- a/src/aig/gia/giaMfs.c
+++ b/src/aig/gia/giaMfs.c
@@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
 {
-    word uTruth, uTruths6[6] = {
+    word uTruth, * pTruth, uTruths6[6] = {
         ABC_CONST(0xAAAAAAAAAAAAAAAA),
         ABC_CONST(0xCCCCCCCCCCCCCCCC),
         ABC_CONST(0xF0F0F0F0F0F0F0F0),
@@ -60,6 +60,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     Vec_Str_t * vEmpty;  // mfs data
     Vec_Wrd_t * vTruths; // mfs data
     Vec_Int_t * vArray;
+    Vec_Int_t * vStarts;
+    Vec_Wrd_t * vTruths2;
     Vec_Int_t * vLeaves;
     Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
     int nBoxes   = Gia_ManBoxNum(p), nVars;
@@ -67,6 +69,9 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
     int i, j, k, curCi, curCo, nBoxIns, nBoxOuts;
     int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0;
+    int nLutSizeMax = Gia_ManLutSizeMax( p );
+    nLutSizeMax = Abc_MaxInt( nLutSizeMax, 6 );
+    assert( nLutSizeMax < 16 );
     //assert( !p->pAigExtra || Gia_ManPiNum(p->pAigExtra) <= 6 );
     if ( pManTime ) Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts );
     // skip PIs due to box outputs
@@ -77,6 +82,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     vFixed   = Vec_StrStart( nMfsVars );
     vEmpty   = Vec_StrStart( nMfsVars );
     vTruths  = Vec_WrdStart( nMfsVars );
+    vStarts  = Vec_IntStart( nMfsVars );
+    vTruths2 = Vec_WrdAlloc( 10000 );
     // set internal PIs
     Gia_ManCleanCopyArray( p );
     Gia_ManForEachCiId( p, Id, i )
@@ -86,8 +93,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     Vec_WrdWriteEntry( vTruths, Counter, (word)0 );
     Gia_ObjSetCopyArray( p, 0, Counter++ );
     // set internal LUTs
-    vLeaves = Vec_IntAlloc( 6 );
-    Gia_ObjComputeTruthTableStart( p, 6 );
+    vLeaves = Vec_IntAlloc( nLutSizeMax );
+    Gia_ObjComputeTruthTableStart( p, nLutSizeMax );
     Gia_ManForEachLut( p, Id )
     {
         Vec_IntClear( vLeaves );
@@ -99,12 +106,22 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
             Vec_IntPush( vArray, Gia_ObjCopyArray(p, iFan) );
             Vec_IntPush( vLeaves, iFan );
         }
-        assert( Vec_IntSize(vLeaves) <= 6 );
+        assert( Vec_IntSize(vLeaves) < 16 );
         assert( Vec_IntSize(vLeaves) == Gia_ObjLutSize(p, Id) );
-        uTruth = *Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves );
-        nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) );
+//        uTruth = *Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves );
+//        nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) );
+        pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves );
+        nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) );
         Vec_IntShrink( vArray, nVars );
-        Vec_WrdWriteEntry( vTruths, Counter, uTruth );
+        if ( nVars <= 6 )
+            Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
+        else
+        {
+            int w, nWords = Abc_Truth6WordNum( nVars );
+            Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
+            for ( w = 0; w < nWords; w++ )
+                Vec_WrdPush( vTruths2, pTruth[w] );
+        }
         if ( Gia_ObjLutIsMux(p, Id) )
         {
             Vec_StrWriteEntry( vFixed, Counter, (char)1 );
@@ -136,7 +153,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     if ( p->pAigExtra )
     {
         int iBbIn = 0, iBbOut = 0;
-        Gia_ObjComputeTruthTableStart( p->pAigExtra, 6 );
+        assert( Gia_ManCiNum(p->pAigExtra) < 16 );
+        Gia_ObjComputeTruthTableStart( p->pAigExtra, Gia_ManCiNum(p->pAigExtra) );
         curCi = nRealPis;
         curCo = 0;
         for ( k = 0; k < nBoxes; k++ )
@@ -148,7 +166,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
             for ( i = 0; i < nBoxIns; i++ )
                 Vec_IntPush( vLeaves, Gia_ObjId(p->pAigExtra, Gia_ManCi(p->pAigExtra, i)) );
             // iterate through box outputs
-            if ( !Tim_ManBoxIsBlack(pManTime, k) && Tim_ManBoxInputNum(pManTime, k) <= 6 )
+            if ( !Tim_ManBoxIsBlack(pManTime, k) ) //&& Tim_ManBoxInputNum(pManTime, k) <= 6 )
             {
                 for ( j = 0; j < nBoxOuts; j++ )
                 {
@@ -168,17 +186,39 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
                     // box output in the extra manager
                     pObjExtra = Gia_ManCo( p->pAigExtra, curCi - nRealPis + j );
                     // compute truth table
+                    pTruth = NULL;
                     if ( Gia_ObjFaninId0p(p->pAigExtra, pObjExtra) == 0 )
+                    {
                         uTruth = 0;
+                        uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth;
+                        pTruth = &uTruth;
+                    }
                     else if ( Gia_ObjIsCi(Gia_ObjFanin0(pObjExtra)) )
+                    {
                         uTruth = uTruths6[Gia_ObjCioId(Gia_ObjFanin0(pObjExtra))];
+                        uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth;
+                        pTruth = &uTruth;
+                    }
                     else
-                        uTruth = *Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves );
-                    uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth;
+                    {
+                        pTruth = Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves );
+                        if ( Gia_ObjFaninC0(pObjExtra) )
+                            Abc_TtNot( pTruth, Abc_Truth6WordNum(Vec_IntSize(vLeaves)) );
+                    }
+                    //uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth;
                     //Dau_DsdPrintFromTruth( &uTruth, Vec_IntSize(vArray) );
-                    nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) );
+                    //nVars = Abc_Tt6MinBase( &uTruth, Vec_IntArray(vArray), Vec_IntSize(vArray) );
+                    nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) );
                     Vec_IntShrink( vArray, nVars );
-                    Vec_WrdWriteEntry( vTruths, Counter, uTruth );
+                    if ( nVars <= 6 )
+                        Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
+                    else
+                    {
+                        int w, nWords = Abc_Truth6WordNum( nVars );
+                        Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
+                        for ( w = 0; w < nWords; w++ )
+                            Vec_WrdPush( vTruths2, pTruth[w] );
+                    }
                 }
             }
             else // create buffers for black box inputs and outputs
@@ -230,7 +270,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     }
     // finalize 
     Vec_IntFree( vLeaves );
-    return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths );
+    return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths, vStarts, vTruths2 );
 }
 
 /**Function*************************************************************
@@ -464,11 +504,16 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars )
         Abc_Print( 1, "Timing manager is given but there is no GIA of boxes.\n" );
         return NULL;
     }
+    if ( p->pManTime != NULL && p->pAigExtra != NULL && Gia_ManCiNum(p->pAigExtra) > 15 )
+    {
+        Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing white-boxes with more than 15 inputs.\n" );
+        return NULL;
+    }
     // count fanouts
     nFaninMax = Gia_ManLutSizeMax( p );
-    if ( nFaninMax > 6 )
+    if ( nFaninMax > 15 )
     {
-        Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+        Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing nodes with more than 15 fanins.\n" );
         return NULL;
     }
     // collect information
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index b0ce2ab7..b91214af 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -457,12 +457,21 @@ char * Abc_SopCreateFromIsop( Mem_Flex_t * pMan, int nVars, Vec_Int_t * vCover )
 char * Abc_SopCreateFromTruthIsop( Mem_Flex_t * pMan, int nVars, word * pTruth, Vec_Int_t * vCover )
 {
     char * pSop = NULL;
-    assert( nVars <= 6 );
-    if ( pTruth[0] == 0 )
-        pSop = Abc_SopRegister( pMan, " 0\n" );
-    else if ( ~pTruth[0] == 0 )
-        pSop = Abc_SopRegister( pMan, " 1\n" );
-    else
+    int w, nWords  = Abc_Truth6WordNum( nVars );
+    assert( nVars < 16 );
+
+    for ( w = 0; w < nWords; w++ )
+        if ( pTruth[w] )
+            break;
+    if ( w == nWords )
+        return Abc_SopRegister( pMan, " 0\n" );
+
+    for ( w = 0; w < nWords; w++ )
+        if ( ~pTruth[w] )
+            break;
+    if ( w == nWords )
+        return Abc_SopRegister( pMan, " 1\n" );
+
     {
         int RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 1 );
         assert( nVars > 0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3dba557c..5df604cc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -44822,9 +44822,9 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has no mapping.\n" );
         return 0;
     }
-    if ( Gia_ManLutSizeMax(pAbc->pGia) > 6 )
+    if ( Gia_ManLutSizeMax(pAbc->pGia) > 15 )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current mapping has nodes with more than 6 inputs. Cannot use \"mfs\".\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current mapping has nodes with more than 15 inputs. Cannot use \"mfs\".\n" );
         return 0;
     }
 /*
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index 5c566074..d91bda66 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -82,6 +82,55 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Assign truth table sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkAssignStarts( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int * pnTotal )
+{
+    Abc_Obj_t * pObj; int i, Counter = 0;
+    Vec_Int_t * vStarts = Vec_IntStart( Abc_NtkObjNum(pNtk) );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter );
+        Counter += Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) );
+    }
+    *pnTotal = Counter;
+    return vStarts;
+}
+
+void Abc_NtkFillTruthStore( word TruthStore[16][1<<10] )
+{
+    if ( TruthStore[0][0] == 0 )
+    {
+        static word Truth6[6] = {
+            0xAAAAAAAAAAAAAAAA,
+            0xCCCCCCCCCCCCCCCC,
+            0xF0F0F0F0F0F0F0F0,
+            0xFF00FF00FF00FF00,
+            0xFFFF0000FFFF0000,
+            0xFFFFFFFF00000000
+        };
+        int nVarsMax = 16;
+        int nWordsMax = (1 << 10);
+        int i, k;
+        assert( nVarsMax <= 16 );
+        for ( i = 0; i < 6; i++ )
+            for ( k = 0; k < nWordsMax; k++ )
+                TruthStore[i][k] = Truth6[i];
+        for ( i = 6; i < nVarsMax; i++ )
+            for ( k = 0; k < nWordsMax; k++ )
+                TruthStore[i][k] = ((k >> (i-6)) & 1) ? ~(word)0 : 0;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Extracts information about the network.]
 
   Description []
@@ -93,28 +142,59 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
 {
+    word TruthStore[16][1<<10] = {{0}}, * pTruths[16] = {NULL}, pCube[1<<10] = {0};
     Vec_Ptr_t * vNodes;
     Vec_Wec_t * vFanins;
     Vec_Str_t * vFixed;
     Vec_Wrd_t * vTruths;
     Vec_Int_t * vArray;
+    Vec_Int_t * vStarts;
+    Vec_Wrd_t * vTruths2;
     Abc_Obj_t * pObj, * pFanin;
-    int i, k, nObjs;
+    int i, k, nObjs, nTotal = 0;
     vNodes  = nFirstFixed ? Abc_NtkAssignIDs2(pNtk) : Abc_NtkAssignIDs(pNtk);
     nObjs   = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + Abc_NtkCoNum(pNtk);
     vFanins = Vec_WecStart( nObjs );
     vFixed  = Vec_StrStart( nObjs );
     vTruths = Vec_WrdStart( nObjs );
+    vStarts = Abc_NtkAssignStarts( pNtk, vNodes, &nTotal );
+    vTruths2= Vec_WrdStart( nTotal );
+    Abc_NtkFillTruthStore( TruthStore );
+    for ( i = 0; i < 16; i++ )
+        pTruths[i] = TruthStore[i];
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
     {
-        word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
-        Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
-        if ( uTruth == 0 || ~uTruth == 0 )
-            continue;
+        if ( Abc_ObjFaninNum(pObj) <= 6 )
+        {
+            word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
+            Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
+            if ( uTruth == 0 || ~uTruth == 0 )
+                continue;
+        }
+        else
+        {
+            int nWords  = Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) );
+            int Offset  = Vec_IntEntry( vStarts, pObj->iTemp );
+            word * pRes = Vec_WrdEntryP( vTruths2, Offset );
+            Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes );
+            // check const0
+            for ( k = 0; k < nWords; k++ )
+                if ( pRes[k] )
+                    break;
+            if ( k == nWords )
+                continue;
+            // check const1
+            for ( k = 0; k < nWords; k++ )
+                if ( ~pRes[k] )
+                    break;
+            if ( k == nWords )
+                continue;
+        }
         vArray = Vec_WecEntry( vFanins, pObj->iTemp );
         Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
         Abc_ObjForEachFanin( pObj, pFanin, k )
             Vec_IntPush( vArray, pFanin->iTemp );
+        //Vec_IntPrint( vArray );
     }
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
@@ -131,28 +211,58 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
 //    for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ )
 //        if ( rand() % 10 == 0 )
 //            Vec_StrWriteEntry( vFixed, i, (char)1 );
-    return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths );
+    return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 );
 }
 Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot )
 {
+    word TruthStore[16][1<<10] = {{0}}, * pTruths[16] = {NULL}, pCube[1<<10] = {0};
     Vec_Ptr_t * vNodes;
     Vec_Wec_t * vFanins;
     Vec_Str_t * vFixed;
     Vec_Wrd_t * vTruths;
     Vec_Int_t * vArray;
+    Vec_Int_t * vStarts;
+    Vec_Wrd_t * vTruths2;
     Abc_Obj_t * pObj, * pFanin;
-    int i, k, nObjs;
+    int i, k, nObjs, nTotal = 0;
     vNodes  = Abc_NtkAssignIDs2(pNtk);
     nObjs   = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + Abc_NtkCoNum(pNtk);
     vFanins = Vec_WecStart( nObjs );
     vFixed  = Vec_StrStart( nObjs );
     vTruths = Vec_WrdStart( nObjs );
+    vStarts = Abc_NtkAssignStarts( pNtk, vNodes, &nTotal );
+    vTruths2= Vec_WrdAlloc( nTotal );
+    Abc_NtkFillTruthStore( TruthStore );
+    for ( i = 0; i < 16; i++ )
+        pTruths[i] = TruthStore[i];
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
     {
-        word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
-        Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
-        if ( uTruth == 0 || ~uTruth == 0 )
-            continue;
+        if ( Abc_ObjFaninNum(pObj) <= 6 )
+        {
+            word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
+            Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
+            if ( uTruth == 0 || ~uTruth == 0 )
+                continue;
+        }
+        else
+        {
+            int nWords  = Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) );
+            int Offset  = Vec_IntEntry( vStarts, pObj->iTemp );
+            word * pRes = Vec_WrdEntryP( vTruths2, Offset );
+            Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes );
+            // check const0
+            for ( k = 0; k < nWords; k++ )
+                if ( pRes[k] )
+                    break;
+            if ( k == nWords )
+                continue;
+            // check const1
+            for ( k = 0; k < nWords; k++ )
+                if ( ~pRes[k] )
+                    break;
+            if ( k == nWords )
+                continue;
+        }
         vArray = Vec_WecEntry( vFanins, pObj->iTemp );
         Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
         Abc_ObjForEachFanin( pObj, pFanin, k )
@@ -170,7 +280,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot )
     Abc_NtkForEachNode( pNtk, pObj, i )
         if ( i >= iPivot )
             Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 );
-    return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths );
+    return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 );
 }
 
 /**Function*************************************************************
@@ -243,9 +353,9 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     Abc_NtkSweep( pNtk, 0 );
     // count fanouts
     nFaninMax = Abc_NtkGetFaninMax( pNtk );
-    if ( nFaninMax > 6 )
+    if ( nFaninMax > 15 )
     {
-        Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+        Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 15 fanins.\n" );
         return 1;
     }
     if ( !Abc_NtkHasSop(pNtk) )
@@ -424,9 +534,9 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t
     assert( Abc_NtkIsLogic(p) );
     // count fanouts
     nFaninMax = Abc_NtkGetFaninMax( p );
-    if ( nFaninMax > 6 )
+    if ( nFaninMax > 15 )
     {
-        Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+        Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 15 fanins.\n" );
         return 0;
     }
     if ( !Abc_NtkHasSop(p) )
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 2b6ba6dc..151bf91d 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -738,7 +738,7 @@ void Tim_ManBlackBoxIoNum( Tim_Man_t * p, int * pnBbIns, int * pnBbOuts )
     if ( Tim_ManBoxNum(p) )
         Tim_ManForEachBox( p, pBox, i )
         {
-            if ( !pBox->fBlack && pBox->nInputs <= 6 )
+            if ( !pBox->fBlack )//&& pBox->nInputs <= 6 )
                 continue;
             *pnBbIns  += Tim_ManBoxInputNum( p, i );
             *pnBbOuts += Tim_ManBoxOutputNum( p, i );
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 002778dc..1aa8b7d0 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -87,7 +87,7 @@ struct Sfm_Par_t_
 extern void         Sfm_ParSetDefault( Sfm_Par_t * pPars );
 extern int          Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
 /*=== sfmNtk.c ==========================================================*/
-extern Sfm_Ntk_t *  Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths );
+extern Sfm_Ntk_t *  Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 );
 extern void         Sfm_NtkFree( Sfm_Ntk_t * p );
 extern Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
 extern word *       Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index ce2f34b8..f6d434f8 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -68,24 +68,63 @@ void Sfm_PrintCnf( Vec_Str_t * vCnf )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
 {
+    int w, nWords = Abc_Truth6WordNum( nVars );
     Vec_StrClear( vCnf );
-    if ( Truth == 0 || ~Truth == 0 )
+    if ( nVars <= 6 )
     {
-//        assert( nVars == 0 );
-        Vec_StrPush( vCnf, (char)(Truth == 0) );
-        Vec_StrPush( vCnf, (char)-1 );
-        return 1;
+        if ( Truth == 0 || ~Truth == 0 )
+        {
+            //assert( nVars == 0 );
+            Vec_StrPush( vCnf, (char)(Truth == 0) );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
+    }
+    else
+    {
+        // const0
+        for ( w = 0; w < nWords; w++ )
+            if ( pTruth[w] )
+                break;
+        if ( w == nWords )
+        {
+            Vec_StrPush( vCnf, (char)1 );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
+        // const1
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pTruth[w] )
+                break;
+        if ( w == nWords )
+        {
+            Vec_StrPush( vCnf, (char)0 );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
     }
-    else 
     {
         int i, k, c, RetValue, Literal, Cube, nCubes = 0;
         assert( nVars > 0 );
         for ( c = 0; c < 2; c ++ )
         {
-            Truth = c ? ~Truth : Truth;
-            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            if ( nVars <= 6 )
+            {
+                Truth = c ? ~Truth : Truth;
+                RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            }
+            else
+            {
+                if ( c )
+                    for ( k = 0; k < nWords; k++ )
+                        pTruth[k] = ~pTruth[k];
+                RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 0 );
+                if ( c )
+                    for ( k = 0; k < nWords; k++ )
+                        pTruth[k] = ~pTruth[k];
+            }
             assert( RetValue == 0 );
             nCubes += Vec_IntSize( vCover );
             Vec_IntForEachEntry( vCover, Cube, i )
@@ -129,7 +168,9 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
     vCnfs = Vec_WecStart( p->nObjs );
     Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
     {
-        nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
+        int Offset  = Vec_IntEntry( p->vStarts, i );
+        word * pRes = Vec_WrdSize(p->vTruths2) ? Vec_WrdEntryP( p->vTruths2, Offset ) : NULL;
+        nCubes = Sfm_TruthToCnf( uTruth, pRes, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) );
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 2b96d4bd..80edd54d 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -81,6 +81,8 @@ struct Sfm_Ntk_t_
     Vec_Str_t *       vEmpty;      // transparent objects
     Vec_Wrd_t *       vTruths;     // truth tables
     Vec_Wec_t         vFanins;     // fanins
+    Vec_Int_t *       vStarts;     // offsets
+    Vec_Wrd_t *       vTruths2;    // truth tables (large)
     // attributes
     Vec_Wec_t         vFanouts;    // fanouts
     Vec_Int_t         vLevels;     // logic level
@@ -195,7 +197,7 @@ extern void        Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 
 /*=== sfmCnf.c ==========================================================*/
 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 int          Sfm_TruthToCnf( word Truth, word * pTruth, 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, int iPivotVar );
 /*=== sfmCore.c ==========================================================*/
diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c
index afb4a48d..18ba0971 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -107,7 +107,7 @@ void Sfm_DecCreateCnf( Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t
     vCover = Vec_IntAlloc( 100 );
     Vec_WrdForEachEntry( vGateFuncs, uTruth, i )
     {
-        nCubes = Sfm_TruthToCnf( uTruth, Vec_IntEntry(vGateSizes, i), vCover, vCnf );
+        nCubes = Sfm_TruthToCnf( uTruth, NULL, Vec_IntEntry(vGateSizes, i), vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vGateCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) );
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 1ded0ede..d410aa0b 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v
   SeeAlso     []
 
 ***********************************************************************/
-Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths )
+Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 )
 {
     Sfm_Ntk_t * p;
     Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
@@ -178,6 +178,8 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     p->vEmpty   = vEmpty;
     p->vTruths  = vTruths;
     p->vFanins  = *vFanins;
+    p->vStarts  = vStarts;
+    p->vTruths2 = vTruths2;
     ABC_FREE( vFanins );
     // attributes
     Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
@@ -217,6 +219,8 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_StrFreeP( &p->vEmpty );
     Vec_WrdFree( p->vTruths );
     Vec_WecErase( &p->vFanins );
+    Vec_IntFree( p->vStarts );
+    Vec_WrdFree( p->vTruths2 );
     // attributes
     Vec_WecErase( &p->vFanouts );
     ABC_FREE( p->vLevels.pArray );
@@ -316,6 +320,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
     int iFanin = Sfm_ObjFanin( p, iNode, f );
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( iFanin != iFaninNew );
+    assert( Sfm_ObjFaninNum(p, iNode) <= 6 );
     if ( uTruth == 0 || ~uTruth == 0 )
     {
         Sfm_ObjForEachFanin( p, iNode, iFanin, f )
@@ -341,7 +346,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
     // update truth table
     Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
-    Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
+    Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
 }
 
 /**Function*************************************************************
@@ -361,7 +366,7 @@ Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
 }
 word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
 {
-    return Vec_WrdEntryP( p->vTruths, i );
+    return Sfm_ObjFaninNum(p, i) <= 6 ? Vec_WrdEntryP( p->vTruths, i ) : Vec_WrdEntryP( p->vTruths2, Vec_IntEntry(p->vStarts, i) );
 }
 int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
 {
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 8bcb7f8a..6ccdd903 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -167,6 +167,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
     sat_solver_setnvars( p->pSat, nVars + 1 );
     pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
     pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
+    assert( Vec_IntSize(p->vDivIds) <= 6 );
     while ( 1 ) 
     {
         // find onset minterm