Version abc60823

27 files changed, 686 insertions, 442 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 10e2eb41..e106d5eb 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -90,12 +90,12 @@ typedef enum {
     ABC_OBJ_PO,         //  4:  primary output terminal
     ABC_OBJ_BI,         //  5:  box input terminal
     ABC_OBJ_BO,         //  6:  box output terminal
-    ABC_OBJ_NET,        //  7:  net
-    ABC_OBJ_NODE,       //  8:  node
-    ABC_OBJ_LATCH,      //  9:  latch
-    ABC_OBJ_ASSERT,     // 10:  assertion output
+    ABC_OBJ_ASSERT,     //  7:  assertion output
+    ABC_OBJ_NET,        //  8:  net
+    ABC_OBJ_NODE,       //  9:  node
+    ABC_OBJ_LATCH,      // 10:  latch
     ABC_OBJ_BOX,        // 11:  box
-    ABC_OBJ_OTHER       // 12:  unused
+    ABC_OBJ_NUMBER      // 12:  unused
 } Abc_ObjType_t;
 
 // latch initial values
@@ -166,7 +166,6 @@ struct Abc_Ntk_t_
     Abc_NtkFunc_t     ntkFunc;       // functionality of the network
     char *            pName;         // the network name
     char *            pSpec;         // the name of the spec file if present
-    int               Id;            // network ID
     Nm_Man_t *        pManName;      // name manager (stores names of objects)
     // components of the network
     Vec_Ptr_t *       vObjs;         // the array of all objects (net, nodes, latches, etc)
@@ -181,9 +180,7 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *       vCutSet;       // the array of cutset nodes (used in the sequential AIG)
     // the number of living objects
     int               nObjs;         // the number of live objs
-    int               nNets;         // the number of live nets
-    int               nNodes;        // the number of live nodes
-    int               nBoxes;        // the number of live nodes
+    int nObjCounts[ABC_OBJ_NUMBER];  // the number of objects by type
     // the backup network and the step number
     Abc_Ntk_t *       pNetBackup;    // the pointer to the previous backup network
     int               iStep;         // the generation number for the given network
@@ -197,6 +194,7 @@ 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 *       pVerLib;       // for structural verilog designs
     void *            pManGlob;      // the global BDD manager
     Vec_Ptr_t *       vFuncsGlob;    // the global BDDs of CO functions
     Abc_ManTime_t *   pManTime;      // the timing manager (for mapped networks) stores arrival/required times for all nodes
@@ -206,6 +204,7 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *       vSupps;        // CO support information
     int *             pModel;        // counter-example (for miters)
     Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
+    void *            pData;         // misc
     // skew values (for latches)
     float             maxMeanCycle;  // maximum mean cycle time
     float             globalSkew;    // global skewing
@@ -215,8 +214,10 @@ struct Abc_Ntk_t_
 struct Abc_Lib_t_ 
 {
     char *            pName;         // the name of the library
-    void *            pManFunc;      // functionality manager for the gates
-    st_table *        tModules;      // the table hashing gate/module names into their networks
+    void *            pManFunc;      // functionality manager for the nodes
+    Vec_Ptr_t *       vModules;      // the array of modules
+    st_table *        tModules;      // the table hashing module names into their networks
+    Abc_Lib_t *       pLibrary;      // the library used to map this design
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -229,21 +230,25 @@ struct Abc_Lib_t_
 #define ABC_INFINITY      (100000000)
 
 // transforming floats into ints and back
-static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
-static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);             }
-static inline int         Abc_BitWordNum( int nBits )                { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
+static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);                       }
+static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);                     }
+static inline int         Abc_BitWordNum( int nBits )                { return (nBits>>5) + ((nBits&31) > 0);        }
+static inline int         Abc_TruthWordNum( int nVars )              { return nVars <= 5 ? 1 : (1 << (nVars - 5));  }
+static inline int         Abc_InfoHasBit( unsigned * p, int i )      { return (p[(i)>>5] & (1<<((i) & 31))) > 0;    }
+static inline void        Abc_InfoSetBit( unsigned * p, int i )      { p[(i)>>5] |= (1<<((i) & 31));                }
+static inline void        Abc_InfoXorBit( unsigned * p, int i )      { p[(i)>>5] ^= (1<<((i) & 31));                }
 
 // checking the network type
-static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST; }
-static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )         { return pNtk->ntkType == ABC_NTK_LOGIC;   }
-static inline bool        Abc_NtkIsStrash( Abc_Ntk_t * pNtk )        { return pNtk->ntkType == ABC_NTK_STRASH;  }
-static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )           { return pNtk->ntkType == ABC_NTK_SEQ;     }
+static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST;     }
+static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )         { return pNtk->ntkType == ABC_NTK_LOGIC;       }
+static inline bool        Abc_NtkIsStrash( Abc_Ntk_t * pNtk )        { return pNtk->ntkType == ABC_NTK_STRASH;      }
+static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )           { return pNtk->ntkType == ABC_NTK_SEQ;         }
 
-static inline bool        Abc_NtkHasSop( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_SOP;    }
-static inline bool        Abc_NtkHasBdd( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_BDD;    }
-static inline bool        Abc_NtkHasAig( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_AIG;    }
-static inline bool        Abc_NtkHasMapping( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_MAP;    }
-static inline bool        Abc_NtkHasBlackbox( Abc_Ntk_t * pNtk )     { return pNtk->ntkFunc == ABC_FUNC_BLACKBOX; }
+static inline bool        Abc_NtkHasSop( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_SOP;        }
+static inline bool        Abc_NtkHasBdd( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_BDD;        }
+static inline bool        Abc_NtkHasAig( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_AIG;        }
+static inline bool        Abc_NtkHasMapping( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_MAP;        }
+static inline bool        Abc_NtkHasBlackbox( Abc_Ntk_t * pNtk )     { return pNtk->ntkFunc == ABC_FUNC_BLACKBOX;   }
 
 static inline bool        Abc_NtkIsSopNetlist( Abc_Ntk_t * pNtk )    { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_NTK_NETLIST;  }
 static inline bool        Abc_NtkIsAigNetlist( Abc_Ntk_t * pNtk )    { return pNtk->ntkFunc == ABC_FUNC_AIG && pNtk->ntkType == ABC_NTK_NETLIST;  }
@@ -252,7 +257,7 @@ static inline bool        Abc_NtkIsSopLogic( Abc_Ntk_t * pNtk )      { return pN
 static inline bool        Abc_NtkIsBddLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_BDD && pNtk->ntkType == ABC_NTK_LOGIC  ;  }
 static inline bool        Abc_NtkIsAigLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_AIG && pNtk->ntkType == ABC_NTK_LOGIC  ;  }
 static inline bool        Abc_NtkIsMappedLogic( Abc_Ntk_t * pNtk )   { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_NTK_LOGIC  ;  }
