Version abc70209

30 files changed, 958 insertions, 553 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 62aac927..e15ca557 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -90,11 +90,10 @@ typedef enum {
     ABC_OBJ_ASSERT,     //  7:  assertion terminal
     ABC_OBJ_NET,        //  8:  net
     ABC_OBJ_NODE,       //  9:  node
-    ABC_OBJ_GATE,       // 10:  mapped node
-    ABC_OBJ_LATCH,      // 11:  latch
-    ABC_OBJ_TRI,        // 12:  tristate element
-    ABC_OBJ_BLACKBOX,   // 13:  box with unknown contents
-    ABC_OBJ_NUMBER      // 14:  unused
+    ABC_OBJ_LATCH,      // 10:  latch
+    ABC_OBJ_WHITEBOX,   // 11:  box with known contents
+    ABC_OBJ_BLACKBOX,   // 12:  box with unknown contents
+    ABC_OBJ_NUMBER      // 13:  unused
 } Abc_ObjType_t;
 
 // latch initial values
@@ -188,8 +187,7 @@ struct Abc_Ntk_t_
     Abc_Ntk_t *       pNetBackup;    // the pointer to the previous backup network
     int               iStep;         // the generation number for the given network
     // hierarchy
-    stmm_table *      tName2Model;   // the table hashing names into network pointers (or NULL if no hierarchy)
-    Vec_Int_t *       pBlackBoxes;   // stores pairs (PI num, PO num) for each model, including the base model (or NULL if no hierarchy)
+    Abc_Lib_t *       pDesign;
     short             fHieVisited;   // flag to mark the visited network
     short             fHiePath;      // flag to mark the network on the path
     // miscellaneous data members
@@ -197,7 +195,6 @@ struct Abc_Ntk_t_
     Extra_MmFixed_t * pMmObj;        // memory manager for objects
     Extra_MmStep_t *  pMmStep;       // memory manager for arrays
     void *            pManFunc;      // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
-    Abc_Lib_t *       pDesign;
 //    Abc_Lib_t *       pVerLib;       // for structural verilog designs
     Abc_ManTime_t *   pManTime;      // the timing manager (for mapped networks) stores arrival/required times for all nodes
     void *            pManCut;       // the cut manager (for AIGs) stores information about the cuts computed for the nodes
@@ -299,9 +296,8 @@ static inline int         Abc_NtkBiNum( Abc_Ntk_t * pNtk )           { return pN
 static inline int         Abc_NtkBoNum( Abc_Ntk_t * pNtk )           { return pNtk->nObjCounts[ABC_OBJ_BO];       }
 static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjCounts[ABC_OBJ_NET];      }
 static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )         { return pNtk->nObjCounts[ABC_OBJ_NODE];     }
-static inline int         Abc_NtkGateNum( Abc_Ntk_t * pNtk )         { return pNtk->nObjCounts[ABC_OBJ_GATE];     }
 static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return pNtk->nObjCounts[ABC_OBJ_LATCH];    }
-static inline int         Abc_NtkTriNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjCounts[ABC_OBJ_TRI];      }
+static inline int         Abc_NtkWhiteboxNum( Abc_Ntk_t * pNtk )     { return pNtk->nObjCounts[ABC_OBJ_WHITEBOX]; }
 static inline int         Abc_NtkBlackboxNum( Abc_Ntk_t * pNtk )     { return pNtk->nObjCounts[ABC_OBJ_BLACKBOX]; }
 static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Abc_NtkLatchNum(pNtk) == 0;                   }
 static inline bool        Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); }
@@ -315,8 +311,7 @@ static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk )        { return Ab
 static inline Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )    { return Abc_NtkCreateObj( pNtk, ABC_OBJ_ASSERT );     }
 static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk )      { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NODE );       }
 static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )     { return Abc_NtkCreateObj( pNtk, ABC_OBJ_LATCH );      }
-static inline Abc_Obj_t * Abc_NtkCreateGate( Abc_Ntk_t * pNtk )      { return Abc_NtkCreateObj( pNtk, ABC_OBJ_GATE );       }
-static inline Abc_Obj_t * Abc_NtkCreateTri( Abc_Ntk_t * pNtk )       { return Abc_NtkCreateObj( pNtk, ABC_OBJ_TRI );        }
+static inline Abc_Obj_t * Abc_NtkCreateWhitebox( Abc_Ntk_t * pNtk )  { return Abc_NtkCreateObj( pNtk, ABC_OBJ_WHITEBOX );   }
 static inline Abc_Obj_t * Abc_NtkCreateBlackbox( Abc_Ntk_t * pNtk )  { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BLACKBOX );   }
 
 // reading objects
@@ -361,11 +356,11 @@ static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pO
 static inline bool        Abc_ObjIsTerm( Abc_Obj_t * pObj )          { return Abc_ObjIsCi(pObj) || Abc_ObjIsCo(pObj); }
 static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_NET;     }
 static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NODE;    }
-static inline bool        Abc_ObjIsGate( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_GATE;    }
 static inline bool        Abc_ObjIsLatch( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_LATCH;   }
-static inline bool        Abc_ObjIsTri( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_TRI;     }
+static inline bool        Abc_ObjIsBox( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_WHITEBOX || pObj->Type == ABC_OBJ_BLACKBOX; }
+static inline bool        Abc_ObjIsWhitebox( Abc_Obj_t * pObj )      { return pObj->Type == ABC_OBJ_WHITEBOX;}
 static inline bool        Abc_ObjIsBlackbox( Abc_Obj_t * pObj )      { return pObj->Type == ABC_OBJ_BLACKBOX;}
-static inline bool        Abc_ObjIsBox( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_TRI || pObj->Type == ABC_OBJ_BLACKBOX; }
+static inline void        Abc_ObjBlackboxToWhitebox( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBlackbox(pObj) ); pObj->Type = ABC_OBJ_WHITEBOX; pObj->pNtk->nObjCounts[ABC_OBJ_BLACKBOX]--; pObj->pNtk->nObjCounts[ABC_OBJ_WHITEBOX]++; }
 
 // working with fanin/fanout edges
 static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )        { return pObj->vFanins.nSize;     }
@@ -470,9 +465,9 @@ static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
 #define Abc_NtkForEachLatchOutput( pNtk, pObj, i )                                                  \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_ObjFanout0(Abc_NtkBox(pNtk, i))), 1); i++ )   \
         if ( !Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) ) {} else
-#define Abc_NtkForEachTri( pNtk, pObj, i )                                                         \
+#define Abc_NtkForEachWhitebox( pNtk, pObj, i )                                                    \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ )   \
-        if ( !Abc_ObjIsTri(pObj) ) {} else
+        if ( !Abc_ObjIsWhitebox(pObj) ) {} else
 #define Abc_NtkForEachBlackbox( pNtk, pObj, i )                                                    \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ )   \
         if ( !Abc_ObjIsBlackbox(pObj) ) {} else
@@ -536,6 +531,7 @@ extern bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
+extern int                Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
@@ -550,6 +546,8 @@ extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNode
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
+extern Vec_Ptr_t *        Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll );
 extern bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
@@ -589,6 +587,10 @@ extern int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect );
 extern int                Abc_NtkLogicToBdd( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicToAig( Abc_Ntk_t * pNtk );
+/*=== abcHie.c ==========================================================*/
+extern Abc_Ntk_t *        Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL );
 /*=== abcLatch.c ==========================================================*/
 extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
@@ -597,7 +599,7 @@ extern Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
  /*=== abcLib.c ==========================================================*/
 extern Abc_Lib_t *        Abc_LibCreate( char * pName );
-extern void               Abc_LibFree( Abc_Lib_t * pLib );
+extern void               Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
 extern void               Abc_LibPrint( Abc_Lib_t * pLib );
 extern int                Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 8d8f98b3..72597881 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -38,8 +38,6 @@ static bool Abc_NtkComparePis( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 static bool Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 static bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 
-static int  Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -112,7 +110,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
         }
     }
 
-    if ( !Abc_NtkBlackboxNum(pNtk) )
+    if ( Abc_NtkHasOnlyLatchBoxes(pNtk) )
     {
         // check CI/CO numbers
         if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) )
@@ -196,7 +194,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     // check the EXDC network if present
     if ( pNtk->pExdc )
         Abc_NtkCheck( pNtk->pExdc );
-
+/*
     // check the hierarchy
     if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
     {
@@ -217,6 +215,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
             return 0;
         }
     }
+*/
     return 1;
 }
 
@@ -746,7 +745,6 @@ bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis,
     return 1;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Returns 0 if the network hierachy contains a cycle.]
@@ -774,6 +772,8 @@ int Abc_NtkIsAcyclicHierarchy_rec( Abc_Ntk_t * pNtk )
     // go through all the children networks
     Abc_NtkForEachBox( pNtk, pObj, i )
     {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
         pNtkNext = pObj->pData;
         assert( pNtkNext != NULL );
         if ( pNtkNext->fHiePath )
@@ -799,9 +799,20 @@ int Abc_NtkIsAcyclicHierarchy_rec( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk )
 {
-    assert( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model );
+    Abc_Ntk_t * pTemp;
+    int i, RetValue;
+    assert( Abc_NtkIsNetlist(pNtk) && pNtk->pDesign );
+    // clear the modules
+    Vec_PtrForEachEntry( pNtk->pDesign->vModules, pTemp, i )
+        pTemp->fHieVisited = pTemp->fHiePath = 0;
+    // traverse
     pNtk->fHiePath = 1;
-    return Abc_NtkIsAcyclicHierarchy_rec( pNtk );
+    RetValue = Abc_NtkIsAcyclicHierarchy_rec( pNtk );
+    pNtk->fHiePath = 0;
+    // clear the modules
+    Vec_PtrForEachEntry( pNtk->pDesign->vModules, pTemp, i )
+        pTemp->fHieVisited = pTemp->fHiePath = 0;
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 7e57c0a4..48ffa489 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -24,20 +24,44 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void     Abc_NtkDfs_iter( Vec_Ptr_t * vStack, Abc_Obj_t * pRoot, Vec_Ptr_t * vNodes );
-static void     Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void     Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void     Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void     Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void     Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels );
-static bool     Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    assert( !Abc_ObjIsNet(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // skip the CI
+    if ( Abc_ObjIsCi(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsConst(pNode)) )
+        return;
+    assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
+    // visit the transitive fanin of the node
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the DFS ordered array of logic nodes.]
 
   Description [Collects only the internal nodes, leaving CIs and CO.
@@ -105,6 +129,7 @@ Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs DFS for one node.]
@@ -116,9 +141,9 @@ Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
-    Abc_Obj_t * pFanin;
+    Abc_Obj_t * pFanout;
     int i;
     assert( !Abc_ObjIsNet(pNode) );
     // if this node is already visited, skip
@@ -127,57 +152,57 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
     // skip the CI
-    if ( Abc_ObjIsCi(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsConst(pNode)) )
+    if ( Abc_ObjIsCo(pNode) )
         return;
-    assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
     // visit the transitive fanin of the node
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+    pNode = Abc_ObjFanout0Ntk(pNode);
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        Abc_NtkDfsReverse_rec( pFanout, vNodes );
     // add the node after the fanins have been added
     Vec_PtrPush( vNodes, pNode );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the DFS ordered array of logic nodes.]
+  Synopsis    [Returns the reverse DFS ordered array of logic nodes.]
 
-  Description [Collects only the internal nodes, leaving CIs and CO.
-  However it marks with the current TravId both CIs and COs.]
+  Description [Collects only the internal nodes, leaving out CIs/COs.
+  However it marks both CIs and COs with the current TravId.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll )
+Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
 {
-    Vec_Ptr_t * vNodes, * vStack;
-    Abc_Obj_t * pObj;
-    int i;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k;
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
-    vNodes = Vec_PtrAlloc( 1000 );
-    vStack = Vec_PtrAlloc( 1000 );
-    Abc_NtkForEachCo( pNtk, pObj, i )
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachCi( pNtk, pObj, i )
     {
         Abc_NodeSetTravIdCurrent( pObj );
-        Abc_NtkDfs_iter( vStack, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)), vNodes );
+        pObj = Abc_ObjFanout0Ntk(pObj);
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            Abc_NtkDfsReverse_rec( pFanout, vNodes );
     }
-    // collect dangling nodes if asked to
-    if ( fCollectAll )
-    {
+    // add constant nodes in the end
+    if ( !Abc_NtkIsStrash(pNtk) )
         Abc_NtkForEachNode( pNtk, pObj, i )
-            if ( !Abc_NodeIsTravIdCurrent(pObj) )
-                Abc_NtkDfs_iter( vStack, pObj, vNodes );
-    }
-    Vec_PtrFree( vStack );
+            if ( Abc_NodeIsConst(pObj) )
+                Vec_PtrPush( vNodes, pObj );
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Iterative version of the DFS procedure.]
+  Synopsis    [Performs DFS for one node.]
 
   Description []
                
@@ -186,89 +211,52 @@ Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDfs_iter( Vec_Ptr_t * vStack, Abc_Obj_t * pRoot, Vec_Ptr_t * vNodes )
+void Abc_NtkDfsSeq_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
-    Abc_Obj_t * pNode, * pFanin;
-    int iFanin;
+    Abc_Obj_t * pFanin;
+    int i;
     // if this node is already visited, skip
-    if ( Abc_NodeIsTravIdCurrent( pRoot ) )
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
         return;
     // mark the node as visited
-    Abc_NodeSetTravIdCurrent( pRoot );
-    // skip the CI
-    if ( Abc_ObjIsCi(pRoot) || (Abc_NtkIsStrash(pRoot->pNtk) && Abc_AigNodeIsConst(pRoot)) )
-        return;
-    // add the CI
-    Vec_PtrClear( vStack );
-    Vec_PtrPush( vStack, pRoot );
-    Vec_PtrPush( vStack, (void *)0 );
-    while ( Vec_PtrSize(vStack) > 0 )
-    {
-        // get the node and its fanin
-        iFanin = (int)Vec_PtrPop(vStack);
-        pNode  = Vec_PtrPop(vStack);
-        assert( !Abc_ObjIsNet(pNode) );
-        // add it to the array of nodes if we finished
-        if ( iFanin == Abc_ObjFaninNum(pNode) )
-        {
-            Vec_PtrPush( vNodes, pNode );
-            continue;
-        }
-        // explore the next fanin
-        Vec_PtrPush( vStack, pNode );
-        Vec_PtrPush( vStack, (void *)(iFanin+1) );
-        // get the fanin
-        pFanin = Abc_ObjFanin0Ntk( Abc_ObjFanin(pNode,iFanin) );
-        // if this node is already visited, skip
-        if ( Abc_NodeIsTravIdCurrent( pFanin ) )
-            continue;
-        // mark the node as visited
-        Abc_NodeSetTravIdCurrent( pFanin );
-        // skip the CI
-        if ( Abc_ObjIsCi(pFanin) || (Abc_NtkIsStrash(pFanin->pNtk) && Abc_AigNodeIsConst(pFanin)) )
-            continue;
-        Vec_PtrPush( vStack, pFanin );
-        Vec_PtrPush( vStack, (void *)0 );   
-    }
+    Abc_NodeSetTravIdCurrent( pNode );
+    // visit the transitive fanin of the node
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkDfsSeq_rec( pFanin, vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    [Returns the reverse DFS ordered array of logic nodes.]
+  Synopsis    [Returns the array of nodes and latches reachable from POs.]
 
-  Description [Collects only the internal nodes, leaving out CIs/COs.
-  However it marks both CIs and COs with the current TravId.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk )
 {
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pObj, * pFanout;
-    int i, k;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( !Abc_NtkIsNetlist(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
     vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachCi( pNtk, pObj, i )
-    {
-        Abc_NodeSetTravIdCurrent( pObj );
-        pObj = Abc_ObjFanout0Ntk(pObj);
-        Abc_ObjForEachFanout( pObj, pFanout, k )
-            Abc_NtkDfsReverse_rec( pFanout, vNodes );
-    }
-    // add constant nodes in the end
-    if ( !Abc_NtkIsStrash(pNtk) )
-        Abc_NtkForEachNode( pNtk, pObj, i )
-            if ( Abc_NodeIsConst(pObj) )
-                Vec_PtrPush( vNodes, pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDfsSeq_rec( pObj, vNodes );
+    // mark the PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDfsSeq_rec( pObj, vNodes );
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs DFS for one node.]
@@ -280,31 +268,25 @@ Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Abc_NtkDfsSeqReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanout;
     int i;
-    assert( !Abc_ObjIsNet(pNode) );
     // if this node is already visited, skip
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
         return;
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
-    // skip the CI
-    if ( Abc_ObjIsCo(pNode) )
-        return;
-    assert( Abc_ObjIsNode( pNode ) );
     // visit the transitive fanin of the node
-    pNode = Abc_ObjFanout0Ntk(pNode);
     Abc_ObjForEachFanout( pNode, pFanout, i )
-        Abc_NtkDfsReverse_rec( pFanout, vNodes );
+        Abc_NtkDfsSeqReverse_rec( pFanout, vNodes );
     // add the node after the fanins have been added
     Vec_PtrPush( vNodes, pNode );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs DFS for one node.]
+  Synopsis    [Returns the array of nodes and latches reachable from POs.]
 
   Description []
                
@@ -313,51 +295,121 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDfsSeq_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pFanin;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
     int i;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDfsSeqReverse_rec( pObj, vNodes );
+    // mark the logic feeding into POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDfsSeq_rec( pObj, vNodes );
+    return vNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Iterative version of the DFS procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfs_iter( Vec_Ptr_t * vStack, Abc_Obj_t * pRoot, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pNode, * pFanin;
+    int iFanin;
     // if this node is already visited, skip
-    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+    if ( Abc_NodeIsTravIdCurrent( pRoot ) )
         return;
     // mark the node as visited
-    Abc_NodeSetTravIdCurrent( pNode );
-    // visit the transitive fanin of the node
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_NtkDfsSeq_rec( pFanin, vNodes );
-    // add the node after the fanins have been added
-    Vec_PtrPush( vNodes, pNode );
+    Abc_NodeSetTravIdCurrent( pRoot );
+    // skip the CI
+    if ( Abc_ObjIsCi(pRoot) || (Abc_NtkIsStrash(pRoot->pNtk) && Abc_AigNodeIsConst(pRoot)) )
+        return;
+    // add the CI
+    Vec_PtrClear( vStack );
+    Vec_PtrPush( vStack, pRoot );
+    Vec_PtrPush( vStack, (void *)0 );
+    while ( Vec_PtrSize(vStack) > 0 )
+    {
+        // get the node and its fanin
+        iFanin = (int)Vec_PtrPop(vStack);
+        pNode  = Vec_PtrPop(vStack);
+        assert( !Abc_ObjIsNet(pNode) );
+        // add it to the array of nodes if we finished
+        if ( iFanin == Abc_ObjFaninNum(pNode) )
+        {
+            Vec_PtrPush( vNodes, pNode );
+            continue;
+        }
+        // explore the next fanin
+        Vec_PtrPush( vStack, pNode );
+        Vec_PtrPush( vStack, (void *)(iFanin+1) );
+        // get the fanin
+        pFanin = Abc_ObjFanin0Ntk( Abc_ObjFanin(pNode,iFanin) );
+        // if this node is already visited, skip
+        if ( Abc_NodeIsTravIdCurrent( pFanin ) )
+            continue;
+        // mark the node as visited
+        Abc_NodeSetTravIdCurrent( pFanin );
+        // skip the CI
+        if ( Abc_ObjIsCi(pFanin) || (Abc_NtkIsStrash(pFanin->pNtk) && Abc_AigNodeIsConst(pFanin)) )
+            continue;
+        Vec_PtrPush( vStack, pFanin );
+        Vec_PtrPush( vStack, (void *)0 );   
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the array of nodes and latches reachable from POs.]
+  Synopsis    [Returns the DFS ordered array of logic nodes.]
 
-  Description []
+  Description [Collects only the internal nodes, leaving CIs and CO.
+  However it marks with the current TravId both CIs and COs.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll )
 {
-    Vec_Ptr_t * vNodes;
+    Vec_Ptr_t * vNodes, * vStack;
     Abc_Obj_t * pObj;
     int i;
-    assert( !Abc_NtkIsNetlist(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkDfsSeq_rec( pObj, vNodes );
-    // mark the PIs
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkDfsSeq_rec( pObj, vNodes );
+    vNodes = Vec_PtrAlloc( 1000 );
+    vStack = Vec_PtrAlloc( 1000 );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        Abc_NodeSetTravIdCurrent( pObj );
+        Abc_NtkDfs_iter( vStack, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)), vNodes );
+    }
+    // collect dangling nodes if asked to
+    if ( fCollectAll )
+    {
+        Abc_NtkForEachNode( pNtk, pObj, i )
+            if ( !Abc_NodeIsTravIdCurrent(pObj) )
+                Abc_NtkDfs_iter( vStack, pObj, vNodes );
+    }
+    Vec_PtrFree( vStack );
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs DFS for one node.]
@@ -369,51 +421,55 @@ Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDfsSeqReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Abc_NtkDfsHie_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
-    Abc_Obj_t * pFanout;
+    Abc_Obj_t * pFanin;
     int i;
     // if this node is already visited, skip
-    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+    if ( Abc_NodeIsTravIdCurrent( pObj ) )
         return;
     // mark the node as visited
-    Abc_NodeSetTravIdCurrent( pNode );
+    Abc_NodeSetTravIdCurrent( pObj );
     // visit the transitive fanin of the node
-    Abc_ObjForEachFanout( pNode, pFanout, i )
-        Abc_NtkDfsSeqReverse_rec( pFanout, vNodes );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Abc_NtkDfsHie_rec( pFanin, vNodes );
     // add the node after the fanins have been added
-    Vec_PtrPush( vNodes, pNode );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the array of nodes and latches reachable from POs.]
+  Synopsis    [Returns the DFS ordered array of all objects.]
 
-  Description []
+  Description [This procedure collects everything from POs to PIs.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj;
     int i;
-    assert( !Abc_NtkIsNetlist(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
     vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkDfsSeqReverse_rec( pObj, vNodes );
-    // mark the logic feeding into POs
     Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkDfsSeq_rec( pObj, vNodes );
+        Abc_NtkDfsHie_rec( pObj, vNodes );
+    // collect dangling nodes if asked to
+    if ( fCollectAll )
+    {
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            if ( !Abc_NodeIsTravIdCurrent(pObj) )
+                Abc_NtkDfs_rec( pObj, vNodes );
+    }
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if the ordering of nodes is DFS.]
@@ -452,6 +508,40 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    assert( !Abc_ObjIsNet(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // collect the CI
+    if ( Abc_ObjIsCi(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+    {
+        Vec_PtrPush( vNodes, pNode );
+        return;
+    }
+    assert( Abc_ObjIsNode( pNode ) );
+    // visit the transitive fanin of the node
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkNodeSupport_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns the set of CI nodes in the support of the given nodes.]
@@ -511,6 +601,7 @@ Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNod
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs DFS for one node.]
@@ -522,29 +613,30 @@ Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNod
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanin;
     int i;
-    assert( !Abc_ObjIsNet(pNode) );
     // if this node is already visited, skip
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
         return;
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
-    // collect the CI
-    if ( Abc_ObjIsCi(pNode) || Abc_ObjFaninNum(pNode) == 0 )
-    {
-        Vec_PtrPush( vNodes, pNode );
+    // skip the PI
+    if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
         return;
-    }
     assert( Abc_ObjIsNode( pNode ) );
     // visit the transitive fanin of the node
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_NtkNodeSupport_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+        Abc_AigDfs_rec( pFanin, vNodes );
+    // visit the equivalent nodes
+    if ( Abc_AigNodeIsChoice( pNode ) )
+        for ( pFanin = pNode->pData; pFanin; pFanin = pFanin->pData )
+            Abc_AigDfs_rec( pFanin, vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Returns the DFS ordered array of logic nodes.]
@@ -585,39 +677,36 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos )
     return vNodes;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Performs DFS for one node.]
+  Synopsis    [Collects nodes in the DFS manner by level.]
 
-  Description []
+  Description [The number of levels should be set!!!]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels )
 {
-    Abc_Obj_t * pFanin;
+    Abc_Obj_t * pFanout;
     int i;
     // if this node is already visited, skip
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
         return;
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
-    // skip the PI
-    if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
+    // skip the terminals
+    if ( Abc_ObjIsCo(pNode) )
         return;
-    assert( Abc_ObjIsNode( pNode ) );
-    // visit the transitive fanin of the node
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_AigDfs_rec( pFanin, vNodes );
-    // visit the equivalent nodes
-    if ( Abc_AigNodeIsChoice( pNode ) )
-        for ( pFanin = pNode->pData; pFanin; pFanin = pFanin->pData )
-            Abc_AigDfs_rec( pFanin, vNodes );
-    // add the node after the fanins have been added
-    Vec_PtrPush( vNodes, pNode );
+    assert( Abc_ObjIsNode(pNode) );
+    // add the node to the structure
+    Vec_VecPush( vLevels, pNode->Level, pNode );
+    // visit the TFO
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        Abc_DfsLevelizedTfo_rec( pFanout, vLevels );
 }
 
 /**Function*************************************************************
@@ -653,37 +742,6 @@ Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi )
     return vLevels;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes in the DFS manner by level.]
-
-  Description [The number of levels should be set!!!]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels )
-{
-    Abc_Obj_t * pFanout;
-    int i;
-    // if this node is already visited, skip
-    if ( Abc_NodeIsTravIdCurrent( pNode ) )
-        return;
-    // mark the node as visited
-    Abc_NodeSetTravIdCurrent( pNode );
-    // skip the terminals
-    if ( Abc_ObjIsCo(pNode) )
-        return;
-    assert( Abc_ObjIsNode(pNode) );
-    // add the node to the structure
-    Vec_VecPush( vLevels, pNode->Level, pNode );
-    // visit the TFO
-    Abc_ObjForEachFanout( pNode, pFanout, i )
-        Abc_DfsLevelizedTfo_rec( pFanout, vLevels );
-}
-
 
 /**Function*************************************************************
 
@@ -823,51 +881,6 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Detects combinational loops.]
-
-  Description [This procedure is based on the idea suggested by Donald Chai. 
-  As we traverse the network and visit the nodes, we need to distinquish 
-  three types of nodes: (1) those that are visited for the first time, 
-  (2) those that have been visited in this traversal but are currently not 
-  on the traversal path, (3) those that have been visited and are currently 
-  on the travesal path. When the node of type (3) is encountered, it means 
-  that there is a combinational loop. To mark the three types of nodes, 
-  two new values of the traversal IDs are used.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int fAcyclic, i;
-    // set the traversal ID for this DFS ordering
-    Abc_NtkIncrementTravId( pNtk );   
-    Abc_NtkIncrementTravId( pNtk );   
-    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
-    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
-    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
-    // traverse the network to detect cycles
-    fAcyclic = 1;
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode));
-        if ( Abc_NodeIsTravIdPrevious(pNode) )
-            continue;
-        // traverse the output logic cone
-        if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) )
-            continue;
-        // stop as soon as the first loop is detected
-        fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(pNode) );
-        break;
-    }
-    return fAcyclic;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Recursively detects combinational loops.]
 
   Description []
@@ -919,6 +932,51 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Detects combinational loops.]
+
+  Description [This procedure is based on the idea suggested by Donald Chai. 
+  As we traverse the network and visit the nodes, we need to distinquish 
+  three types of nodes: (1) those that are visited for the first time, 
+  (2) those that have been visited in this traversal but are currently not 
+  on the traversal path, (3) those that have been visited and are currently 
+  on the travesal path. When the node of type (3) is encountered, it means 
+  that there is a combinational loop. To mark the three types of nodes, 
+  two new values of the traversal IDs are used.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int fAcyclic, i;
+    // set the traversal ID for this DFS ordering
+    Abc_NtkIncrementTravId( pNtk );   
+    Abc_NtkIncrementTravId( pNtk );   
+    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
+    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
+    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
+    // traverse the network to detect cycles
+    fAcyclic = 1;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode));
+        if ( Abc_NodeIsTravIdPrevious(pNode) )
+            continue;
+        // traverse the output logic cone
+        if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) )
+            continue;
+        // stop as soon as the first loop is detected
+        fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(pNode) );
+        break;
+    }
+    return fAcyclic;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 154fe149..ff6d0590 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -53,6 +53,8 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     {
         int x = 0; 
     }
+//    printf( "Adding fanin of %s ", Abc_ObjName(pObj) );
+//    printf( "to be %s\n", Abc_ObjName(pFanin) );
 }
 
 
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index c42cff45..a804203f 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -24,18 +24,131 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
-extern void        Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkHie, Abc_Ntk_t * pNtk );
-
-static void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Recursively flattens logic hierarchy of the netlist.]
+
+  Description [When this procedure is called, the PI/PO nets of the old 
+  netlist point to the corresponding nets of the flattened netlist.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter )
+{
+    char Suffix[1000] = {0};
+    Abc_Ntk_t * pNtkModel;
+    Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin;
+    int i, k;
+
+    // process the blackbox
+    if ( Abc_NtkHasBlackbox(pNtk) )
+    {
+        // duplicate the blackbox
+        assert( Abc_NtkBoxNum(pNtk) == 1 );
+        pObj = Abc_NtkBox( pNtk, 0 );
+        Abc_NtkDupBox( pNtkNew, pObj, 1 );
+
+        // connect blackbox fanins to the PI nets
+        assert( Abc_ObjFaninNum(pObj->pCopy) == Abc_NtkPiNum(pNtk) );
+        Abc_NtkForEachPi( pNtk, pTerm, i )
+            Abc_ObjAddFanin( Abc_ObjFanin(pObj->pCopy,i), Abc_ObjFanout0(pTerm) );
+
+        // connect blackbox fanouts to the PO nets
+        assert( Abc_ObjFanoutNum(pObj->pCopy) == Abc_NtkPoNum(pNtk) );
+        Abc_NtkForEachPo( pNtk, pTerm, i )
+            Abc_ObjAddFanin( Abc_ObjFanin0(pTerm), Abc_ObjFanout(pObj->pCopy,i) );
+        return;
+    }
+
+    (*pCounter)++;
+
+    // create the prefix, which will be appended to the internal names
+    if ( *pCounter )
+        sprintf( Suffix, "_%s_%d", Abc_NtkName(pNtk), *pCounter );
+
+    // duplicate nets of all boxes, including latches
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+        {
+            pNet = Abc_ObjFanin0(pTerm);
+            if ( pNet->pCopy )
+                continue;
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNameSuffix(pNet, Suffix) );
+        }
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+        {
+            pNet = Abc_ObjFanout0(pTerm);
+            if ( pNet->pCopy )
+                continue;
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNameSuffix(pNet, Suffix) );
+        }
+    }
+
+    // mark objects that will not be used
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+        Abc_NodeSetTravIdCurrent( pTerm );
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+        Abc_NodeSetTravIdCurrent( pTerm );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        Abc_NodeSetTravIdCurrent( pObj );
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NodeSetTravIdCurrent( pTerm );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NodeSetTravIdCurrent( pTerm );
+    }
+
+    // duplicate objects that do not have prototypes yet
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            continue;
+        if ( pObj->pCopy )
+            continue;
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    }
+
+    // connect objects
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                    Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+
+    // call recursively
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        pNtkModel = pObj->pData;
+        // check the match between the number of actual and formal parameters
+        assert( Abc_ObjFaninNum(pObj) == Abc_NtkPiNum(pNtkModel) );
+        assert( Abc_ObjFanoutNum(pObj) == Abc_NtkPoNum(pNtkModel) );
+        // clean the node copy fields
+        Abc_NtkCleanCopy( pNtkModel );
+        // map PIs/POs
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_ObjFanout0( Abc_NtkPi(pNtkModel, k) )->pCopy = Abc_ObjFanin0(pTerm)->pCopy;
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy;
+        // call recursively
+        Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Flattens the logic hierarchy of the netlist.]
 
   Description []
@@ -48,121 +161,61 @@ static void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * p
 Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pNet;
-    int i, Counter = 0;
+    Abc_Obj_t * pTerm, * pNet;
+    int i, Counter;
     assert( Abc_NtkIsNetlist(pNtk) );
+
     // start the network
     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
     // clean the node copy fields
     Abc_NtkCleanCopy( pNtk );
+
     // duplicate PIs/POs and their nets
-    Abc_NtkForEachPi( pNtk, pObj, i )
+    Abc_NtkForEachPi( pNtk, pTerm, i )
     {
-        Abc_NtkDupObj( pNtkNew, pObj, 0 );
-        pNet = Abc_ObjFanout0( pObj );
-        Abc_NtkDupObj( pNtkNew, pNet, 1 );
-        Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
+        Abc_NtkDupObj( pNtkNew, pTerm, 0 );
+        pNet = Abc_ObjFanout0( pTerm );
+        pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+        Abc_ObjAddFanin( pNet->pCopy, pTerm->pCopy );
     }
-    Abc_NtkForEachPo( pNtk, pObj, i )
+    Abc_NtkForEachPo( pNtk, pTerm, i )
     {
-        Abc_NtkDupObj( pNtkNew, pObj, 0 );
-        pNet = Abc_ObjFanin0( pObj );
+        Abc_NtkDupObj( pNtkNew, pTerm, 0 );
+        pNet = Abc_ObjFanin0( pTerm );
         pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
-        Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+        Abc_ObjAddFanin( pTerm->pCopy, pNet->pCopy );
     }
+
     // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
+    Counter = -1;
     Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter );
-    printf( "Abc_NtkFlattenLogicHierarchy(): Flattened %d logic boxes. Left %d block boxes.\n", 
-        Counter - 1, Abc_NtkBlackboxNum(pNtkNew) );
+    printf( "Abc_NtkFlattenLogicHierarchy(): Flattened %d logic instances. Preserved %d black boxes.\n", 
+        Counter, Abc_NtkBlackboxNum(pNtkNew) );
+
     // copy the timing information
 //    Abc_ManTimeDup( pNtk, pNtkNew );
     // duplicate EXDC 
     if ( pNtk->pExdc )
         printf( "EXDC is not transformed.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkFlattenLogicHierarchy(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively flattens the logic hierarchy of the netlist.]
-
-  Description [When this procedure is called, the PI/PO nets of the netlist
-  are already assigned.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Ntk_t * pNtkModel;
-    Abc_Obj_t * pObj, * pTerm, * pFanin, * pNet;
-    int i, k;
-    (*pCounter)++;
-    // collect nodes and boxes in topological order
-    vNodes = Abc_NtkDfs( pNtkOld, 0 );
-    // duplicate nodes and blackboxes, call recursively for logic boxes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        if ( Abc_ObjIsNode(pObj) )
-        {
-            // duplicate the node 
-            Abc_NtkDupObj( pNtkNew, pObj, 0 );
-            Abc_ObjForEachFanin( pObj, pNet, k )
-                Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
-            // duplicate the net
-            pNet = Abc_ObjFanout0( pObj );
-            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
-            Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
-            continue;
-        }
-        if ( Abc_ObjIsBlackbox(pObj) )
-        {
-            // duplicate the box 
-            Abc_NtkDupObj( pNtkNew, pObj, 1 );
-            // connect the fanins
-            Abc_ObjForEachFanin( pObj, pNet, k )
-                Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
-            // duplicate fanout nets and connect them
-            Abc_ObjForEachFanout( pObj, pNet, i )
-            {
-                pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
-                Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
-            }
-            continue;
-        }
-        assert( Abc_ObjIsBox(pObj) );
-        pNtkModel = pObj->pData;
-        assert( pNtkModel && !Abc_NtkHasBlackbox(pNtkModel) );
-        // clean the node copy fields
-        Abc_NtkCleanCopy( pNtkModel );
-        // consider this blackbox
-        // copy the PIs/POs of the box
-        Abc_NtkForEachPi( pNtkModel, pTerm, k )
-            Abc_ObjFanout(pTerm, k)->pCopy = Abc_ObjFanin(pObj, k);
-        Abc_NtkForEachPo( pNtkModel, pTerm, k )
-            Abc_ObjFanin(pTerm, k)->pCopy = Abc_ObjFanout(pObj, k);
-        // call recursively
-        Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter );
+        fprintf( stdout, "Abc_NtkFlattenLogicHierarchy(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
     }
-    // connect the POs
-    Abc_NtkForEachPo( pNtkOld, pTerm, k )
-        pTerm->pCopy = Abc_ObjFanin0(pTerm)->pCopy;
-    Vec_PtrFree( vNodes );
+    return pNtkNew;
 }
 
 /**Function*************************************************************
 
   Synopsis    [Extracts blackboxes by making them into additional PIs/POs.]
 
-  Description []
+  Description [The input netlist has not logic hierarchy. The resulting
+  netlist has additional PIs/POs for each blackbox input/output.]
                
   SideEffects []
 
@@ -172,68 +225,74 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld,
 Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pNet;
+    Abc_Obj_t * pObj, * pNet, * pFanin, * pTerm;
     int i, k;
+
     assert( Abc_NtkIsNetlist(pNtk) );
-    assert( Abc_NtkBlackboxNum(pNtk) == Abc_NtkBoxNum(pNtk) - Abc_NtkLatchNum(pNtk) );
+    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
+
     // start the network
     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
-    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec );
+//    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec );
+
     // clean the node copy fields
     Abc_NtkCleanCopy( pNtk );
-    // create PIs/POs for the box inputs outputs
+
+    // create PIs/POs for the box inputs/outputs
+    // mark the nodes that should not be connected
+    Abc_NtkIncrementTravId( pNtk );
     Abc_NtkForEachBlackbox( pNtk, pObj, i )
     {
-        pObj->pCopy = pObj; // placeholder
-        Abc_ObjForEachFanout( pObj, pNet, k )
+        Abc_NodeSetTravIdCurrent( pObj );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
         {
+            pNet = Abc_ObjFanout0(pTerm);
             if ( pNet->pCopy )
-                continue;
-            pNet->pCopy = Abc_NtkCreatePi( pNtkNew );
-            Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), NULL );
+            {
+                printf( "Error in Abc_NtkConvertBlackboxes(): Output %s of a black box has a non-unique name.\n", Abc_ObjName(pNet->pCopy) );
+                Abc_NtkDelete( pNtkNew );
+                return NULL;
+            }
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+            pTerm->pCopy = Abc_NtkCreatePi( pNtkNew );
+            Abc_NodeSetTravIdCurrent( pTerm );
         }
-        Abc_ObjForEachFanin( pObj, pNet, k )
+    }
+    Abc_NtkForEachBlackbox( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pTerm, k )
         {
+            pNet = Abc_ObjFanin0(pTerm);
             if ( pNet->pCopy )
+            {
+                Abc_NodeSetTravIdCurrent( pTerm );
                 continue;
-            pNet->pCopy = Abc_NtkCreatePo( pNtkNew );
-            Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), NULL );
+            }
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+            pTerm->pCopy = Abc_NtkCreatePo( pNtkNew );
         }
     }
+
     // duplicate other objects
     Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( pObj->pCopy == NULL )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) && pObj->pCopy == NULL )
             Abc_NtkDupObj( pNtkNew, pObj, Abc_ObjIsNet(pObj) );
-    // connect all objects
-
-
-
-
 
-    // duplicate all objects besides the boxes
+    // connect all objects
     Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( !Abc_ObjIsBlackbox(pObj) )
-            Abc_NtkDupObj( pNtkNew, pObj, Abc_ObjIsNet(pObj) );
-    // create PIs/POs for the nets belonging to the boxes
-    Abc_NtkForEachBlackbox( pNtk, pObj, i )
-    {
-        Abc_ObjForEachFanin( pObj, pNet, k )
-            if ( !Abc_ObjIsPi(Abc_ObjFanin0(pNet)) )
-                Abc_NtkCreatePi(pNtkNew)
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
 
-    }
-    // connect all objects, besides blackboxes
-    Abc_NtkForEachObj( pNtk, pObj, i )
+    // check integrity
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
-        if ( !Abc_ObjIsBlackbox(pObj) )
-            continue;
-        Abc_ObjForEachFanin( pObj, pNet, k )
-            Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
+        fprintf( stdout, "Abc_NtkConvertBlackboxes(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
     }
-    if ( !Abc_NtkCheck( pNtkHie ) )
-        fprintf( stdout, "Abc_NtkInsertNewLogic(): Network check has failed.\n" );
     return pNtkNew;
 }
 
@@ -242,99 +301,129 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk )
   Synopsis    [Inserts blackboxes into the netlist.]
 
   Description [The first arg is the netlist with blackboxes without logic hierarchy.
-  The second arg is a non-hierarchical netlist derived from logic network after processing.
-  This procedure inserts the logic back into the original hierarhical netlist.
-  The result is updated original hierarchical netlist.]
+  The second arg is a non-hierarchical netlist derived from the above netlist after processing.
+  This procedure create a new netlist, which is comparable to the original netlist with
+  blackboxes, except that it contains logic nodes from the netlist after processing.]
                
-  SideEffects []
+  SideEffects [This procedure silently assumes that blackboxes appear
+  only in the top-level model. If they appear in other models as well, 
+  the name of the model and its number were appended to the names of 
+  blackbox inputs/outputs.]
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkHie, Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL )
 {
-    Abc_Obj_t * pObj, * pNet, * pNetLogic;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjH, * pObjL, * pNetH, * pNetL, * pTermH;
     int i, k;
-    assert( Abc_NtkIsNetlist(pNtkHie) );
-    assert( Abc_NtkIsNetlist(pNtk) );
-    assert( Abc_NtkBlackboxNum(pNtk) == 0 );
-    Abc_NtkCleanCopy( pNtk );
-    // mark PIs/POs/blackboxes and their nets
-    // map the nets into the corresponding nets of the logic design
-    Abc_NtkForEachPi( pNtkHie, pObj, i )
+
+    assert( Abc_NtkIsNetlist(pNtkH) );
+    assert( Abc_NtkWhiteboxNum(pNtkH) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtkL) > 0 );
+
+    assert( Abc_NtkIsNetlist(pNtkL) );
+    assert( Abc_NtkWhiteboxNum(pNtkL) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtkL) == 0 );
+
+    // prepare the logic network for copying
+    Abc_NtkCleanCopy( pNtkL );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtkH->ntkType, pNtkH->ntkFunc, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav( pNtkH->pName );
+    pNtkNew->pSpec = Extra_UtilStrsav( pNtkH->pSpec );
+
+    // make sure every PI/PO has a PI/PO in the processed network
+    Abc_NtkForEachPi( pNtkH, pObjH, i )
     {
-        pObj->fMarkA = 1;
-        pNet = Abc_ObjFanout0(pObj);
-        pNet->fMarkA = 1;
-        pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
-        assert( pNetLogic );
-        pNetLogic->pCopy = pNet;
+        pNetH = Abc_ObjFanout0(pObjH);
+        pNetL = Abc_NtkFindNet( pNtkL, Abc_ObjName(pNetH) );
+        if ( pNetL == NULL || !Abc_ObjIsPi( Abc_ObjFanin0(pNetL) ) )
+        {
+            printf( "There is no PI corresponding to the PI %s.\n", Abc_ObjName(pNetH) );
+            Abc_NtkDelete( pNtkNew );
+            return NULL;
+        }
+        // duplicate 
+        pNetL->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNetH) );
+        Abc_NtkDupObj( pNtkNew, Abc_ObjFanin0(pNetL), 0 );
     }
-    Abc_NtkForEachPo( pNtkHie, pObj, i )
+    Abc_NtkForEachPo( pNtkH, pObjH, i )
     {
-        pObj->fMarkA = 1;
-        pNet = Abc_ObjFanin0(pObj);
-        pNet->fMarkA = 1;
-        pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
-        assert( pNetLogic );
-        pNetLogic->pCopy = pNet;
+        pNetH = Abc_ObjFanin0(pObjH);
+        pNetL = Abc_NtkFindNet( pNtkL, Abc_ObjName(pNetH) );
+        if ( pNetL == NULL || !Abc_ObjIsPo( Abc_ObjFanout0(pNetL) ) )
+        {
+            printf( "There is no PO corresponding to the PO %s.\n", Abc_ObjName(pNetH) );
+            Abc_NtkDelete( pNtkNew );
+            return NULL;
+        }
+        // duplicate 
+        pNetL->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNetH) );
+        Abc_NtkDupObj( pNtkNew, Abc_ObjFanout0(pNetL), 0 );
     }
-    Abc_NtkForEachBlackbox( pNtkHie, pObj, i )
+
+    // make sure every BB has a PI/PO in the processed network
+    Abc_NtkForEachBlackbox( pNtkH, pObjH, i )
     {
-        pObj->fMarkA = 1;
-        Abc_ObjForEachFanin( pObj, pNet, k )
+        // duplicate the box 
+        Abc_NtkDupObj( pNtkNew, pObjH, 1 );
+        // look and fanins/fanouts of the box
+        Abc_ObjForEachFanin( pObjH, pTermH, k )
         {
-            pNet->fMarkA = 1;
-            pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
-            assert( pNetLogic );
-            pNetLogic->pCopy = pNet;
+            pNetH = Abc_ObjFanin0( pTermH );
+            pNetL = Abc_NtkFindNet( pNtkL, Abc_ObjName(pNetH) );
+            if ( pNetL == NULL || !Abc_ObjIsPo( Abc_ObjFanout0(pNetL) ) )
+            {
+                printf( "There is no PO corresponding to the input %s of blackbox %s.\n", Abc_ObjName(pNetH), Abc_ObjName(pObjH) );
+                Abc_NtkDelete( pNtkNew );
+                return NULL;
+            }
+            // duplicate 
+            pNetL->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNetH) );
+            Abc_NtkDupObj( pNtkNew, Abc_ObjFanout0(pNetL), 0 );
+            // connect 
+            Abc_ObjAddFanin( pObjH->pCopy, Abc_ObjFanout0(pNetL)->pCopy );
         }
-        Abc_ObjForEachFanout( pObj, pNet, k )
+        Abc_ObjForEachFanout( pObjH, pTermH, k )
         {
-            pNet->fMarkA = 1;
-            pNetLogic = Abc_NtkFindNet( pNtk, Abc_ObjName(pNet) );
-            assert( pNetLogic );
-            pNetLogic->pCopy = pNet;
+            pNetH = Abc_ObjFanout0( pTermH );
+            pNetL = Abc_NtkFindNet( pNtkL, Abc_ObjName(pNetH) );
+            if ( pNetL == NULL || !Abc_ObjIsPi( Abc_ObjFanin0(pNetL) ) )
+            {
+                printf( "There is no PI corresponding to the inpout %s of blackbox %s.\n", Abc_ObjName(pNetH), Abc_ObjName(pObjH) );
+                Abc_NtkDelete( pNtkNew );
+                return NULL;
+            }
+            // duplicate 
+            pNetL->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNetH) );
+            Abc_NtkDupObj( pNtkNew, Abc_ObjFanin0(pNetL), 0 );
+            // connect 
+            Abc_ObjAddFanin( Abc_ObjFanin0(pNetL)->pCopy, pObjH->pCopy );
         }
     }
-    // remove all other logic fro the hierarchical netlist
-    Abc_NtkForEachObj( pNtkHie, pObj, i )
-    {
-        if ( pObj->fMarkA )
-            pObj->fMarkA = 0;
-        else
-            Abc_NtkDeleteObj( pObj );
-    }
-    // mark PI/PO nets of the network
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_ObjFanout0(pObj)->fMarkA = 1;
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_ObjFanin0(pObj)->fMarkA = 1;
-    // make sure only these nodes are assigned the copy
-    Abc_NtkForEachObj( pNtk, pObj, i )
-    {
-        assert( pObj->fMarkA == (pObj->pCopy != NULL) );
-        pObj->fMarkA = 0;
-        if ( pObj->pCopy )
-            continue;
-        if ( Abc_ObjIsPi(pObj) || Abc_ObjIsPi(pObj) )
-            continue;
-        Abc_NtkDupObj( pNtkHie, pObj, 0 );
-    }
-    // connect all the nodes, except the PIs and POs
-    Abc_NtkForEachObj( pNtk, pObj, i )
-    {
-        if ( Abc_ObjIsPi(pObj) || Abc_ObjIsPi(pObj) )
-            continue;
-        Abc_ObjForEachFanin( pObj, pNet, k )
-            Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
-    }
-    if ( !Abc_NtkCheck( pNtkHie ) )
+
+    // duplicate other objects of the logic network
+    Abc_NtkForEachObj( pNtkL, pObjL, i )
+        if ( pObjL->pCopy )
+            Abc_NtkDupObj( pNtkNew, pObjL, 0 );
+
+    // connect objects
+    Abc_NtkForEachObj( pNtkL, pObjL, i )
+        Abc_ObjForEachFanin( pObjL, pNetL, k )
+            Abc_ObjAddFanin( pObjL->pCopy, pNetL->pCopy );
+
+    // check integrity
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         fprintf( stdout, "Abc_NtkInsertNewLogic(): Network check has failed.\n" );
-        return 0;
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
     }
-    return 1;
+    return pNtkNew;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 773ef2df..b31fed6b 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -64,7 +64,7 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_LibFree( Abc_Lib_t * pLib )
+void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
 {
     Abc_Ntk_t * pNtk;
     int i;
@@ -79,6 +79,8 @@ void Abc_LibFree( Abc_Lib_t * pLib )
         Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
         {
 //            pNtk->pManFunc = NULL;
+            if ( pNtk == pNtkSave )
+                continue;
             Abc_NtkDelete( pNtk );
         }
         Vec_PtrFree( pLib->vModules );
@@ -108,11 +110,15 @@ void Abc_LibPrint( Abc_Lib_t * pLib )
     Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
     {
         printf( "%2d : %20s   ", i+1, pNtk->pName );
-        printf( "nd = %6d   lat = %6d   box = %3d\n", Abc_NtkNodeNum(pNtk), Abc_NtkLatchNum(pNtk), Abc_NtkBlackboxNum(pNtk) );
+        printf( "nd = %6d   lat = %6d   whitebox = %3d   blackbox = %3d\n", 
+            Abc_NtkNodeNum(pNtk), Abc_NtkLatchNum(pNtk), 
+            Abc_NtkWhiteboxNum(pNtk), Abc_NtkBlackboxNum(pNtk) );
         if ( Abc_NtkBlackboxNum(pNtk) == 0 )
             continue;
+        Abc_NtkForEachWhitebox( pNtk, pObj, k )
+            printf( "     %20s (whitebox)\n", Abc_NtkName(pObj->pData) );
         Abc_NtkForEachBlackbox( pNtk, pObj, k )
-            printf( "     %20s (submodel)\n", Abc_NtkName(pObj->pData) );
+            printf( "     %20s (blackbox)\n", Abc_NtkName(pObj->pData) );
     }
 }
 
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 2029994c..a649fe43 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -414,9 +414,9 @@ void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pObj, * pTerm;
-    int nDigits, nDigitsF, i, k;
-    char * pName;
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    assert( !Abc_NtkIsNetlist(pNtk) );
     nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pObj, i )
     {
@@ -424,14 +424,7 @@ void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk )
         Abc_ObjAssignName( Abc_ObjFanin0(pObj),  Abc_ObjNameDummy("Li", i, nDigits), NULL );
         Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjNameDummy("Lo", i, nDigits), NULL );
     }
-    nDigits = Extra_Base10Log( Abc_NtkTriNum(pNtk) );
-    Abc_NtkForEachTri( pNtk, pObj, i )
-    {
-        Abc_ObjAssignName( pObj, Abc_ObjNameDummy("T", i, nDigits), NULL );
-        Abc_ObjAssignName( Abc_ObjFanin0(pObj),  Abc_ObjNameDummy("Ti0", i, nDigits), NULL );
-        Abc_ObjAssignName( Abc_ObjFanin1(pObj),  Abc_ObjNameDummy("Ti1", i, nDigits), NULL );
-        Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjNameDummy("To", i, nDigits), NULL );
-    }
+/*
     nDigits = Extra_Base10Log( Abc_NtkBlackboxNum(pNtk) );
     Abc_NtkForEachBlackbox( pNtk, pObj, i )
     {
@@ -443,6 +436,7 @@ void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk )
         Abc_ObjForEachFanout( pObj, pTerm, k )
             Abc_ObjAssignName( Abc_ObjFanin0(pObj), pName, Abc_ObjNameDummy("o", k, nDigitsF) );
     }
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 2a20617c..30c7d621 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -49,7 +49,8 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     int i, k;
     assert( Abc_NtkIsNetlist(pNtk) );
     // consider simple case when there is hierarchy
-    assert( pNtk->tName2Model == NULL );
+    assert( pNtk->pDesign == NULL );
+//    assert( pNtk->tName2Model == NULL );
 //    if ( pNtk->tName2Model )
 //        return Abc_NtkNetlistToLogicHie( pNtk );
     // start the network
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 5e5cee69..66426268 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -840,17 +840,13 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     // free the hierarchy
-    if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
+    if ( pNtk->pDesign )
     {
-        stmm_generator * gen;
-        Abc_Ntk_t * pNtkTemp;
-        char * pName;
-        stmm_foreach_item( pNtk->tName2Model, gen, &pName, (char **)&pNtkTemp )
-            Abc_NtkDelete( pNtkTemp );
-        stmm_free_table( pNtk->tName2Model );
+        Abc_LibFree( pNtk->pDesign, pNtk );
+        pNtk->pDesign = NULL;
     }
-    if ( pNtk->pBlackBoxes ) 
-        Vec_IntFree( pNtk->pBlackBoxes );
+//    if ( pNtk->pBlackBoxes ) 
+//        Vec_IntFree( pNtk->pBlackBoxes );
     // free node attributes
     Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i )
         if ( pAttrMan )
@@ -879,7 +875,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
 
     if ( Abc_NtkNodeNum(pNtk) == 0 )
     {
-        pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
+//        pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
         return;
     }
 
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 8d347404..d55ccfcf 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -140,11 +140,10 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
             break;
         case ABC_OBJ_NET:  
         case ABC_OBJ_NODE: 
-        case ABC_OBJ_GATE: 
             break;
         case ABC_OBJ_LATCH:     
             pObj->pData = (void *)ABC_INIT_NONE;
-        case ABC_OBJ_TRI:     
+        case ABC_OBJ_WHITEBOX:     
         case ABC_OBJ_BLACKBOX:     
             if ( pNtk->vBoxes ) Vec_PtrPush( pNtk->vBoxes, pObj );
             break;
@@ -220,7 +219,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
             Vec_PtrRemove( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_NET:  
-        case ABC_OBJ_GATE:  
             break;
         case ABC_OBJ_NODE: 
             if ( Abc_NtkHasBdd(pNtk) )
@@ -228,7 +226,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
             pObj->pData = NULL;
             break;
         case ABC_OBJ_LATCH:     
-        case ABC_OBJ_TRI:     
+        case ABC_OBJ_WHITEBOX:     
         case ABC_OBJ_BLACKBOX:     
             if ( pNtk->vBoxes ) Vec_PtrRemove( pNtk->vBoxes, pObj );
             break;
@@ -324,9 +322,15 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
     if ( fCopyName )
     {
         if ( Abc_ObjIsCi(pObj) )
-            Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL );
+        {
+            if ( !Abc_NtkIsNetlist(pNtkNew) )
+                Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL );
+        }
         else if ( Abc_ObjIsCo(pObj) )
-            Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL );
+        {
+            if ( !Abc_NtkIsNetlist(pNtkNew) )
+                Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL );
+        }
         else if ( Abc_ObjIsBox(pObj) || Abc_ObjIsNet(pObj) )
             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
     }
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 4e9a6548..0836bb89 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -840,6 +840,12 @@ char * Abc_SopFromTruthBin( char * pTruth )
         if ( Digit == 1 )
             Vec_IntPush( vMints, nTruthSize - 1 - i );
     }
+    if ( Vec_IntSize( vMints ) == 0 || Vec_IntSize( vMints ) == nTruthSize )
+    {
+        Vec_IntFree( vMints );
+        printf( "Cannot create constant function.\n" );
+        return NULL;
+    }
 
     // create the SOP representation of the minterms
     Length = Vec_IntSize(vMints) * (nVars + 3);
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 3070e01a..f5c5536a 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -735,6 +735,12 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
     Abc_NtkIncrementTravId( pNtk );
     Abc_NtkForEachCo( pNtk, pNode, i ) 
     {
+/*
+        if ( strcmp( Abc_ObjName(pNode), "g704" ) == 0 )
+        {
+            int s = 1;
+        }
+*/
         // if the driver is complemented, this is an error
         pDriver = Abc_ObjFanin0(pNode);
         if ( Abc_ObjFaninC0(pNode) )
@@ -1564,6 +1570,31 @@ int Abc_NtkCrossCut( Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Prints all 3-var functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrint256()
+{
+    FILE * pFile;
+    int i;
+    pFile = fopen( "4varfs.txt", "w" );
+    for ( i = 1; i < (1<<16)-1; i++ )
+    {
+        fprintf( pFile, "read_truth " );
+        Extra_PrintBinary( pFile, &i, 16 );
+        fprintf( pFile, "; clp; st; w 1.blif; map; cec 1.blif\n" );
+    }
+    fclose( pFile );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index 113b1f08..5edf9000 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -3,6 +3,7 @@ SRC +=    src/base/abc/abcAig.c \
     src/base/abc/abcDfs.c \
     src/base/abc/abcFanio.c \
     src/base/abc/abcFunc.c \
+    src/base/abc/abcHie.c \
     src/base/abc/abcLatch.c \
     src/base/abc/abcLib.c \
     src/base/abc/abcMinBase.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f1ec7920..30602af5 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -288,7 +288,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Map_Var3Print();
 //    Map_Var4Test();
 
-}
+//    Abc_NtkPrint256();
+} 
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 177c269b..59ce1674 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -896,14 +896,11 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
         case ABC_OBJ_NODE: 
             fprintf( pFile, "Node   " );  
             break;
-        case ABC_OBJ_GATE: 
-            fprintf( pFile, "Gate   " );  
-            break;
         case ABC_OBJ_LATCH:     
             fprintf( pFile, "Latch  " );  
             break;
-        case ABC_OBJ_TRI:     
-            fprintf( pFile, "Tristate" );  
+        case ABC_OBJ_WHITEBOX: 
+            fprintf( pFile, "Whitebox" );  
             break;
         case ABC_OBJ_BLACKBOX:     
             fprintf( pFile, "Blackbox" );  
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index b6aecef9..2ce80a8f 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -218,7 +218,6 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
 ***********************************************************************/
 void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, bool fAllNodes )
 {
-    extern Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
     ProgressBar * pProgress;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNodeOld;
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 6e470aa8..08584290 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1271,7 +1271,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
         goto usage;
     }
-    Io_WriteBlifNetlist( pNetlist, "_sis_in.blif", 1 );
+    Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
     // create the file for sis
@@ -1412,7 +1412,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
         goto usage;
     }
-    Io_WriteBlifNetlist( pNetlist, "_mvsis_in.blif", 1 );
+    Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
     // create the file for MVSIS
@@ -1558,7 +1558,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
         goto usage;
     }
-    Io_WriteBlifNetlist( pNetlist, "_capo_in.blif", 1 );
+    Io_WriteBlif( pNetlist, "_capo_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
     // create the file for Capo
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 8d5b8ad6..64451118 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -40,6 +40,7 @@ static int IoCommandReadVer     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerLib  ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWrite       ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteHie    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteAiger  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBaf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -75,7 +76,7 @@ extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fC
 void Io_Init( Abc_Frame_t * pAbc )
 {
     Cmd_CommandAdd( pAbc, "I/O", "read",          IoCommandRead,         1 );
-    Cmd_CommandAdd( pAbc, "I/O", "rh",            IoCommandReadHie,      1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_hie",      IoCommandReadHie,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_aiger",    IoCommandReadAiger,    1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_baf",      IoCommandReadBaf,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
@@ -89,6 +90,7 @@ void Io_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "I/O", "read_verlib",   IoCommandReadVerLib,   0 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_hie",     IoCommandWriteHie,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_aiger",   IoCommandWriteAiger,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_baf",     IoCommandWriteBaf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
@@ -169,6 +171,7 @@ usage:
     fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
     fprintf( pAbc->Err, "\t         replaces the current network by the network read from <file>\n" );
     fprintf( pAbc->Err, "\t         by calling the parser that matches the extension of <file>\n" );
+    fprintf( pAbc->Err, "\t         (to read a hierarchical design, use \"read_hie\")\n" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
@@ -190,7 +193,7 @@ int IoCommandReadHie( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
     char * pFileName;
-    int fCheck, fBlifMv;
+    int fCheck;
     int c;
 
     fCheck = 1;
@@ -213,18 +216,7 @@ int IoCommandReadHie( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the input file name
     pFileName = argv[globalUtilOptind];
     // read the file using the corresponding file reader
-//    pNtk = Io_Read( pFileName, Io_ReadFileType(pFileName), fCheck );
-    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
-        fBlifMv = 1;
-    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
-        fBlifMv = 0;
-    else
-    {
-        printf( "Wrong file type.\n" );
-        return 1;
-    }
-    Io_ReadBlifMv( pFileName, fBlifMv, fCheck );
-    pNtk = NULL;
+    pNtk = Io_ReadHie( pFileName, Io_ReadFileType(pFileName), fCheck );
     if ( pNtk == NULL )
         return 0;
     // replace the current network
@@ -232,7 +224,7 @@ int IoCommandReadHie( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: rh [-ch] <file>\n" );
+    fprintf( pAbc->Err, "usage: read_hie [-ch] <file>\n" );
     fprintf( pAbc->Err, "\t         reads hierarchical design represented in BLIF or BLIF-MV\n" );
     fprintf( pAbc->Err, "\t         by calling the parser that matches the extension of <file>\n" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
@@ -820,7 +812,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // derive root design
     pNtk = Abc_LibDeriveRoot( pDesign );
-    Abc_LibFree( pDesign );
+    Abc_LibFree( pDesign, NULL );
     if ( pNtk == NULL )
     {
         fprintf( pAbc->Err, "Deriving root module has failed.\n" );
@@ -910,7 +902,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     printf( "The library contains %d gates.\n", st_count(pLibrary->tModules) );
     // free old library
     if ( Abc_FrameReadLibVer() )
-        Abc_LibFree( Abc_FrameReadLibVer() );
+        Abc_LibFree( Abc_FrameReadLibVer(), NULL );
     // read new library
     Abc_FrameSetLibVer( pLibrary );
     return 0;
@@ -980,6 +972,53 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    char * pBaseName, * pFileName;
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 2 )
+        goto usage;
+    // get the output file name
+    pBaseName = argv[globalUtilOptind];
+    pFileName = argv[globalUtilOptind+1];
+    // call the corresponding file writer
+//    Io_Write( pAbc->pNtkCur, pFileName, Io_ReadFileType(pFileName) );
+    Io_WriteHie( pAbc->pNtkCur, pFileName, Io_ReadFileType(pFileName), pBaseName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_hie [-h] <orig> <file>\n" );
+    fprintf( pAbc->Err, "\t         writes the current network into <file> by calling\n" );
+    fprintf( pAbc->Err, "\t         the hierarchical writer that matches the extension of <file>\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\torig   : the name of the original file with the hierarchical design\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 78bc4563..91be5ee5 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -75,7 +75,7 @@ extern Abc_Ntk_t *        Io_ReadBaf( char * pFileName, int fCheck );
 /*=== abcReadBlif.c ===========================================================*/
 extern Abc_Ntk_t *        Io_ReadBlif( char * pFileName, int fCheck );
 /*=== abcReadBlifMv.c =========================================================*/
-extern Abc_Lib_t *        Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck );
+extern Abc_Ntk_t *        Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck );
 /*=== abcReadBench.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadBench( char * pFileName, int fCheck );
 /*=== abcReadEdif.c ===========================================================*/
@@ -92,7 +92,7 @@ extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName );
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBlif.c ==========================================================*/
 extern void               Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
-extern void               Io_WriteBlifNetlist( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
+extern void               Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
 extern void               Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
 /*=== abcWriteBlifMv.c ==========================================================*/ 
 extern void               Io_WriteBlifMvDesign( Abc_Lib_t * pLib, char * FileName );
@@ -119,7 +119,9 @@ extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, in
 extern Io_FileType_t      Io_ReadFileType( char * pFileName );
 extern Abc_Ntk_t *        Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck );
 extern Abc_Ntk_t *        Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck );
+extern Abc_Ntk_t *        Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck );
 extern void               Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType );
+extern void               Io_WriteHie( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType, char * pBaseName );
 extern Abc_Obj_t *        Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 5eb9a4ce..d0750178 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -157,6 +157,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
             p->pNtkMaster = pNtkMaster = pNtk;
             continue;
         }
+/*
         // make sure hierarchy does not have the network with this name
         if ( pNtkMaster->tName2Model && stmm_is_member( pNtkMaster->tName2Model, pNtk->pName ) )
         {
@@ -172,8 +173,9 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
         if ( pNtkMaster->tName2Model == NULL )
             pNtkMaster->tName2Model = stmm_init_table(strcmp, stmm_strhash);
         stmm_insert( pNtkMaster->tName2Model, pNtk->pName, (char *)pNtk );
+*/
     }
-
+/*
     // if there is a hierarchy, connect the boxes
     if ( pNtkMaster && pNtkMaster->tName2Model )
     {
@@ -183,7 +185,9 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
             return NULL;
         }
     }
-    else if ( !p->fError )
+    else 
+*/
+    if ( !p->fError )
         Abc_NtkFinalizeRead( pNtkMaster );
     // return the master network
     return pNtkMaster;
@@ -252,8 +256,8 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
             fStatus = Io_ReadBlifNetworkInputArrival( p, p->vTokens );
         else if ( !strcmp( pDirective, ".default_input_arrival" ) )
             fStatus = Io_ReadBlifNetworkDefaultInputArrival( p, p->vTokens );
-        else if ( !strcmp( pDirective, ".subckt" ) )
-            fStatus = Io_ReadBlifNetworkSubcircuit( p, p->vTokens );
+//        else if ( !strcmp( pDirective, ".subckt" ) )
+//            fStatus = Io_ReadBlifNetworkSubcircuit( p, p->vTokens );
         else if ( !strcmp( pDirective, ".exdc" ) )
             break;
         else if ( !strcmp( pDirective, ".end" ) )
@@ -1064,6 +1068,8 @@ int Io_ReadBlifNetworkConnectBoxesOne( Io_ReadBlif_t * p, Abc_Ntk_t * pNtk, stmm
     return 0;
 }
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Connect the boxes in the hierarchy of networks.]
@@ -1090,6 +1096,8 @@ int Io_ReadBlifNetworkConnectBoxes( Io_ReadBlif_t * p, Abc_Ntk_t * pNtkMaster )
     return 0;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index e6831dba..99656422 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -119,12 +119,12 @@ extern void              Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Lib_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
+Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
 {
     FILE * pFile;
     Io_MvMan_t * p;
-    Abc_Lib_t * pDesign;
     Abc_Ntk_t * pNtk;
+    Abc_Lib_t * pDesign;
     char * pDesignName;
     int i;
 
@@ -171,18 +171,33 @@ Abc_Lib_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
             if ( !Abc_NtkCheckRead( pNtk ) )
             {
                 printf( "Io_ReadBlifMv: The network check has failed for network %s.\n", pNtk->pName );
-                Abc_LibFree( pDesign );
+                Abc_LibFree( pDesign, NULL );
                 return NULL;
             }
         }
     }
 // pDesign should be linked to all models of the design
 
-Io_WriteBlifMvDesign( pDesign, "_temp_.mv" );
-Abc_LibPrint( pDesign );
-Abc_LibFree( pDesign );
-return NULL;
-//    return pDesign;
+    // extract the master network
+    pNtk = Vec_PtrEntry( pDesign->vModules, 0 );
+    pNtk->pDesign = pDesign;
+
+    // verify the design for cyclic dependence
+    assert( Vec_PtrSize(pDesign->vModules) > 0 );
+    if ( Vec_PtrSize(pDesign->vModules) == 1 )
+    {
+        printf( "Warning: The design is not hierarchical.\n" );
+        Abc_LibFree( pDesign, pNtk );
+        pNtk->pDesign = NULL;
+    }
+    else
+        Abc_NtkIsAcyclicHierarchy( pNtk );
+
+//Io_WriteBlifMvDesign( pDesign, "_temp_.mv" );
+//Abc_LibPrint( pDesign );
+//Abc_LibFree( pDesign );
+//return NULL;
+    return pNtk;
 }
 
 /**Function*************************************************************
@@ -225,7 +240,7 @@ static void Io_MvFree( Io_MvMan_t * p )
     Io_MvMod_t * pMod;
     int i;
     if ( p->pDesign )
-        Abc_LibFree( p->pDesign );
+        Abc_LibFree( p->pDesign, NULL );
     if ( p->pBuffer )  
         free( p->pBuffer );
     if ( p->vLines )
@@ -899,7 +914,10 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
     ppNames = (char **)Vec_PtrArray(vTokens) + 2 + p->pMan->fBlifMv;
 
     // create the box with these terminals
-    pBox = Abc_NtkCreateBlackbox( p->pNtk );
+    if ( Abc_NtkHasBlackbox(pModel) )
+        pBox = Abc_NtkCreateBlackbox( p->pNtk );
+    else
+        pBox = Abc_NtkCreateWhitebox( p->pNtk );
     pBox->pData = pModel;
     if ( p->pMan->fBlifMv )
         Abc_ObjAssignName( pBox, Vec_PtrEntry(vTokens,2), NULL );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index ed197ab4..ca9f06b4 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -179,6 +179,69 @@ Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck )
 
 /**Function*************************************************************
 
+  Synopsis    [Read the network from a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    // detect the file type
+
+    if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
+        pNtk = Io_ReadBlifMv( pFileName, 0, fCheck );
+//    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
+//        pNtk = Io_ReadBlifMv( pFileName, 1, fCheck );
+    else
+    {
+        printf( "Wrong file type.\n" );
+        return NULL;
+    }
+    if ( pNtk == NULL )
+        return NULL;
+//    printf( "\n" );
+    // flatten logic hierarchy
+    assert( Abc_NtkIsNetlist(pNtk) );
+    if ( Abc_NtkWhiteboxNum(pNtk) > 0 )
+    {
+        pNtk = Abc_NtkFlattenLogicHierarchy( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+        if ( pNtk == NULL )
+        {
+            fprintf( stdout, "Flattening logic hierarchy has failed.\n" );
+            return NULL;
+        }
+    }
+    // convert blackboxes
+    if ( Abc_NtkBlackboxNum(pNtk) > 0 )
+    {
+        printf( "Hierarchical parser is converting %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+        if ( pNtk == NULL )
+        {
+            fprintf( stdout, "Converting blackboxes has failed.\n" );
+            return NULL;
+        }
+    }
+    // convert the netlist into the logic network
+    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    Abc_NtkDelete( pTemp );
+    if ( pNtk == NULL )
+    {
+        fprintf( stdout, "Converting netlist to logic network after reading has failed.\n" );
+        return NULL;
+    }
+    return pNtk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Write the network into file.]
 
   Description []
@@ -269,7 +332,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
         return;
     }
     if ( FileType == IO_FILE_BLIF )
-        Io_WriteBlifNetlist( pNtkTemp, pFileName, 1 );
+        Io_WriteBlif( pNtkTemp, pFileName, 1 );
     else if ( FileType == IO_FILE_BENCH )
         Io_WriteBench( pNtkTemp, pFileName );
     else if ( FileType == IO_FILE_PLA )
@@ -293,6 +356,63 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
 
 /**Function*************************************************************
 
+  Synopsis    [Write the network into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteHie( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType, char * pBaseName )
+{
+    Abc_Ntk_t * pNtkTemp, * pNtkBase, * pNtkResult;
+    // check if the current network is available
+    if ( pNtk == NULL )
+    {
+        fprintf( stdout, "Empty network.\n" );
+        return;
+    }
+    // check if the file extension if given
+    if ( FileType == IO_FILE_NONE || FileType == IO_FILE_UNKNOWN )
+    {
+        fprintf( stdout, "The generic file writer requires a known file extension.\n" );
+        return;
+    }
+    // write the AIG formats
+    if ( FileType == IO_FILE_BLIF )
+    {
+        pNtkBase = Io_ReadBlifMv( pBaseName, 0, 1 );
+        if ( Abc_NtkWhiteboxNum(pNtk) > 0 )
+        {
+            pNtkBase = Abc_NtkFlattenLogicHierarchy( pNtkTemp = pNtkBase );
+            Abc_NtkDelete( pNtkTemp );
+        }
+        if ( Abc_NtkBlackboxNum(pNtk) > 0 )
+        {
+            pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 );
+            pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult );
+            Abc_NtkDelete( pNtkTemp );
+            printf( "Hierarchy writer reintroduced %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        }
+        else
+        {
+            printf( "Warning: The output network does not contain blackboxes.\n" );
+            pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 );
+        }
+        Abc_NtkDelete( pNtkBase );
+        if ( pNtkResult == NULL )
+            return;
+        Io_WriteBlif( pNtkResult, pFileName, 0 );
+        Abc_NtkDelete( pNtkResult );
+    }
+    else 
+        fprintf( stderr, "Unknown file format.\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates PI terminal and net.]
 
   Description []
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 3b8c41fa..7c9db8bb 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -61,7 +61,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
         fprintf( stdout, "Writing BLIF has failed.\n" );
         return;
     }
-    Io_WriteBlifNetlist( pNtkTemp, FileName, fWriteLatches );
+    Io_WriteBlif( pNtkTemp, FileName, fWriteLatches );
     Abc_NtkDelete( pNtkTemp );
 }
 
@@ -76,28 +76,34 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteBlifNetlist( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
+void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
-    stmm_generator * gen;
-    Abc_Ntk_t * pNtkTemp;
     FILE * pFile;
     assert( Abc_NtkIsNetlist(pNtk) );
     // start writing the file
     pFile = fopen( FileName, "w" );
     if ( pFile == NULL )
     {
-        fprintf( stdout, "Io_WriteBlifNetlist(): Cannot open the output file.\n" );
+        fprintf( stdout, "Io_WriteBlif(): Cannot open the output file.\n" );
         return;
     }
     fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     // write the master network
     Io_NtkWrite( pFile, pNtk, fWriteLatches );
+    // make sure there is no logic hierarchy
+    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
     // write the hierarchy if present
-    if ( pNtk->tName2Model )
+    if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
-        fprintf( pFile, "\n\n" );
-        stmm_foreach_item( pNtk->tName2Model, gen, NULL, (char **)&pNtkTemp )
+        Abc_Ntk_t * pNtkTemp;
+        Abc_Obj_t * pObj;
+        int i;
+        Abc_NtkForEachBlackbox( pNtk, pObj, i )
+        {
+            pNtkTemp = pObj->pData;
+            assert( pNtkTemp != NULL && Abc_NtkHasBlackbox(pNtkTemp) );
             Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
+        }
     }
     fclose( pFile );
 }
diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c
index dc3a8b2d..1c7e7bed 100644
--- a/src/base/io/ioWriteBlifMv.c
+++ b/src/base/io/ioWriteBlifMv.c
@@ -187,7 +187,8 @@ void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk )
     }
 
     // write the subcircuits
-    if ( !Abc_NtkBlackboxNum(pNtk) )
+    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
+    if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
         fprintf( pFile, "\n" );
         Abc_NtkForEachBlackbox( pNtk, pNode, i )
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 46834e3f..166925e4 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -142,7 +142,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     undefine_cube_size();
     Rwt_ManGlobalStop();
 //    Ivy_TruthManStop();
-    if ( p->pLibVer ) Abc_LibFree( p->pLibVer );
+    if ( p->pLibVer ) Abc_LibFree( p->pLibVer, NULL );
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 9048337b..bbef90be 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -220,7 +220,7 @@ void Ver_ParseFreeData( Ver_Man_t * p )
     }
     if ( p->pDesign )
     {
-        Abc_LibFree( p->pDesign );
+        Abc_LibFree( p->pDesign, NULL );
         p->pDesign = NULL;
     }
 }
diff --git a/src/map/mapper/mapperCanon.c b/src/map/mapper/mapperCanon.c
index c888f2f8..203c9142 100644
--- a/src/map/mapper/mapperCanon.c
+++ b/src/map/mapper/mapperCanon.c
@@ -218,7 +218,7 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
     if ( uCanon0 >= uCanon1 ) // using nCanon1 as the main one
     {
         assert( p->pCounters[uTruth1] > 0 );
-        uCanonBest = 0xFFFF;
+        uCanonBest = 0xFFFFFFFF;
         for ( i = 0; i < p->pCounters[uTruth1]; i++ )
         {
             uCanon0 = Extra_TruthPolarize( uTruth0, p->uPhases[uTruth1][i], 4 );
@@ -226,6 +226,7 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
             {
                 uCanonBest = uCanon0;
                 uPhaseBest = p->uPhases[uTruth1][i];
+                assert( uPhaseBest < 16 );
             }
         }
         uTruthRes[0] = (uCanon1 << 16) | uCanonBest;
@@ -236,7 +237,7 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
     else if ( uCanon0 < uCanon1 )
     {
         assert( p->pCounters[uTruth0] > 0 );
-        uCanonBest = 0xFFFF;
+        uCanonBest = 0xFFFFFFFF;
         for ( i = 0; i < p->pCounters[uTruth0]; i++ )
         {
             uCanon1 = Extra_TruthPolarize( uTruth1, p->uPhases[uTruth0][i], 4 );
@@ -244,6 +245,7 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
             {
                 uCanonBest = uCanon1;
                 uPhaseBest = p->uPhases[uTruth0][i];
+                assert( uPhaseBest < 16 );
             }
         }
         uTruthRes[0] = (uCanon0 << 16) | uCanonBest;
diff --git a/src/map/mapper/mapperRefs.c b/src/map/mapper/mapperRefs.c
index 039ee444..a50b134a 100644
--- a/src/map/mapper/mapperRefs.c
+++ b/src/map/mapper/mapperRefs.c
@@ -237,7 +237,7 @@ float Map_CutGetAreaRefed( Map_Cut_t * pCut, int fPhase )
     float aResult, aResult2;
     aResult2 = Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
     aResult  = Map_CutRefDeref( pCut, fPhase, 1 ); // reference
-    assert( aResult == aResult2 );
+//    assert( aResult == aResult2 );
     return aResult;
 }
 
@@ -257,7 +257,7 @@ float Map_CutGetAreaDerefed( Map_Cut_t * pCut, int fPhase )
     float aResult, aResult2;
     aResult2 = Map_CutRefDeref( pCut, fPhase, 1 ); // reference
     aResult  = Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
-    assert( aResult == aResult2 );
+//    assert( aResult == aResult2 );
     return aResult;
 }
 
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index e56c58f3..99942a88 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -179,7 +179,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     // consider the case when cube pairs should be preprocessed
     // before adding them to the set of divisors
     if ( nPairsTotal > pData->nPairsMax )
-        Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax );
+        if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
+            return NULL;
 
     // add the var pairs to the heap
     Fxu_MatrixComputeSingles( p );
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 3f3bc8fc..0ab8a157 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -90,6 +90,16 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
         pnPairCounters[ pnLitsDiff[k] ]++;
     // determine what pairs to take starting from the lower
     // so that there would be exactly pPairsMax pairs
+    if ( pnPairCounters[0] != 0 )
+    {
+        printf( "The SOPs of the nodes are not cube-free. Run \"bdd; sop\" before \"fx\".\n" );
+        return 0;
+    }
+    if ( pnPairCounters[1] != 0 )
+    {
+        printf( "The SOPs of the nodes are not SCC-free. Run \"bdd; sop\" before \"fx\".\n" );
+        return 0;
+    }
     assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
     assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
     nSum = 0;