Renamed Abc_Lib_t into Abc_Des_t and removed some dead code.

11 files changed, 105 insertions, 452 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index ad74c2a7..d6aafd08 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -111,7 +111,7 @@ typedef enum {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Abc_Lib_t_       Abc_Lib_t;
+typedef struct Abc_Des_t_       Abc_Des_t;
 typedef struct Abc_Ntk_t_       Abc_Ntk_t;
 typedef struct Abc_Obj_t_       Abc_Obj_t;
 typedef struct Abc_Aig_t_       Abc_Aig_t;
@@ -176,7 +176,8 @@ struct Abc_Ntk_t_
     Abc_Ntk_t *       pNetBackup;    // the pointer to the previous backup network
     int               iStep;         // the generation number for the given network
     // hierarchy
-    Abc_Lib_t *       pDesign;
+    Abc_Des_t *       pDesign;       // design (hierarchical networks only)     
+    Abc_Ntk_t *       pAltView;      // alternative structural view of the network
     int               fHieVisited;   // flag to mark the visited network
     int               fHiePath;      // flag to mark the network on the path
     int               Id;            // model ID
@@ -187,7 +188,6 @@ struct Abc_Ntk_t_
     Mem_Fixed_t *     pMmObj;        // memory manager for objects
     Mem_Step_t *      pMmStep;       // memory manager for arrays
     void *            pManFunc;      // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
-//    Abc_Lib_t *       pVerLib;       // for structural verilog designs
     Abc_ManTime_t *   pManTime;      // the timing manager (for mapped networks) stores arrival/required times for all nodes
     void *            pManCut;       // the cut manager (for AIGs) stores information about the cuts computed for the nodes
     float             AndGateDelay;  // an average estimated delay of one AND gate
@@ -214,14 +214,14 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
 };
 
-struct Abc_Lib_t_ 
+struct Abc_Des_t_ 
 {
     char *            pName;         // the name of the library
     void *            pManFunc;      // functionality manager for the nodes
     Vec_Ptr_t *       vTops;         // the array of top-level modules
     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
+    Abc_Des_t *       pLibrary;      // the library used to map this design
     void *            pGenlib;       // the genlib library used to map this design
 };
 
@@ -667,13 +667,13 @@ extern ABC_DLL Abc_Obj_t *        Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t *
 extern ABC_DLL void               Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
  /*=== abcLib.c ==========================================================*/
-extern ABC_DLL Abc_Lib_t *        Abc_LibCreate( char * pName );
-extern ABC_DLL void               Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
-extern ABC_DLL void               Abc_LibPrint( Abc_Lib_t * pLib );
-extern ABC_DLL int                Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
-extern ABC_DLL Abc_Ntk_t *        Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
-extern ABC_DLL int                Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
-extern ABC_DLL Abc_Ntk_t *        Abc_LibDeriveRoot( Abc_Lib_t * pLib );
+extern ABC_DLL Abc_Des_t *        Abc_DesCreate( char * pName );
+extern ABC_DLL void               Abc_DesFree( Abc_Des_t * p, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_DesPrint( Abc_Des_t * p );
+extern ABC_DLL int                Abc_DesAddModel( Abc_Des_t * p, Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_DesFindModelByName( Abc_Des_t * p, char * pName );
+extern ABC_DLL int                Abc_DesFindTopLevelModels( Abc_Des_t * p );
+extern ABC_DLL Abc_Ntk_t *        Abc_DesDeriveRoot( Abc_Des_t * p );
 /*=== abcLog.c ==========================================================*/
 extern ABC_DLL void               Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pSeqCex, int Status, int nFrames, char * pCommand );
 /*=== abcMap.c ==========================================================*/
diff --git a/src/base/abc/abcBarBuf.c b/src/base/abc/abcBarBuf.c
index 7c95b8d3..6df8fd5a 100644
--- a/src/base/abc/abcBarBuf.c
+++ b/src/base/abc/abcBarBuf.c
@@ -179,6 +179,7 @@ Abc_Obj_t * Abc_NtkToBarBufs_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNet )
 }
 Abc_Ntk_t * Abc_NtkToBarBufs( Abc_Ntk_t * pNtk )
 {
+    char Buffer[1000];
     Vec_Ptr_t * vLiMaps, * vLoMaps;
     Abc_Ntk_t * pNtkNew, * pTemp;
     Abc_Obj_t * pLatch, * pObjLi, * pObjLo;
@@ -208,8 +209,10 @@ Abc_Ntk_t * Abc_NtkToBarBufs( Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pLatch, pObjLi );
         Abc_ObjAddFanin( pObjLo, pLatch );
         pLatch->pData = (void *)ABC_INIT_ZERO;
-        Abc_ObjAssignName( pObjLi, Abc_ObjName(Abc_ObjFanin0(pLiMap)), "_li" );
-        Abc_ObjAssignName( pObjLo, Abc_ObjName(Abc_ObjFanout0(pLoMap)), "_lo" );
+        sprintf( Buffer, "_%s_in", Abc_NtkName(Abc_ObjFanin0(pLiMap)->pNtk) );
+        Abc_ObjAssignName( pObjLi, Abc_ObjName(Abc_ObjFanin0(pLiMap)), Buffer );
+        sprintf( Buffer, "_%s_out", Abc_NtkName(Abc_ObjFanout0(pLoMap)->pNtk) );
+        Abc_ObjAssignName( pObjLo, Abc_ObjName(Abc_ObjFanout0(pLoMap)), Buffer );
         pLiMap->pCopy = pObjLi;
         Abc_ObjFanout0(pLoMap)->pCopy = pObjLo;
         assert( Abc_ObjIsNet(Abc_ObjFanout0(pLoMap)) );
@@ -277,9 +280,9 @@ Abc_Ntk_t * Abc_NtkFromBarBufs( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtk )
                 pObj->pCopy->pData = Abc_ObjModel(pObj)->pCopy;
     // create the design
     pNtkNew = pNtkBase->pCopy;
-    pNtkNew->pDesign = Abc_LibCreate( pNtkBase->pDesign->pName );
+    pNtkNew->pDesign = Abc_DesCreate( pNtkBase->pDesign->pName );
     Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkBase->pDesign->vModules, pTemp, i )
