New MFS package.

5 files changed, 34 insertions, 15 deletions

diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index c87c1a75..2371e49a 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -111,9 +111,9 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
     {
         word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
         Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
-        vArray = Vec_WecEntry( vFanins, pObj->iTemp );
         if ( uTruth == 0 || ~uTruth == 0 )
             continue;
+        vArray = Vec_WecEntry( vFanins, pObj->iTemp );
         Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
         Abc_ObjForEachFanin( pObj, pFanin, k )
             Vec_IntPush( vArray, pFanin->iTemp );
@@ -146,11 +146,10 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
 ***********************************************************************/
 void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
 {
-    Vec_Int_t * vCover = Sfm_NodeReadCover(p);
-    Vec_Int_t * vMap, * vArray;
+    Vec_Int_t * vCover, * vMap, * vArray;
     Abc_Obj_t * pNode;
-    int i, k, Fanin;
     word * pTruth;
+    int i, k, Fanin;
     // map new IDs into old nodes
     vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachCi( pNtk, pNode, i )
@@ -162,6 +161,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
     Abc_NtkForEachNode( pNtk, pNode, i )
         Abc_ObjRemoveFanins( pNode );
     // create new fanins
+    vCover = Vec_IntAlloc( 1 << 16 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         if ( pNode->iTemp == 0 || Sfm_NodeReadFixed(p, pNode->iTemp) )
@@ -192,6 +192,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
         }
         assert( Abc_SopGetVarNum((char *)pNode->pData) == Vec_IntSize(vArray) );
     }
+    Vec_IntFree( vCover );
     Vec_IntFree( vMap );
 }
 
diff --git a/src/map/if/ifCom.c b/src/map/if/ifCom.c
index fda791c2..dd6477d1 100644
--- a/src/map/if/ifCom.c
+++ b/src/map/if/ifCom.c
@@ -290,7 +290,7 @@ int If_CommandReadBox( Abc_Frame_t * pAbc, int argc, char **argv )
     pLib = fExtended ? If_LibBoxRead2( FileName ) : If_LibBoxRead( FileName );
     if ( pLib == NULL )
     {
-        fprintf( pErr, "Reading LUT library has failed.\n" );
+        fprintf( pErr, "Reading box library has failed.\n" );
         goto usage;
     }
     // replace the current library
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 9323aa47..18960183 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -75,7 +75,6 @@ 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 );
-extern Vec_Int_t *  Sfm_NodeReadCover( Sfm_Ntk_t * p );
 /*=== sfmSat.c ==========================================================*/
 
 
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 79b7bb6a..2042eaec 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -57,7 +57,7 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
             assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
         // POs have one fanout
         if ( i + nPos >= Vec_WecSize(vFanins) )
-            assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
+            assert( Vec_StrEntry(vFixed, i) == (char)0 );
     }
 }
 
@@ -248,7 +248,7 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
 void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
-    if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
+    if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) || Sfm_ObjIsFixed(p, iNode) )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
@@ -258,6 +258,7 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
             Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
+    Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
 }
 void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
 {
@@ -327,10 +328,6 @@ int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
 {
     return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
 }
-Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p )
-{
-    return p->vCover;
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 8ddd7865..3c30c480 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -190,9 +190,9 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
     {
         // skip some of the fanouts if the number is large
         if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax )
-            break;
+            return;
         // skip TFI nodes, PO nodes, or nodes with high logic level
-        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || Sfm_ObjIsFixed(p, iFanout) ||
+        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
             (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
             continue;
         // handle single-input nodes
@@ -213,6 +213,28 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
 
 /**Function*************************************************************
 
+  Synopsis    [Fixed object is useful when it has a non-fixed fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sfm_ObjIsUseful( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanout;
+    if ( !Sfm_ObjIsFixed(p, iNode) )
+        return 1;
+    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
+        if ( !Sfm_ObjIsFixed(p, iFanout) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes structural window.]
 
   Description []
@@ -309,7 +331,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     // compact divisors
     k = 0;
     Vec_IntForEachEntry( p->vDivs, iTemp, i )
-        if ( !Sfm_ObjIsTravIdCurrent2( p, iTemp ) )
+        if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) && Sfm_ObjIsUseful(p, iTemp) )
             Vec_IntWriteEntry( p->vDivs, k++, iTemp );
     Vec_IntShrink( p->vDivs, k );
     assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );