Integrating new MFS package with GIA manager.

8 files changed, 480 insertions, 9 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 15f57ac3..6175d0fa 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3591,6 +3591,10 @@ SOURCE=.\src\aig\gia\giaMem.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaMfs.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaMini.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d09129a5..f0769e79 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1112,6 +1112,7 @@ extern int                 Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pPar
 extern void *              Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
 extern Gia_Man_t *         Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
 /*=== giaTruth.c ===========================================================*/
+extern word                Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp );
 extern word                Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
 extern int                 Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern word *              Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
new file mode 100644
index 00000000..aebbb58e
--- /dev/null
+++ b/src/aig/gia/giaMfs.c
@@ -0,0 +1,389 @@
+/**CFile****************************************************************
+
+  FileName    [giaMfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Interface with the MFS package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaMfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "bool/kit/kit.h"
+#include "opt/sfm/sfm.h"
+#include "misc/tim/tim.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static word s_ElemVar  = ABC_CONST(0xAAAAAAAAAAAAAAAA);
+static word s_ElemVar2 = ABC_CONST(0xCCCCCCCCCCCCCCCC);
+
+extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManExtractMfs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vId2Mfs, Vec_Wec_t * vFanins, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths, Vec_Wrd_t * vTruthsTemp )
+{
+    Vec_Int_t * vArray;
+    int i, Fanin;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    assert( Gia_ObjIsLut(p, iObj) );
+    if ( !~pObj->Value )
+        return;
+    Gia_LutForEachFanin( p, iObj, Fanin, i )
+        Gia_ManExtractMfs_rec( p, Fanin, vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp );
+    pObj->Value = Vec_WecSize(vFanins);
+    vArray = Vec_WecPushLevel( vFanins );
+    Vec_IntGrow( vArray, Gia_ObjLutSize(p, iObj) );
+    Gia_LutForEachFanin( p, iObj, Fanin, i )
+        Vec_IntPush( vArray, Gia_ManObj(p, Fanin)->Value );
+    Vec_StrPush( vFixed, (char)0 );
+    Vec_WrdPush( vTruths, Gia_ObjComputeTruthTable6Lut(p, iObj, vTruthsTemp) );
+    Vec_IntWriteEntry( vId2Mfs, iObj, pObj->Value );
+}
+void Gia_ManExtractMfs_rec2( Gia_Man_t * p, int iObj, Vec_Int_t * vId2Mfs, Vec_Wec_t * vFanins, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths )
+{
+    Vec_Int_t * vArray;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManExtractMfs_rec2( p, Gia_ObjFaninId0(pObj, iObj), vId2Mfs, vFanins, vFixed, vTruths );
+    Gia_ManExtractMfs_rec2( p, Gia_ObjFaninId1(pObj, iObj), vId2Mfs, vFanins, vFixed, vTruths );
+    pObj->Value = Vec_WecSize(vFanins);
+    vArray = Vec_WecPushLevel( vFanins );
+    Vec_IntGrow( vArray, 2 );
+    Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value );
+    Vec_IntPush( vArray, Gia_ObjFanin1(pObj)->Value );
+    Vec_StrPush( vFixed, (char)1 );
+    Vec_WrdPush( vTruths, (Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar) & (Gia_ObjFaninC1(pObj) ? ~s_ElemVar2 : s_ElemVar2) );
+    Vec_IntWriteEntry( vId2Mfs, iObj, pObj->Value );
+}
+Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t ** pvId2Mfs )
+{
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    Vec_Int_t * vPoNodes;
+    Vec_Int_t * vId2Mfs;
+    Vec_Wec_t * vFanins;
+    Vec_Str_t * vFixed;
+    Vec_Wrd_t * vTruths, * vTruthsTemp;
+    Vec_Int_t * vArray;
+    Gia_Obj_t * pObj, * pObjBox;
+    int i, k, nRealPis, nRealPos, nPiNum, nPoNum, curCi, curCo;
+    assert( pManTime == NULL || Tim_ManCiNum(pManTime) == Gia_ManCiNum(p) );
+    assert( pManTime == NULL || Tim_ManCoNum(pManTime) == Gia_ManCoNum(p) );
+    // get the real number of PIs and POs
+    nRealPis = pManTime ? Tim_ManPiNum(pManTime) : Gia_ManCiNum(p);
+    nRealPos = pManTime ? Tim_ManPoNum(pManTime) : Gia_ManCoNum(p);
+    // create mapping from GIA into MFS
+    vId2Mfs  = Vec_IntStartFull( Gia_ManObjNum(p) );
+    // collect PO nodes
+    vPoNodes = Vec_IntAlloc( 1000 );
+    // create the arrays
+    vFanins  = Vec_WecAlloc( 1000 );
+    vFixed   = Vec_StrAlloc( 1000 );
+    vTruths  = Vec_WrdAlloc( 1000 );
+    vTruthsTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    // assign MFS ids to primary inputs
+    Gia_ManFillValue( p );
+    for ( i = 0; i < nRealPis; i++ )
+    {
+        pObj = Gia_ManPi( p, i );
+        pObj->Value = Vec_WecSize(vFanins);
+        Vec_WecPushLevel( vFanins );
+        Vec_StrPush( vFixed, (char)0 );
+        Vec_WrdPush( vTruths, (word)0 );
+        Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+    }
+    // assign MFS ids to black box outputs
+    curCi = nRealPis;
+    curCo = 0;
+    if ( pManTime )
+    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
+    {
+        if ( !Tim_ManBoxIsBlack(pManTime, i) )
+        {
+            // collect POs
+            for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
+            {
+                pObj = Gia_ManPo( p, curCo + k );
+                Vec_IntPush( vPoNodes, Gia_ObjId(p, pObj) );
+            }
+            // assign values to the PIs
+            for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
+            {
+                pObj = Gia_ManPi( p, curCi + k );
+                pObj->Value = Vec_WecSize(vFanins);
+                Vec_WecPushLevel( vFanins );
+                Vec_StrPush( vFixed, (char)1 );
+                Vec_WrdPush( vTruths, (word)0 );
+                Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+            }
+        }
+        curCo += Tim_ManBoxInputNum(pManTime, i);
+        curCi += Tim_ManBoxOutputNum(pManTime, i);
+    }
+    // collect POs
+//    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
+    for ( i = Gia_ManCoNum(p) - nRealPos; i < Gia_ManCoNum(p); i++ )
+    {
+        pObj = Gia_ManPo( p, i );
+        Vec_IntPush( vPoNodes, Gia_ObjId(p, pObj) );
+    }
+    curCo += nRealPos;
+    // verify counts
+    assert( curCi == Gia_ManPiNum(p) );
+    assert( curCo == Gia_ManPoNum(p) );
+    // remeber the end of PIs
+    nPiNum = Vec_WecSize(vFanins);
+    nPoNum = Vec_IntSize(vPoNodes);
+    // assign value to constant node
+    pObj = Gia_ManConst0(p);
+    Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), Vec_WecSize(vFanins) );
+    pObj->Value = Vec_WecSize(vFanins);
+    Vec_WecPushLevel( vFanins );
+    Vec_StrPush( vFixed, (char)0 );
+    Vec_WrdPush( vTruths, (word)0 );
+    Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+    // create internal nodes
+    curCi = nRealPis;
+    curCo = 0;
+    if ( pManTime )
+    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
+    {
+        // recursively add for box inputs
+        Gia_ManIncrementTravId( pBoxes );
+        for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
+        {
+            // build logic
+            pObj = Gia_ManPo( p, curCo + k );
+            Gia_ManExtractMfs_rec( p, Gia_ObjFaninId0p(p, pObj), vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp );
+            // add buffer/inverter
+            pObj->Value = Vec_WecSize(vFanins);
+            vArray = Vec_WecPushLevel( vFanins );
+            Vec_IntGrow( vArray, 1 );
+            assert( !~Gia_ObjFanin0(pObj)->Value );
+            Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value );
+            Vec_StrPush( vFixed, (char)0 );
+            Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar );
+            Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+            // transfer to the PI
+            pObjBox = Gia_ManPi( pBoxes, k );
+            pObjBox->Value = pObj->Value;
+            Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+        }
+        if ( !Tim_ManBoxIsBlack(pManTime, i) )
+        {
+            pObjBox = Gia_ManConst0(pBoxes);
+            pObjBox->Value = Vec_WecSize(vFanins);
+            Vec_WecPushLevel( vFanins );
+            Vec_StrPush( vFixed, (char)0 );
+            Vec_WrdPush( vTruths, (word)0 );
+            Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+            // add internal nodes and transfer
+            for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
+            {
+                // build logic
+                pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k );
+                Gia_ManExtractMfs_rec2( pBoxes, Gia_ObjFaninId0p(pBoxes, pObjBox), vId2Mfs, vFanins, vFixed, vTruths );
+                // add buffer/inverter
+                vArray = Vec_WecPushLevel( vFanins );
+                Vec_IntGrow( vArray, 1 );
+                assert( !~Gia_ObjFanin0(pObjBox)->Value );
+                Vec_IntPush( vArray, Gia_ObjFanin0(pObjBox)->Value );
+                Vec_StrPush( vFixed, (char)1 );
+                Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObjBox) ? ~s_ElemVar : s_ElemVar );
+                // transfer to the PI
+                pObj = Gia_ManPi( p, curCi + k );
+                pObj->Value = pObjBox->Value;
+            }
+        }
+        curCo += Tim_ManBoxInputNum(pManTime, i);
+        curCi += Tim_ManBoxOutputNum(pManTime, i);
+    }
+    // create POs with buffers
+    Gia_ManForEachObjVec( vPoNodes, p, pObj, i )
+    {
+        Gia_ManExtractMfs_rec( p, Gia_ObjFaninId0p(p, pObj), vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp );
+        pObj->Value = Vec_WecSize(vFanins);
+        // add buffer/inverter
+        vArray = Vec_WecPushLevel( vFanins );
+        Vec_IntGrow( vArray, 1 );
+        assert( !~Gia_ObjFanin0(pObj)->Value );
+        Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value );
+        Vec_StrPush( vFixed, (char)0 );
+        Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar );
+        Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+    }
+    Vec_IntFree( vPoNodes );
+    Vec_WrdFree( vTruthsTemp );
+    *pvId2Mfs = vId2Mfs;
+    return Sfm_NtkConstruct( vFanins, nPiNum, nPoNum, vFixed, vTruths );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, Vec_Int_t * vId2Mfs )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vMfsTopo, * vMfs2New, * vArray, * vCover;
+    int i, k, Fanin, iMfsId, iLitNew;
+    word * pTruth;
+    // collect MFS nodes in the topo order
+    vMfsTopo = Sfm_NtkDfs( pNtk );
+    // create mapping from MFS to new GIA literals
+    vMfs2New = Vec_IntStartFull( Vec_IntCap(vMfsTopo) );
+    // start new GIA
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // map primary inputs
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        iMfsId = Vec_IntEntry( vId2Mfs, Gia_ObjId(p, pObj) );
+        assert( iMfsId >= 0 );
+        Vec_IntWriteEntry( vMfs2New, iMfsId, Gia_ManAppendCi(pNew) );
+    }
+    // map internal nodes
+    vCover = Vec_IntAlloc( 1 << 16 );
+    Vec_IntForEachEntry( vMfsTopo, iMfsId, i )
+    {
+        assert( Sfm_NodeReadUsed(pNtk, iMfsId) );
+        pTruth = Sfm_NodeReadTruth( pNtk, iMfsId );
+        if ( pTruth[0] == 0 || ~pTruth[0] == 0 )
+        {
+            Vec_IntWriteEntry( vMfs2New, iMfsId, 0 );
+            continue;
+        }
+        vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk
+        Vec_IntForEachEntry( vArray, Fanin, k )
+        {
+            iLitNew = Vec_IntEntry( vMfs2New, Fanin );
+            assert( iLitNew >= 0 );
+            Vec_IntWriteEntry( vArray, k, iLitNew );            
+        }
+        // derive new function
+        iLitNew = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vArray), vCover, vArray, 0 );
+        Vec_IntWriteEntry( vMfs2New, iMfsId, iLitNew );
+    }
+    Vec_IntFree( vCover );
+    // map output nodes
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        iMfsId = Vec_IntEntry( vId2Mfs, Gia_ObjId(p, pObj) );
+        assert( iMfsId >= 0 );
+        vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk
+        assert( Vec_IntSize(vArray) == 1 );
+        // get the fanin
+        iLitNew = Vec_IntEntry( vMfs2New, Vec_IntEntry(vArray, 0) );
+        assert( iLitNew >= 0 );
+        // create CO
+        assert( pTruth[0] == s_ElemVar || ~pTruth[0] == s_ElemVar );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond(iLitNew, (int)(pTruth[0] != s_ElemVar)) );
+    }
+    Vec_IntFree( vMfs2New );
+    Vec_IntFree( vMfsTopo );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars )
+{
+    Sfm_Ntk_t * pNtk;
+    Vec_Int_t * vId2Mfs;
+    Gia_Man_t * pNew;
+    int nFaninMax, nNodes;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( p->vMapping != NULL );
+    if ( p->pManTime != NULL && p->pAigExtra == NULL )
+    {
+        Abc_Print( 1, "Timing manager is given but there is no GIA of boxes.\n" );
+        return NULL;
+    }
+    // count fanouts
+    nFaninMax = Gia_ManLutSizeMax( p );
+    if ( nFaninMax > 6 )
+    {
+        Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+        return NULL;
+    }
+    // collect information
+    pNtk = Gia_ManExtractMfs( p, p->pAigExtra, &vId2Mfs );
+    // perform optimization
+    nNodes = Sfm_NtkPerform( pNtk, pPars );
+    // call the fast extract procedure
+    if ( nNodes == 0 )
+    {
+        Abc_Print( 1, "The network is not changed by \"&mfs\".\n" );
+        pNew = Gia_ManDup( p );
+        pNew->vMapping = Vec_IntDup( p->vMapping );
+    }
+    else
+    {
+        pNew = Gia_ManInsertMfs( p, pNtk, vId2Mfs );
+        if( pPars->fVerbose )
+            Abc_Print( 1, "The network has %d nodes changed by \"&mfs\".\n", nNodes );
+    }
+    Vec_IntFree( vId2Mfs );
+    Sfm_NtkFree( pNtk );
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c
index 26a380d7..f8a9e043 100644
--- a/src/aig/gia/giaTruth.c
+++ b/src/aig/gia/giaTruth.c
@@ -27,6 +27,15 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static word s_Truth6[6] = {
+    ABC_CONST(0xAAAAAAAAAAAAAAAA),
+    ABC_CONST(0xCCCCCCCCCCCCCCCC),
+    ABC_CONST(0xF0F0F0F0F0F0F0F0),
+    ABC_CONST(0xFF00FF00FF00FF00),
+    ABC_CONST(0xFFFF0000FFFF0000),
+    ABC_CONST(0xFFFFFFFF00000000)
+};
+
 static inline word * Gla_ObjTruthElem( Gia_Man_t * p, int i )            { return (word *)Vec_PtrEntry( p->vTtInputs, i );                                           }
 static inline word * Gla_ObjTruthNode( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * Gia_ObjNum(p, pObj);                    }
 static inline word * Gla_ObjTruthFree1( Gia_Man_t * p )                  { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * 254;                                    }
@@ -40,6 +49,44 @@ static inline word * Gla_ObjTruthDup( Gia_Man_t * p, word * pDst, word * pSrc, i
 
 /**Function*************************************************************
 
+  Synopsis    [Computes truth table of a 6-LUT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ObjComputeTruthTable6Lut_rec( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp )
+{
+    word uTruth0, uTruth1;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    Gia_ObjComputeTruthTable6Lut_rec( p, Gia_ObjFaninId0p(p, pObj), vTemp );
+    Gia_ObjComputeTruthTable6Lut_rec( p, Gia_ObjFaninId1p(p, pObj), vTemp );
+    uTruth0 = Vec_WrdEntry( vTemp, Gia_ObjFanin0(pObj)->Value );
+    uTruth0 = Gia_ObjFaninC0(pObj) ? ~uTruth0 : uTruth0;
+    uTruth1 = Vec_WrdEntry( vTemp, Gia_ObjFanin1(pObj)->Value );
+    uTruth1 = Gia_ObjFaninC1(pObj) ? ~uTruth1 : uTruth1;
+    Vec_WrdWriteEntry( vTemp, iObj, uTruth0 & uTruth1 );
+}
+word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    int i, Fanin;
+    assert( Vec_WrdSize(vTemp) == Gia_ManObjNum(p) );
+    assert( Gia_ObjIsLut(p, iObj) );
+    Gia_LutForEachFanin( p, iObj, Fanin, i )
+        Vec_WrdWriteEntry( vTemp, Fanin, s_Truth6[i] );
+    assert( i <= 6 );
+    Gia_ObjComputeTruthTable6Lut_rec( p, iObj, vTemp );
+    return Vec_WrdEntry( vTemp, iObj );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes truth table up to 6 inputs.]
 
   Description []
@@ -68,14 +115,6 @@ void Gia_ObjComputeTruthTable6_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Wrd_t *
 }
 word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths )
 {
-    static word s_Truth6[6] = {
-        ABC_CONST(0xAAAAAAAAAAAAAAAA),
-        ABC_CONST(0xCCCCCCCCCCCCCCCC),
-        ABC_CONST(0xF0F0F0F0F0F0F0F0),
-        ABC_CONST(0xFF00FF00FF00FF00),
-        ABC_CONST(0xFFFF0000FFFF0000),
-        ABC_CONST(0xFFFFFFFF00000000)
-    };
     Gia_Obj_t * pLeaf;
     int i;
     assert( Vec_IntSize(vSupp) <= 6 );
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 34985059..8cdbe137 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -28,6 +28,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaIso2.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMem.c \
+    src/aig/gia/giaMfs.c \
     src/aig/gia/giaMini.c \
     src/aig/gia/giaMuxes.c \
     src/aig/gia/giaPat.c \
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 078026c5..cc797afc 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -75,7 +75,8 @@ extern Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
 extern word *       Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
-/*=== sfmSat.c ==========================================================*/
+/*=== sfmWin.c ==========================================================*/
+extern Vec_Int_t *  Sfm_NtkDfs( Sfm_Ntk_t * p );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index b193fd9e..b3e1909d 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -162,6 +162,8 @@ extern void        Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Sfm_NtkForEachPi( p, i )                 for ( i = 0; i < p->nPis; i++ )
+#define Sfm_NtkForEachPo( p, i )                 for ( i = p->nObjs - p->nPos; i < p->nObjs; i++ )
 #define Sfm_NtkForEachNode( p, i )               for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
 #define Sfm_NtkForEachNodeReverse( p, i )        for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- )
 #define Sfm_ObjForEachFanin( p, Node, Fan, i )   for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index fa0b484b..e39516b1 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -123,6 +123,40 @@ static inline int   Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id )   { return
 
 /**Function*************************************************************
 
+  Synopsis    [Collects used internal nodes in a topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes )
+{
+    int i, iFanin;
+    if ( Sfm_ObjIsPi(p, iNode) )
+        return;
+    if ( Sfm_ObjIsTravIdCurrent(p, iNode) )
+        return;
+    Sfm_ObjSetTravIdCurrent(p, iNode);
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        Sfm_NtkDfs_rec( p, iFanin, vNodes );
+    Vec_IntPush( vNodes, iNode );
+}
+Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p )
+{
+    Vec_Int_t * vNodes;
+    int i;
+    vNodes = Vec_IntAlloc( p->nObjs );
+    Sfm_NtkIncrementTravId( p );
+    Sfm_NtkForEachPo( p, i )
+        Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Check if this fanout overlaps with TFI cone of the node.]
 
   Description []