-        Abc_LibAddModel( pNtkNew->pDesign, pTemp->pCopy );
+        Abc_DesAddModel( pNtkNew->pDesign, pTemp->pCopy );
     Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkBase->pDesign->vTops, pTemp, i )
         Vec_PtrPush( pNtkNew->pDesign->vTops, pTemp->pCopy );
     assert( Vec_PtrEntry(pNtkNew->pDesign->vTops, 0) == pNtkNew );
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index c8f4e8aa..dc22930c 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -187,7 +187,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy2( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pTerm, * pNet;
     int i, Counter;
-    extern Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave );
+    extern Abc_Des_t * Abc_DesDupBlackboxes( Abc_Des_t * p, Abc_Ntk_t * pNtkSave );
 
     assert( Abc_NtkIsNetlist(pNtk) );
     // start the network
@@ -225,7 +225,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy2( Abc_Ntk_t * pNtk )
     {
         // pass on the design
         assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk );
-        pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew );
+        pNtkNew->pDesign = Abc_DesDupBlackboxes( pNtk->pDesign, pNtkNew );
         // update the pointers
         Abc_NtkForEachBlackbox( pNtkNew, pTerm, i )
             pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
@@ -512,7 +512,7 @@ void Abc_NtkPrintBoxInfo( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
 {
-    extern Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave );
+    extern Abc_Des_t * Abc_DesDupBlackboxes( Abc_Des_t * p, Abc_Ntk_t * pNtkSave );
     Vec_Str_t * vPref;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pTerm, * pNet;
@@ -558,7 +558,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
     {
         // pass on the design
         assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk );
-        pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew );
+        pNtkNew->pDesign = Abc_DesDupBlackboxes( pNtk->pDesign, pNtkNew );
         // update the pointers
         Abc_NtkForEachBlackbox( pNtkNew, pTerm, i )
             pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