-static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Vec_PtrSize(pNtk->vLatches) == 0;   }
+static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Vec_PtrSize(pNtk->vLatches) == 0;     }
 
 // reading data members of the network
 static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )            { return pNtk->pName;            }
@@ -271,19 +276,20 @@ static inline void        Abc_NtkSetStep  ( Abc_Ntk_t * pNtk, int iStep )
 // getting the number of objects 
 static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )       { return Vec_PtrSize(pNtk->vObjs);         }
 static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjs;                      }
-static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )          { return pNtk->nNets;                      }
-static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )         { return pNtk->nNodes;                     }
-static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return Vec_PtrSize(pNtk->vLatches);      }
-static inline int         Abc_NtkAssertNum( Abc_Ntk_t * pNtk )       { return Vec_PtrSize(pNtk->vAsserts);      }
-static inline int         Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk )   { return Vec_PtrSize(pNtk->vCutSet);       }
+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_NtkBoxNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjCounts[ABC_OBJ_BOX];    }
 static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vPis);          }
 static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vPos);          }
 static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vCis);          }
 static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vCos);          }
-static inline int         Abc_NtkBoxNum( Abc_Ntk_t * pNtk )          { return Vec_PtrSize(pNtk->vBoxes);        }
+static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return Vec_PtrSize(pNtk->vLatches);      }
+static inline int         Abc_NtkAssertNum( Abc_Ntk_t * pNtk )       { return Vec_PtrSize(pNtk->vAsserts);      }
+static inline int         Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk )   { return Vec_PtrSize(pNtk->vCutSet);       }
 
 // reading objects
 static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vObjs, i );   }
+static inline Abc_Obj_t * Abc_NtkBox( Abc_Ntk_t * pNtk, int i )      { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i );  }
 static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vLatches, i );}
 static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i )   { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vAsserts, i );}
 static inline Abc_Obj_t * Abc_NtkCutSetNode( Abc_Ntk_t * pNtk, int i){ return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCutSet, i ); }
@@ -353,6 +359,18 @@ static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Ab
 static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );    }
 static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );    }
 
+// creating simple objects
+extern inline Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+static inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) { return Abc_NtkObjAdd( pNtk, Type ); }
+static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk )      { return Abc_NtkObjAdd( pNtk, ABC_OBJ_NODE );       }
+static inline Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk )       { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BOX );        }
+static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )        { return Abc_NtkObjAdd( pNtk, ABC_OBJ_PI );         }
+static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )        { return Abc_NtkObjAdd( pNtk, ABC_OBJ_PO );         }
+static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk )        { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BI );         }
+static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk )        { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BO );         }
+static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )     { return Abc_NtkObjAdd( pNtk, ABC_OBJ_LATCH );      }
+static Abc_Obj_t *        Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )    { return Abc_NtkObjAdd( pNtk, ABC_OBJ_ASSERT );     }
+
 // checking the AIG node types
 static inline bool        Abc_AigNodeIsConst( Abc_Obj_t * pNode )    { assert(Abc_NtkIsStrash(Abc_ObjRegular(pNode)->pNtk)||Abc_NtkIsSeq(Abc_ObjRegular(pNode)->pNtk));  return Abc_ObjRegular(pNode)->Type == ABC_OBJ_CONST1;       }
 static inline bool        Abc_AigNodeIsAnd( Abc_Obj_t * pNode )      { assert(!Abc_ObjIsComplement(pNode)); assert(Abc_NtkIsStrash(pNode->pNtk)||Abc_NtkIsSeq(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2;                         }
@@ -405,9 +423,9 @@ static inline float       Abc_NtkGetLatSkew ( Abc_Ntk_t * pNtk, int lat )
 #define Abc_AigForEachAnd( pNtk, pNode, i )                                                        \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ )   \
         if ( (pNode) == NULL || !Abc_AigNodeIsAnd(pNode) ) {} else
-#define Abc_NtkForEachBox( pNtk, pNode, i )                                                       \
-    for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ )   \
-        if ( (pNode) == NULL || !Abc_ObjIsBox(pNode) ) {} else
+#define Abc_NtkForEachBox( pNtk, pNode, i )                                                        \
+    for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pNode) = Abc_NtkBox(pNtk, i)), 1); i++ )  \
+        if ( (pNode) == NULL ) {} else
 #define Abc_SeqForEachCutsetNode( pNtk, pNode, i )                                                 \
     for ( i = 0; (i < Abc_NtkCutSetNodeNum(pNtk)) && (((pNode) = Abc_NtkCutSetNode(pNtk, i)), 1); i++ )\
         if ( (pNode) == NULL ) {} else
@@ -498,6 +516,7 @@ extern void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin
 extern void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
 extern void               Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
 extern void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
+extern Abc_Obj_t *        Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type );
 extern void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 extern void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 /*=== abcFraig.c ==========================================================*/
@@ -549,21 +568,15 @@ extern Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fIni
 /*=== abcObj.c ==========================================================*/
 extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );
-extern void               Abc_ObjAdd( Abc_Obj_t * pObj );
-extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
-extern Abc_Obj_t *        Abc_NtkCloneObj( Abc_Obj_t * pNode );
+extern Abc_Obj_t *        Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
 extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
+extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
+extern Abc_Obj_t *        Abc_NtkCloneObj( Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreateBox( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreatePi( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreatePo( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreateLatch( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreateAssert( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
@@ -611,7 +624,7 @@ extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
 extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly, int fReorder, int fVerbose );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 75e0292e..7a261cf4 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -136,12 +136,10 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
     pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
     // create the constant node
-    pMan->pConst1  = Abc_ObjAlloc( pNtkAig, ABC_OBJ_CONST1 );
-    // add to the array of objects, count it as object but not as node
     assert( pNtkAig->vObjs->nSize == 0 );
-    pMan->pConst1->Id = pNtkAig->vObjs->nSize;
-    Vec_PtrPush( pNtkAig->vObjs, pMan->pConst1 );
-    pNtkAig->nObjs++;
+    pMan->pConst1 = Abc_NtkObjAdd( pNtkAig, ABC_OBJ_NODE );
+    pMan->pConst1->Type = ABC_OBJ_CONST1;
+    pNtkAig->nObjCounts[ABC_OBJ_NODE]--;
     // save the current network
     pMan->pNtkAig = pNtkAig;
     return pMan;
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index af6f4ef7..12a2fab7 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -117,14 +117,14 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     {
         fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
         fprintf( stdout, "One possible reason is that latches are added twice:\n" );
-        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" );
         return 0;
     }
     if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
         fprintf( stdout, "One possible reason is that latches are added twice:\n" );
-        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" );
         return 0;
     }
 
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 1d2ae23b..8e78ae61 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -167,6 +167,47 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
 
 /**Function*************************************************************
 
+  Synopsis    [Inserts one-input node of the type specified between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type )
+{
+    Abc_Obj_t * pNodeNew;
+    int iFanoutIndex, iFaninIndex;
+    // find pNodeOut among the fanouts of pNodeIn
+    if ( (iFanoutIndex = Vec_IntFind( &pNodeIn->vFanouts, pNodeOut->Id )) == -1 )
+    {
+        printf( "Node %s is not among", Abc_ObjName(pNodeOut) );
+        printf( " the fanouts of node %s...\n", Abc_ObjName(pNodeIn) );
+        return NULL;
+    }
+    // find pNodeIn among the fanins of pNodeOut
+    if ( (iFaninIndex = Vec_IntFind( &pNodeOut->vFanins, pNodeIn->Id )) == -1 )
+    {
+        printf( "Node %s is not among", Abc_ObjName(pNodeIn) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pNodeOut) );
+        return NULL;
+    }
+    // create the new node
+    pNodeNew = Abc_NtkCreateObj( pNodeIn->pNtk, Type );
+    // add pNodeIn as fanin and pNodeOut as fanout
+    Vec_IntPushMem( pNodeNew->pNtk->pMmStep, &pNodeNew->vFanins,  pNodeIn->Id  );
+    Vec_IntPushMem( pNodeNew->pNtk->pMmStep, &pNodeNew->vFanouts, pNodeOut->Id );
+    // update the fanout of pNodeIn
+    Vec_IntWriteEntry( &pNodeIn->vFanouts, iFanoutIndex, pNodeNew->Id );
+    // update the fanin of pNodeOut
+    Vec_IntWriteEntry( &pNodeOut->vFanins, iFaninIndex, pNodeNew->Id );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers fanout from the old node to the new node.]
 
   Description []
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 80bcc516..1d6619f0 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -46,7 +46,9 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
     memset( p, 0, sizeof(Abc_Lib_t) );
     p->pName    = Extra_UtilStrsav( pName );
     p->tModules = st_init_table( strcmp, st_strhash );
+    p->vModules = Vec_PtrAlloc( 100 );
     p->pManFunc = Aig_ManStart();
+    p->pLibrary = NULL;
     return p;
 }
 
@@ -63,18 +65,22 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
 ***********************************************************************/
 void Abc_LibFree( Abc_Lib_t * pLib )
 {
-    st_generator * gen;
     Abc_Ntk_t * pNtk;
-    char * pName;
+    int i;
     if ( pLib->pName )
         free( pLib->pName );
     if ( pLib->pManFunc )
         Aig_ManStop( pLib->pManFunc );
     if ( pLib->tModules )
+        st_free_table( pLib->tModules );
+    if ( pLib->vModules )
     {
-        st_foreach_item( pLib->tModules, gen, (char**)&pName, (char**)&pNtk )
+        Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
+        {
+            pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
-        st_free_table( pLib->tModules );
+        }
+        Vec_PtrFree( pLib->vModules );
     }
     free( pLib );
 }
@@ -92,21 +98,198 @@ void Abc_LibFree( Abc_Lib_t * pLib )
 ***********************************************************************/
 Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib )
 {
-    st_generator * gen;
     Abc_Ntk_t * pNtk;
-    char * pName;
-    if ( st_count(pLib->tModules) > 1 )
+    if ( Vec_PtrSize(pLib->vModules) > 1 )
     {
         printf( "The design includes more than one module and is currently not used.\n" );
         return NULL;
     }
-    // find the network
-    st_foreach_item( pLib->tModules, gen, (char**)&pName, (char**)&pNtk )
+    pNtk = Vec_PtrEntry( pLib->vModules, 0 );  Vec_PtrClear( pLib->vModules );
+    pNtk->pManFunc = pLib->pManFunc;           pLib->pManFunc = NULL;
+    return pNtk;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Surround boxes without content (black boxes) with BIs/BOs.]
+
+  Description [Returns the number of black boxes converted.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
+{
+    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    int i, k;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // collect blackbox nodes
+    assert( Vec_PtrSize(pNtk->vBoxes) == 0 );
+    Vec_PtrClear( pNtk->vBoxes );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        if ( Abc_NtkNodeNum(pObj->pData) == 0 )
+            Vec_PtrPush( pNtk->vBoxes, pObj );
+    // return if there is no black boxes without content
+    if ( Vec_PtrSize(pNtk->vBoxes) == 0 )
+        return 0;
+    // print the boxes
+    printf( "Black boxes are: " );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        printf( " %s", ((Abc_Ntk_t *)pObj->pData)->pName );
+    printf( "\n" );
+    // iterate through the boxes and add BIs/BOs
+    Abc_NtkForEachBox( pNtk, pObj, i )
     {
-        st_free_gen(gen);
-        break;
+        // go through the fanin nets
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BO );
+        // go through the fanout nets
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BI );
+            // if the name is not given assign name
+            if ( pFanout->pData == NULL )
+            {
+                pFanout->pData = Abc_ObjName( pFanout );
+                Nm_ManStoreIdName( pNtk->pManName, pFanout->Id, pFanout->pData, NULL );
+            }
+        }
     }
-    return pNtk;
+    return Vec_PtrSize(pNtk->vBoxes);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the AIG of the logic in the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeStrashUsingNetwork_rec( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    assert( !Abc_ObjIsNet(pObj) );
+    if ( pObj->pCopy )
+        return;
+    // call for the fanins
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
+    // compute for the node
+    pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+    // set for the fanout net
+    Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the AIG of the logic in the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeStrashUsingNetwork( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pBox )
+{
+    Abc_Ntk_t * pNtkGate;
+    Abc_Obj_t * pObj;
+    unsigned * pPolarity;
+    int i, fCompl;
+    assert( Abc_ObjIsBox(pBox) );
+    pNtkGate = pBox->pData;
+    pPolarity = (unsigned *)pBox->pNext;
+    assert( Abc_NtkIsNetlist(pNtkGate) );
+    assert( Abc_NtkLatchNum(pNtkGate) == 0 );
+    Abc_NtkCleanCopy( pNtkGate );
+    // set the PI values
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+    {
+        fCompl = (pPolarity && Abc_InfoHasBit(pPolarity, i));
+        pObj->pCopy = Abc_ObjNotCond( Abc_ObjFanin(pBox,i)->pCopy, fCompl );
+        Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+    }
+    // build recursively and set the PO values
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+    {
+        Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
+        Abc_ObjFanout(pBox,i)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the AIG of the logic in the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
+{
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i, nBoxes;
+    // explicitly derive black boxes
+    assert( Abc_NtkIsNetlist(pNtk) );
+    nBoxes = Abc_LibDeriveBlackBoxes( pNtk, pLib );
+    if ( nBoxes )
+        printf( "Detected and transformed %d black boxes.\n", nBoxes );
+    // create the new network with black boxes in place
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transer to the nets
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+    // build the AIG for the remaining logic in the netlist
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_ObjIsNode(pObj) )
+        {
+            pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+            Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+            continue;
+        }
+        Abc_NodeStrashUsingNetwork( pNtkAig, pObj );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+    // deallocate memory manager, which remembers the phase
+    if ( pNtk->pData )
+    {
+        Extra_MmFlexStop( pNtk->pData, 0 );
+        pNtk->pData = NULL;
+    }
+    // set the COs
+//    Abc_NtkFinalize( pNtk, pNtkAig );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    Abc_AigCleanup( pNtkAig->pManFunc );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_LibDeriveAig: The network check has failed.\n" );
+        return 0;
+    }
+    return pNtkAig;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index ef1d0980..0deb20e3 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -166,8 +166,8 @@ char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * p
 ***********************************************************************/
 void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 {
-    Abc_Obj_t * pObj;
-    int i;
+    Abc_Obj_t * pObj, * pTerm;
+    int i, k;
     assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
     assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
     assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) );
@@ -181,6 +181,13 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),      Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
     Abc_NtkForEachAssert( pNtk, pObj, i ) 
         Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NtkLogicStoreName( pTerm->pCopy,          Abc_ObjName(Abc_ObjFanin0Ntk(pTerm)) );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NtkLogicStoreName( pTerm->pCopy,          Abc_ObjName(Abc_ObjFanout0Ntk(pTerm)) );
+    }
     if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i),   Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 456d2aa2..145531db 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -95,11 +95,11 @@ Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
     int i, Counter = 0;
     assert( Abc_NtkIsNetlist(pNtk) );
     // start the network
-//    pNtkNew = Abc_NtkAlloc( Type, Func );
+//    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     if ( !Abc_NtkHasMapping(pNtk) )
-        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     else
-        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP );
+        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index f21d79be..e94e0a2f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -43,7 +43,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan )
 {
     Abc_Ntk_t * pNtk;
     pNtk = ALLOC( Abc_Ntk_t, 1 );
@@ -63,8 +63,8 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     pNtk->vBoxes      = Vec_PtrAlloc( 100 );
     pNtk->vSkews      = Vec_FltAlloc( 100 );
     // start the memory managers
-    pNtk->pMmObj      = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
-    pNtk->pMmStep     = Extra_MmStepStart( ABC_NUM_STEPS );
+    pNtk->pMmObj      = fUseMemMan? Extra_MmFixedStart( sizeof(Abc_Obj_t) ) : NULL;
+    pNtk->pMmStep     = fUseMemMan? Extra_MmStepStart( ABC_NUM_STEPS ) : NULL;
     // get ready to assign the first Obj ID
     pNtk->nTravIds    = 1;
     // start the functionality manager
@@ -101,12 +101,12 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj;
-    int i;
+    Abc_Obj_t * pObj, * pTerm;
+    int i, k;
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
+    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -125,6 +125,16 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkNew, pObj);
+        if ( Abc_NtkIsNetlist(pNtk) )
+            continue;
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NtkDupObj(pNtkNew, pTerm);
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NtkDupObj(pNtkNew, pTerm);
+    }
     // transfer the names
     if ( Type != ABC_NTK_NETLIST )
         Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
@@ -155,7 +165,7 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
+    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -172,6 +182,8 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachAssert( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     // transfer the names
     if ( Type != ABC_NTK_NETLIST )
         Abc_NtkDupCioNamesTableNoLatches( pNtk, pNtkNew );
@@ -201,7 +213,7 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
+    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = NULL;
@@ -228,6 +240,8 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     // transfer the names
     Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
     // check that the CI/CO/latches are copied correctly
@@ -276,7 +290,7 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 {
     Abc_Ntk_t * pNtkNew; 
     // allocate the empty network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     // set the specs
     pNtkNew->pName = Extra_FileNameGeneric(pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pName);
@@ -426,7 +440,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
     assert( Abc_ObjIsNode(pNode) ); 
     
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // set the name
     sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName );
     pNtkNew->pName = Extra_UtilStrsav(Buffer);
@@ -496,7 +510,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
     assert( Abc_ObjIsNode(pNode) ); 
     
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // set the name
     sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName );
     pNtkNew->pName = Extra_UtilStrsav(Buffer);
@@ -571,7 +585,7 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t
     
     // start the network
     Abc_NtkCleanCopy( pNtk );
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
 
     // collect the nodes in the TFI of the output
@@ -626,7 +640,7 @@ Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin, * pNodePo;
     int i;
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     pNtkNew->pName = Extra_UtilStrsav(Abc_ObjName(pNode));
     // add the PIs corresponding to the fanins of the node
     Abc_ObjForEachFanin( pNode, pFanin, i )
@@ -665,7 +679,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop )
     Vec_Ptr_t * vNames;
     int i, nVars;
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     pNtkNew->pName = Extra_UtilStrsav("ex");
     // create PIs
     Vec_PtrPush( pNtkNew->vObjs, NULL );
@@ -706,11 +720,20 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
+    // free EXDC Ntk
+    if ( pNtk->pExdc )
+        Abc_NtkDelete( pNtk->pExdc );
+    // dereference the BDDs
+    if ( Abc_NtkHasBdd(pNtk) )
+    {
+        Abc_NtkForEachNode( pNtk, pObj, i )
+            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+    }
     // make sure all the marks are clean
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
         // free large fanout arrays
-        if ( pObj->vFanouts.nCap * 4 > LargePiece )
+        if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
             FREE( pObj->vFanouts.pArray );
         // these flags should be always zero
         // if this is not true, something is wrong somewhere
@@ -718,17 +741,23 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         assert( pObj->fMarkB == 0 );
         assert( pObj->fMarkC == 0 );
     }
-
-    // dereference the BDDs
-    if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkForEachNode( pNtk, pObj, i )
-            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+    // free the nodes
+    if ( pNtk->pMmStep == NULL )
+    {
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            FREE( pObj->vFanouts.pArray );
+            FREE( pObj->vFanins.pArray );
+        }
+    }
+    if ( pNtk->pMmObj == NULL )
+    {
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            free( pObj );
+    }
         
     FREE( pNtk->pName );
     FREE( pNtk->pSpec );
-    // copy the EXDC Ntk
-    if ( pNtk->pExdc )
-        Abc_NtkDelete( pNtk->pExdc );
     // free the arrays
     Vec_PtrFree( pNtk->vPios );
     Vec_PtrFree( pNtk->vPis );
