Version abc70219

36 files changed, 1493 insertions, 759 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bbe6b078..f638097f 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -222,6 +222,7 @@ struct Abc_Lib_t_
     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
+    void *            pGenlib;       // the genlib library used to map this design
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -468,11 +469,11 @@ static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ )   \
         if ( !Abc_ObjIsLatch(pObj) ) {} else
 #define Abc_NtkForEachLatchInput( pNtk, pObj, i )                                                  \
-    for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_ObjFanin0(Abc_NtkBox(pNtk, i))), 1); i++ )   \
-        if ( !Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) ) {} else
-#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
+    for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)); i++ )                                          \
+        if ( !(Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) && (((pObj) = Abc_ObjFanin0(Abc_NtkBox(pNtk, i))), 1)) ) {} else
+#define Abc_NtkForEachLatchOutput( pNtk, pObj, i )                                                 \
+    for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)); i++ )                                          \
+        if ( !(Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) && (((pObj) = Abc_ObjFanout0(Abc_NtkBox(pNtk, i))), 1)) ) {} else
 #define Abc_NtkForEachWhitebox( pNtk, pObj, i )                                                    \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ )   \
         if ( !Abc_ObjIsWhitebox(pObj) ) {} else
@@ -596,9 +597,9 @@ extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
 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 );
+extern int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkToAig( 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 );
@@ -680,12 +681,9 @@ extern void               Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect );
-extern Abc_Ntk_t *        Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkToLogic( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect );
+extern Abc_Ntk_t *        Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 5e13807a..0947b58a 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -53,7 +53,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     DdManager * dd;
     int nFaninsMax, i;
 
-    assert( Abc_NtkIsSopLogic(pNtk) ); 
+    assert( Abc_NtkHasSop(pNtk) ); 
 
     // start the functionality manager
     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
@@ -159,7 +159,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     int nFaninsMax, fFound, i;
 
-    assert( Abc_NtkIsSopLogic(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
 
     // check if there are nodes with complemented SOPs
     fFound = 0;
@@ -221,7 +221,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     else
         fMode = -1;
 
-    assert( Abc_NtkIsBddLogic(pNtk) );
+    assert( Abc_NtkHasBdd(pNtk) );
     if ( dd->size > 0 )
     Cudd_zddVarsFromBddVars( dd, 2 );
     // create the new manager
@@ -481,7 +481,7 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
 ***********************************************************************/
 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
 {
-    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
+    assert( Abc_NtkHasBdd(pNode->pNtk) ); 
     *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
     *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 );
 }
@@ -554,7 +554,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
     Hop_Man_t * pMan;
     int i;
 
-    assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsSopNetlist(pNtk) ); 
+    assert( Abc_NtkHasSop(pNtk) ); 
 
     // start the functionality manager
     pMan = Hop_ManStart();
@@ -664,7 +664,7 @@ int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk )
     DdManager * dd;
     int nFaninsMax, i;
 
-    assert( Abc_NtkIsAigLogic(pNtk) ); 
+    assert( Abc_NtkHasAig(pNtk) ); 
 
     // start the functionality manager
     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
@@ -863,7 +863,7 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
     char * pSop;
     int i;
 
-    assert( Abc_NtkIsMappedLogic(pNtk) );
+    assert( Abc_NtkHasMapping(pNtk) );
     // update the functionality manager
     assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
     pNtk->pManFunc = Extra_MmFlexStart();
@@ -889,10 +889,10 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect )
+int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
 {
-    assert( Abc_NtkIsLogic(pNtk) );
-    if ( Abc_NtkIsSopLogic(pNtk) )
+    assert( !Abc_NtkIsStrash(pNtk) );
+    if ( Abc_NtkHasSop(pNtk) )
     {
         if ( !fDirect )
             return 1;
@@ -900,11 +900,11 @@ int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect )
             return 0;
         return Abc_NtkBddToSop(pNtk, fDirect);
     }
-    if ( Abc_NtkIsMappedLogic(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return Abc_NtkMapToSop(pNtk);
-    if ( Abc_NtkIsBddLogic(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return Abc_NtkBddToSop(pNtk, fDirect);
-    if ( Abc_NtkIsAigLogic(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
         if ( !Abc_NtkAigToBdd(pNtk) )
             return 0;
@@ -925,19 +925,19 @@ int Abc_NtkLogicToSop( Abc_Ntk_t * pNtk, int fDirect )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkLogicToBdd( Abc_Ntk_t * pNtk )
+int Abc_NtkToBdd( Abc_Ntk_t * pNtk )
 {
-    assert( Abc_NtkIsLogic(pNtk) );
-    if ( Abc_NtkIsBddLogic(pNtk) )
+    assert( !Abc_NtkIsStrash(pNtk) );
+    if ( Abc_NtkHasBdd(pNtk) )
         return 1;
-    if ( Abc_NtkIsMappedLogic(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
     {
         Abc_NtkMapToSop(pNtk);
         return Abc_NtkSopToBdd(pNtk);
     }
-    if ( Abc_NtkIsSopLogic(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_NtkSopToBdd(pNtk);
-    if ( Abc_NtkIsAigLogic(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return Abc_NtkAigToBdd(pNtk);
     assert( 0 );
     return 0;
@@ -954,23 +954,23 @@ int Abc_NtkLogicToBdd( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkLogicToAig( Abc_Ntk_t * pNtk )
+int Abc_NtkToAig( Abc_Ntk_t * pNtk )
 {
-    assert( Abc_NtkIsLogic(pNtk) );
-    if ( Abc_NtkIsAigLogic(pNtk) )
+    assert( !Abc_NtkIsStrash(pNtk) );
+    if ( Abc_NtkHasAig(pNtk) )
         return 1;
-    if ( Abc_NtkIsMappedLogic(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
     {
         Abc_NtkMapToSop(pNtk);
         return Abc_NtkSopToAig(pNtk);
     }
-    if ( Abc_NtkIsBddLogic(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
     {
         if ( !Abc_NtkBddToSop(pNtk,0) )
             return 0;
         return Abc_NtkSopToAig(pNtk);
     }
-    if ( Abc_NtkIsSopLogic(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_NtkSopToAig(pNtk);
     assert( 0 );
     return 0;
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index 342d6c83..b38afb59 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -195,7 +195,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
     // 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( "Hierarchy reader flattened %d logic instances. Preserved %d black boxes.\n", 
+    printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", 
         Counter, Abc_NtkBlackboxNum(pNtkNew) );
 
     // pass the design
@@ -249,44 +249,29 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk )
     // clean the node copy fields
     Abc_NtkCleanCopy( pNtk );
 
-    // create PIs/POs for the box inputs/outputs
     // mark the nodes that should not be connected
     Abc_NtkIncrementTravId( pNtk );
     Abc_NtkForEachBlackbox( pNtk, pObj, i )
-    {
         Abc_NodeSetTravIdCurrent( pObj );
+    Abc_NtkForEachCi( pNtk, pTerm, i )
+        Abc_NodeSetTravIdCurrent( pTerm );
+    Abc_NtkForEachCo( pNtk, pTerm, i )
+        Abc_NodeSetTravIdCurrent( pTerm );
+    // unmark PIs and LIs/LOs
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+        Abc_NodeSetTravIdPrevious( pTerm );
+    Abc_NtkForEachLatchInput( pNtk, pTerm, i )
+        Abc_NodeSetTravIdPrevious( pTerm );
+    Abc_NtkForEachLatchOutput( pNtk, pTerm, i )
+        Abc_NodeSetTravIdPrevious( pTerm );
+    // copy the box outputs
+    Abc_NtkForEachBlackbox( pNtk, pObj, i )
         Abc_ObjForEachFanout( pObj, pTerm, k )
-        {
-            pNet = Abc_ObjFanout0(pTerm);
-            if ( pNet->pCopy )
-            {
-                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_NtkForEachBlackbox( pNtk, pObj, i )
-    {
-        Abc_ObjForEachFanin( pObj, pTerm, k )
-        {
-            pNet = Abc_ObjFanin0(pTerm);
-            if ( pNet->pCopy && !Abc_ObjIsCi(Abc_ObjFanin0(pNet)) )
-            {
-                Abc_NodeSetTravIdCurrent( pTerm );
-                continue;
-            }
-            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
-            pTerm->pCopy = Abc_NtkCreatePo( pNtkNew );
-        }
-    }
 
     // duplicate other objects
     Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( !Abc_NodeIsTravIdCurrent(pObj) && pObj->pCopy == NULL )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
             Abc_NtkDupObj( pNtkNew, pObj, Abc_ObjIsNet(pObj) );
 
     // connect all objects
@@ -295,6 +280,23 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
 
+    // create unique PO for each net feeding into blackboxes or POs
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCo( pNtk, pTerm, i )
+    {
+        // skip latch inputs
+        assert( Abc_ObjFanoutNum(pTerm) <= 1 );
+        if ( Abc_ObjFanoutNum(pTerm) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pTerm)) )
+            continue;
+        // check if the net is visited
+        pNet = Abc_ObjFanin0(pTerm);
+        if ( Abc_NodeIsTravIdCurrent(pNet) )
+            continue;
+        // create PO
+        Abc_NodeSetTravIdCurrent( pNet );
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNet->pCopy );
+    }
+
     // check integrity
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
@@ -337,18 +339,11 @@ Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL )
     assert( Abc_NtkWhiteboxNum(pNtkL) == 0 );
     assert( Abc_NtkBlackboxNum(pNtkL) == 0 );
 
-    if ( Abc_NtkIsSopNetlist(pNtkH) && Abc_NtkIsAigNetlist(pNtkL) )
-        Abc_NtkSopToAig( pNtkH );
-    if ( Abc_NtkIsAigNetlist(pNtkH) && Abc_NtkIsSopNetlist(pNtkL) )
-        Abc_NtkSopToAig( pNtkL );
-
-    assert( pNtkH->ntkFunc == pNtkL->ntkFunc );
-
     // prepare the logic network for copying
     Abc_NtkCleanCopy( pNtkL );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtkH->ntkType, pNtkH->ntkFunc, 1 );
+    pNtkNew = Abc_NtkAlloc( pNtkL->ntkType, pNtkL->ntkFunc, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav( pNtkH->pName );
     pNtkNew->pSpec = Extra_UtilStrsav( pNtkH->pSpec );
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 247f3915..1f741ca8 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -82,6 +82,7 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
             if ( pNtk == pNtkSave )
                 continue;
             pNtk->pManFunc = NULL;
+            pNtk->pDesign = NULL;
             Abc_NtkDelete( pNtk );
         }
         Vec_PtrFree( pLib->vModules );
@@ -166,6 +167,7 @@ int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk )
         return 0;
     st_insert( pLib->tModules, (char *)pNtk->pName, (char *)pNtk );
     Vec_PtrPush( pLib->vModules, pNtk );
+    pNtk->pDesign = pLib;
     return 1;
 }
 
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 30c7d621..f57bcc21 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -26,6 +26,9 @@
 ////////////////////////////////////////////////////////////////////////
 
 static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,22 +45,21 @@ static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin;
     int i, k;
+    // consider the case of the AIG
+    if ( Abc_NtkIsStrash(pNtk) )
+        return Abc_NtkAigToLogicSop( pNtk );
     assert( Abc_NtkIsNetlist(pNtk) );
     // consider simple case when there is hierarchy
     assert( pNtk->pDesign == NULL );
-//    assert( pNtk->tName2Model == NULL );
-//    if ( pNtk->tName2Model )
-//        return Abc_NtkNetlistToLogicHie( pNtk );
+    assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
+    assert( Abc_NtkBlackboxNum(pNtk) == 0 );
     // start the network
-    if ( Abc_NtkHasMapping(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
-    else
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc );
     // duplicate the nodes 
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj, 0);
@@ -71,9 +73,9 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc );
+        pNtkNew->pExdc = Abc_NtkToLogic( pNtk->pExdc );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkToLogic(): Network check has failed.\n" );
     return pNtkNew;
 }
 
@@ -88,36 +90,18 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
+Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
     if ( Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkAigToLogicSop(pNtk);
-        pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
+        pNtkNew = Abc_NtkLogicToNetlist( pNtkTemp );
         Abc_NtkDelete( pNtkTemp );
+        return pNtkNew;
     }
-    else if ( Abc_NtkIsBddLogic(pNtk) )
-    {
-        if ( !Abc_NtkBddToSop(pNtk, fDirect) )
-            return NULL;
-        pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
-        Abc_NtkSopToBdd(pNtk);
-    }
-    else if ( Abc_NtkIsAigLogic(pNtk) )
-    {
-        if ( !Abc_NtkAigToBdd(pNtk) )
-            return NULL;
-        if ( !Abc_NtkBddToSop(pNtk, fDirect) )
-            return NULL;
-        pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
-        Abc_NtkSopToAig(pNtk);
-    }
-    else if ( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsMappedLogic(pNtk) )
-        pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
-    else assert( 0 );
-    return pNtkNew;
+    return Abc_NtkLogicToNetlist( pNtk );
 }
 
 /**Function*************************************************************
@@ -131,12 +115,12 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
     assert( Abc_NtkIsStrash(pNtk) );
     pNtkTemp = Abc_NtkAigToLogicSopBench( pNtk );
-    pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
+    pNtkNew = Abc_NtkLogicToNetlist( pNtkTemp );
     Abc_NtkDelete( pNtkTemp );
     return pNtkNew;
 }
@@ -156,32 +140,24 @@ Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin;
     int i, k;
 
+    assert( Abc_NtkIsLogic(pNtk) );
+
     // remove dangling nodes
     Abc_NtkCleanup( pNtk, 0 );
 
-    assert( Abc_NtkIsLogic(pNtk) );
 //    assert( Abc_NtkLogicHasSimpleCos(pNtk) );
     if ( !Abc_NtkLogicHasSimpleCos(pNtk) )
     {
-        printf( "Abc_NtkLogicSopToNetlist() warning: The network is converted to have simple COs.\n" );
+        printf( "Abc_NtkLogicToNetlist() warning: The network is converted to have simple COs.\n" );
         Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
     }
 
-    if ( Abc_NtkIsBddLogic(pNtk) )
-    {
-        if ( !Abc_NtkBddToSop(pNtk,0) )
-            return NULL;
-    }
-
-//    Abc_NtkForEachCo(pNtk, pObj, i)
-//        Abc_ObjPrint( stdout, Abc_ObjFanin0(pObj) );
-
     // start the netlist by creating PI/PO/Latch objects
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc );
     // create the CI nets and remember them in the new CI nodes
@@ -227,7 +203,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
         if ( pObj->pCopy->pCopy ) // the net of the new object is already created
             continue;
         // create the new net
-        pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) );
+        pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); // here we create ridiculous names net line "n48", where 48 is the ID of the node
         Abc_ObjAddFanin( pNet, pObj->pCopy );
         pObj->pCopy->pCopy = pNet;
     }
@@ -237,9 +213,9 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc, 0 );
+        pNtkNew->pExdc = Abc_NtkToNetlist( pNtk->pExdc, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkLogicToNetlist(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 18b4a7c4..deddb712 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -242,9 +242,9 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 ***********************************************************************/
 void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pBox, * pObj, * pTerm;
+    Abc_Obj_t * pBox, * pObj, * pTerm, * pNet;
     int i;
-    if ( Abc_NtkHasBlackbox(pNtk) )
+    if ( Abc_NtkHasBlackbox(pNtk) && Abc_NtkBoxNum(pNtk) == 0 )
     {
         pBox = Abc_NtkCreateBlackbox(pNtk);
         Abc_NtkForEachPi( pNtk, pObj, i )
@@ -262,8 +262,23 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
         return;
     }
     assert( Abc_NtkIsNetlist(pNtk) );
+
+    // check if constant 0 net is used
+    pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
+    if ( Abc_ObjFanoutNum(pNet) == 0 )
+        Abc_NtkDeleteObj(pNet);
+    else if ( Abc_ObjFaninNum(pNet) == 0 )
+        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) );
+    // check if constant 1 net is used
+    pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
+    if ( Abc_ObjFanoutNum(pNet) == 0 )
+        Abc_NtkDeleteObj(pNet);
+    else if ( Abc_ObjFaninNum(pNet) == 0 )
+        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) );
+
     // fix the net drivers
     Abc_NtkFixNonDrivenNets( pNtk );
+
     // reorder the CI/COs to PI/POs first
     Abc_NtkOrderCisCos( pNtk );
 }
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index ee86e8aa..40d1dcad 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -164,7 +164,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames, int fSeq, int fUseReverse )
     }
     // convert to logic SOP
     if ( Abc_NtkIsLogic(pNtk) )
-        Abc_NtkLogicToSop( pNtk, 0 );
+        Abc_NtkToSop( pNtk, 0 );
     // create the file name
     Abc_ShowGetFileName( pNtk->pName, FileNameDot );
     // check that the file can be opened
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 9a40fce9..353bf046 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1404,6 +1404,8 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
 
     // rehash the AIG
     Abc_AigRehash( pNtk->pManFunc );
+
+    // update the name manager!!!
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ae00ce5c..cf7cc0e9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3395,7 +3395,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+    pNtkRes = Abc_NtkToLogic( pNtk );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Converting to a logic network has failed.\n" );
@@ -3984,7 +3984,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Converting to SOP is possible only for logic networks.\n" );
         return 1;
     }
-    if ( !Abc_NtkLogicToSop(pNtk, fDirect) )
+    if ( !Abc_NtkToSop(pNtk, fDirect) )
     {
         fprintf( pErr, "Converting to SOP has failed.\n" );
         return 1;
@@ -4047,7 +4047,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pOut, "The logic network is already in the BDD form.\n" );
         return 0;
     }
-    if ( !Abc_NtkLogicToBdd(pNtk) )
+    if ( !Abc_NtkToBdd(pNtk) )
     {
         fprintf( pErr, "Converting to BDD has failed.\n" );
         return 1;
@@ -4109,7 +4109,7 @@ int Abc_CommandAig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pOut, "The logic network is already in the AIG form.\n" );
         return 0;
     }
-    if ( !Abc_NtkLogicToAig(pNtk) )
+    if ( !Abc_NtkToAig(pNtk) )
     {
         fprintf( pErr, "Converting to AIG has failed.\n" );
         return 1;
@@ -7719,7 +7719,7 @@ int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // convert the network into the SOP network
-    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+    pNtkRes = Abc_NtkToLogic( pNtk );
 
     // get the new network
     if ( !Abc_NtkSuperChoiceLut( pNtkRes, nLutSize, nCutSizeMax, fVerbose ) )
@@ -8716,7 +8716,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         // convert the network into an SOP network
-        pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+        pNtkRes = Abc_NtkToLogic( pNtk );
         // perform the retiming
         Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose );
         // replace the current network
@@ -8725,7 +8725,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the network in the SOP form
-    if ( !Abc_NtkLogicToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0) )
     {
         printf( "Converting to SOPs has failed.\n" );
         return 0;
@@ -9712,7 +9712,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         assert( Abc_NtkIsLogic(pNtk) );
-        Abc_NtkLogicToBdd( pNtk );
+        Abc_NtkToBdd( pNtk );
         RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL );
     }
 
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index 7771148e..95b95d89 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -196,7 +196,7 @@ Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1
 
     Abc_NtkSweep( pNtk, 0 );
     Abc_NtkCleanupSeq( pNtk, 0, 0, 0 );