@@ -689,7 +689,7 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL )
 {
-    Abc_Lib_t * pDesign;
+    Abc_Des_t * pDesign;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObjH, * pObjL, * pNetH, * pNetL, * pTermH;
     int i, k;
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index a529ea82..8e229975 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -42,11 +42,11 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Lib_t * Abc_LibCreate( char * pName )
+Abc_Des_t * Abc_DesCreate( char * pName )
 {
-    Abc_Lib_t * p;
-    p = ABC_ALLOC( Abc_Lib_t, 1 );
-    memset( p, 0, sizeof(Abc_Lib_t) );
+    Abc_Des_t * p;
+    p = ABC_ALLOC( Abc_Des_t, 1 );
+    memset( p, 0, sizeof(Abc_Des_t) );
     p->pName    = Abc_UtilStrsav( pName );
     p->tModules = st__init_table( strcmp, st__strhash );
     p->vTops    = Vec_PtrAlloc( 100 );
@@ -67,19 +67,19 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
+void Abc_DesFree( Abc_Des_t * p, Abc_Ntk_t * pNtkSave )
 {
     Abc_Ntk_t * pNtk;
     int i;
-    if ( pLib->pName )
-        ABC_FREE( pLib->pName );
-    if ( pLib->pManFunc )
-        Hop_ManStop( (Hop_Man_t *)pLib->pManFunc );
-    if ( pLib->tModules )
-        st__free_table( pLib->tModules );
-    if ( pLib->vModules )
+    if ( p->pName )
+        ABC_FREE( p->pName );
+    if ( p->pManFunc )
+        Hop_ManStop( (Hop_Man_t *)p->pManFunc );
+    if ( p->tModules )
+        st__free_table( p->tModules );
+    if ( p->vModules )
     {
-        Vec_PtrForEachEntry( Abc_Ntk_t *, pLib->vModules, pNtk, i )
+        Vec_PtrForEachEntry( Abc_Ntk_t *, p->vModules, pNtk, i )
         {
             if ( pNtk == pNtkSave )
                 continue;
@@ -89,11 +89,11 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
                 pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
         }
-        Vec_PtrFree( pLib->vModules );
+        Vec_PtrFree( p->vModules );
     }
-    if ( pLib->vTops )
-        Vec_PtrFree( pLib->vTops );
-    ABC_FREE( pLib );
+    if ( p->vTops )
+        Vec_PtrFree( p->vTops );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -107,21 +107,21 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
+Abc_Des_t * Abc_DesDupBlackboxes( Abc_Des_t * p, Abc_Ntk_t * pNtkSave )
 {
-    Abc_Lib_t * pLibNew;
+    Abc_Des_t * pNew;
     Abc_Ntk_t * pNtkTemp;
     int i;
-    assert( Vec_PtrSize(pLib->vTops) > 0 );
-    assert( Vec_PtrSize(pLib->vModules) > 1 );
-    pLibNew = Abc_LibCreate( pLib->pName );
-//    pLibNew->pManFunc = pNtkSave->pManFunc;
-    Vec_PtrPush( pLibNew->vTops, pNtkSave );
-    Vec_PtrPush( pLibNew->vModules, pNtkSave );
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pLib->vModules, pNtkTemp, i )
+    assert( Vec_PtrSize(p->vTops) > 0 );
+    assert( Vec_PtrSize(p->vModules) > 1 );
+    pNew = Abc_DesCreate( p->pName );
+//    pNew->pManFunc = pNtkSave->pManFunc;
+    Vec_PtrPush( pNew->vTops, pNtkSave );
+    Vec_PtrPush( pNew->vModules, pNtkSave );
+    Vec_PtrForEachEntry( Abc_Ntk_t *, p->vModules, pNtkTemp, i )
         if ( Abc_NtkHasBlackbox( pNtkTemp ) )
-            Vec_PtrPush( pLibNew->vModules, Abc_NtkDup(pNtkTemp) );
-    return pLibNew;
+            Vec_PtrPush( pNew->vModules, Abc_NtkDup(pNtkTemp) );
+    return pNew;
 }
 
 
@@ -136,13 +136,13 @@ Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_LibPrint( Abc_Lib_t * pLib )
+void Abc_DesPrint( Abc_Des_t * p )
 {
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pObj;
     int i, k;
-    printf( "Models of design %s:\n", pLib->pName );
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pLib->vModules, pNtk, i )
+    printf( "Models of design %s:\n", p->pName );
+    Vec_PtrForEachEntry( Abc_Ntk_t *, p->vModules, pNtk, i )
     {
         printf( "%2d : %20s   ", i+1, pNtk->pName );
         printf( "nd = %6d   lat = %6d   whitebox = %3d   blackbox = %3d\n", 
@@ -168,15 +168,15 @@ void Abc_LibPrint( Abc_Lib_t * pLib )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk )
+int Abc_DesAddModel( Abc_Des_t * p, Abc_Ntk_t * pNtk )
 {
-    if ( st__is_member( pLib->tModules, (char *)pNtk->pName ) )
+    if ( st__is_member( p->tModules, (char *)pNtk->pName ) )
         return 0;
-    st__insert( pLib->tModules, (char *)pNtk->pName, (char *)pNtk );
+    st__insert( p->tModules, (char *)pNtk->pName, (char *)pNtk );
     assert( pNtk->Id == 0 );
-    pNtk->Id = Vec_PtrSize(pLib->vModules);
-    Vec_PtrPush( pLib->vModules, pNtk );
-    pNtk->pDesign = pLib;
+    pNtk->Id = Vec_PtrSize(p->vModules);
+    Vec_PtrPush( p->vModules, pNtk );
+    pNtk->pDesign = p;
     return 1;
 }
 
@@ -191,12 +191,12 @@ int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName )
+Abc_Ntk_t * Abc_DesFindModelByName( Abc_Des_t * p, char * pName )
 {
     Abc_Ntk_t * pNtk;
-    if ( ! st__is_member( pLib->tModules, (char *)pName ) )
+    if ( ! st__is_member( p->tModules, (char *)pName ) )
         return NULL;
-    st__lookup( pLib->tModules, (char *)pName, (char **)&pNtk );
+    st__lookup( p->tModules, (char *)pName, (char **)&pNtk );
     return pNtk;
 }
 
@@ -211,16 +211,16 @@ Abc_Ntk_t * Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib )
+Abc_Ntk_t * Abc_DesDeriveRoot( Abc_Des_t * p )
 {
     Abc_Ntk_t * pNtk;
-    if ( Vec_PtrSize(pLib->vModules) > 1 )
+    if ( Vec_PtrSize(p->vModules) > 1 )
     {
         printf( "The design includes more than one module and is currently not used.\n" );
         return NULL;
     }
-    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pLib->vModules, 0 );  Vec_PtrClear( pLib->vModules );
-    pNtk->pManFunc = pLib->pManFunc;           pLib->pManFunc = NULL;
+    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( p->vModules, 0 );  Vec_PtrClear( p->vModules );
+    pNtk->pManFunc = p->pManFunc;           p->pManFunc = NULL;
     return pNtk;
 }
 
@@ -235,17 +235,17 @@ Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib )
+int Abc_DesFindTopLevelModels( Abc_Des_t * p )
 {
     Abc_Ntk_t * pNtk, * pNtkBox;
     Abc_Obj_t * pObj;
     int i, k;
-    assert( Vec_PtrSize( pLib->vModules ) > 0 );
+    assert( Vec_PtrSize( p->vModules ) > 0 );
     // clear the models
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pLib->vModules, pNtk, i )
+    Vec_PtrForEachEntry( Abc_Ntk_t *, p->vModules, pNtk, i )
         pNtk->fHieVisited = 0;
     // mark all the models reachable from other models
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pLib->vModules, pNtk, i )
+    Vec_PtrForEachEntry( Abc_Ntk_t *, p->vModules, pNtk, i )
     {
         Abc_NtkForEachBox( pNtk, pObj, k )
         {
@@ -258,74 +258,20 @@ int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib )
         }
     }
     // collect the models that are not marked
-    Vec_PtrClear( pLib->vTops );
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pLib->vModules, pNtk, i )
+    Vec_PtrClear( p->vTops );
+    Vec_PtrForEachEntry( Abc_Ntk_t *, p->vModules, pNtk, i )
     {
         if ( pNtk->fHieVisited == 0 )
-            Vec_PtrPush( pLib->vTops, pNtk );
+            Vec_PtrPush( p->vTops, pNtk );
         else
             pNtk->fHieVisited = 0;
     }
-    return Vec_PtrSize( pLib->vTops );
+    return Vec_PtrSize( p->vTops );
 }
 
 
 /**Function*************************************************************
 
-  Synopsis    [Surround boxes without content (black boxes) with BIs/BOs.]
-
-  Description [Returns the number of black boxes converted.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
-{
-/*
-    Abc_Obj_t * pObj, * pFanin, * pFanout;
-    int i, k;
-    assert( Abc_NtkIsNetlist(pNtk) );
-    // collect blackbox nodes
-    assert( Vec_PtrSize(pNtk->vBoxes) == 0 );
-    Vec_PtrClear( pNtk->vBoxes );
-    Abc_NtkForEachBox( pNtk, pObj, i )
-        if ( Abc_NtkNodeNum(pObj->pData) == 0 )
-            Vec_PtrPush( pNtk->vBoxes, pObj );
-    // return if there is no black boxes without content
-    if ( Vec_PtrSize(pNtk->vBoxes) == 0 )
-        return 0;
-    // print the boxes
-    printf( "Black boxes are: " );
-    Abc_NtkForEachBox( pNtk, pObj, i )
-        printf( " %s", ((Abc_Ntk_t *)pObj->pData)->pName );
-    printf( "\n" );
-    // iterate through the boxes and add BIs/BOs
-    Abc_NtkForEachBox( pNtk, pObj, i )
-    {
-        // go through the fanin nets
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BI );
-        // go through the fanout nets
-        Abc_ObjForEachFanout( pObj, pFanout, k )
-        {
-            Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BO );
-            // if the name is not given assign name
-            if ( pFanout->pData == NULL )
-            {
-                pFanout->pData = Abc_ObjName( pFanout );
-                Nm_ManStoreIdName( pNtk->pManName, pFanout->Id, pFanout->pData, NULL );
-            }
-        }
-    }
-    return Vec_PtrSize(pNtk->vBoxes);
-*/
-    return 0;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Derive the AIG of the logic in the netlist.]
 
   Description []