@@ -743,12 +772,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_FltFree( pNtk->vSkews );
     if ( pNtk->pModel ) free( pNtk->pModel );
     TotalMemory  = 0;
-    TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
-    TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
+    TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj)  : 0;
+    TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
 //    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
     // free the storage 
-    Extra_MmFixedStop( pNtk->pMmObj,   0 );
-    Extra_MmStepStop ( pNtk->pMmStep,  0 );
+    if ( pNtk->pMmObj )
+        Extra_MmFixedStop( pNtk->pMmObj,   0 );
+    if ( pNtk->pMmStep )
+        Extra_MmStepStop ( pNtk->pMmStep,  0 );
     // name manager
     Nm_ManFree( pNtk->pManName );
     // free the timing manager
@@ -764,7 +795,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( pNtk->pManFunc );
     else if ( Abc_NtkHasAig(pNtk) )
-        Aig_ManStop( pNtk->pManFunc );
+        { if ( pNtk->pManFunc ) Aig_ManStop( pNtk->pManFunc ); }
     else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = NULL;
     else if ( !Abc_NtkHasBlackbox(pNtk) )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 2811be16..27f5040c 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -33,7 +33,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a new Obj.]
+  Synopsis    [Creates a new object.]
 
   Description []
                
@@ -45,7 +45,10 @@
 Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
 {
     Abc_Obj_t * pObj;
-    pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj );
+    if ( pNtk->pMmObj )
+        pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj );
+    else
+        pObj = (Abc_Obj_t *)ALLOC( Abc_Obj_t, 1 );
     memset( pObj, 0, sizeof(Abc_Obj_t) );
     pObj->pNtk = pNtk;
     pObj->Type = Type;
@@ -55,7 +58,7 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
 
 /**Function*************************************************************
 
-  Synopsis    [Recycles the Obj.]
+  Synopsis    [Recycles the object.]
 
   Description []
                
@@ -69,12 +72,20 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
     Abc_Ntk_t * pNtk = pObj->pNtk;
     int LargePiece = (4 << ABC_NUM_STEPS);
     // free large fanout arrays
-    if ( pObj->vFanouts.nCap * 4 > LargePiece )
+    if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
+        FREE( pObj->vFanouts.pArray );
+    if ( pNtk->pMmStep == NULL )
+    {
         FREE( pObj->vFanouts.pArray );
+        FREE( pObj->vFanins.pArray );
+    }
     // clean the memory to make deleted object distinct from the live one
     memset( pObj, 0, sizeof(Abc_Obj_t) );
     // recycle the object
-    Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
+    if ( pNtk->pMmObj )
+        Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
+    else
+        free( pObj );
 }
 
 /**Function*************************************************************
@@ -88,58 +99,177 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_ObjAdd( Abc_Obj_t * pObj )
+Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( !Abc_ObjIsComplement(pObj) );
-    // add to the array of objects
+    Abc_Obj_t * pObj;
+    // create new object, assign ID, and add to the array
+    pObj = Abc_ObjAlloc( pNtk, Type );
     pObj->Id = pNtk->vObjs->nSize;
     Vec_PtrPush( pNtk->vObjs, pObj );
+    pNtk->nObjCounts[Type]++;
     pNtk->nObjs++;
     // perform specialized operations depending on the object type
-    if ( Abc_ObjIsNode(pObj) )
+    switch (Type)
     {
-        pNtk->nNodes++;
+        case ABC_OBJ_NONE:   
+            assert(0); 
+            break;
+        case ABC_OBJ_CONST1: 
+            assert(0); 
+            break;
+        case ABC_OBJ_PIO:    
+            assert(0); 
+            break;
+        case ABC_OBJ_PI:     
+            Vec_PtrPush( pNtk->vPis, pObj );
+            Vec_PtrPush( pNtk->vCis, pObj );
+            break;
+        case ABC_OBJ_PO:     
+            Vec_PtrPush( pNtk->vPos, pObj );
+            Vec_PtrPush( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_BI:     
+            Vec_PtrPush( pNtk->vCis, pObj );
+            break;
+        case ABC_OBJ_BO:     
+            Vec_PtrPush( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_ASSERT:     
+            Vec_PtrPush( pNtk->vAsserts, pObj );
+            Vec_PtrPush( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_NET:  
+            break;
+        case ABC_OBJ_NODE: 
+            break;
+        case ABC_OBJ_LATCH:     
+            pObj->pData = (void *)ABC_INIT_NONE;
+            Vec_PtrPush( pNtk->vLatches, pObj );
+            Vec_PtrPush( pNtk->vCis, pObj );
+            Vec_PtrPush( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_BOX:     
+            break;
+        default:
+            assert(0); 
+            break;
     }
-    else if ( Abc_ObjIsNet(pObj) )
-    {
-        pNtk->nNets++;
-    }
-    else if ( Abc_ObjIsPi(pObj) )
-    {
-        Vec_PtrPush( pNtk->vPis, pObj );
-        Vec_PtrPush( pNtk->vCis, pObj );
-    }
-    else if ( Abc_ObjIsPo(pObj) )
-    {
-        Vec_PtrPush( pNtk->vPos, pObj );
-        Vec_PtrPush( pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsLatch(pObj) )
-    {
-        Vec_PtrPush( pNtk->vLatches, pObj );
-        Vec_PtrPush( pNtk->vCis, pObj );
-        Vec_PtrPush( pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsAssert(pObj) )
-    {
-        Vec_PtrPush( pNtk->vAsserts, pObj );
-        Vec_PtrPush( pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsBi(pObj) )
-    {
-        Vec_PtrPush( pNtk->vCis, pObj );
-    }
-    else if ( Abc_ObjIsBo(pObj) )
-    {
-        Vec_PtrPush( pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsBox(pObj) )
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the object from the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    Vec_Ptr_t * vNodes;
+    int i;
+    // delete fanins and fanouts
+    assert( !Abc_ObjIsComplement(pObj) );
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NodeCollectFanouts( pObj, vNodes );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        Abc_ObjDeleteFanin( vNodes->pArray[i], pObj );
+    Abc_NodeCollectFanins( pObj, vNodes );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        Abc_ObjDeleteFanin( pObj, vNodes->pArray[i] );
+    Vec_PtrFree( vNodes );
+    // remove from the list of objects
+    Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
+    pObj->Id = (1<<26)-1;
+    pNtk->nObjCounts[pObj->Type]--;
+    pNtk->nObjs--;
+    // remove from the table of names
+//    if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
+//        Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
+    // perform specialized operations depending on the object type
+    switch (pObj->Type)
     {
-        pNtk->nBoxes++;
-        Vec_PtrPush( pNtk->vBoxes, pObj );
+        case ABC_OBJ_NONE:   
+            assert(0); 
+            break;
+        case ABC_OBJ_CONST1: 
+            assert(0); 
+            break;
+        case ABC_OBJ_PIO:    
+            assert(0); 
+            break;
+        case ABC_OBJ_PI:     
+            Vec_PtrRemove( pNtk->vPis, pObj );
+            Vec_PtrRemove( pNtk->vCis, pObj );
+            break;
+        case ABC_OBJ_PO:     
+            Vec_PtrRemove( pNtk->vPos, pObj );
+            Vec_PtrRemove( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_BI:     
+            Vec_PtrRemove( pNtk->vCis, pObj );
+            break;
+        case ABC_OBJ_BO:     
+            Vec_PtrRemove( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_ASSERT:     
+            Vec_PtrRemove( pNtk->vAsserts, pObj );
+            Vec_PtrRemove( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_NET:  
+            pObj->pData = NULL;
+            break;
+        case ABC_OBJ_NODE: 
+            if ( Abc_NtkHasBdd(pNtk) )
+                Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+            pObj->pData = NULL;
+            break;
+        case ABC_OBJ_LATCH:     
+            Vec_PtrRemove( pNtk->vLatches, pObj );
+            Vec_PtrRemove( pNtk->vCis, pObj );
+            Vec_PtrRemove( pNtk->vCos, pObj );
+            break;
+        case ABC_OBJ_BOX:     
+            break;
+        default:
+            assert(0); 
+            break;
     }
-    else assert( 0 );
+    // recycle the object memory
+    Abc_ObjRecycle( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node and MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    Vec_Ptr_t * vNodes;
+    int i;
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( Abc_ObjFanoutNum(pObj) == 0 );
+    // delete fanins and fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NodeCollectFanins( pObj, vNodes );
+    Abc_NtkDeleteObj( pObj );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+            Abc_NtkDeleteObj_rec( pObj );
+    Vec_PtrFree( vNodes );
 }
 
 /**Function*************************************************************
@@ -157,9 +287,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pObjNew;
     // create the new object
-    pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
-    // add the object to the network
-    Abc_ObjAdd( pObjNew );
+    pObjNew = Abc_NtkObjAdd( pNtkNew, pObj->Type );
     // copy functionality/names
     if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible
     {
@@ -203,132 +331,12 @@ Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pClone, * pFanin;
     int i;
-    pClone = Abc_ObjAlloc( pObj->pNtk, pObj->Type );   
-    Abc_ObjAdd( pClone );
+    pClone = Abc_NtkObjAdd( pObj->pNtk, pObj->Type );   
     Abc_ObjForEachFanin( pObj, pFanin, i )
         Abc_ObjAddFanin( pClone, pFanin );
     return pClone;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Deletes the object from the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
-{
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    Vec_Ptr_t * vNodes;
-    int i;
-
-    assert( !Abc_ObjIsComplement(pObj) );
-
-    // delete fanins and fanouts
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NodeCollectFanouts( pObj, vNodes );
-    for ( i = 0; i < vNodes->nSize; i++ )
-        Abc_ObjDeleteFanin( vNodes->pArray[i], pObj );
-    Abc_NodeCollectFanins( pObj, vNodes );
-    for ( i = 0; i < vNodes->nSize; i++ )
-        Abc_ObjDeleteFanin( pObj, vNodes->pArray[i] );
-    Vec_PtrFree( vNodes );
-
-    // remove from the list of objects
-    Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
-    pObj->Id = (1<<26)-1;
-    pNtk->nObjs--;
-
-    // remove from the table of names
-    if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
-        Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
-
-    // perform specialized operations depending on the object type
-    if ( Abc_ObjIsNet(pObj) )
-    {
-        pObj->pData = NULL;
-        pNtk->nNets--;
-    }
-    else if ( Abc_ObjIsNode(pObj) )
-    {
-        if ( Abc_NtkHasBdd(pNtk) )
-            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
-        pObj->pData = NULL;
-        pNtk->nNodes--;
-    }
-    else if ( Abc_ObjIsLatch(pObj) )
-    {
-        Vec_PtrRemove( pNtk->vLatches, pObj );
-        Vec_PtrRemove( pNtk->vCis, pObj );
-        Vec_PtrRemove( pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsPi(pObj) )
-    {
-        Vec_PtrRemove( pObj->pNtk->vPis, pObj );
-        Vec_PtrRemove( pObj->pNtk->vCis, pObj );
-    }
-    else if ( Abc_ObjIsPo(pObj) )
-    {
-        Vec_PtrRemove( pObj->pNtk->vPos, pObj );
-        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsBi(pObj) )
-    {
-        Vec_PtrRemove( pObj->pNtk->vCis, pObj );
-    }
-    else if ( Abc_ObjIsBo(pObj) )
-    {
-        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsAssert(pObj) )
-    {
-        Vec_PtrRemove( pObj->pNtk->vAsserts, pObj );
-        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
-    }
-    else if ( Abc_ObjIsBox(pObj) )
-    {
-        pNtk->nBoxes--;
-        Vec_PtrRemove( pObj->pNtk->vBoxes, pObj );
-    }
-    else
-        assert( 0 );
-    // recycle the net itself
-    Abc_ObjRecycle( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the node and MFFC of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
-{
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    Vec_Ptr_t * vNodes;
-    int i;
-    assert( !Abc_ObjIsComplement(pObj) );
-    assert( Abc_ObjFanoutNum(pObj) == 0 );
-    // delete fanins and fanouts
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NodeCollectFanins( pObj, vNodes );
-    Abc_NtkDeleteObj( pObj );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
-            Abc_NtkDeleteObj_rec( pObj );
-    Vec_PtrFree( vNodes );
-}
-
 
 /**Function*************************************************************
 
@@ -458,129 +466,13 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
 {
     Abc_Obj_t * pNet;
     assert( Abc_NtkIsNetlist(pNtk) );
-    if ( pNet = Abc_NtkFindNet( pNtk, pName ) )
+    if ( pName && (pNet = Abc_NtkFindNet( pNtk, pName )) )
         return pNet;
     // create a new net
-    pNet = Abc_ObjAlloc( pNtk, ABC_OBJ_NET );
-    Abc_ObjAdd( pNet );
-    pNet->pData = Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL );
+    pNet = Abc_NtkObjAdd( pNtk, ABC_OBJ_NET );
+    pNet->pData = pName? Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL ) : NULL;
     return pNet;
 }
-    
-/**Function*************************************************************
-
-  Synopsis    [Create node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_NODE );     
-    Abc_ObjAdd( pObj );
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create multi-input/multi-output box.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_BOX );     
-    Abc_ObjAdd( pObj );
-    return pObj;
-}
-    
-/**Function*************************************************************
-
-  Synopsis    [Create primary input.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_PI );     
-    Abc_ObjAdd( pObj );
-    return pObj;
-}
-    
-/**Function*************************************************************
-
-  Synopsis    [Create primary output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_PO );     
-    Abc_ObjAdd( pObj );
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates latch.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_LATCH );     
-    pObj->pData = (void *)ABC_INIT_NONE;
-    Abc_ObjAdd( pObj );
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates assert.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_ASSERT );     
-    Abc_ObjAdd( pObj );
-    return pObj;
-}
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index dfd49f6e..ff05fe69 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     assert( Abc_NtkIsStrash(pNtk2) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -304,7 +304,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -356,7 +356,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
     assert( 1 == Abc_NtkCoNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_miter", pNtk->pName );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -423,7 +423,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
     assert( In2 < Abc_NtkCiNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -488,7 +488,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
     assert( In < Abc_NtkCiNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
 
     // get the root output
@@ -669,7 +669,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkIsDfsOrdered(pNtk) );
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
     // create new latches (or their initial values) and remember them in the new latches
@@ -806,7 +806,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
     assert( nFrames > 0 );
     assert( Abc_NtkIsStrash(pNtk) );   
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
     // create new latches (or their initial values) and remember them in the new latches
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 99ed5636..ac46501c 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -78,7 +78,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
         return NULL;
 
     // start the network
-    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
     pNtk->pName = Extra_UtilStrsav(pNamePo);
     // make sure the new manager has enough inputs
     Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index cb1d2a38..e3bb764d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -66,7 +66,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     if ( Abc_NtkIsNetlist(pNtk) )
     {
         fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
-        fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  nd = %5d",  Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  box = %5d", Abc_NtkBoxNum(pNtk) );
     }
     else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
     {        
@@ -83,7 +84,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
-    if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) || Abc_NtkIsNetlist(pNtk) )
     {
     }
     else if ( Abc_NtkHasSop(pNtk) )   
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 61bc8b09..03073075 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -676,7 +676,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav( "temp" );
     // map the constant nodes
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 86f13884..02bfca17 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -436,6 +436,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     int clk1 = clock(), clk;
     int fOrderCiVarsFirst = 0;
     int nLevelsMax = Abc_AigGetLevelNum(pNtk);
+    int RetValue = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -481,7 +482,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         }
         // add the trivial clause
         if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
-            return 0;
+            goto Quits;
     }
 
     // add the clauses
@@ -515,7 +516,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             }
             // add the clauses
             if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
-                return 0;
+                goto Quits;
         }
         else
         {
@@ -537,12 +538,12 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             {
                 if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
 //                if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
-                    return 0;
+                    goto Quits;
             }
             else
             {
                 if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
-                    return 0;
+                    goto Quits;
             }
         }
         // add the variables to the J-frontier
@@ -597,11 +598,13 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) );
     Vec_IntFree( vLevels );
 */
+    RetValue = 1;
+Quits :
     // delete
     Vec_IntFree( vVars );
     Vec_PtrFree( vNodes );
     Vec_PtrFree( vSuper );
-    return 1;
+    return RetValue;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index c69aeabf..c54ea33c 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -250,7 +250,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
     Abc_Obj_t * pFanin;
     int i;
     assert( Abc_ObjIsNode(pNodeOld) );
-    assert( Abc_NtkIsAigLogic(pNodeOld->pNtk) );
+    assert( Abc_NtkHasAig(pNodeOld->pNtk) && !Abc_NtkIsStrash(pNodeOld->pNtk) );
     // get the local AIG manager and the local root node
     pMan = pNodeOld->pNtk->pManFunc;
     pRoot = pNodeOld->pData;
@@ -317,7 +317,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
     // get the cutoff level
     LevelCut = ABC_MAX( 0, Abc_AigGetLevelNum(pNtk) - nLevels );
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
     // create PIs below the cut and nodes above the cut
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index b5306bea..156d9b3d 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -284,7 +284,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     int i;
 
     // start the new network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
     pNtkNew->pName = Extra_UtilStrsav( "exdc" );
     pNtkNew->pSpec = NULL;
 
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index 58d9f64e..50baa285 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -514,7 +514,7 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
     if ( vCorresp )
         Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL );
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     if ( fShortNames )
     {
         pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName);
@@ -719,7 +719,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     pNtkNew->pName = Extra_UtilStrsav("exdc");
     pNtkNew->pSpec = NULL;
 
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
index 29b5d3a6..339d64d1 100644
--- a/src/base/abci/abcVanImp.c
+++ b/src/base/abci/abcVanImp.c
@@ -877,7 +877,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
     assert( Abc_NtkIsStrash(pNtk) );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     pNtkNew->pName = Extra_UtilStrsav( "exdc" );
     pNtkNew->pSpec = NULL;
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 0cc3c7d9..86e8845b 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -50,6 +50,8 @@ static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 
+extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -667,13 +669,13 @@ usage:
 ***********************************************************************/
 int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk, * pNtkNew;
     Abc_Lib_t * pDesign;
     char * FileName;
     FILE * pFile;
     int fCheck;
     int c;
-    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
+    extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib );
 
     fCheck = 1;
     Extra_UtilGetoptReset();
@@ -709,21 +711,32 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // set the new network
-    pDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck );
+    pDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck, 1 );
     if ( pDesign == NULL )
     {
         fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
         return 1;
     }
+
     // derive root design
     pNtk = Abc_LibDeriveRoot( pDesign );
+    Abc_LibFree( pDesign );
     if ( pNtk == NULL )
     {
         fprintf( pAbc->Err, "Deriving root module has failed.\n" );
         return 1;
     }
+
+    // derive the AIG network from this design
+    pNtkNew = Abc_LibDeriveAig( pNtk, Abc_FrameReadLibVer() );
+    Abc_NtkDelete( pNtk );
+    if ( pNtkNew == NULL )
+    {
+        fprintf( pAbc->Err, "Converting root module to AIG has failed.\n" );
+        return 1;
+    }
     // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
     return 0;
 
 usage:
@@ -753,7 +766,6 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     int fCheck;
     int c;
-    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
 
     fCheck = 1;
     Extra_UtilGetoptReset();
@@ -789,7 +801,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // set the new network
-    pLibrary = Ver_ParseFile( FileName, NULL, fCheck );
+    pLibrary = Ver_ParseFile( FileName, NULL, fCheck, 0 );
     if ( pLibrary == NULL )
     {
         fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
@@ -1613,7 +1625,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( pAbc->Out, "Writing PLA has failed.\n" );
         return 0;
     }
-    Io_WriteVerilog( pNtkTemp, FileName );
+    Io_WriteVerilog( pNtkTemp, FileName, 0 );
     Abc_NtkDelete( pNtkTemp );
     return 0;
 
@@ -1638,10 +1650,10 @@ usage:
 ***********************************************************************/
 int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
 {
-    st_table * tLibrary;
+    Abc_Lib_t * pLibrary;
     char * FileName;
     int c;
-    extern void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName );
+    extern void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
@@ -1663,13 +1675,13 @@ int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[globalUtilOptind];
 
     // derive the netlist
-    tLibrary = Abc_FrameReadLibVer();
-    if ( tLibrary == NULL )
+    pLibrary = Abc_FrameReadLibVer();
+    if ( pLibrary == NULL )
     {
         fprintf( pAbc->Out, "Verilog library is not specified.\n" );
         return 0;
     }
-    Io_WriteVerilogLibrary( tLibrary, FileName );
+    Io_WriteVerilogLibrary( pLibrary, FileName );
     return 0;
 
 usage:
@@ -1741,7 +1753,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         int i;
         if ( pFile == NULL )
         {
-            fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName );
+            fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", FileName );
             return 1;
         }
         if ( fNames )
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 8c8d6bed..c42d2016 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -97,7 +97,7 @@ extern void               Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int
 /*=== abcWritePla.c ==========================================================*/
 extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteVerilog.c ==========================================================*/
-extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
+extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fVerLibStyle );
 
 #ifdef __cplusplus
 }
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 83b642a0..367d693b 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -73,7 +73,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
     nAnds = atoi( pCur );     while ( *pCur++ );
 
     // allocate the empty AIG
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav( pName );
     pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index ade9051f..5d6bc2f1 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -211,7 +211,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     assert( p->vTokens != NULL );
 
     // create the new network
-    p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+    p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
         pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index a4610cac..4550d286 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -271,7 +271,7 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p )
     pModelName = vTokens->pArray[1];
 
     // allocate the empty network
-    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     pNtk->pName = Extra_UtilStrsav( pModelName );
     pNtk->pSpec = Extra_UtilStrsav( p->pFileName );
 
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
index 594bf4eb..2234b3a3 100644
--- a/src/base/io/ioWriteVer.c
+++ b/src/base/io/ioWriteVer.c
@@ -26,7 +26,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle );
 static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
@@ -34,6 +34,7 @@ static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogVerLibStyle( FILE * pFile, Abc_Ntk_t * pNtk );
 static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
 static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
@@ -53,7 +54,7 @@ static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle )
 {
     FILE * pFile;
 
@@ -75,7 +76,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
 
     // write the equations for the network
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
-    Io_WriteVerilogInt( pFile, pNtk );
+    Io_WriteVerilogInt( pFile, pNtk, fVerLibStyle );
     fprintf( pFile, "\n" );
     fclose( pFile );
 }
@@ -91,12 +92,11 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
+void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName )
 {
     FILE * pFile;
-    st_generator * gen;
     Abc_Ntk_t * pNtk, * pNetlist;
-    char * pName;
+    int i;
 
     // start the output stream
     pFile = fopen( pFileName, "w" );
@@ -109,15 +109,17 @@ void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
     fprintf( pFile, "// Verilog library \"%s\" written by ABC on %s\n", pFileName, Extra_TimeStamp() );
     fprintf( pFile, "\n" );
     // write modules
-    st_foreach_item( tLibrary, gen, (char**)&pName, (char**)&pNtk )
+    Vec_PtrForEachEntry( pLibrary->vModules, pNtk, i )
     {
         // create netlist
-        pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+//        pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+        assert( Abc_NtkIsNetlist(pNtk) );
+        pNetlist = pNtk;
         // write the equations for the network
-        Io_WriteVerilogInt( pFile, pNetlist );
+        Io_WriteVerilogInt( pFile, pNetlist, 1 );
         fprintf( pFile, "\n" );
         // delete the netlist
-        Abc_NtkDelete( pNetlist );
+//        Abc_NtkDelete( pNetlist );
     }
 
     fclose( pFile );
@@ -134,7 +136,7 @@ void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle )
 {
     // write inputs and outputs
     fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
@@ -161,8 +163,10 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
     Io_WriteVerilogWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
     }
-    // write the nodes
-    if ( Abc_NtkHasMapping(pNtk) )
+    // write nodes
+    if ( fVerLibStyle )
+        Io_WriteVerilogVerLibStyle( pFile, pNtk );        
+    else if ( Abc_NtkHasMapping(pNtk) )
         Io_WriteVerilogGates( pFile, pNtk );
     else
         Io_WriteVerilogNodes( pFile, pNtk );
@@ -438,6 +442,65 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes the nodes and boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogVerLibStyle( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Vec_Vec_t * vLevels;
+    Abc_Ntk_t * pNtkGate;
+    Abc_Obj_t * pObj, * pTerm, * pFanin;
+    Aig_Obj_t * pFunc;
+    int i, k, Counter, nDigits;
+
+    Counter = 1;
+    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+
+    // write boxes
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        pNtkGate = pObj->pData;
+        fprintf( pFile, "  %s g%0*d", pNtkGate->pName, nDigits, Counter++ );
+        fprintf( pFile, "(" );
+        Abc_NtkForEachPi( pNtkGate, pTerm, k )
+        {
+            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanout0(pTerm)) );
+            fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjFanin(pObj,k)) );
+        }
+        Abc_NtkForEachPo( pNtkGate, pTerm, k )
+        {
+            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanin0(pTerm)) );
+            fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjFanout(pObj,k)), k==Abc_NtkPoNum(pNtkGate)-1? "":", " );
+        }
+        fprintf( pFile, ");\n" );
+    }
+    // write nodes
+    vLevels = Vec_VecAlloc( 10 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        pFunc = pObj->pData;
+        fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        // set the input names
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Aig_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(pFanin));
+        // write the formula
+        Aig_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
+        fprintf( pFile, ";\n" );
+        // clear the input names
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            free( Aig_IthVar(pNtk->pManFunc, k)->pData );
+    }
+    Vec_VecFree( vLevels );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the gates.]
 
   Description []
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 358d306c..21215af6 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -303,7 +303,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
 
     // create the network for the initial state computation
     // start the table and the array of PO values
-    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     tTable   = stmm_init_table( stmm_numcmp, stmm_numhash );
     vValues  = Vec_IntAlloc( 100 );
 
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index 30a21086..8dc29855 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -109,7 +109,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         Vec_PtrWriteEntry( pNtkNew->vObjs, pObj->pCopy->Id, pObj->pCopy );
         pNtkNew->nObjs++;
     }
-    pNtkNew->nNodes = pNtk->nNodes;
+    pNtkNew->nObjCounts[ABC_OBJ_NODE] = pNtk->nObjCounts[ABC_OBJ_NODE];
 
     // create PI/PO and their names
     Abc_NtkForEachPi( pNtk, pObj, i )
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 080abcb2..1945826f 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -116,7 +116,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);