-    Abc_NtkLogicToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0 );
     Abc_NtkCycleInitStateSop( pNtk, 50, 0 );
     return pNtk;
 }
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
index d7bb70fe..cc9ce0b9 100644
--- a/src/base/abci/abcDress.c
+++ b/src/base/abci/abcDress.c
@@ -63,7 +63,7 @@ void Abc_NtkDress( Abc_Ntk_t * pNtkLogic, char * pFileName, int fVerbose )
     Abc_NtkCleanCopy(pNtkOrig);
 
     // convert it into the logic network
-    pNtkLogicOrig = Abc_NtkNetlistToLogic( pNtkOrig );
+    pNtkLogicOrig = Abc_NtkToLogic( pNtkOrig );
     // check that the networks have the same PIs/POs/latches
     if ( !Abc_NtkCompareSignals( pNtkLogic, pNtkLogicOrig, 1, 1 ) )
     {
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index b6d57a5c..45515dd1 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -61,7 +61,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 //        Abc_NtkBddToSop(pNtk);
     }
     // get the network in the SOP form
-    if ( !Abc_NtkLogicToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0) )
     {
         printf( "Abc_NtkFastExtract(): Converting to SOPs has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 0f0d9c8b..abcde7ce 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -27,9 +27,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
-static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
-static Ivy_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
+static Abc_Ntk_t *  Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Abc_Ntk_t *  Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
+static Ivy_Man_t *  Abc_NtkToIvy( Abc_Ntk_t * pNtkOld );
 
 static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
 static Ivy_Obj_t *  Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode );
@@ -93,7 +93,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // convert to the AIG manager
-    pMan = Abc_NtkToAig( pNtk );
+    pMan = Abc_NtkToIvy( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
         printf( "AIG check has failed.\n" );
@@ -130,9 +130,9 @@ Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int f
     int nNodes, fCleanup = 1;
     // convert from the AIG manager
     if ( fSeq )
-        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig );
+        pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig );
     else
-        pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+        pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
     // report the cleanup results
     if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
         printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
@@ -608,7 +608,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
 
     // convert to the AIG manager