@@ -390,70 +336,6 @@ void Abc_NodeStrashUsingNetwork( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pBox )
 //printf( "processing %d\n", pBox->Id );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Derive the AIG of the logic in the netlist.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
-{
-    ProgressBar * pProgress;
-    Vec_Ptr_t * vNodes;
-    Abc_Ntk_t * pNtkAig;
-    Abc_Obj_t * pObj;
-    int i, nBoxes;
-    // explicitly derive black boxes
-    assert( Abc_NtkIsNetlist(pNtk) );
-    nBoxes = Abc_LibDeriveBlackBoxes( pNtk, pLib );
-    if ( nBoxes )
-        printf( "Detected and transformed %d black boxes.\n", nBoxes );
-    // create the new network with black boxes in place
-    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
-    // transer to the nets
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
-    // build the AIG for the remaining logic in the netlist
-    vNodes = Abc_NtkDfs( pNtk, 0 );
-    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
-    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
-    {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( Abc_ObjIsNode(pObj) )
-        {
-            pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj, 0 );
-            Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
-            continue;
-        }
-        Abc_NodeStrashUsingNetwork( pNtkAig, pObj );
-    }
-    Extra_ProgressBarStop( pProgress );
-    Vec_PtrFree( vNodes );
-    // deallocate memory manager, which remembers the phase
-    if ( pNtk->pData )
-    {
-        Mem_FlexStop( (Mem_Flex_t *)pNtk->pData, 0 );
-        pNtk->pData = NULL;
-    }
-    // set the COs
-//    Abc_NtkFinalize( pNtk, pNtkAig );
-    Abc_NtkForEachCo( pNtk, pObj, i )
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
-    Abc_AigCleanup( (Abc_Aig_t *)pNtkAig->pManFunc );
-    // make sure that everything is okay
-    if ( !Abc_NtkCheck( pNtkAig ) )
-    {
-        printf( "Abc_LibDeriveAig: The network check has failed.\n" );
-        return 0;
-    }
-    return pNtkAig;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 4567d332..c3294d98 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1319,7 +1319,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // free the hierarchy
     if ( pNtk->pDesign )
     {
-        Abc_LibFree( pNtk->pDesign, pNtk );
+        Abc_DesFree( pNtk->pDesign, pNtk );
         pNtk->pDesign = NULL;
     }
 //    if ( pNtk->pBlackBoxes ) 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 3e969915..68a4ade1 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -44,8 +44,6 @@ static int IoCommandReadInit    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
-static int IoCommandReadVer     ( Abc_Frame_t * pAbc, int argc, char **argv );
-static int IoCommandReadVerLib  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadStatus  ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWrite       ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -68,7 +66,6 @@ static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 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 );
 static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteTruth  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -110,8 +107,6 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
-//    Cmd_CommandAdd( pAbc, "I/O", "read_ver",      IoCommandReadVer,      1 );
-//    Cmd_CommandAdd( pAbc, "I/O", "read_verlib",   IoCommandReadVerLib,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_status",   IoCommandReadStatus,   0 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
@@ -1082,182 +1077,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk, * pNtkNew;
-    Abc_Lib_t * pDesign;
-    char * pFileName;
-    FILE * pFile;
-    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 );
-
-    printf( "Stand-alone structural Verilog reader is available as command \"read_verilog\".\n" );
-    return 0;
-
-    fCheck = 1;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
-    {
-        switch ( c )
-        {
-            case 'c':
-                fCheck ^= 1;
-                break;
-            case 'h':
-                goto usage;
-            default:
-                goto usage;
-        }
-    }
-
-    if ( argc != globalUtilOptind + 1 )
-    {
-        goto usage;
-    }
-
-    // get the input file name
-    pFileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( pFileName, "r" )) == NULL )
-    {
-        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", pFileName );
-        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" )) )
-            fprintf( pAbc->Err, "Did you mean \"%s\"?", pFileName );
-        fprintf( pAbc->Err, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-
-    // set the new network
-    pDesign = Ver_ParseFile( pFileName, (Abc_Lib_t *)Abc_FrameReadLibVer(), fCheck, 1 );
-    if ( pDesign == NULL )
-    {
-        fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
-        return 1;
-    }
-
-    // derive root design
-    pNtk = Abc_LibDeriveRoot( pDesign );
-    Abc_LibFree( pDesign, NULL );
-    if ( pNtk == NULL )
-    {
-        fprintf( pAbc->Err, "Deriving root module has failed.\n" );
-        return 1;
-    }
-
-    // derive the AIG network from this design
-    pNtkNew = Abc_LibDeriveAig( pNtk, (Abc_Lib_t *)Abc_FrameReadLibVer() );
-    Abc_NtkDelete( pNtk );
-    if ( pNtkNew == NULL )
-    {
-        fprintf( pAbc->Err, "Converting root module to AIG has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
-    Abc_FrameClearVerifStatus( pAbc );
-    return 0;
-
-usage:
-    fprintf( pAbc->Err, "usage: read_ver [-ch] <file>\n" );
-    fprintf( pAbc->Err, "\t         reads a network in structural verilog (using current library)\n" );
-    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
-    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Lib_t * pLibrary;
-    char * pFileName;
-    FILE * pFile;
-    int fCheck;
-    int c;
-    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
-
-    fCheck = 1;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
-    {
-        switch ( c )
-        {
-            case 'c':
-                fCheck ^= 1;
-                break;
-            case 'h':
-                goto usage;
-            default:
-                goto usage;
-        }
-    }
-
-    if ( argc != globalUtilOptind + 1 )
-    {
-        goto usage;
-    }
-
-    // get the input file name
-    pFileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( pFileName, "r" )) == NULL )
-    {
-        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", pFileName );
-        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" )) )
-            fprintf( pAbc->Err, "Did you mean \"%s\"?", pFileName );
-        fprintf( pAbc->Err, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-
-    // set the new network
-    pLibrary = Ver_ParseFile( pFileName, NULL, fCheck, 0 );
-    if ( pLibrary == NULL )
-    {
-        fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
-        return 1;
-    }
-    printf( "The library contains %d gates.\n", st__count(pLibrary->tModules) );
-    // free old library
-    if ( Abc_FrameReadLibVer() )
-        Abc_LibFree( (Abc_Lib_t *)Abc_FrameReadLibVer(), NULL );
-    // read new library
-    Abc_FrameSetLibVer( pLibrary );
-    Abc_FrameClearVerifStatus( pAbc );
-    return 0;
-
-usage:
-    fprintf( pAbc->Err, "usage: read_verlib [-ch] <file>\n" );
-    fprintf( pAbc->Err, "\t         reads a gate library in structural verilog\n" );
-    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
-    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char * pFileName;
@@ -2617,57 +2436,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    Abc_Lib_t * pLibrary;
-    char * pFileName;
-    int c;
-    extern void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName );
-
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-            case 'h':
-                goto usage;
-            default:
-                goto usage;
-        }
-    }
-    if ( argc != globalUtilOptind + 1 )
-        goto usage;
-    // get the input file name
-    pFileName = argv[globalUtilOptind];
-    // derive the netlist
-    pLibrary = (Abc_Lib_t *)Abc_FrameReadLibVer();
-    if ( pLibrary == NULL )
-    {
-        fprintf( pAbc->Out, "Verilog library is not specified.\n" );
-        return 0;
-    }
-//    Io_WriteVerilogLibrary( pLibrary, pFileName );
-    return 0;
-
-usage:
-    fprintf( pAbc->Err, "usage: write_verlib [-h] <file>\n" );
-    fprintf( pAbc->Err, "\t         writes the current verilog library\n" );
-    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 323c8273..a26b7dca 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -76,7 +76,7 @@ struct Io_MvMan_t_
     char *               pBuffer;      // the contents of the file
     Vec_Ptr_t *          vLines;       // the line beginnings
     // the results of reading
-    Abc_Lib_t *          pDesign;      // the design under construction
+    Abc_Des_t *          pDesign;      // the design under construction
     int                  nNDnodes;     // the counter of ND nodes
     // intermediate storage for models
     Vec_Ptr_t *          vModels;      // vector of models
@@ -100,7 +100,7 @@ static void              Io_MvModFree( Io_MvMod_t * p );
 static char *            Io_MvLoadFile( char * pFileName );
 static void              Io_MvReadPreparse( Io_MvMan_t * p );
 static int               Io_MvReadInterfaces( Io_MvMan_t * p );
-static Abc_Lib_t *       Io_MvParse( Io_MvMan_t * p );
+static Abc_Des_t *       Io_MvParse( Io_MvMan_t * p );
 static int               Io_MvParseLineModel( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine );
@@ -142,7 +142,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     FILE * pFile;
     Io_MvMan_t * p;
     Abc_Ntk_t * pNtk, * pExdc;
-    Abc_Lib_t * pDesign = NULL; 
+    Abc_Des_t * pDesign = NULL; 
     char * pDesignName;
     int RetValue, i;
     char * pLtlProp;
@@ -169,7 +169,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     }
     // set the design name
     pDesignName  = Extra_FileNameGeneric( pFileName );
-    p->pDesign   = Abc_LibCreate( pDesignName );
+    p->pDesign   = Abc_DesCreate( pDesignName );
     ABC_FREE( pDesignName );
     // free the HOP manager
     Hop_ManStop( (Hop_Man_t *)p->pDesign->pManFunc );
@@ -194,13 +194,13 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
             if ( !Abc_NtkCheckRead( pNtk ) )
             {
                 printf( "Io_ReadBlifMv: The network check has failed for model %s.\n", pNtk->pName );
-                Abc_LibFree( pDesign, NULL );
+                Abc_DesFree( pDesign, NULL );
                 return NULL;
             }
         }
     }
 
-//Abc_LibPrint( pDesign );
+//Abc_DesPrint( pDesign );
 
     // check if there is an EXDC network
     if ( Vec_PtrSize(pDesign->vModules) > 1 )
@@ -220,7 +220,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     }
 
     // detect top-level model
-    RetValue = Abc_LibFindTopLevelModels( pDesign );
+    RetValue = Abc_DesFindTopLevelModels( pDesign );
     pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
     if ( RetValue > 1 )
         printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
@@ -235,7 +235,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     if ( Vec_PtrSize(pDesign->vModules) == 1 )
     {
 //        printf( "Warning: The design is not hierarchical.\n" );
-        Abc_LibFree( pDesign, pNtk );
+        Abc_DesFree( pDesign, pNtk );
         pNtk->pDesign = NULL;
         pNtk->pSpec = Extra_UtilStrsav( pFileName );
     }
@@ -293,7 +293,7 @@ static void Io_MvFree( Io_MvMan_t * p )
     Io_MvMod_t * pMod;
     int i;
     if ( p->pDesign )
-        Abc_LibFree( p->pDesign, NULL );
+        Abc_DesFree( p->pDesign, NULL );
     if ( p->pBuffer )  
         ABC_FREE( p->pBuffer );
     if ( p->vLines )
@@ -729,7 +729,7 @@ static int Io_MvReadInterfaces( Io_MvMan_t * p )
         if ( !Io_MvParseLineModel( pMod, pMod->pName ) )
             return 0;
         // add model to the design
-        if ( !Abc_LibAddModel( p->pDesign, pMod->pNtk ) )
+        if ( !Abc_DesAddModel( p->pDesign, pMod->pNtk ) )
         {
             sprintf( p->sError, "Line %d: Model %s is defined twice.", Io_MvGetLine(p, pMod->pName), pMod->pName );
             return 0;
@@ -774,9 +774,9 @@ static int Io_MvReadInterfaces( Io_MvMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
+static Abc_Des_t * Io_MvParse( Io_MvMan_t * p )
 {
-    Abc_Lib_t * pDesign;
+    Abc_Des_t * pDesign;
     Io_MvMod_t * pMod;
     char * pLine;
     int i, k;
@@ -1244,7 +1244,7 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
             break;
         }
     // find the model
-    pModel = Abc_LibFindModelByName( p->pMan->pDesign, pName );
+    pModel = Abc_DesFindModelByName( p->pMan->pDesign, pName );
     if ( pModel == NULL )
     {
         sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Io_MvGetLine(p->pMan, pToken), pName );
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 4907c784..da4c0edb 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-//extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+//extern Abc_Des_t * Ver_ParseFile( char * pFileName, Abc_Des_t * pGateLib, int fCheck, int fUseMemMan );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,7 +48,7 @@ ABC_NAMESPACE_IMPL_START
 Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
 {
     Abc_Ntk_t * pNtk, * pTemp;
-    Abc_Lib_t * pDesign;
+    Abc_Des_t * pDesign;
     int i, RetValue;
 
     // parse the verilog file
@@ -57,7 +57,7 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
         return NULL;
 
     // detect top-level model
-    RetValue = Abc_LibFindTopLevelModels( pDesign );
+    RetValue = Abc_DesFindTopLevelModels( pDesign );
     pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
     if ( RetValue > 1 )
     {
@@ -77,7 +77,7 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
     if ( Vec_PtrSize(pDesign->vModules) == 1 )
     {
 //        printf( "Warning: The design is not hierarchical.\n" );
-        Abc_LibFree( pDesign, pNtk );
+        Abc_DesFree( pDesign, pNtk );
         pNtk->pDesign = NULL;
         pNtk->pSpec = Extra_UtilStrsav( pFileName );
     }
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index fe60b7db..277c86ee 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -189,7 +189,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     if ( p->vCexVec   )  Vec_PtrFreeFree( p->vCexVec );
     if ( p->vPoEquivs )  Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
     if ( p->vStatuses )  Vec_IntFree( p->vStatuses );
-    if ( p->pLibVer   )  Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
+    if ( p->pLibVer   )  Abc_DesFree( (Abc_Des_t *)p->pLibVer, NULL );
     if ( p->pManDec   )  Dec_ManStop( (Dec_Man_t *)p->pManDec );
     if ( p->dd        )  Extra_StopManager( p->dd );
     if ( p->vStore    )  Vec_PtrFree( p->vStore );
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index 88be8a2e..69ac9410 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -57,7 +57,7 @@ struct Ver_Man_t_
     int             fNameLast;
     ProgressBar *   pProgress;
     // current design
-    Abc_Lib_t *     pDesign;
+    Abc_Des_t *     pDesign;
     st__table *      tName2Suffix;
     // error handling
     FILE *          Output;
@@ -85,7 +85,7 @@ struct Ver_Man_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== verCore.c ========================================================*/
-extern Abc_Lib_t *    Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+extern Abc_Des_t *    Ver_ParseFile( char * pFileName, Abc_Des_t * pGateLib, int fCheck, int fUseMemMan );
 extern void           Ver_ParsePrintErrorMessage( Ver_Man_t * p );
 /*=== verFormula.c ========================================================*/
 extern void *         Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage );
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 875a16b4..bb0f243f 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -51,7 +51,7 @@ typedef enum {
     VER_GATE_NOT
 } Ver_GateType_t;
 
-static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib );
+static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Des_t * pGateLib );
 static void Ver_ParseStop( Ver_Man_t * p );
 static void Ver_ParseFreeData( Ver_Man_t * p );
 static void Ver_ParseInternal( Ver_Man_t * p );
@@ -101,7 +101,7 @@ struct Ver_Bundle_t_
   SeeAlso     []
 
 ***********************************************************************/
-Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
+Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Des_t * pGateLib )
 {
     Ver_Man_t * p;
     p = ABC_ALLOC( Ver_Man_t, 1 );
@@ -119,7 +119,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
     p->vStackOp  = Vec_IntAlloc( 100 );
     p->vPerm     = Vec_IntAlloc( 100 );
     // create the design library and assign the technology library
-    p->pDesign   = Abc_LibCreate( pFileName );
+    p->pDesign   = Abc_DesCreate( pFileName );
     p->pDesign->pLibrary = pGateLib;
     // derive library from SCL
 //    if ( Abc_FrameReadLibScl() )
@@ -162,10 +162,10 @@ void Ver_ParseStop( Ver_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan )
+Abc_Des_t * Ver_ParseFile( char * pFileName, Abc_Des_t * pGateLib, int fCheck, int fUseMemMan )
 {
     Ver_Man_t * p;
-    Abc_Lib_t * pDesign;
+    Abc_Des_t * pDesign;
     // start the parser
     p = Ver_ParseStart( pFileName, pGateLib );
     p->fMapped    = glo_fMapped;
@@ -259,7 +259,7 @@ void Ver_ParseFreeData( Ver_Man_t * p )
 {
     if ( p->pDesign )
     {
-        Abc_LibFree( p->pDesign, NULL );
+        Abc_DesFree( p->pDesign, NULL );
         p->pDesign = NULL;
     }
 }
@@ -302,7 +302,7 @@ 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 )) )
+    if ( (pNtkNew = Abc_DesFindModelByName( pMan->pDesign, pName )) )
         return pNtkNew;
 //printf( "Creating network %s.\n", pName );
     // create new network
@@ -310,7 +310,7 @@ Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName )
     pNtkNew->pName = Extra_UtilStrsav( pName );
     pNtkNew->pSpec = NULL;
     // add module to the design
-    Abc_LibAddModel( pMan->pDesign, pNtkNew );
+    Abc_DesAddModel( pMan->pDesign, pNtkNew );
     return pNtkNew;
 }