-    pMan = Abc_NtkToAig( pNtk );
+    pMan = Abc_NtkToIvy( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
         Vec_IntFree( vInit );
@@ -654,8 +654,8 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
 /*
     // convert from the AIG manager
-    pNtkAig = Abc_NtkFromAig( pNtk, pMan );
-//    pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
+    pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
+//    pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan );
     Ivy_ManStop( pMan );
 
     // report the cleanup results
@@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
 {
     Vec_Int_t * vNodes;
     Abc_Ntk_t * pNtk;
@@ -732,7 +732,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     }
     Vec_IntFree( vNodes );
     if ( !Abc_NtkCheck( pNtk ) )
-        fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" );
     return pNtk;
 }
 
@@ -747,7 +747,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
+Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
 {
     Vec_Int_t * vNodes, * vLatches;
     Abc_Ntk_t * pNtk;
@@ -830,7 +830,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig
     Vec_IntFree( vLatches );
     Vec_IntFree( vNodes );
     if ( !Abc_NtkCheck( pNtk ) )
-        fprintf( stdout, "Abc_NtkFromAigSeq(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
     return pNtk;
 }
 
@@ -845,7 +845,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
+Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld )
 {
     Ivy_Man_t * pMan;
     Abc_Obj_t * pObj;
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index dc90bee0..92985423 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan );
+static Hop_Man_t * Abc_NtkToMini( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,7 +48,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
     Hop_Man_t * pMan, * pTemp;
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
-    pMan = Abc_NtkToAig( pNtk );
+    pMan = Abc_NtkToMini( pNtk );
     if ( pMan == NULL )
         return NULL;
     if ( !Hop_ManCheck( pMan ) )
@@ -64,7 +64,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
     Hop_ManStop( pTemp );
     Hop_ManPrintStats( pMan );
     // convert from the AIG manager
-    pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+    pNtkAig = Abc_NtkFromMini( pNtk, pMan );
     if ( pNtkAig == NULL )
         return NULL;
     Hop_ManStop( pMan );
@@ -89,7 +89,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
+Hop_Man_t * Abc_NtkToMini( Abc_Ntk_t * pNtk )
 {
     Hop_Man_t * pMan;
     Abc_Obj_t * pObj;
@@ -121,7 +121,7 @@ Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
@@ -142,7 +142,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
     Hop_ManForEachPo( pMan, pObj, i )
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Hop_ObjChild0Copy(pObj) );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkFromMini(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 77d640c2..8591663e 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -30,6 +30,39 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs fast synthesis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
+{
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+
+    pNtk = *ppNtk;
+
+    Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
+    Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+    pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+    Abc_NtkDelete( pNtkTemp );
+
+    if ( fMoreEffort )
+    {
+        Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
+        Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+        Abc_NtkDelete( pNtkTemp );
+    }
+
+    *ppNtk = pNtk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Existentially quantifies one variable.]
 
   Description []
@@ -113,6 +146,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObj, * pMiter;
     int i, nLatches;
+    int fSynthesis = 1;
 
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) );
@@ -136,7 +170,10 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     // create PI variables
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkDupObj( pNtkNew, pObj, 1 );
+    // create the PO
+    Abc_NtkCreatePo( pNtkNew );
     // restrash the nodes (assuming a topological order of the old network)
+    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
     Abc_NtkForEachNode( pNtk, pObj, i )
         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
     // create the function of the primary output
@@ -150,7 +187,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
     Vec_PtrFree( vPairs );
     // add the primary output
-    Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), Abc_ObjNot(pMiter) );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );
     Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
 
     // quantify inputs
@@ -158,7 +195,20 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     {
         assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
+//        for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
+        {
             Abc_NtkQuantify( pNtkNew, i, fVerbose );
+//            if ( fSynthesis && (i % 3 == 2) )
+            if ( fSynthesis  )
+            {
+                Abc_NtkCleanData( pNtkNew );
+                Abc_AigCleanup( pNtkNew->pManFunc );
+                Abc_NtkSynthesize( &pNtkNew, 1 );
+            }
+//            printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) );
+//            printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) );
+        }
+//        printf( "\n" );
         Abc_NtkCleanData( pNtkNew );
         Abc_AigCleanup( pNtkNew->pManFunc );
         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
@@ -169,7 +219,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
         }
     }
 
-    // make sure that everything is okay
+    // check consistency of the network
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkTransRel: The network check has failed.\n" );
@@ -263,6 +313,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
     int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
     int fFixedPoint = 0;
     int fSynthesis  = 1;
+    int fMoreEffort = 1;
 
     assert( Abc_NtkIsStrash(pNtkRel) );
     assert( Abc_NtkLatchNum(pNtkRel) == 0 );
@@ -273,8 +324,8 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
     pNtkReached = Abc_NtkDup( pNtkFront );
 //Abc_NtkShow( pNtkReached, 0, 0, 0 );
 
-    if ( fVerbose )
-        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
+//    if ( fVerbose )
+//        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
 
     // perform iterations of reachability analysis
     nNodesPrev = Abc_NtkNodeNum(pNtkFront);
@@ -293,25 +344,13 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
             {
                 Abc_NtkCleanData( pNtkNext );
                 Abc_AigCleanup( pNtkNext->pManFunc );
-
-                Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
-                pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
-                Abc_NtkDelete( pNtkTemp );
+                Abc_NtkSynthesize( &pNtkNext, fMoreEffort );
             }
         }
         Abc_NtkCleanData( pNtkNext );
         Abc_AigCleanup( pNtkNext->pManFunc );
         if ( fSynthesis )
-        {
-            Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
-            pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
-
-            Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
-            Abc_NtkRefactor( pNtkReached, 10, 16, 0, 0, 0, 0 );
-            pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
-        }
+            Abc_NtkSynthesize( &pNtkNext, 1 );
         // map the next states into the current states
         pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
         Abc_NtkDelete( pNtkTemp );
@@ -333,20 +372,15 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
         nNodesOld = Abc_NtkNodeNum(pNtkFront);
         if ( fSynthesis )
         {
-            Abc_NtkRewrite( pNtkFront, 0, 0, 0, 0, 0 );
-            pNtkFront = Abc_NtkBalance( pNtkTemp = pNtkFront, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
-
-            Abc_NtkRewrite( pNtkReached, 0, 0, 0, 0, 0 );
-            pNtkReached = Abc_NtkBalance( pNtkTemp = pNtkReached, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
+            Abc_NtkSynthesize( &pNtkFront, fMoreEffort );
+            Abc_NtkSynthesize( &pNtkReached, fMoreEffort );
         }
         nNodesNew = Abc_NtkNodeNum(pNtkFront);
         // print statistics
         if ( fVerbose )
         {
-            printf( "I = %3d : Reached = %6d  Front = %6d  FrontM = %6d  %6.2f %%   ", 
-                i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesNew );
+            printf( "I = %3d : Reach = %6d  Fr = %6d  FrM = %6d  %7.2f %%   ", 
+                i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev );
             PRT( "T", clock() - clk );
         }
         nNodesPrev = Abc_NtkNodeNum(pNtkFront);
@@ -354,13 +388,6 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
     if ( !fFixedPoint )
         fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
 
-    // report the stats
-    if ( fVerbose )
-    {
-//        nMints = 1;
-//        fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
-    }
-
     // complement the output to represent the set of unreachable states
     Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
 
@@ -372,7 +399,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
         Abc_NtkDeleteObj( pObj );
     }
 
-    // make sure that everything is okay
+    // check consistency of the network
     if ( !Abc_NtkCheck( pNtkReached ) )
     {
         printf( "Abc_NtkReachability: The network check has failed.\n" );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 88ef009b..45fc9089 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -105,7 +105,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     if ( Abc_NtkIsStrash(pNtk) )
         return Abc_NtkRestrash( pNtk, fCleanup );
     // convert the node representation in the logic network to the AIG form
-    if ( !Abc_NtkLogicToAig(pNtk) )
+    if ( !Abc_NtkToAig(pNtk) )
     {
         printf( "Converting to AIGs has failed.\n" );
         return NULL;
@@ -156,7 +156,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
     // the first network should be an AIG
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
-    if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkLogicToAig(pNtk2) )
+    if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkToAig(pNtk2) )
     {
         printf( "Converting to AIGs has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 1b63b23c..4791c859 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -536,7 +536,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     int i, nNodesOld;
     assert( Abc_NtkIsLogic(pNtk) ); 
     // convert network to BDD representation
-    if ( !Abc_NtkLogicToBdd(pNtk) )
+    if ( !Abc_NtkToBdd(pNtk) )
     {
         fprintf( stdout, "Converting to BDD has failed.\n" );
         return 1;
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 08584290..92691d6c 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1265,7 +1265,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    pNetlist = Abc_NtkToNetlist(pNtk,0);
     if ( pNetlist == NULL )
     {
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
@@ -1406,7 +1406,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    pNetlist = Abc_NtkToNetlist(pNtk,0);
     if ( pNetlist == NULL )
     {
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
@@ -1552,7 +1552,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    pNetlist = Abc_NtkToNetlist(pNtk,0);
     if ( pNetlist == NULL )
     {
         fprintf( pErr, "Cannot produce the intermediate network.\n" );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2267d4e7..3603519f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -55,7 +55,7 @@ static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 
-extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+extern int glo_fMapped;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -139,11 +139,15 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
 
     fCheck = 1;
+    glo_fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mch" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                glo_fMapped ^= 1;
+                break;
             case 'c':
                 fCheck ^= 1;
                 break;
@@ -166,10 +170,11 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
+    fprintf( pAbc->Err, "usage: read [-mch] <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-m     : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
     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" );
@@ -332,7 +337,13 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtk = Io_ReadBlifAsAig( pFileName, fCheck );
     else
 //        pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck );
+    {
+        Abc_Ntk_t * pTemp;
         pNtk = Io_ReadBlif( pFileName, fCheck );
+        pNtk = Abc_NtkToLogic( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+    }
+
     if ( pNtk == NULL )
         return 1;
     // replace the current network
@@ -657,11 +668,15 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
     fCheck = 1;
+    glo_fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mch" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                glo_fMapped ^= 1;
+                break;
             case 'c':
                 fCheck ^= 1;
                 break;
@@ -684,8 +699,9 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_verilog [-ch] <file>\n" );
-    fprintf( pAbc->Err, "\t         read the network in Verilog (IWLS 2005 subset)\n" );
+    fprintf( pAbc->Err, "usage: read_verilog [-mch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in Verilog (IWLS 2002/2005 subset)\n" );
+    fprintf( pAbc->Err, "\t-m     : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
     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" );
@@ -712,6 +728,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCheck;
     int c;
     extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib );
+    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
 
     fCheck = 1;
     Extra_UtilGetoptReset();
@@ -921,11 +938,15 @@ int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pBaseName, * pFileName;
     int c;
 
+    glo_fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                glo_fMapped ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -946,6 +967,7 @@ 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-m     : toggle reading mapped Verilog for <orig> [default = %s]\n", glo_fMapped? "yes":"no" );
     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" );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index d8213994..7e54e5e3 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
                 else
                 {
-                    printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
+                    printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
                     Vec_StrFree( vString );
                     Abc_NtkDelete( pNtk );
                     return NULL;
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 46a202e1..3e09caf0 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -98,6 +98,7 @@ static int               Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
 static int               Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
+static int               Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens );
 
 static int               Io_MvCharIsSpace( char s )  { return s == ' ' || s == '\t' || s == '\r' || s == '\n';  }
 static int               Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!';  }
@@ -568,7 +569,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
         // parse directives
         if ( *(pCur-1) != '.' )
             continue;
-        if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) )
+        if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) || !strncmp(pCur, "gate", 4) )
             Vec_PtrPush( p->pLatest->vNames, pCur );
         else if ( p->fBlifMv && (!strncmp(pCur, "def ", 4) || !strncmp(pCur, "default ", 8)) )
             continue;
@@ -1464,6 +1465,10 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
     char * pName;
     assert( !p->pMan->fBlifMv );
     Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
+    // parse the mapped node
+    if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") )
+        return Io_MvParseLineGateBlif( p, vTokens );
+    // parse the regular name line
     assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
     pName = Vec_PtrEntryLast( vTokens );
     pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
@@ -1483,6 +1488,104 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
 }
 
 
+#include "mio.h"
+#include "main.h"
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Io_ReadBlifCleanName( char * pName )
+{
+    int i, Length;
+    Length = strlen(pName);
+    for ( i = 0; i < Length; i++ )
+        if ( pName[i] == '=' )
+            return pName + i + 1;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
+{
+    Mio_Library_t * pGenlib; 
+    Mio_Gate_t * pGate;
+    Abc_Obj_t * pNode;
+    char ** ppNames, * pName;
+    int i, nNames;
+
+    pName = vTokens->pArray[0];
+
+    // check that the library is available
+    pGenlib = Abc_FrameReadLibGen();
+    if ( pGenlib == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
+        return 0;
+    }
+
+    // create a new node and add it to the network
+    if ( vTokens->nSize < 2 )
+    {
+        sprintf( p->pMan->sError, "Line %d: The .gate line has less than two tokens.", Io_MvGetLine(p->pMan, pName) );
+        return 0;
+    }
+
+    // get the gate
+    pGate = Mio_LibraryReadGateByName( pGenlib, vTokens->pArray[1] );
+    if ( pGate == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), vTokens->pArray[1] );
+        return 0;
+    }
+
+    // if this is the first line with gate, update the network type
+    if ( Abc_NtkNodeNum(p->pNtk) == 0 )
+    {
+        assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
+        p->pNtk->ntkFunc = ABC_FUNC_MAP;
+        Extra_MmFlexStop( p->pNtk->pManFunc );
+        p->pNtk->pManFunc = pGenlib;
+    }
+
+    // remove the formal parameter names
+    for ( i = 2; i < vTokens->nSize; i++ )
+    {
+        vTokens->pArray[i] = Io_ReadBlifCleanName( vTokens->pArray[i] );
+        if ( vTokens->pArray[i] == NULL )
+        {
+            sprintf( p->pMan->sError, "Line %d: Invalid gate input assignment.", Io_MvGetLine(p->pMan, pName) );
+            return 0;
+        }
+    }
+
+    // create the node
+    ppNames = (char **)vTokens->pArray + 2;
+    nNames  = vTokens->nSize - 3;
+    pNode   = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames );
+
+    // set the pointer to the functionality of the node
+    Abc_ObjSetData( pNode, pGate );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 5956a9bc..090cf254 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -45,13 +45,12 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
 {
     Abc_Ntk_t * pNtk;
     Abc_Lib_t * pDesign;
-    int i;
 
     // parse the verilog file
-    pDesign = Ver_ParseFile( pFileName, NULL, 1, fCheck );
+    pDesign = Ver_ParseFile( pFileName, NULL, fCheck, 1 );
     if ( pDesign == NULL )
         return NULL;
-
+/*
     // extract the master network
     pNtk = Vec_PtrEntryLast( pDesign->vModules );
     pNtk->pDesign = pDesign;
@@ -75,6 +74,28 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
         // check that there is no cyclic dependency
         Abc_NtkIsAcyclicHierarchy( pNtk );
     }
+*/
+    // extract the master network
+    pNtk = Vec_PtrEntry( pDesign->vModules, 0 );
+    pNtk->pDesign = pDesign;
+    pDesign->pManFunc = NULL;
+
+//Io_WriteVerilog( pNtk, "_temp.v" );
+
+    // 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;
+        pNtk->pSpec = Extra_UtilStrsav( pFileName );
+    }
+    else
+    {
+        // check that there is no cyclic dependency
+        Abc_NtkIsAcyclicHierarchy( pNtk );
+    }
     return pNtk;
 }
 
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 2de93ddf..0ac3181a 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -209,7 +209,7 @@ Abc_NtkPrintStats( stdout, pNtk, 0 );
     // convert blackboxes
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
-        printf( "Hierarchy reader converted %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
         pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
         Abc_NtkDelete( pTemp );
         if ( pNtk == NULL )
@@ -219,7 +219,7 @@ Abc_NtkPrintStats( stdout, pNtk, 0 );
         }
     }
     // convert the netlist into the logic network
-    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    pNtk = Abc_NtkToLogic( pTemp = pNtk );
     Abc_NtkDelete( pTemp );
     if ( pNtk == NULL )
     {
@@ -244,7 +244,6 @@ 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 )
@@ -274,7 +273,7 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
     // convert blackboxes
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
-        printf( "Hierarchy reader converted %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
         pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
         Abc_NtkDelete( pTemp );
         if ( pNtk == NULL )
@@ -284,7 +283,7 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
         }
     }
     // convert the netlist into the logic network
-    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    pNtk = Abc_NtkToLogic( pTemp = pNtk );
     Abc_NtkDelete( pTemp );
     if ( pNtk == NULL )
     {
@@ -350,6 +349,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
         Io_WriteGml( pNtk, pFileName );
         return;
     }
+
     // convert logic network into netlist
     if ( FileType == IO_FILE_PLA )
     {
@@ -359,13 +359,13 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( Abc_NtkIsComb(pNtk) )
-            pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 1 );
+            pNtkTemp = Abc_NtkToNetlist( pNtk, 1 );
         else
         {
             fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
             pNtkCopy = Abc_NtkDup( pNtk );
             Abc_NtkMakeComb( pNtkCopy );
-            pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 1 );
+            pNtkTemp = Abc_NtkToNetlist( pNtk, 1 );
             Abc_NtkDelete( pNtkCopy );
         }
     }
@@ -376,31 +376,37 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             fprintf( stdout, "Writing BENCH is available for AIGs.\n" );
             return;
         }
-        pNtkTemp = Abc_NtkLogicToNetlistBench( pNtk );
+        pNtkTemp = Abc_NtkToNetlistBench( pNtk );
     }
     else
-        pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 0 );
+        pNtkTemp = Abc_NtkToNetlist( pNtk, 0 );
+
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Converting to netlist has failed.\n" );
         return;
     }
+
     if ( FileType == IO_FILE_BLIF )
+    {
+        if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
+            Abc_NtkToSop( pNtkTemp, 0 );
         Io_WriteBlif( pNtkTemp, pFileName, 1 );
+    }
     else if ( FileType == IO_FILE_BENCH )
         Io_WriteBench( pNtkTemp, pFileName );
     else if ( FileType == IO_FILE_PLA )
         Io_WritePla( pNtkTemp, pFileName );
     else if ( FileType == IO_FILE_EQN )
     {
-        if ( Abc_NtkIsSopNetlist(pNtkTemp) )
-            Abc_NtkSopToAig( pNtkTemp );
+        if ( !Abc_NtkHasAig(pNtkTemp) )
+            Abc_NtkToAig( pNtkTemp );
         Io_WriteEqn( pNtkTemp, pFileName );
     }
     else if ( FileType == IO_FILE_VERILOG )
     {
-        if ( Abc_NtkIsSopNetlist(pNtkTemp) )
-            Abc_NtkSopToAig( pNtkTemp );
+        if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
+            Abc_NtkToAig( pNtkTemp );
         Io_WriteVerilog( pNtkTemp, pFileName );
     }
     else 
@@ -451,25 +457,17 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
     // reintroduce the boxes into the netlist
     if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
     {
-        // bring the current network to the same representation
-        if ( Abc_NtkIsLogic(pNtk) )
-        {
-            if ( Abc_NtkIsSopNetlist(pNtkBase) )
-                Abc_NtkLogicToSop( pNtk, 0 );
-            else if ( Abc_NtkIsAigNetlist(pNtkBase) )
-                Abc_NtkLogicToAig( pNtk );
-        }
         // derive the netlist
-        pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 );
+        pNtkResult = Abc_NtkToNetlist( pNtk, 0 );
         pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult );
         Abc_NtkDelete( pNtkTemp );
         if ( pNtkResult )
-            printf( "Hierarchy writer reintroduced %d blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) );
+            printf( "Hierarchy writer reintroduced %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) );
     }
     else
     {
         printf( "Warning: The output network does not contain blackboxes.\n" );
-        pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 );
+        pNtkResult = Abc_NtkToNetlist( pNtk, 0 );
     }
     Abc_NtkDelete( pNtkBase );
     if ( pNtkResult == NULL )
@@ -477,11 +475,15 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
 
     // write the resulting network
     if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
+    {
+        if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
+            Abc_NtkToSop( pNtkResult, 0 );
         Io_WriteBlif( pNtkResult, pFileName, 1 );
+    }
     else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG )
     {
-        if ( Abc_NtkIsSopNetlist(pNtkResult) )
-            Abc_NtkSopToAig( pNtkResult );
+        if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
+            Abc_NtkToAig( pNtkResult );
         Io_WriteVerilog( pNtkResult, pFileName );
     }
     else 
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index e48d0be8..417fe2a3 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -32,9 +32,9 @@ static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWriteSubckt( FILE * pFile, Abc_Obj_t * pNode );
 static void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length );
 static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode );
-static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length );
 static void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch );
 
 ////////////////////////////////////////////////////////////////////////
@@ -56,7 +56,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
     Abc_Ntk_t * pNtkTemp;
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
+    pNtkTemp = Abc_NtkToNetlist(pNtk,0);
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Writing BLIF has failed.\n" );
@@ -97,13 +97,22 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
         Abc_Ntk_t * pNtkTemp;
-        Abc_Obj_t * pObj;
         int i;
+/*
+        Abc_Obj_t * pObj;
         Abc_NtkForEachBlackbox( pNtk, pObj, i )
         {
             pNtkTemp = pObj->pData;
             assert( pNtkTemp != NULL && Abc_NtkHasBlackbox(pNtkTemp) );
-            fprintf( pFile, "\n\n", Abc_NtkName(pNtk) );
+            fprintf( pFile, "\n\n" );
+            Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
+        }
+*/
+        Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
+        {
+            if ( pNtkTemp == pNtk )
+                continue;
+            fprintf( pFile, "\n\n" );
             Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
         }
     }
@@ -156,7 +165,7 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
 {
     ProgressBar * pProgress;
     Abc_Obj_t * pNode, * pLatch;
-    int i;
+    int i, Length;
 
     // write the PIs
     fprintf( pFile, ".inputs" );
@@ -206,11 +215,12 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     }
 
     // write each internal node
+    Length = Abc_NtkHasMapping(pNtk)? Mio_LibraryReadGateNameMax(pNtk->pManFunc) : 0;
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        Io_NtkWriteNode( pFile, pNode );
+        Io_NtkWriteNode( pFile, pNode, Length );
     }
     Extra_ProgressBarStop( pProgress );
 }
@@ -454,13 +464,13 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
+void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length )
 {
     if ( Abc_NtkHasMapping(pNode->pNtk) )
     {
         // write the .gate line
         fprintf( pFile, ".gate" );
-        Io_NtkWriteNodeGate( pFile, pNode );
+        Io_NtkWriteNodeGate( pFile, pNode, Length );
         fprintf( pFile, "\n" );
     }
     else
@@ -485,17 +495,17 @@ void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode )
+void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length )
 {
     Mio_Gate_t * pGate = pNode->pData;
     Mio_Pin_t * pGatePin;
     int i;
     // write the node
-    fprintf( pFile, " %s ", Mio_GateReadName(pGate) );
+    fprintf( pFile, " %-*s ", Length, Mio_GateReadName(pGate) );
     for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
         fprintf( pFile, "%s=%s ", Mio_PinReadName(pGatePin), Abc_ObjName( Abc_ObjFanin(pNode,i) ) );
     assert ( i == Abc_ObjFaninNum(pNode) );
-    fprintf( pFile, "%s=%s", Mio_GateReadOutName(pGate), Abc_ObjName(pNode) );
+    fprintf( pFile, "%s=%s", Mio_GateReadOutName(pGate), Abc_ObjName( Abc_ObjFanout0(pNode) ) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 88695668..e1b2d956 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -66,7 +66,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
     }
     // convert to logic BDD network
     if ( Abc_NtkIsLogic(pNtk) )
-        Abc_NtkLogicToBdd( pNtk );
+        Abc_NtkToBdd( pNtk );
     // create solver with clauses
     pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
     if ( pSat == NULL )
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index 9524bdef..bf5182fb 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -34,7 +34,7 @@ static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk );
 static int  Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
-static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+static char * Io_WriteVerilogGetName( char * pName );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,9 +57,9 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     FILE * pFile;
     int i;
     // can only write nodes represented using local AIGs
-    if ( !Abc_NtkIsAigNetlist(pNtk) )
+    if ( !Abc_NtkIsAigNetlist(pNtk) && !Abc_NtkIsMappedNetlist(pNtk) )
     {
-        printf( "Io_WriteVerilog(): Can produce Verilog for AIG netlists only.\n" );
+        printf( "Io_WriteVerilog(): Can produce Verilog for mapped or AIG netlists only.\n" );
         return;
     }
     // start the output stream
@@ -77,16 +77,17 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     // write modules
     if ( pNtk->pDesign )
     {
+        // write the network first
+        Io_WriteVerilogInt( pFile, pNtk );
+        // write other things
         Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNetlist, i )
         {
             assert( Abc_NtkIsNetlist(pNetlist) );
             if ( pNetlist == pNtk )
                 continue;
-            Io_WriteVerilogInt( pFile, pNetlist );
             fprintf( pFile, "\n" );
+            Io_WriteVerilogInt( pFile, pNetlist );
         }
-        // write the network last
-        Io_WriteVerilogInt( pFile, pNtk );
     }
     else
     {
@@ -185,7 +186,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
     {
         pNet = Abc_ObjFanout0(pTerm);
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -193,7 +194,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -224,7 +225,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
     {
         pNet = Abc_ObjFanin0(pTerm);
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -232,7 +233,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -273,7 +274,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             continue;
         Counter++;
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -281,7 +282,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -290,7 +291,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj));
         Counter++;
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -298,7 +299,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -311,7 +312,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             pNet = Abc_ObjFanin0(pTerm);
             Counter++;
             // get the line length after this name is written
-            AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+            AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
             if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
             { // write the line extender
                 fprintf( pFile, "\n   " );
@@ -319,7 +320,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
                 LineLength  = 3;
                 NameCounter = 0;
             }
-            fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+            fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
             LineLength += AddedLength;
             NameCounter++;
         }
@@ -330,7 +331,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
                 continue;
             Counter++;
             // get the line length after this name is written
-            AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+            AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
             if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
             { // write the line extender
                 fprintf( pFile, "\n   " );
@@ -338,7 +339,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
                 LineLength  = 3;
                 NameCounter = 0;
             }
-            fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+            fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
             LineLength += AddedLength;
             NameCounter++;
         }
@@ -377,7 +378,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         pNet = Abc_ObjFanout0(Abc_ObjFanout0(pLatch));
         Counter++;
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -385,7 +386,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -402,35 +403,6 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogLatches2( FILE * pFile, Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pLatch;
-    int i;
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-//        fprintf( pFile, "  always @(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
-        fprintf( pFile, "  always begin %s",     Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-        fprintf( pFile, " = %s; end\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) );
-        if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
-//            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) );
-            fprintf( pFile, "  initial begin %s = 0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-        else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
-//            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) );
-            fprintf( pFile, "  initial begin %s = 1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the latches.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pLatch;
@@ -442,8 +414,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "  always begin\n" );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        fprintf( pFile, "    %s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-        fprintf( pFile, " <= %s;\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) );
+        fprintf( pFile, "    %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
+        fprintf( pFile, " <= %s;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch)))) );
     }
     fprintf( pFile, "  end\n" );
     // check if there are initial values
@@ -453,13 +425,13 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     if ( i == Abc_NtkLatchNum(pNtk) )
         return;
     // write the initial values
-    fprintf( pFile, "  initial begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) );
+    fprintf( pFile, "  initial begin\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0)))) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
-            fprintf( pFile, "    %s <= 1\'b0;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
+            fprintf( pFile, "    %s <= 1\'b0;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
         else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
-            fprintf( pFile, "    %s <= 1\'b1;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
+            fprintf( pFile, "    %s <= 1\'b1;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
     }
     fprintf( pFile, "  end\n" );
 }
@@ -481,48 +453,73 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkBox;
     Abc_Obj_t * pObj, * pTerm, * pFanin;
     Hop_Obj_t * pFunc;
-    int i, k, Counter, nDigits;
-
-    Counter = 1;
-    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+    int i, k, Counter, nDigits, Length;
 
     // write boxes
+    nDigits = Extra_Base10Log( Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
+    Counter = 0;
     Abc_NtkForEachBox( pNtk, pObj, i )
     {
         if ( Abc_ObjIsLatch(pObj) )
             continue;
         pNtkBox = pObj->pData;
-        fprintf( pFile, "  %s g%0*d", pNtkBox->pName, nDigits, Counter++ );
+        fprintf( pFile, "  %s box%0*d", pNtkBox->pName, nDigits, Counter++ );
         fprintf( pFile, "(" );
         Abc_NtkForEachPi( pNtkBox, pTerm, k )
         {
-            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanout0(pTerm)) );
-            fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin(pObj,k))) );
+            fprintf( pFile, ".%s",   Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pTerm))) );
+            fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin(pObj,k)))) );
         }
         Abc_NtkForEachPo( pNtkBox, pTerm, k )
         {
-            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanin0(pTerm)) );
-            fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout(pObj,k))), k==Abc_NtkPoNum(pNtkBox)-1? "":", " );
+            fprintf( pFile, ".%s",   Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(pTerm))) );
+            fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout(pObj,k)))), k==Abc_NtkPoNum(pNtkBox)-1? "":", " );
         }
         fprintf( pFile, ");\n" );
     }
     // write nodes
-    vLevels = Vec_VecAlloc( 10 );
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    if ( Abc_NtkHasMapping(pNtk) )
     {
-        pFunc = pObj->pData;
-        fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
-        // set the input names
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(pFanin));
-        // write the formula
-        Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
-        fprintf( pFile, ";\n" );
-        // clear the input names
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            free( Hop_IthVar(pNtk->pManFunc, k)->pData );
+        Length  = Mio_LibraryReadGateNameMax(pNtk->pManFunc);
+        nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+        Counter = 0;
+        Abc_NtkForEachNode( pNtk, pObj, k )
+        {
+            Mio_Gate_t * pGate = pObj->pData;
+            Mio_Pin_t * pGatePin;
+            // write the node
+            fprintf( pFile, "  %-*s g%0*d", Length, Mio_GateReadName(pGate), nDigits, Counter++ );
+            fprintf( pFile, "(" );
+            for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+            {
+                fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_PinReadName(pGatePin)) );
+                fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanin(pObj,i) )) );
+            }
+            assert ( i == Abc_ObjFaninNum(pObj) );
+            fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_GateReadOutName(pGate)) );
+            fprintf( pFile, "(%s)", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanout0(pObj) )) );
+            fprintf( pFile, ");\n" );
+        }
+    }
+    else
+    {
+        vLevels = Vec_VecAlloc( 10 );
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            pFunc = pObj->pData;
+            fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+            // set the input names
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin)));
+            // write the formula
+            Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
+            fprintf( pFile, ";\n" );
+            // clear the input names
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                free( Hop_IthVar(pNtk->pManFunc, k)->pData );
+        }
+        Vec_VecFree( vLevels );
     }
-    Vec_VecFree( vLevels );
 }
 
 /**Function*************************************************************
@@ -577,12 +574,10 @@ int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+char * Io_WriteVerilogGetName( char * pName )
 {
     static char Buffer[500];
-    char * pName;
     int Length, i;
-    pName = Abc_ObjName(pObj);
     Length = strlen(pName);
     // consider the case of a signal having name "0" or "1"
     if ( !(Length == 1 && (pName[0] == '0' || pName[0] == '1')) )
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index 575ae7bb..0ba081db 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -45,18 +45,18 @@ typedef struct Ver_Stream_t_    Ver_Stream_t;
 
 struct Ver_Man_t_
 {
+    // internal parameters
+    int             fMapped;       // mapped verilog
+    int             fUseMemMan;    // allocate memory manager in the networks
+    int             fCheck;        // checks network for currectness
     // input file stream
     char *          pFileName;
     Ver_Stream_t *  pReader;
     int             fNameLast;
     ProgressBar *   pProgress;
-    // current network and library
-    Abc_Ntk_t *     pNtkCur;       // the network under construction
-    Abc_Lib_t *     pDesign;       // the current design 
-    // parameters
-    int             fUseMemMan;    // allocate memory manager in the networks
-    int             fCheck;        // checks network for currectness
-    // error recovery
+    // current design
+    Abc_Lib_t *     pDesign;
+    // error handling
     FILE *          Output;
     int             fTopLevel;
     int             fError;
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index a8ac99e5..6c036288 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "ver.h"
+#include "mio.h"
+#include "main.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -51,50 +53,29 @@ static void Ver_ParseStop( Ver_Man_t * p );
 static void Ver_ParseFreeData( Ver_Man_t * p );
 static void Ver_ParseInternal( Ver_Man_t * p );
 static int  Ver_ParseModule( Ver_Man_t * p );
-static int  Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType );
-static int  Ver_ParseAssign( Ver_Man_t * p );
-static int  Ver_ParseAlways( Ver_Man_t * p );
-static int  Ver_ParseInitial( Ver_Man_t * p );
-static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate );
-static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType );
+static int  Ver_ParseSignal( Ver_Man_t * p, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType );
+static int  Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk );
+static int  Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk );
+static int  Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk );
+static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType );
+static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
+static int  Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
+static int  Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
+static int  Vec_ParseAttachBoxes( Ver_Man_t * pMan );
 
 static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
 static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
 static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO );
 static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
 
+static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox )  { assert( pNtkBox->pName );     return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox);  }
+static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj )   { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
+
+int glo_fMapped = 0; // this is bad!
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
- 
-/**Function*************************************************************
-
-  Synopsis    [File parser.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan )
-{
-    Ver_Man_t * p;
-    Abc_Lib_t * pDesign;
-    // start the parser
-    p = Ver_ParseStart( pFileName, pGateLib );
-    p->fCheck     = fCheck;
-    p->fUseMemMan = fUseMemMan;
-    // parse the file
-    Ver_ParseInternal( p );
-    // save the result
-    pDesign = p->pDesign;
-    p->pDesign = NULL;
-    // stop the parser
-    Ver_ParseStop( p );
-    return pDesign;
-}
 
 /**Function*************************************************************
 
@@ -114,6 +95,8 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
     memset( p, 0, sizeof(Ver_Man_t) );
     p->pFileName = pFileName;
     p->pReader   = Ver_StreamAlloc( pFileName );
+    if ( p->pReader == NULL )
+        return NULL;
     p->Output    = stdout;
     p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) );
     p->vNames    = Vec_PtrAlloc( 100 );
@@ -122,6 +105,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
     // create the design library and assign the technology library
     p->pDesign   = Abc_LibCreate( pFileName );
     p->pDesign->pLibrary = pGateLib;
+    p->pDesign->pGenlib = Abc_FrameReadLibGen();
     return p;
 }
 
@@ -138,7 +122,6 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
 ***********************************************************************/
 void Ver_ParseStop( Ver_Man_t * p )
 {
-    assert( p->pNtkCur == NULL );
     Ver_StreamFree( p->pReader );
     Extra_ProgressBarStop( p->pProgress );
     Vec_PtrFree( p->vNames   );
@@ -146,6 +129,41 @@ void Ver_ParseStop( Ver_Man_t * p )
     Vec_IntFree( p->vStackOp );
     free( p );
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan )
+{
+    Ver_Man_t * p;
+    Abc_Lib_t * pDesign;
+    // start the parser
+    p = Ver_ParseStart( pFileName, pGateLib );
+    p->fMapped    = glo_fMapped;
+    p->fCheck     = fCheck;
+    p->fUseMemMan = fUseMemMan;
+    if ( glo_fMapped )
+    {
+        Hop_ManStop(p->pDesign->pManFunc);
+        p->pDesign->pManFunc = NULL;
+    }
+    // parse the file
+    Ver_ParseInternal( p );
+    // save the result
+    pDesign = p->pDesign;
+    p->pDesign = NULL;
+    // stop the parser
+    Ver_ParseStop( p );
+    return pDesign;
+}
 
 /**Function*************************************************************
 
@@ -160,7 +178,11 @@ void Ver_ParseStop( Ver_Man_t * p )
 ***********************************************************************/
 void Ver_ParseInternal( Ver_Man_t * pMan )
 {
+    Abc_Ntk_t * pNtk;
     char * pToken;
+    int i;
+
+    // preparse the modeles
     while ( 1 )
     {
         // get the next token
@@ -173,30 +195,28 @@ void Ver_ParseInternal( Ver_Man_t * pMan )
             Ver_ParsePrintErrorMessage( pMan );
             return;
         }
-
         // parse the module
-        if ( !Ver_ParseModule( pMan ) )
+        if ( !Ver_ParseModule(pMan) )
             return;
+    }
+
+    // process defined and undefined boxes
+    if ( !Vec_ParseAttachBoxes( pMan ) )
+        return;
 
+    // connect the boxes and check
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        // fix the dangling nets
+        Abc_NtkFinalizeRead( pNtk );
         // check the network for correctness
-        if ( pMan->fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) )
-        {
-            pMan->fTopLevel = 1;
-            sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName );
-            Ver_ParsePrintErrorMessage( pMan );
-            return;
-        }
-        // add the module to the hash table
-        if ( st_is_member( pMan->pDesign->tModules, pMan->pNtkCur->pName ) )
+        if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
         {
             pMan->fTopLevel = 1;
-            sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName );
+            sprintf( pMan->sError, "The network check has failed.", pNtk->pName );
             Ver_ParsePrintErrorMessage( pMan );
             return;
         }
-        Vec_PtrPush( pMan->pDesign->vModules, pMan->pNtkCur );
-        st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur );
-        pMan->pNtkCur = NULL;
     }
 }
 
@@ -213,12 +233,6 @@ void Ver_ParseInternal( Ver_Man_t * pMan )
 ***********************************************************************/
 void Ver_ParseFreeData( Ver_Man_t * p )
 {
-    if ( p->pNtkCur )
-    {
-        p->pNtkCur->pManFunc = NULL;
-        Abc_NtkDelete( p->pNtkCur );
-        p->pNtkCur = NULL;
-    }
     if ( p->pDesign )
     {
         Abc_LibFree( p->pDesign, NULL );
@@ -249,7 +263,105 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
     Ver_ParseFreeData( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Finds the network by name or create a new blackbox network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName )
+{
+    Abc_Ntk_t * pNtkNew;
+    // check if the network exists
+    if ( pNtkNew = Abc_LibFindModelByName( pMan->pDesign, pName ) )
+        return pNtkNew;
+//printf( "Creating network %s.\n", pName );
+    // create new network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
+    pNtkNew->pName = Extra_UtilStrsav( pName );
+    pNtkNew->pSpec = NULL;
+    // add module to the design
+    Abc_LibAddModel( pMan->pDesign, pNtkNew );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the network by name or create a new blackbox network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pObj;
+    if ( pObj = Abc_NtkFindNet(pNtk, pName) )
+        return pObj;
+    if ( !strcmp( pName, "1\'b0" ) )
+        return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
+    if ( !strcmp( pName, "1\'b1" ) )
+        return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the blackbox type into a different one.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConvertNetwork( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, int fMapped )
+{
+    if ( fMapped )
+    {
+        // convert from the blackbox into the network with local functions representated by AIGs
+        if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+        {
+            // change network type
+            assert( pNtk->pManFunc == NULL );
+            pNtk->ntkFunc = ABC_FUNC_MAP;
+            pNtk->pManFunc = pMan->pDesign->pGenlib;
+        }
+        else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
+        {
+            sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+    }
+    else
+    {
+        // convert from the blackbox into the network with local functions representated by AIGs
+        if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+        {
+            // change network type
+            assert( pNtk->pManFunc == NULL );
+            pNtk->ntkFunc = ABC_FUNC_AIG;
+            pNtk->pManFunc = pMan->pDesign->pManFunc;
+        }
+        else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
+        {
+            sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+    }
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -264,26 +376,17 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
 ***********************************************************************/
 int Ver_ParseModule( Ver_Man_t * pMan )
 {
+    Mio_Gate_t * pGate;
     Ver_Stream_t * p = pMan->pReader;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    Abc_Obj_t * pNet;
     char * pWord, Symbol;
     int RetValue;
 
-    // start the current network
-    assert( pMan->pNtkCur == NULL );
-    pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
-    pNtk->ntkFunc  = ABC_FUNC_AIG;
-    pNtk->pManFunc = pMan->pDesign->pManFunc;
-
     // get the network name
     pWord = Ver_ParseGetName( pMan );
-    pNtk->pName = Extra_UtilStrsav( pWord );
-    pNtk->pSpec = NULL;
 
-    // create constant nets
-    Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
-    Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
+    // get the network with this name
+    pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord );
 
     // make sure we stopped at the opening paranthesis
     if ( Ver_StreamPopChar(p) != '(' )
@@ -313,15 +416,15 @@ int Ver_ParseModule( Ver_Man_t * pMan )
         if ( pWord == NULL )
             return 0;
         if ( !strcmp( pWord, "input" ) )
-            RetValue = Ver_ParseSignal( pMan, VER_SIG_INPUT );
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT );
         else if ( !strcmp( pWord, "output" ) )
-            RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT );
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT );
         else if ( !strcmp( pWord, "reg" ) )
-            RetValue = Ver_ParseSignal( pMan, VER_SIG_REG );
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG );
         else if ( !strcmp( pWord, "wire" ) )
-            RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE );
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
         else if ( !strcmp( pWord, "inout" ) )
-            RetValue = Ver_ParseSignal( pMan, VER_SIG_INOUT );
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT );
         else 
             break;
         if ( RetValue == 0 )
@@ -334,43 +437,38 @@ int Ver_ParseModule( Ver_Man_t * pMan )
         Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
 
         if ( !strcmp( pWord, "and" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_AND );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND );
         else if ( !strcmp( pWord, "or" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_OR );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR );
         else if ( !strcmp( pWord, "xor" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XOR );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR );
         else if ( !strcmp( pWord, "buf" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_BUF );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF );
         else if ( !strcmp( pWord, "nand" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NAND );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND );
         else if ( !strcmp( pWord, "nor" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOR );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR );
         else if ( !strcmp( pWord, "xnor" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XNOR );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR );
         else if ( !strcmp( pWord, "not" ) )
-            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOT );
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
 
         else if ( !strcmp( pWord, "assign" ) )
-            RetValue = Ver_ParseAssign( pMan );
+            RetValue = Ver_ParseAssign( pMan, pNtk );
         else if ( !strcmp( pWord, "always" ) )
-            RetValue = Ver_ParseAlways( pMan );
+            RetValue = Ver_ParseAlways( pMan, pNtk );
         else if ( !strcmp( pWord, "initial" ) )
-            RetValue = Ver_ParseInitial( pMan );
+            RetValue = Ver_ParseInitial( pMan, pNtk );
         else if ( !strcmp( pWord, "endmodule" ) )
             break;
-        else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
-            RetValue = Ver_ParseGate( pMan, pNtkTemp );
-        else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design
-            RetValue = Ver_ParseGate( pMan, pNtkTemp );
-        else
+        else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName(pMan->pDesign->pGenlib, pWord)) ) // current design
+            RetValue = Ver_ParseGate( pMan, pNtk, pGate );
+//        else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
+//            RetValue = Ver_ParseGate( pMan, pNtkTemp );
+        else // assume this is the box used in the current design
         {
-            printf( "Cannot find \"%s\".\n", pWord );
-            Ver_StreamSkipToChars( p, ";" );
-            Ver_StreamPopChar(p);
-
-//            sprintf( pMan->sError, "Cannot find \"%s\" in the library.", pWord );
-//            Ver_ParsePrintErrorMessage( pMan );
-//            return 0;
+            pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord );
+            RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp );
         }
         if ( RetValue == 0 )
             return 0;
@@ -383,28 +481,33 @@ int Ver_ParseModule( Ver_Man_t * pMan )
             return 0;
     }
 
-    // check if constant 0 net is used
-    pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
-    if ( Abc_ObjFanoutNum(pNet) == 0 )
-        Abc_NtkDeleteObj(pNet);
-    else
-        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) );
-    // check if constant 1 net is used
-    pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
-    if ( Abc_ObjFanoutNum(pNet) == 0 )
-        Abc_NtkDeleteObj(pNet);
-    else
-        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) );
-
-    // check the functionality to blackbox if insides are not defined
-    if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 )
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
     {
-        pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
-        pNtk->pManFunc = NULL;
+        if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 )
+        {
+            if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+                return 0;
+        }
+        else
+        {
+            Abc_Obj_t * pObj, * pBox, * pTerm;
+            int i; 
+            pBox = Abc_NtkCreateBlackbox(pNtk);
+            Abc_NtkForEachPi( pNtk, pObj, i )
+            {
+                pTerm = Abc_NtkCreateBi(pNtk);
+                Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) );
+                Abc_ObjAddFanin( pBox, pTerm );
+            }
+            Abc_NtkForEachPo( pNtk, pObj, i )
+            {
+                pTerm = Abc_NtkCreateBo(pNtk);
+                Abc_ObjAddFanin( pTerm, pBox );
+                Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm );
+            }
+        }
     }
-
-    // fix the dangling nets
-    Abc_NtkFinalizeRead( pNtk );
     return 1;
 }
 
@@ -419,19 +522,21 @@ int Ver_ParseModule( Ver_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
+int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType )
 {
     Ver_Stream_t * p = pMan->pReader;
-    Abc_Ntk_t * pNtk = pMan->pNtkCur;
     char Buffer[1000];
     int Lower, Upper, i;
     char * pWord;
     char Symbol;
+    Lower = Upper = 0;
     while ( 1 )
     {
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
             return 0;
+
+        // check if the range is specified
         if ( pWord[0] == '[' && !pMan->fNameLast )
         {
             Lower = atoi( pWord + 1 );
@@ -472,6 +577,20 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
                 if ( pWord == NULL )
                     return 0;
             }
+        }
+
+        // create signals
+        if ( Lower == 0 && Upper == 0 )
+        {
+            if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
+                Ver_ParseCreatePi( pNtk, pWord );
+            if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
+                Ver_ParseCreatePo( pNtk, pWord );
+            if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
+                Abc_NtkFindOrCreateNet( pNtk, pWord );
+        }
+        else
+        {
             for ( i = Lower; i <= Upper; i++ )
             {
                 sprintf( Buffer, "%s[%d]", pWord, i );
@@ -483,15 +602,7 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
                     Abc_NtkFindOrCreateNet( pNtk, Buffer );
             }
         }
-        else
-        {
-            if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
-                Ver_ParseCreatePi( pNtk, pWord );
-            if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
-                Ver_ParseCreatePo( pNtk, pWord );
-            if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
-                Abc_NtkFindOrCreateNet( pNtk, pWord );
-        }
+
         Symbol = Ver_StreamPopChar(p);
         if ( Symbol == ',' )
             continue;
@@ -515,137 +626,9 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
   SeeAlso     []
 
 ***********************************************************************/
-int Ver_ParseAssign( Ver_Man_t * pMan )
-{
-    Ver_Stream_t * p = pMan->pReader;
-    Abc_Ntk_t * pNtk = pMan->pNtkCur;
-    Abc_Obj_t * pNode, * pNet;
-    char * pWord, * pName, * pEquation;
-    Hop_Obj_t * pFunc;
-    char Symbol;
-    int i, Length, fReduction;
-
-//    if ( Ver_StreamGetLineNumber(p) == 2756 )
-//    {
-//        int x = 0;
-//    }
-
-    // convert from the mapped netlist into the BDD netlist
-    if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
-    {
-        pNtk->ntkFunc = ABC_FUNC_AIG;
-        assert( pNtk->pManFunc == NULL );
-        pNtk->pManFunc = pMan->pDesign->pManFunc;
-    }
-    else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
-    {
-        sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
-        Ver_ParsePrintErrorMessage( pMan );
-        return 0;
-    }
-
-    while ( 1 )
-    {
-        // get the name of the output signal
-        pWord = Ver_ParseGetName( pMan );
-        if ( pWord == NULL )
-            return 0;
-        // consider the case of reduction operations
-        fReduction = 0;
-        if ( pWord[0] == '{' && !pMan->fNameLast )
-            fReduction = 1;
-        if ( fReduction )
-        {
-            pWord++;
-            pWord[strlen(pWord)-1] = 0;
-            assert( pWord[0] != '\\' );
-        }
-        // get the fanout net
-        pNet = Abc_NtkFindNet( pNtk, pWord );
-        if ( pNet == NULL )
-        {
-            sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-        // get the equality sign
-        if ( Ver_StreamPopChar(p) != '=' )
-        {
-            sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-        // skip the comments
-        if ( !Ver_ParseSkipComments( pMan ) )
-            return 0;
-        // get the second name
-        if ( fReduction )
-            pEquation = Ver_StreamGetWord( p, ";" );
-        else
-            pEquation = Ver_StreamGetWord( p, ",;" );
-        if ( pEquation == NULL )
-        {
-            sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-
-        // parse the formula
-        if ( fReduction )
-            pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );  
-        else
-            pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
-        if ( pFunc == NULL )
-        {
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-
-        // create the node with the given inputs
-        pNode = Abc_NtkCreateNode( pMan->pNtkCur );
-        pNode->pData = pFunc;
-        Abc_ObjAddFanin( pNet, pNode );
-        // connect to fanin nets
-        for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
-        {
-            // get the name of this signal
-            Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
-            pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
-            pName[Length] = 0;
-            // find the corresponding net
-            pNet = Abc_NtkFindNet( pNtk, pName );
-            if ( pNet == NULL )
-            {
-                sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName );
-                Ver_ParsePrintErrorMessage( pMan );
-                return 0;
-            }
-            Abc_ObjAddFanin( pNode, pNet );
-        }
-        Symbol = Ver_StreamPopChar(p);
-        if ( Symbol == ',' )
-            continue;
-        if ( Symbol == ';' )
-            return 1;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses one directive.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ver_ParseAlways( Ver_Man_t * pMan )
+int Ver_ParseAlways( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
     Ver_Stream_t * p = pMan->pReader;
-    Abc_Ntk_t * pNtk = pMan->pNtkCur;
     Abc_Obj_t * pNet, * pNet2;
     int fStopAfterOne;
     char * pWord, * pWord2;
@@ -681,7 +664,7 @@ int Ver_ParseAlways( Ver_Man_t * pMan )
                 break;
         }
         // get the fanout net
-        pNet = Abc_NtkFindNet( pNtk, pWord );
+        pNet = Ver_ParseFindNet( pNtk, pWord );
         if ( pNet == NULL )
         {
             sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
@@ -708,11 +691,11 @@ int Ver_ParseAlways( Ver_Man_t * pMan )
         // check if the name is complemented
         if ( pWord2[0] == '~' )
         {
-            pNet2 = Abc_NtkFindNet( pNtk, pWord2+1 );
+            pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 );
             pNet2 = Ver_ParseCreateInv( pNtk, pNet2 );
         }
         else
-            pNet2 = Abc_NtkFindNet( pNtk, pWord2 );
+            pNet2 = Ver_ParseFindNet( pNtk, pWord2 );
         if ( pNet2 == NULL )
         {
             sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
@@ -742,10 +725,9 @@ int Ver_ParseAlways( Ver_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-int Ver_ParseInitial( Ver_Man_t * pMan )
+int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
     Ver_Stream_t * p = pMan->pReader;
-    Abc_Ntk_t * pNtk = pMan->pNtkCur;
     Abc_Obj_t * pNode, * pNet;
     int fStopAfterOne;
     char * pWord, * pEquation;
@@ -772,7 +754,7 @@ int Ver_ParseInitial( Ver_Man_t * pMan )
                 break;
         }
         // get the fanout net
-        pNet = Abc_NtkFindNet( pNtk, pWord );
+        pNet = Ver_ParseFindNet( pNtk, pWord );
         if ( pNet == NULL )
         {
             sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
@@ -839,40 +821,287 @@ int Ver_ParseInitial( Ver_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
+int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
     Ver_Stream_t * p = pMan->pReader;
-    Abc_Ntk_t * pNtk = pMan->pNtkCur;
-    Abc_Obj_t * pNetFormal, * pNetActual;
-    Abc_Obj_t * pObj, * pNode, * pTerm;
-    char * pWord, Symbol, * pGateName;
-    int i, fCompl, fComplUsed = 0;
-    unsigned * pPolarity;
-
-    // clean the PI/PO pointers
-    Abc_NtkForEachPi( pNtkGate, pObj, i )
-        pObj->pCopy = NULL;
-    Abc_NtkForEachPo( pNtkGate, pObj, i )
-        pObj->pCopy = NULL;
+    Abc_Obj_t * pNode, * pNet;
+    char * pWord, * pName, * pEquation;
+    Hop_Obj_t * pFunc;
+    char Symbol;
+    int i, Length, fReduction;
+
+//    if ( Ver_StreamGetLineNumber(p) == 2756 )
+//    {
+//        int x = 0;
+//    }
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+        return 0;
+
+    while ( 1 )
+    {
+        // get the name of the output signal
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // consider the case of reduction operations
+        fReduction = 0;
+        if ( pWord[0] == '{' && !pMan->fNameLast )
+            fReduction = 1;
+        if ( fReduction )
+        {
+            pWord++;
+            pWord[strlen(pWord)-1] = 0;
+            assert( pWord[0] != '\\' );
+        }
+        // get the fanout net
+        pNet = Ver_ParseFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // get the equality sign
+        if ( Ver_StreamPopChar(p) != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get the second name
+        if ( fReduction )
+            pEquation = Ver_StreamGetWord( p, ";" );
+        else
+            pEquation = Ver_StreamGetWord( p, ",;" );
+        if ( pEquation == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // consider the case of mapped network
+        if ( pMan->fMapped )
+        {
+            Vec_PtrClear( pMan->vNames );
+            if ( !strcmp( pEquation, "1\'b0" ) )
+                pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
+            else if ( !strcmp( pEquation, "1\'b1" ) )
+                pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
+            else
+            {
+                if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
+                {
+                    sprintf( pMan->sError, "Cannot read Verilog with non-trivail assignments in the mapped netlist.", pEquation );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+                Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
+                Vec_PtrPush( pMan->vNames, pEquation );
+                // get the buffer
+                pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+            }
+        }
+        else
+        {
+            // parse the formula
+            if ( fReduction )
+                pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );  
+            else
+                pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
+            if ( pFunc == NULL )
+            {
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        }
+
+        // create the node with the given inputs
+        pNode = Abc_NtkCreateNode( pNtk );
+        pNode->pData = pFunc;
+        Abc_ObjAddFanin( pNet, pNode );
+        // connect to fanin nets
+        for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
+        {
+            // get the name of this signal
+            Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
+            pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
+            pName[Length] = 0;
+            // find the corresponding net
+            pNet = Ver_ParseFindNet( pNtk, pName );
+            if ( pNet == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            Abc_ObjAddFanin( pNode, pNet );
+        }
+
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ',' )
+            continue;
+        if ( Symbol == ';' )
+            return 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNet, * pNode;
+    char * pWord, Symbol;
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+        return 0;
+
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // create the node
+    pNode = Abc_NtkCreateNode( pNtk );
+
+    // parse pairs of formal/actural inputs
+    while ( 1 )
+    {
+        // parse the output name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // get the net corresponding to this output
+        pNet = Ver_ParseFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // if this is the first net, add it as an output
+        if ( Abc_ObjFanoutNum(pNode) == 0 )
+            Abc_ObjAddFanin( pNet, pNode );
+        else
+            Abc_ObjAddFanin( pNode, pNet );
+        // check if it is the end of gate
+        Ver_ParseSkipComments( pMan );
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ')' )
+            break;
+        // skip comma
+        if ( Symbol != ',' )
+        {
+            sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Ver_ParseSkipComments( pMan );
+    }
+    if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
+    {
+        sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // add logic function
+    if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
+        pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
+        pNode->pData = Hop_CreateOr( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
+        pNode->pData = Hop_CreateExor( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
+        pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
+        pNode->pData = Hop_Not( pNode->pData );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
+{
+    Mio_Pin_t * pGatePin;
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNetActual, * pNode;
+    char * pWord, Symbol;
+
+    // convert from the blackbox into the network with local functions representated by gates
+    if ( 1 != pMan->fMapped )
+    {
+        sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // update the network type if needed
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) )
+        return 0;
+
     // parse the directive and set the pointers to the PIs/POs of the gate
     pWord = Ver_ParseGetName( pMan );
     if ( pWord == NULL )
         return 0;
     // this is gate name - throw it away
-    pGateName = pWord;
     if ( Ver_StreamPopChar(p) != '(' )
     {
-        sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName );
+        sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Mio_GateReadName(pGate) );
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
+
+    // start the node
+    pNode = Abc_NtkCreateNode( pNtk );
+    pNode->pData = pGate;
+
     // parse pairs of formal/actural inputs
+    pGatePin = Mio_GateReadPins(pGate);
     while ( 1 )
     {
         // process one pair of formal/actual parameters
         if ( Ver_StreamPopChar(p) != '.' )
         {
-            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName );
+            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
@@ -881,22 +1110,31 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
             return 0;
-        // get the formal net
-        if ( Abc_NtkIsNetlist(pNtkGate) )
-            pNetFormal = Abc_NtkFindNet( pNtkGate, pWord );
-        else // if ( Abc_NtkIsStrash(pNtkGate) )
-            assert( 0 );
-        if ( pNetFormal == NULL )
+
+        // make sure that the formal name is the same as the gate's
+        if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) 
         {
-            sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
+            if ( strcmp(pWord, Mio_GateReadOutName(pGate)) )
+            {
+                sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        }
+        else
+        {
+            if ( strcmp(pWord, Mio_PinReadName(pGatePin)) )
+            {
+                sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
         }
 
         // open the paranthesis
         if ( Ver_StreamPopChar(p) != '(' )
         {
-            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, pNtkGate->pName );
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Mio_GateReadName(pGate) );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
@@ -906,19 +1144,22 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
         if ( pWord == NULL )
             return 0;
         // check if the name is complemented
+        assert( pWord[0] != '~' );
+/*
         fCompl = (pWord[0] == '~');
         if ( fCompl )
         {
             fComplUsed = 1;
             pWord++;
-            if ( pMan->pNtkCur->pData == NULL )
-                pMan->pNtkCur->pData = Extra_MmFlexStart();
+            if ( pNtk->pData == NULL )
+                pNtk->pData = Extra_MmFlexStart();
         }
+*/
         // get the actual net
-        pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord );
+        pNetActual = Ver_ParseFindNet( pNtk, pWord );
         if ( pNetActual == NULL )
         {
-            sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord );
+            sprintf( pMan->sError, "Actual net %s is missing.", pWord );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
@@ -926,112 +1167,55 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
         // close the paranthesis
         if ( Ver_StreamPopChar(p) != ')' )
         {
-            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName );
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
 
-        // process the pair
-        if ( Abc_ObjFaninNum(pNetFormal) > 0 && Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) )  // PI net (with polarity!)
-            Abc_ObjFanin0Ntk(pNetFormal)->pCopy = Abc_ObjNotCond( pNetActual, fCompl );
-        else if ( Abc_ObjFanoutNum(pNetFormal) > 0 && Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) )  // P0 net
-        {
-            assert( fCompl == 0 );
-            Abc_ObjFanout0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
-        }
+        // add the fanin
+        if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) )
+            Abc_ObjAddFanin( pNetActual, pNode ); // fanout
         else
-        {
-            sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
+            Abc_ObjAddFanin( pNode, pNetActual ); // fanin
 
         // check if it is the end of gate
         Ver_ParseSkipComments( pMan );
         Symbol = Ver_StreamPopChar(p);
         if ( Symbol == ')' )
             break;
+
         // skip comma
         if ( Symbol != ',' )
         {
-            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName );
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
         Ver_ParseSkipComments( pMan );
+
+        // get the next pin
+        pGatePin = Mio_PinReadNext(pGatePin);
     }
 
-    // check if it is the end of gate
-    Ver_ParseSkipComments( pMan );
-    if ( Ver_StreamPopChar(p) != ';' )
+    // check that the gate as the same number of input
+    if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) )
     {
-        sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName );
+        sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
 
-    // make sure each input net is driven
-    Abc_NtkForEachPi( pNtkGate, pObj, i )
-        if ( pObj->pCopy == NULL )
-        {
-            sprintf( pMan->sError, "Formal input %s of gate %s has no actual input.", Abc_ObjName(Abc_ObjFanout0(pObj)), pNtkGate->pName );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-/*
-    // make sure each output net is driving something
-    Abc_NtkForEachPo( pNtkGate, pObj, i )
-        if ( pObj->pCopy == NULL )
-        {
-            sprintf( pMan->sError, "Formal output %s of gate %s has no actual output.", Abc_ObjName(Abc_ObjFanin0(pObj)), pNtkGate->pName );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
-*/
-
-    // allocate memory to remember the phase
-    pPolarity = NULL;
-    if ( fComplUsed )
-    {
-        int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) );
-        pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes );
-        memset( pPolarity, 0, nBytes );
-    }
-    // create box to represent this gate
-    if ( Abc_NtkHasBlackbox(pNtkGate) )
-        pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur );
-    else
-        pNode = Abc_NtkCreateWhitebox( pMan->pNtkCur );
-    pNode->pNext = (Abc_Obj_t *)pPolarity;
-    pNode->pData = pNtkGate;
-    // connect to fanin nets
-    Abc_NtkForEachPi( pNtkGate, pObj, i )
-    {
-        if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) )
-        {
-            Abc_InfoSetBit( pPolarity, i );
-            pObj->pCopy = Abc_ObjRegular( pObj->pCopy );
-        }
-        assert( !Abc_ObjIsComplement(pObj->pCopy) );
-//        Abc_ObjAddFanin( pNode, pObj->pCopy );
-        pTerm = Abc_NtkCreateBi( pNtk );
-        Abc_ObjAddFanin( pTerm, pObj->pCopy );
-        Abc_ObjAddFanin( pNode, pTerm );
-    }
-    // connect to fanout nets
-    Abc_NtkForEachPo( pNtkGate, pObj, i )
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
     {
-        if ( pObj->pCopy == NULL )
-            pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL);
-//        Abc_ObjAddFanin( pObj->pCopy, pNode );
-        pTerm = Abc_NtkCreateBo( pNtk );
-        Abc_ObjAddFanin( pTerm, pNode );
-        Abc_ObjAddFanin( pObj->pCopy, pTerm );
+        sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
     }
     return 1;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Parses one directive.]
@@ -1043,42 +1227,105 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
   SeeAlso     []
 
 ***********************************************************************/
-int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType )
+int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
 {
     Ver_Stream_t * p = pMan->pReader;
-    Hop_Man_t * pAig = pMan->pNtkCur->pManFunc;
-    Abc_Obj_t * pNet, * pNode;
+    Vec_Ptr_t * vNetPairs;
+    Abc_Obj_t * pNetFormal, * pNetActual;
+    Abc_Obj_t * pNode;
     char * pWord, Symbol;
-    // this is gate name - throw it away
+    int fCompl;
+
+    // parse the directive and set the pointers to the PIs/POs of the gate
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+
+    // create box to represent this gate
+    pNode = Abc_NtkCreateBlackbox( pNtk );
+    pNode->pData = pNtkBox;
+    Abc_ObjAssignName( pNode, pWord, NULL );
+
+    // continue parsing the box
     if ( Ver_StreamPopChar(p) != '(' )
     {
-        sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
+        sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Abc_ObjName(pNode) );
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
-    Ver_ParseSkipComments( pMan );
-    // create the node
-    pNode = Abc_NtkCreateNode( pMan->pNtkCur );
+
     // parse pairs of formal/actural inputs
+    vNetPairs = Vec_PtrAlloc( 16 );
+    pNode->pCopy = (Abc_Obj_t *)vNetPairs;
     while ( 1 )
     {
-        // parse the output name
+        // process one pair of formal/actual parameters
+        if ( Ver_StreamPopChar(p) != '.' )
+        {
+            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the formal name
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
             return 0;
-        // get the net corresponding to this output
-        pNet = Abc_NtkFindNet( pMan->pNtkCur, pWord );
-        if ( pNet == NULL )
+        // get the formal net
+        pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord );
+        Vec_PtrPush( vNetPairs, pNetFormal );
+
+        // open the paranthesis
+        if ( Ver_StreamPopChar(p) != '(' )
         {
-            sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
-        // if this is the first net, add it as an output
-        if ( Abc_ObjFanoutNum(pNode) == 0 )
-            Abc_ObjAddFanin( pNet, pNode );
+
+        // parse the actual name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // consider the case of empty name
+        fCompl = 0;
+        if ( pWord[0] == 0 )
+        {
+            // remove the formal net
+//            Vec_PtrPop( vNetPairs );
+            pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+        }
         else
-            Abc_ObjAddFanin( pNode, pNet );
+        {
+/*
+            // check if the name is complemented
+            fCompl = (pWord[0] == '~');
+            if ( fCompl )
+            {
+                pWord++;
+                if ( pNtk->pData == NULL )
+                    pNtk->pData = Extra_MmFlexStart();
+            }
+*/
+            // get the actual net
+            pNetActual = Ver_ParseFindNet( pNtk, pWord );
+            if ( pNetActual == NULL )
+            {
+                sprintf( pMan->sError, "Actual net is missing in gate %s.", Abc_ObjName(pNode) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        }
+        Vec_PtrPush( vNetPairs, Abc_ObjNotCond( pNetActual, fCompl ) );
+
+        // close the paranthesis
+        if ( Ver_StreamPopChar(p) != ')' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
         // check if it is the end of gate
         Ver_ParseSkipComments( pMan );
         Symbol = Ver_StreamPopChar(p);
@@ -1087,38 +1334,288 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType )
         // skip comma
         if ( Symbol != ',' )
         {
-            sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
         Ver_ParseSkipComments( pMan );
     }
-    if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
-    {
-        sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
-        Ver_ParsePrintErrorMessage( pMan );
-        return 0;
-    }
 
     // check if it is the end of gate
     Ver_ParseSkipComments( pMan );
     if ( Ver_StreamPopChar(p) != ';' )
     {
-        sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Abc_ObjName(pNode) );
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
-    // add logic function
-    if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
-        pNode->pData = Hop_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
-    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
-        pNode->pData = Hop_CreateOr( pAig, Abc_ObjFaninNum(pNode) );
-    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
-        pNode->pData = Hop_CreateExor( pAig, Abc_ObjFaninNum(pNode) );
-    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
-        pNode->pData = Hop_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
-    if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
-        pNode->pData = Hop_Not( pNode->pData );
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects one box to the network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
+{
+    Vec_Ptr_t * vNetPairs = (Vec_Ptr_t *)pBox->pCopy;
+    Abc_Ntk_t * pNtk = pBox->pNtk;
+    Abc_Ntk_t * pNtkBox = pBox->pData;
+    Abc_Obj_t * pNet, * pTerm, * pTermNew;
+    int i;
+
+    assert( !Ver_ObjIsConnected(pBox) );
+    assert( Ver_NtkIsDefined(pNtkBox) );
+    assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
+
+    // clean the PI/PO nets
+    Abc_NtkForEachPi( pNtkBox, pTerm, i )
+        Abc_ObjFanout0(pTerm)->pCopy = NULL;
+    Abc_NtkForEachPo( pNtkBox, pTerm, i )
+        Abc_ObjFanin0(pTerm)->pCopy = NULL;
+
+    // map formal nets into actual nets
+    Vec_PtrForEachEntry( vNetPairs, pNet, i )
+    {
+        // get the actual net corresponding to this formal net (pNet)
+        pNet->pCopy = Vec_PtrEntry( vNetPairs, ++i );
+        // make sure the actual net is not complemented (otherwise need to use polarity)
+        assert( !Abc_ObjIsComplement(pNet->pCopy) );
+    }
+
+    // make sure all PI nets are assigned
+    Abc_NtkForEachPi( pNtkBox, pTerm, i )
+    {
+        if ( Abc_ObjFanout0(pTerm)->pCopy == NULL )
+        {
+            sprintf( pMan->sError, "Input formal net %s of network %s is not driven in box %s.", 
+                Abc_ObjName(Abc_ObjFanout0(pTerm)), pNtkBox->pName, Abc_ObjName(pBox) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        pTermNew = Abc_NtkCreateBi( pNtk );
+        Abc_ObjAddFanin( pBox, pTermNew );
+        Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy );
+    }
+
+    // create fanins of the box
+    Abc_NtkForEachPo( pNtkBox, pTerm, i )
+    {
+        if ( Abc_ObjFanin0(pTerm)->pCopy == NULL )
+            Abc_ObjFanin0(pTerm)->pCopy = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+        pTermNew = Abc_NtkCreateBo( pNtk );
+        Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, pTermNew );
+        Abc_ObjAddFanin( pTermNew, pBox );
+    }
+
+    // free the mapping
+    Vec_PtrFree( vNetPairs );
+    pBox->pCopy = NULL;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Attaches the boxes to the network.]
+
+  Description [Makes sure that the undefined boxes are connected correctly.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Vec_ParseAttachBoxes( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk, * pNtkBox;
+    Vec_Ptr_t * vEnvoys, * vNetPairs, * vPivots;
+    Abc_Obj_t * pBox, * pTerm, * pNet, * pNetDr, * pNetAct;
+    int i, k, m, nBoxes;
+
+    // connect defined boxes
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        {
+            if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) )
+                if ( !Ver_ParseConnectBox( pMan, pBox ) )
+                    return 0;
+        }
+    }
+
+    // convert blackboxes to whiteboxes
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        {
+            pNtkBox = pBox->pData;
+            if ( pNtkBox == NULL )
+                continue;
+
+            if ( !strcmp( pNtkBox->pName, "ADDHX1" ) )
+            {
+                int x = 0;
+            }
+
+            if ( pBox->pData && !Abc_NtkHasBlackbox(pBox->pData) )
+                Abc_ObjBlackboxToWhitebox( pBox );
+        }   
+
+
+    // search for undefined boxes
+    nBoxes = 0;
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        nBoxes += !Ver_NtkIsDefined(pNtk);
+    // quit if no undefined boxes are found
+    if ( nBoxes == 0 )
+        return 1;
+
+    // count how many times each box occurs
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        assert( pNtk->pData == NULL );
+        pNtk->pData = NULL;
+    }
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        {
+            if ( pBox->pData == NULL )
+                continue;
+            pNtkBox = pBox->pData;
+            pNtkBox->pData = (void *)((int)pNtkBox->pData + 1);
+        }
+
+    // print the boxes
+    printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes );
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        if ( !Ver_NtkIsDefined(pNtk) )
+            printf( "%s (%d)  ", Abc_NtkName(pNtk), (int)pNtk->pData );
+    printf( "\n" );
+
+    // clean the boxes
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        pNtk->pData = NULL;
+
+
+    // map actual nets into formal nets belonging to the undef boxes
+    vPivots = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        {
+            if ( pBox->pData == NULL || Ver_NtkIsDefined(pBox->pData) )
+                continue;
+            vNetPairs = (Vec_Ptr_t *)pBox->pCopy;
+            Vec_PtrForEachEntry( vNetPairs, pNet, m )
+            {
+                pNetAct = Vec_PtrEntry( vNetPairs, ++m );
+                // skip already driven nets and constants
+                if ( Abc_ObjFaninNum(pNetAct) == 1 )
+                    continue;
+                if ( !(strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1")) ) // constant
+                    continue;
+                // add this net
+                if ( pNetAct->pData == NULL )
+                {
+                    pNetAct->pData = Vec_PtrAlloc( 16 );
+                    Vec_PtrPush( vPivots, pNetAct );
+                }
+                vEnvoys = pNetAct->pData;
+                Vec_PtrPush( vEnvoys, pNet );
+            }
+        }
+    }
+
+    // for each pivot net, find the driver
+    Vec_PtrForEachEntry( vPivots, pNetAct, i )
+    {
+        char * pName = Abc_ObjName(pNetAct);
+/*
+        if ( !strcmp( Abc_ObjName(pNetAct), "dma_fifo_ff_cnt[2]" ) )
+        {
+            int x = 0;
+        }
+*/
+        assert( Abc_ObjFaninNum(pNetAct) == 0 );
+        assert( strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1") );
+        vEnvoys = pNetAct->pData; pNetAct->pData = NULL;
+        // find the driver starting from the last nets
+        pNetDr = NULL;
+        for ( m = 0; m < 64; m++ )
+        {
+            Vec_PtrForEachEntry( vEnvoys, pNet, k )
+            {
+                if ( Abc_ObjId(pNet) == 0 )
+                    continue;
+                if ( (int)Abc_ObjId(pNet) == Abc_NtkObjNumMax(pNet->pNtk) - 1 - m )
+                {
+                    pNetDr = pNet;
+                    break;
+                }
+            }
+            if ( pNetDr )
+                break;
+        }
+        assert( pNetDr != NULL );
+        Vec_PtrWriteEntry( vPivots, i, pNetDr );
+        Vec_PtrFree( vEnvoys );
+    }
+
+    // for each pivot net, create driver
+    Vec_PtrForEachEntry( vPivots, pNetDr, i )
+    {
+        if ( pNetDr == NULL )
+            continue;
+        assert( Abc_ObjFaninNum(pNetDr) <= 1 );
+        if ( Abc_ObjFaninNum(pNetDr) == 1 )
+            continue;
+        // drive this net with the box
+        pTerm = Abc_NtkCreateBo( pNetDr->pNtk );
+        assert( Abc_NtkBoxNum(pNetDr->pNtk) <= 1 );
+        pBox = Abc_NtkBoxNum(pNetDr->pNtk)? Abc_NtkBox(pNetDr->pNtk,0) : Abc_NtkCreateBlackbox(pNetDr->pNtk);
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNetDr->pNtk), pNetDr );
+        Abc_ObjAddFanin( pNetDr, pTerm );
+        Abc_ObjAddFanin( pTerm, pBox );
+    }
+    Vec_PtrFree( vPivots );
+
+    // connect the remaining boxes
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        if ( Abc_NtkPiNum(pNtk) )
+            continue;
+        Abc_NtkForEachNet( pNtk, pNet, k )
+        {
+            if ( Abc_ObjFaninNum(pNet) )
+                continue;
+            // drive this net
+            pTerm = Abc_NtkCreateBi( pNet->pNtk );
+            assert( Abc_NtkBoxNum(pNet->pNtk) <= 1 );
+            pBox = Abc_NtkBoxNum(pNet->pNtk)? Abc_NtkBox(pNet->pNtk,0) : Abc_NtkCreateBlackbox(pNet->pNtk);
+            Abc_ObjAddFanin( pBox, pTerm );
+            Abc_ObjAddFanin( pTerm, pNet );
+            Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(pNet->pNtk) );
+        }
+    }
+
+    // connect the remaining boxes
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        {
+            char * pName = Abc_ObjName(pBox);
+            if ( !Ver_ObjIsConnected(pBox) )
+                if ( !Ver_ParseConnectBox( pMan, pBox ) )
+                    return 0;
+        }
+    }
     return 1;
 }
 
@@ -1138,9 +1635,9 @@ Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName )
 {
     Abc_Obj_t * pNet, * pTerm;
     // get the PI net
-    pNet  = Abc_NtkFindNet( pNtk, pName );
-    if ( pNet )
-        printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
+//    pNet  = Ver_ParseFindNet( pNtk, pName );
+//    if ( pNet )
+//        printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
     pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
     // add the PI node
     pTerm = Abc_NtkCreatePi( pNtk );
@@ -1163,9 +1660,9 @@ Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName )
 {
     Abc_Obj_t * pNet, * pTerm;
     // get the PO net
-    pNet  = Abc_NtkFindNet( pNtk, pName );
-    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
-        printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
+//    pNet  = Ver_ParseFindNet( pNtk, pName );
+//    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
+//        printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
     pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
     // add the PO node
     pTerm = Abc_NtkCreatePo( pNtk );
@@ -1224,6 +1721,50 @@ Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
     return pNet;
 }
 
+
+
+/*
+    // allocate memory to remember the phase
+    pPolarity = NULL;
+    if ( fComplUsed )
+    {
+        int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkBox) );
+        pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pNtk->pData, nBytes );
+        memset( pPolarity, 0, nBytes );
+    }
+    // create box to represent this gate
+    if ( Abc_NtkHasBlackbox(pNtkBox) )
+        pNode = Abc_NtkCreateBlackbox( pNtk );
+    else
+        pNode = Abc_NtkCreateWhitebox( pNtk );
+    pNode->pNext = (Abc_Obj_t *)pPolarity;
+    pNode->pData = pNtkBox;
+    // connect to fanin nets
+    Abc_NtkForEachPi( pNtkBox, pObj, i )
+    {
+        if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) )
+        {
+            Abc_InfoSetBit( pPolarity, i );
+            pObj->pCopy = Abc_ObjRegular( pObj->pCopy );
+        }
+        assert( !Abc_ObjIsComplement(pObj->pCopy) );
+//        Abc_ObjAddFanin( pNode, pObj->pCopy );
+        pTerm = Abc_NtkCreateBi( pNtk );
+        Abc_ObjAddFanin( pTerm, pObj->pCopy );
+        Abc_ObjAddFanin( pNode, pTerm );
+    }
+    // connect to fanout nets
+    Abc_NtkForEachPo( pNtkBox, pObj, i )
+    {
+        if ( pObj->pCopy == NULL )
+            pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL);
+//        Abc_ObjAddFanin( pObj->pCopy, pNode );
+        pTerm = Abc_NtkCreateBo( pNtk );
+        Abc_ObjAddFanin( pTerm, pNode );
+        Abc_ObjAddFanin( pObj->pCopy, pTerm );
+    }
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c
index 16192f6a..253754ae 100644
--- a/src/base/ver/verFormula.c
+++ b/src/base/ver/verFormula.c
@@ -72,8 +72,8 @@ static int         Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames
 ***********************************************************************/
 void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
 {
-    Hop_Obj_t * bFunc, * bTemp;
     char * pTemp;
+    Hop_Obj_t * bFunc, * bTemp;
     int nParans, Flag;
     int Oper, Oper1, Oper2;
     int v;
diff --git a/src/base/ver/verParse.c b/src/base/ver/verParse.c
index f3afaca0..9462fc8b 100644
--- a/src/base/ver/verParse.c
+++ b/src/base/ver/verParse.c
@@ -100,7 +100,7 @@ char * Ver_ParseGetName( Ver_Man_t * pMan )
     {
         pMan->fNameLast = 1;
         Ver_StreamPopChar( p );
-        pWord = Ver_StreamGetWord( p, " " );
+        pWord = Ver_StreamGetWord( p, " \r\n" );
     }
     else
         pWord = Ver_StreamGetWord( p, " \t\n\r(),;" );
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index dabc05dd..dbe2420b 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -98,6 +98,7 @@ extern float             Mio_LibraryReadDelayAnd2Max( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadAreaInv    ( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadAreaBuf    ( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadAreaNand2  ( Mio_Library_t * pLib );
+extern int               Mio_LibraryReadGateNameMax( Mio_Library_t * pLib );
 extern char *            Mio_GateReadName          ( Mio_Gate_t * pGate );      
 extern char *            Mio_GateReadOutName       ( Mio_Gate_t * pGate );      
 extern double            Mio_GateReadArea          ( Mio_Gate_t * pGate );      
@@ -120,8 +121,8 @@ extern double            Mio_PinReadDelayFanoutFall( Mio_Pin_t * pPin );
 extern double            Mio_PinReadDelayBlockMax  ( Mio_Pin_t * pPin );  
 extern Mio_Pin_t *       Mio_PinReadNext           ( Mio_Pin_t * pPin );  
 /*=== mioRead.c =============================================================*/
-extern Mio_Library_t *   Mio_LibraryRead( Abc_Frame_t * pAbc, char * FileName, char * ExcludeFile, int fVerbose );
-extern int               Mio_LibraryReadExclude( Abc_Frame_t * pAbc, char * ExcludeFile, st_table * tExcludeGate );
+extern Mio_Library_t *   Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFile, int fVerbose );
+extern int               Mio_LibraryReadExclude( void * pAbc, char * ExcludeFile, st_table * tExcludeGate );
 /*=== mioFunc.c =============================================================*/
 extern int               Mio_LibraryParseFormulas( Mio_Library_t * pLib );
 /*=== mioUtils.c =============================================================*/
diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c
index a9aaac19..73473f8b 100644
--- a/src/map/mio/mioApi.c
+++ b/src/map/mio/mioApi.c
@@ -60,6 +60,30 @@ float             Mio_LibraryReadAreaNand2     ( Mio_Library_t * pLib )  { retur
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the longest gate name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_LibraryReadGateNameMax( Mio_Library_t * pLib )
+{
+    Mio_Gate_t * pGate;
+    int LenMax = 0, LenCur;
+    Mio_LibraryForEachGate( pLib, pGate )
+    {
+        LenCur = strlen( Mio_GateReadName(pGate) );
+        if ( LenMax < LenCur )
+            LenMax = LenCur;
+    }
+    return LenMax;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Read Mvc of the gate by name.]
 
   Description []
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 95728e9a..4cc5e56b 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -197,7 +197,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
     Abc_NtkSweep( pNtk, 0 );
 
     // convert into the AIG
-    if ( !Abc_NtkLogicToAig(pNtk) )
+    if ( !Abc_NtkToAig(pNtk) )
     {
         fprintf( stdout, "Converting to BDD has failed.\n" );
         Res_ManFree( p );
diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c
index 93181898..551ec594 100644
--- a/src/opt/ret/retCore.c
+++ b/src/opt/ret/retCore.c
@@ -116,7 +116,7 @@ int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk )
     extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
     Abc_Ntk_t * pNtkRet;
     assert( Abc_NtkIsLogic(pNtk) );
-    Abc_NtkLogicToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0 );
 //    if ( !Abc_NtkCheck( pNtk ) )
 //        fprintf( stdout, "Abc_NtkRetimeDebug(): Network check has failed.\n" );
 //    Io_WriteBlifLogic( pNtk, "debug_temp.blif", 1 );
diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c
index 156df0dc..dcb71c60 100644
--- a/src/opt/ret/retInit.c
+++ b/src/opt/ret/retInit.c
@@ -50,7 +50,7 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue
         return Vec_IntDup( vValues );
     // convert the target network to AIG
     pNtkLogic = Abc_NtkDup( pNtkCone );
-    Abc_NtkLogicToAig( pNtkLogic );
+    Abc_NtkToAig( pNtkLogic );
     // get the miter
     pNtkMiter = Abc_NtkCreateTarget( pNtkLogic, pNtkLogic->vCos, vValues );
     if ( fVerbose )
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index c7340824..9d27e892 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -677,7 +677,7 @@ void ABC_Dump_Bench_File( ABC_Manager mng )
  
     // derive the netlist
     pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0 );
-    pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig );
+    pNtkTemp = Abc_NtkToNetlistBench( pNtkAig );
     Abc_NtkDelete( pNtkAig );
     if ( pNtkTemp == NULL ) 
         { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }