Improvements to Cba data-structure.

8 files changed, 539 insertions, 200 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 3a735d36..bf060652 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -219,8 +219,6 @@ static inline Cba_Ntk_t *    Cba_ManNtkFind( Cba_Man_t * p, char * pName )   { r
 static inline Cba_Ntk_t *    Cba_ManRoot( Cba_Man_t * p )                    { return Cba_ManNtk(p, p->iRoot);                                                             }
 static inline char *         Cba_ManStr( Cba_Man_t * p, int i )              { return Abc_NamStr(p->pStrs, i);                                                             }
 static inline int            Cba_ManStrId( Cba_Man_t * p, char * pStr )      { return Abc_NamStrFind(p->pStrs, pStr);                                                      }
-static inline int            Cba_ManNewStrId( Cba_Man_t * p, char * pName )  { return Abc_NamStrFindOrAdd(p->pStrs, pName, NULL);                                          }
-static inline int            Cba_ManNewStrId_( Cba_Man_t * p, char * pPref, int n, char * pSuff ) { char pStr[100]; sprintf(pStr, "%s%d%s", pPref?pPref:"", n, pSuff?pSuff:""); return Abc_NamStrFindOrAdd(p->pStrs, pStr, NULL); }
 static inline int            Cba_ManNameIdMax( Cba_Man_t * p )               { return Abc_NamObjNumMax(p->pStrs) + 1;                                                      }
 static inline char *         Cba_ManConst( Cba_Man_t * p, int i )            { return Abc_NamStr(p->pFuns, i);                                                             }
 static inline int            Cba_ManConstId( Cba_Man_t * p, char * pStr )    { return Abc_NamStrFind(p->pFuns, pStr);                                                      }
@@ -233,9 +231,9 @@ static inline int            Cba_NtkPi( Cba_Ntk_t * p, int i )               { r
 static inline int            Cba_NtkPo( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vOutputs, i);                                                       }
 static inline int            Cba_NtkPioOrder( Cba_Ntk_t * p, int i )         { return Vec_IntEntry(&p->vOrder, i);                                                         }
 static inline int            Cba_NtkBoxSeq( Cba_Ntk_t * p, int i )           { return Vec_IntEntry(&p->vSeq, i);                                                           }
+static inline Abc_Nam_t *    Cba_NtkNam( Cba_Ntk_t * p )                     { return p->pDesign->pStrs;                                                                   }
 static inline char *         Cba_NtkStr( Cba_Ntk_t * p, int i )              { return Cba_ManStr(p->pDesign, i);                                                           }
 static inline int            Cba_NtkStrId( Cba_Ntk_t * p, char * pName )     { return Cba_ManStrId(p->pDesign, pName);                                                     }
-static inline int            Cba_NtkNewStrId( Cba_Ntk_t * p, char * pName )  { return Cba_ManNewStrId(p->pDesign, pName);                                                  }
 static inline char *         Cba_NtkConst( Cba_Ntk_t * p, int i )            { return Cba_ManConst(p->pDesign, i);                                                         }
 static inline char *         Cba_NtkSop( Cba_Ntk_t * p, int i )              { return Cba_ManConst(p->pDesign, i);                                                         }
 static inline int            Cba_NtkNameId( Cba_Ntk_t * p )                  { return p->NameId;                                                                           }
@@ -351,7 +349,7 @@ static inline int            Cba_ObjFinFon( Cba_Ntk_t * p, int i, int k )    { a
 static inline int *          Cba_ObjFinFons( Cba_Ntk_t * p, int i )          { assert(i>0); return Vec_IntEntryP(&p->vFinFon, Cba_ObjFin0(p, i));                          }
 
 static inline void           Cba_ObjSetFinFon( Cba_Ntk_t * p, int i, int k, int x ) { assert(i>0); assert(Cba_ObjFinFon(p, i, k)== 0); Vec_IntWriteEntry(&p->vFinFon, Cba_ObjFin(p, i, k), x); }
-static inline void           Cba_ObjCleanFinFon( Cba_Ntk_t * p, int i, int k)       { assert(i>0); assert(Cba_ObjFinFon(p, i, k) > 0); Vec_IntWriteEntry(&p->vFinFon, Cba_ObjFin(p, i, k), 0); }
+static inline void           Cba_ObjCleanFinFon( Cba_Ntk_t * p, int i, int k)       { assert(i>0); assert(Cba_ObjFinFon(p, i, k)!= 0); Vec_IntWriteEntry(&p->vFinFon, Cba_ObjFin(p, i, k), 0); }
 static inline void           Cba_ObjPatchFinFon( Cba_Ntk_t * p, int i, int k, int x){ assert(i>0); Cba_ObjCleanFinFon(p, i, k); Cba_ObjSetFinFon(p, i, k, x);                                  }
 
 static inline int            Cba_ObjNtkId( Cba_Ntk_t * p, int i )            { assert(i>0); return (Cba_ObjIsBoxUser(p, i) && Cba_NtkHasObjFuncs(p)) ? Cba_ObjFunc(p, i) : 0;}
@@ -550,6 +548,23 @@ static inline void Cba_NtkFree( Cba_Ntk_t * p )
     if ( p->vOther ) Vec_VecFree( (Vec_Vec_t *)p->vOther );
     ABC_FREE( p );
 }
+static inline int Cba_NtkNewStrId( Cba_Ntk_t * pNtk, const char * format, ...  )
+{
+    Abc_Nam_t * p = Cba_NtkNam( pNtk );
+    Vec_Str_t * vBuf = Abc_NamBuffer( p );
+    int nAdded, nSize = 1000; 
+    va_list args;   va_start( args, format );
+    Vec_StrGrow( vBuf, Vec_StrSize(vBuf) + nSize );
+    nAdded = vsnprintf( Vec_StrLimit(vBuf), nSize, format, args );
+    if ( nAdded > nSize )
+    {
+        Vec_StrGrow( vBuf, Vec_StrSize(vBuf) + nAdded + nSize );
+        nSize = vsnprintf( Vec_StrLimit(vBuf), nAdded, format, args );
+        assert( nSize == nAdded );
+    }
+    va_end( args );
+    return Abc_NamStrFindOrAddLim( p, Vec_StrLimit(vBuf), Vec_StrLimit(vBuf) + nAdded, NULL );
+}
 static inline void Cba_NtkAdd( Cba_Man_t * p, Cba_Ntk_t * pNtk )
 {    
     int fFound, NtkId = Abc_NamStrFindOrAdd( p->pMods, Cba_NtkName(pNtk), &fFound );
@@ -589,7 +604,7 @@ static inline void Cba_NtkCreateFonNames( Cba_Ntk_t * p, char * pPref )
             Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
     Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
         if ( NameId == 0 )
-            Vec_IntWriteEntry( &p->vFonName, iFon, Cba_ManNewStrId_(p->pDesign, pPref, iFon, NULL) );
+            Vec_IntWriteEntry( &p->vFonName, iFon, Cba_NtkNewStrId(p, "%s%d", pPref, iFon) );
 }
 static inline void Cba_NtkMissingFonNames( Cba_Ntk_t * p, char * pPref )
 {
@@ -602,7 +617,7 @@ static inline void Cba_NtkMissingFonNames( Cba_Ntk_t * p, char * pPref )
             Cba_FonSetName( p, iFon, Cba_ObjName(p, iObj) );
     Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
         if ( NameId == 0 )
-            Cba_FonSetName( p, iFon, Cba_ManNewStrId_(p->pDesign, pPref, iFon, NULL) );
+            Cba_FonSetName( p, iFon, Cba_NtkNewStrId(p, "%s%d", pPref, iFon) );
 }
 static inline int Cba_NtkIsSeq( Cba_Ntk_t * p )
 {
@@ -865,6 +880,10 @@ static inline void Cba_ManSetMap( Cba_Man_t * p, int i, int x )
     Vec_IntSetEntry( &p->vNameMap, i, x );
     Vec_IntPush( &p->vUsed, i );
 }
+static inline void Cba_ManUnsetMap( Cba_Man_t * p, int i )
+{
+    Vec_IntSetEntry( &p->vNameMap, i, 0 );
+}
 static inline void Cba_ManCleanMap( Cba_Man_t * p )
 {
     int i, Entry;
@@ -874,6 +893,7 @@ static inline void Cba_ManCleanMap( Cba_Man_t * p )
 }
 static inline int  Cba_NtkGetMap( Cba_Ntk_t * p, int i )          { return Cba_ManGetMap(p->pDesign, i); }
 static inline void Cba_NtkSetMap( Cba_Ntk_t * p, int i, int x )   { Cba_ManSetMap(p->pDesign, i, x);     }
+static inline void Cba_NtkUnsetMap( Cba_Ntk_t * p, int i )        { Cba_ManUnsetMap(p->pDesign, i);      }
 static inline void Cba_NtkCleanMap( Cba_Ntk_t * p )               { Cba_ManCleanMap(p->pDesign);         }
 
 static inline int Cba_ManGetMap2( Cba_Man_t * p, int i )
@@ -886,6 +906,10 @@ static inline void Cba_ManSetMap2( Cba_Man_t * p, int i, int x )
     Vec_IntSetEntry( &p->vNameMap2, i, x );
     Vec_IntPush( &p->vUsed2, i );
 }
+static inline void Cba_ManUnsetMap2( Cba_Man_t * p, int i )
+{
+    Vec_IntSetEntry( &p->vNameMap2, i, 0 );
+}
 static inline void Cba_ManCleanMap2( Cba_Man_t * p )
 {
     int i, Entry;
@@ -895,6 +919,7 @@ static inline void Cba_ManCleanMap2( Cba_Man_t * p )
 }
 static inline int  Cba_NtkGetMap2( Cba_Ntk_t * p, int i )          { return Cba_ManGetMap2(p->pDesign, i); }
 static inline void Cba_NtkSetMap2( Cba_Ntk_t * p, int i, int x )   { Cba_ManSetMap2(p->pDesign, i, x);     }
+static inline void Cba_NtkUnsetMap2( Cba_Ntk_t * p, int i )        { Cba_ManUnsetMap2(p->pDesign, i);      }
 static inline void Cba_NtkCleanMap2( Cba_Ntk_t * p )               { Cba_ManCleanMap2(p->pDesign);         }
 
 static inline int Cba_ManNewConstId( Cba_Man_t * p, Vec_Str_t * vBits ) 
@@ -1005,6 +1030,8 @@ extern Cba_Man_t *   Cba_ManReadCba( char * pFileName );
 extern void          Cba_ManWriteCba( char * pFileName, Cba_Man_t * p );
 /*=== cbaCom.c ===============================================================*/
 /*=== cbaNtk.c ===============================================================*/
+extern void          Cba_ManPrintDistrib( Cba_Man_t * p );
+extern void          Cba_NtkPrintDistrib( Cba_Ntk_t * p );
 //extern void           Cba_ManPrepareTypeNames( Cba_Man_t * p );
 extern void          Cba_NtkObjOrder( Cba_Ntk_t * p, Vec_Int_t * vObjs, Vec_Int_t * vNameIds );
 extern int           Cba_NtkCiFonNum( Cba_Ntk_t * p );
@@ -1026,6 +1053,7 @@ extern Cba_Man_t *   Cba_ManReadVerilog( char * pFileName );
 extern void          Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * p );
 extern void          Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p );
 /*=== cbaWriteVer.c ==========================================================*/
+extern void          Cba_ManCreatePrimMap( char ** pMap );
 extern void          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
 extern void          Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fInlineConcat );
 
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index f8a3d18e..752744f1 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -32,6 +32,73 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_NtkCollectDistrib( Cba_Ntk_t * p, int * pCounts, int * pUserCounts )
+{
+    int i;
+    Cba_NtkForEachBox( p, i )
+        if ( Cba_ObjIsBoxUser(p, i) )
+            pUserCounts[Cba_ObjNtkId(p, i)]++;
+        else
+            pCounts[Cba_ObjType(p, i)]++;
+}
+
+void Cba_NtkPrintDistribStat( Cba_Ntk_t * p, int * pCounts, int * pUserCounts )
+{
+    Cba_Ntk_t * pNtk; int i;
+    printf( "Primitives (%d):\n", Cba_NtkBoxPrimNum(p) );
+    for ( i = 0; i < CBA_BOX_LAST; i++ )
+        if ( pCounts[i] )
+            printf( "%-20s = %5d\n", Cba_NtkTypeName(p, i), pCounts[i] );
+    printf( "User hierarchy (%d):\n", Cba_NtkBoxUserNum(p) );
+    Cba_ManForEachNtk( p->pDesign, pNtk, i )
+        if ( pUserCounts[i] )
+            printf( "%-20s = %5d\n", Cba_NtkName(pNtk), pUserCounts[i] );
+}
+void Cba_NtkPrintDistrib( Cba_Ntk_t * p )
+{
+    int pCounts[CBA_BOX_LAST] = {0};
+    int * pUserCounts = ABC_CALLOC( int, Cba_ManNtkNum(p->pDesign) + 1 );
+    Cba_ManCreatePrimMap( p->pDesign->pTypeNames );
+    Cba_NtkCollectDistrib( p, pCounts, pUserCounts );
+    Cba_NtkPrintDistribStat( p, pCounts, pUserCounts );
+    ABC_FREE( pUserCounts );
+}
+
+void Cba_ManPrintDistribStat( Cba_Man_t * p, int * pCounts, int * pUserCounts )
+{
+    Cba_Ntk_t * pNtk = Cba_ManRoot(p); int i;
+    printf( "Primitives:\n" );
+    for ( i = 0; i < CBA_BOX_LAST; i++ )
+        if ( pCounts[i] )
+            printf( "%-20s = %5d\n", Cba_NtkTypeName(pNtk, i), pCounts[i] );
+    printf( "User hierarchy:\n" );
+    Cba_ManForEachNtk( p, pNtk, i )
+        if ( pUserCounts[i] )
+            printf( "%-20s = %5d\n", Cba_NtkName(pNtk), pUserCounts[i] );
+}
+void Cba_ManPrintDistrib( Cba_Man_t * p )
+{
+    Cba_Ntk_t * pNtk; int i;
+    int pCounts[CBA_BOX_LAST] = {0};
+    int * pUserCounts = ABC_CALLOC( int, Cba_ManNtkNum(p) + 1 );
+    Cba_ManCreatePrimMap( p->pTypeNames );
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_NtkCollectDistrib( pNtk, pCounts, pUserCounts );
+    Cba_ManPrintDistribStat( p, pCounts, pUserCounts );
+    ABC_FREE( pUserCounts );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Order objects by box type and then by name.]
 
   Description []
@@ -686,7 +753,7 @@ Cba_Man_t * Cba_ManDeriveFromGia( Gia_Man_t * pGia )
     Cba_NtkCleanObjNames( pNtk );
     Gia_ManForEachCiId( pGia, iObj, i )
     {
-        NameId = pGia->vNamesIn? Abc_NamStrFindOrAdd(p->pStrs, Vec_PtrEntry(pGia->vNamesIn, i), NULL) : Cba_ManNewStrId_(p, "i", i, NULL);
+        NameId = pGia->vNamesIn? Abc_NamStrFindOrAdd(p->pStrs, Vec_PtrEntry(pGia->vNamesIn, i), NULL) : Cba_NtkNewStrId(pNtk, "i%d", i);
         iObjNew = Cba_ObjAlloc( pNtk, CBA_OBJ_PI, 0, 1 );
         Cba_ObjSetName( pNtk, iObjNew, NameId );
         Vec_IntWriteEntry( vLit2Fon, Abc_Var2Lit(iObj, 0), Cba_ObjFon0(pNtk, iObjNew) );
@@ -708,7 +775,7 @@ Cba_Man_t * Cba_ManDeriveFromGia( Gia_Man_t * pGia )
         iObjNew = Cba_ObjAlloc( pNtk, CBA_BOX_BUF, 1, 1 );
         Cba_ObjSetFinFon( pNtk, iObjNew, 0, iFon0 );
         iFon0 = Cba_ObjFon0(pNtk, iObjNew); // non-const fon unique for this output
-        NameId = pGia->vNamesOut? Abc_NamStrFindOrAdd(p->pStrs, Vec_PtrEntry(pGia->vNamesOut, i), NULL) : Cba_ManNewStrId_(p, "o", i, NULL);
+        NameId = pGia->vNamesOut? Abc_NamStrFindOrAdd(p->pStrs, Vec_PtrEntry(pGia->vNamesOut, i), NULL) : Cba_NtkNewStrId(pNtk, "o%d", i);
         iObjNew = Cba_ObjAlloc( pNtk, CBA_OBJ_PO, 1, 0 );
         Cba_ObjSetName( pNtk, iObjNew, NameId );
         Cba_ObjSetFinFon( pNtk, iObjNew, 0, iFon0 );
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index 2657583d..32cd1b59 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -175,7 +175,7 @@ static const char * s_VerNames[100] =
     "wide_prio_select_",     
     "pow_",                  
     "PrioEncoder_",          
-    "abs",                   
+    "abs_",                   
     NULL
 };
 
@@ -206,10 +206,10 @@ static const Prs_VerInfo_t s_VerInfo[100] =
     {-1,              0, "VERIFIC_PULLUP",         /* "PRIM_PULLUP"             */ {"o"}},
     {-1,              0, "VERIFIC_PULLDOWN",       /* "PRIM_PULLDOWN"           */ {"o"}},
     {CBA_BOX_TRI,     3, "VERIFIC_TRI",            /* "PRIM_TRI"                */ {"i","c","o"}},
-    {CBA_BOX_LATCH,   4, "VERIFIC_DLATCH",         /* "PRIM_DLATCH"             */ {"d","async_val","async_cond","gate","q"}}, // changed order
     {CBA_BOX_LATCHRS, 4, "VERIFIC_DLATCHRS",       /* "PRIM_DLATCHRS"           */ {"d","s","r","gate","q"}},                  // changed order
-    {CBA_BOX_DFF,     4, "VERIFIC_DFF",            /* "PRIM_DFF"                */ {"d","async_val","async_cond","clk","q"}},  // changed order
+    {CBA_BOX_LATCH,   4, "VERIFIC_DLATCH",         /* "PRIM_DLATCH"             */ {"d","async_val","async_cond","gate","q"}}, // changed order
     {CBA_BOX_DFFRS,   4, "VERIFIC_DFFRS",          /* "PRIM_DFFRS"              */ {"d","s","r","clk","q"}},                   // changed order
+    {CBA_BOX_DFF,     4, "VERIFIC_DFF",            /* "PRIM_DFF"                */ {"d","async_val","async_cond","clk","q"}},  // changed order
     {-1,              2, "VERIFIC_NMOS",           /* "PRIM_NMOS"               */ {"c","d","o"}},
     {-1,              2, "VERIFIC_PMOS",           /* "PRIM_PMOS"               */ {"c","d","o"}},
     {-1,              3, "VERIFIC_CMOS",           /* "PRIM_CMOS"               */ {"d","nc","pc","o"}},
@@ -242,9 +242,9 @@ static const Prs_VerInfo_t s_VerInfo[100] =
     {CBA_BOX_EDEC,    2, "EnabledDecoder_",        /* "OPER_ENABLED_DECODER"    */ {"en","i","o"}},
     {CBA_BOX_PSEL,    3, "PrioSelect_",            /* "OPER_PRIO_SELECTOR"      */ {"cin","sel","data","o"}},
     {CBA_BOX_RAM,     4, "DualPortRam_",           /* "OPER_DUAL_PORT_RAM"      */ {"write_enable","write_address","write_data","read_address","read_data"}},
-    {CBA_BOX_RAMR,    3, "ReadPort_",              /* "OPER_READ_PORT"          */ {"read_enable", "read_address", "RAM", "read_data" }},
-    {CBA_BOX_RAMW,    3, "WritePort_",             /* "OPER_WRITE_PORT"         */ {"write_enable","write_address","write_data", "RAM"}},
-    {CBA_BOX_RAMWC,   4, "ClockedWritePort_",      /* "OPER_CLOCKED_WRITE_PORT" */ {"clk","write_enable","write_address","write_data", "RAM"}},
+    {CBA_BOX_RAMR,    3, "ReadPort_",              /* "OPER_READ_PORT"          */ {"read_enable", "read_address", "Ram", "read_data" }},
+    {CBA_BOX_RAMW,    3, "WritePort_",             /* "OPER_WRITE_PORT"         */ {"write_enable","write_address","write_data", "Ram"}},
+    {CBA_BOX_RAMWC,   4, "ClockedWritePort_",      /* "OPER_CLOCKED_WRITE_PORT" */ {"clk","write_enable","write_address","write_data", "Ram"}},
     {CBA_BOX_LUT,     1, "lut",                    /* "OPER_LUT"                */ {"i","o"}},
     {CBA_BOX_AND,     2, "and_",                   /* "OPER_WIDE_AND"           */ {"a","b","o"}},
     {CBA_BOX_OR,      2, "or_",                    /* "OPER_WIDE_OR"            */ {"a","b","o"}},
@@ -269,7 +269,7 @@ static const Prs_VerInfo_t s_VerInfo[100] =
     {CBA_BOX_PSEL,    3, "wide_prio_select_",      /* "OPER_WIDE_PRIO_SELECTOR" */ {"sel","data","carry_in","o"}},
     {CBA_BOX_POW,     2, "pow_",                   /* "OPER_POW"                */ {"a","b","o"}},
     {CBA_BOX_PENC,    1, "PrioEncoder_",           /* "OPER_PRIO_ENCODER"       */ {"sel","o"}},
-    {CBA_BOX_ABS,     1, "abs",                    /* "OPER_ABS"                */ {"i","o"}},
+    {CBA_BOX_ABS,     1, "abs_",                   /* "OPER_ABS"                */ {"i","o"}},
     {-1,              0, NULL,                     /* "PRIM_END"                */ {NULL}}
 }; 
 
@@ -286,24 +286,31 @@ static inline int Prs_ManIsVerilogPrim( char * pName )
 // check if it is a known module
 static inline int Prs_ManIsKnownModule( char * pName )
 {
-    int i;
+    int i, Length;
     for ( i = 1; s_VerNames[i]; i++ )
-        if ( !strncmp(pName, s_VerNames[i], strlen(s_VerNames[i])) )
+    {
+        Length = strlen(s_VerNames[i]);
+//        if ( !strncmp(pName, s_VerNames[i], Length) && (i == 1 || (pName[Length] >= '0' && pName[Length] <= '9')) )
+        if ( !strncmp(pName, s_VerNames[i], Length) )
             return i;
+    }
     return 0;
 }
 // check if it is a known module
 static inline int Prs_ManFindType( char * pName, int * pInputs, int fOut, char *** ppNames )
 {
-    int i;
+    int i, Length;
     *pInputs = -1;
     for ( i = 1; s_VerInfo[i].pTypeName; i++ )
-        if ( !strncmp(pName, s_VerInfo[i].pTypeName, strlen(s_VerInfo[i].pTypeName)) )
+    {
+        Length = strlen(s_VerInfo[i].pTypeName);
+        if ( !strncmp(pName, s_VerInfo[i].pTypeName, Length) )
         {
             *pInputs = s_VerInfo[i].nInputs;
             *ppNames = (char **)s_VerInfo[i].pSigNames + (fOut ? s_VerInfo[i].nInputs : 0);
             return s_VerInfo[i].Type;
         }
+    }
     return CBA_OBJ_BOX;
 }
 
@@ -505,6 +512,7 @@ static inline int Prs_ManReadRange( Prs_Man_t * p )
     if ( !Prs_ManIsChar(p, ']') )           return Prs_ManErrorSet(p, "Cannot read closing brace in range specification.", 0);
     Vec_StrPush( &p->vCover, *p->pCur++ );
     Vec_StrPush( &p->vCover, '\0' );
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 6a.", 0);
     return Abc_NamStrFindOrAdd( p->pStrs, Vec_StrArray(&p->vCover), NULL );
 }
 static inline int Prs_ManReadConcat( Prs_Man_t * p, Vec_Int_t * vTemp2 )
@@ -584,6 +592,7 @@ static inline int Prs_ManReadSignalList2( Prs_Man_t * p, Vec_Int_t * vTemp )
         p->pCur++;
         FormId = Prs_ManReadName( p );
         if ( FormId == 0 )                  return Prs_ManErrorSet(p, "Cannot read formal name of the instance.", 0);
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 17.", 0);
         if ( !Prs_ManIsChar(p, '(') )       return Prs_ManErrorSet(p, "Cannot read \"(\" in the instance.", 0);
         p->pCur++;
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 17.", 0);
@@ -771,6 +780,8 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
     assert( Prs_ManIsChar(p, '(') );
     p->pCur++;
     if ( Prs_ManUtilSkipSpaces(p) )             return Prs_ManErrorSet(p, "Error number 30.", 0);
+    if ( Prs_ManIsChar(p, ')') )
+        return 1;
     while ( 1 )
     {
         int iName = Prs_ManReadName( p );
@@ -972,6 +983,8 @@ void Prs_ManReadVerilogTest( char * pFileName )
     printf( "Memory = %.2f MB. ", 1.0*Prs_ManMemory(vPrs)/(1<<20) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     Prs_ManWriteVerilog( Extra_FileNameGenericAppend(pFileName, "_out.v"), vPrs );
+
+    Abc_NamPrint( Prs_ManNameMan(vPrs) );
     Prs_ManVecFree( vPrs );
 }
 
@@ -998,6 +1011,7 @@ int Prs_CreateSlice( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Left, int Ri
 {
     char Buffer[1000];
     int iObj, iFonNew, NameId;
+    assert( Cba_FonIsReal(iFon) );
     if ( Left != Right )
         sprintf( Buffer, "%s[%d:%d]", Cba_FonNameStr(p, iFon), Left, Right );
     else
@@ -1021,13 +1035,14 @@ int Prs_CreateSlice( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Left, int Ri
 int Prs_CreateCatIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Con )
 {
     extern int Prs_CreateSignalIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Sig );
-    char Buffer[100]; int i, Sig, iObj, iFon, NameId, nBits = 0;
+    int i, Sig, iObj, iFon, NameId, nBits = 0;
     Vec_Int_t * vSigs = Prs_CatSignals(pNtk, Con);
     // create input concatenation
     iObj = Cba_ObjAlloc( p, CBA_BOX_CATIN, Vec_IntSize(vSigs), 1 );
     iFon = Cba_ObjFon0(p, iObj);
-    sprintf( Buffer, "_icc%d_", iObj );
-    NameId = Cba_NtkNewStrId( p, Buffer );
+    //sprintf( Buffer, "_icc%d_", iObj );
+    //NameId = Cba_NtkNewStrId( p, Buffer );
+    NameId = Cba_NtkNewStrId( p, "_icc%d_", iObj );
     Cba_FonSetName( p, iFon, NameId );
     Cba_NtkSetMap( p, NameId, iFon );
     // set inputs
@@ -1064,44 +1079,89 @@ int Prs_CreateSignalIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Sig )
     assert( Type == CBA_PRS_CONCAT );
     return Prs_CreateCatIn( p, pNtk, Value );
 }
-
+int Prs_CreateRange( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int NameId )
+{
+    int Left, Right, RangeId = -Cba_NtkGetMap(p, NameId);
+    if ( RangeId < 0 ) // this variable is already created
+        return Cba_FonRange( p, -RangeId );
+    Cba_NtkUnsetMap( p, NameId );
+    Cba_NtkSetMap( p, NameId, iFon );
+    if ( RangeId == 0 )
+        return 1;
+    assert( RangeId > 0 );
+    Prs_NtkParseRange( pNtk, RangeId, &Left, &Right );
+    Cba_FonSetLeft( p, iFon, Left );
+    Cba_FonSetRight( p, iFon, Right );
+    return Cba_FonRange( p, iFon );
+}
 int Prs_CreateCatOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Con )
 {
-    int i, Sig, iObj, iFonNew, NameId;
-    Vec_Int_t * vSigs = Prs_CatSignals(pNtk, Con);
-    char FonName[100]; sprintf( FonName, "_occ%d_", iFon );
-    NameId = Cba_NtkNewStrId( p, FonName ); 
+    int i, Sig, iObj, iFonNew, NameId, Left, Right, nBits = 0;
+    Vec_Int_t * vSigs = Prs_CatSignals(pNtk, Con); char * pSigName;
+    NameId = Cba_NtkNewStrId( p, "_occ%d_", iFon );
     Cba_FonSetName( p, iFon, NameId );
     Cba_NtkSetMap( p, NameId, iFon );
-    // range of iFon is not ready and will be set later
     // create output concatenation
     iObj = Cba_ObjAlloc( p, CBA_BOX_CATOUT, 1, Vec_IntSize(vSigs) );
     Cba_ObjSetFinFon( p, iObj, 0, iFon );
     // set outputs
     Vec_IntForEachEntry( vSigs, Sig, i )
     {
+        int Value = Abc_Lit2Var2(Sig);
         Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
-        assert( Type == CBA_PRS_NAME );
-        NameId = Cba_NtkNewStrId( p, Prs_NtkStr(pNtk, Abc_Lit2Var2(Sig)) ); 
         iFonNew = Cba_ObjFon( p, iObj, Vec_IntSize(vSigs)-1-i );
-        Cba_FonSetName( p, iFonNew, NameId );
-        Cba_NtkSetMap( p, NameId, iFonNew );
+        if ( Type == CBA_PRS_NAME  )
+        {
+            pSigName = Prs_NtkStr(pNtk, Value);
+            NameId = Cba_NtkNewStrId( p, pSigName ); 
+            Cba_FonSetName( p, iFonNew, NameId );
+            nBits += Prs_CreateRange( p, iFonNew, pNtk, NameId );
+        }
+        else if ( Type == CBA_PRS_SLICE )
+        {
+            Prs_NtkParseRange( pNtk, Prs_SliceRange(pNtk, Value), &Left, &Right );
+            pSigName = Prs_NtkStr(pNtk, Prs_SliceName(pNtk, Value));
+            NameId = Cba_NtkNewStrId( p, pSigName );
+            Cba_FonSetName( p, iFonNew, NameId );
+            Prs_CreateRange( p, iFonNew, pNtk, NameId );
+            // create slice of this concat
+            Prs_CreateSlice( p, iFonNew, pNtk, Left, Right );
+            nBits += Abc_AbsInt(Left-Right)+1;
+        }
+        else assert( 0 );
     }
+    Cba_FonSetLeft( p, iFon, nBits-1 );
+    Cba_FonSetRight( p, iFon, 0 );
     return iObj;
 }
 void Prs_CreateSignalOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Sig )
 {
-    int Value = Abc_Lit2Var2( Sig );
+    int iObj, NameId, Left, Right, Value = Abc_Lit2Var2( Sig );
     Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
     if ( !Sig ) return;
     if ( Type == CBA_PRS_NAME )
     {
         int NameId = Cba_NtkNewStrId(p, Prs_NtkStr(pNtk, Value));
         Cba_FonSetName( p, iFon, NameId );
-        Cba_NtkSetMap( p, NameId, iFon );
+        Prs_CreateRange( p, iFon, pNtk, NameId );
+        return;
+    }
+    if ( Type == CBA_PRS_SLICE )
+    {
+        char * pSigName = Prs_NtkStr(pNtk, Prs_SliceName(pNtk, Value));
+        Prs_NtkParseRange( pNtk, Prs_SliceRange(pNtk, Value), &Left, &Right );
+        // create buffer
+        iObj = Cba_ObjAlloc( p, CBA_BOX_BUF, 1, 1 );
+        Cba_ObjSetFinFon( p, iObj, 0, iFon );
+        iFon = Cba_ObjFon0( p, iObj );
+        NameId = Cba_NtkNewStrId( p, pSigName );
+        Cba_FonSetName( p, iFon, NameId );
+        Prs_CreateRange( p, iFon, pNtk, NameId );
+        // create slice of this concat
+        Prs_CreateSlice( p, iFon, pNtk, Left, Right );
         return;
     }
-    assert( Type == CBA_PRS_SLICE );
+    assert( Type == CBA_PRS_CONCAT );
     Prs_CreateCatOut( p, iFon, pNtk, Value );
 }
 // looks at multi-bit signal; if one bit is repeated, returns this bit; otherwise, returns -1
@@ -1148,8 +1208,6 @@ int Prs_CreateBitSignal( Prs_Ntk_t * pNtk, int Sig )
 
 int Prs_CreateFlopSetReset( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, Vec_Int_t * vBox, int * pIndexSet, int * pIndexRst, int * pBitSet, int * pBitRst )
 {
-    // handle constants
-
     int iSigSet = -1, iSigRst = -1;
     int IndexSet = -1, IndexRst = -1;
     int FormId, ActId, k;
@@ -1159,9 +1217,9 @@ int Prs_CreateFlopSetReset( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, Vec_Int_t * vBox, i
     Cba_NtkSetMap2( p, Cba_NtkStrId(p, "reset"), 2 );
     // check the inputs
     Vec_IntForEachEntryDouble( vBox, FormId, ActId, k )
-        if ( Cba_NtkGetMap2(p, FormId) == 2 ) // plus 1
+        if ( Cba_NtkGetMap2(p, FormId) == 1 ) // set
             iSigSet = ActId, IndexSet = k+1;
-        else if ( Cba_NtkGetMap2(p, FormId) == 3 ) // plus 1
+        else if ( Cba_NtkGetMap2(p, FormId) == 2 ) // reset
             iSigRst = ActId, IndexRst = k+1;
     assert( iSigSet >= 0 && iSigRst >= 0 );
     if ( pIndexSet ) *pBitSet = 0;
@@ -1170,27 +1228,77 @@ int Prs_CreateFlopSetReset( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, Vec_Int_t * vBox, i
     if ( pBitRst )   *pBitRst = 0;
     if ( iSigSet == -1 || iSigRst == -1 )
         return 0;
+    iSigSet = Prs_CreateBitSignal(pNtk, iSigSet);
+    iSigRst = Prs_CreateBitSignal(pNtk, iSigRst);
+    if ( iSigSet == -1 || iSigRst == -1 )
+        return 0;
     if ( pIndexSet ) *pIndexSet = IndexSet;
     if ( pIndexRst ) *pIndexRst = IndexRst;
     if ( pBitSet )   *pBitSet = iSigSet;
     if ( pBitRst )   *pBitRst = iSigRst;
     return 1;
 }
+char * Prs_CreateDetectRamPort( Prs_Ntk_t * pNtk, Vec_Int_t * vBox, int NameRamId )
+{
+    int i, FormId, ActId;
+    Vec_IntForEachEntryDouble( vBox, FormId, ActId, i )
+        if ( FormId == NameRamId )
+            return Abc_NamStr(pNtk->pStrs, Abc_Lit2Var2(ActId));
+    return NULL;
+}
+int Prs_CreateGetMemSize( char * pName )
+{
+    char * pPtr1 = strchr( pName, '_' );
+    char * pPtr2 = strchr( pPtr1+1, '_' );
+    int Num1 = atoi( pPtr1 + 1 );
+    int Num2 = atoi( pPtr2 + 1 );
+    assert( Num1 + Abc_Base2Log(Num2) < 32 );
+    return (1 << Num1) * Num2;
+}
 Vec_Ptr_t * Prs_CreateDetectRams( Prs_Ntk_t * pNtk )
 {
-    Vec_Ptr_t * vRes = NULL; 
-    Vec_Int_t * vBox; int i;
+    Vec_Ptr_t * vAllRams = NULL, * vRam; 
+    Vec_Int_t * vBox, * vBoxCopy; 
+    char * pNtkName, * pRamName;
+    int NameRamId = Abc_NamStrFind( pNtk->pStrs, "Ram" );
+    int i, k, fWrite;
     Prs_NtkForEachBox( pNtk, vBox, i )
     {
-        char * pNtkName;
         if ( Prs_BoxIsNode(pNtk, i) ) // node
             continue;
         pNtkName = Prs_NtkStr(pNtk, Prs_BoxNtk(pNtk, i));
-        if ( !strncmp(pNtkName, "ClockedWritePort_", strlen("ClockedWritePort_")) )
+        fWrite = !strncmp(pNtkName, "ClockedWritePort_", strlen("ClockedWritePort_"));
+        if ( fWrite || !strncmp(pNtkName, "ReadPort_", strlen("ReadPort_")) )
         {
+            pRamName = Prs_CreateDetectRamPort( pNtk, vBox, NameRamId ); assert( pRamName );
+            if ( vAllRams == NULL )
+                vAllRams = Vec_PtrAlloc( 4 );
+            Vec_PtrForEachEntry( Vec_Ptr_t *, vAllRams, vRam, k )
+                if ( pRamName == (char *)Vec_PtrEntry(vRam, 0) )
+                {
+                    if ( fWrite )
+                    {
+                        vBoxCopy = Vec_IntDup(vBox);
+                        Vec_IntPush( vBoxCopy, i );
+                        Vec_PtrPush( vRam, vBoxCopy );
+                    }
+                    break;
+                }
+            if ( k < Vec_PtrSize(vAllRams) )
+                continue;
+            vRam = Vec_PtrAlloc( 4 );
+            Vec_PtrPush( vRam, pRamName );
+            Vec_PtrPush( vRam, Abc_Int2Ptr(Prs_CreateGetMemSize(pNtkName)) );
+            if ( fWrite )
+            {
+                vBoxCopy = Vec_IntDup(vBox);
+                Vec_IntPush( vBoxCopy, i );
+                Vec_PtrPush( vRam, vBoxCopy );
+            }
+            Vec_PtrPush( vAllRams, vRam );
         }
     }
-    return vRes;
+    return vAllRams;
 }
 void Prs_CreateVerilogPio( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
 {
@@ -1234,19 +1342,67 @@ void Prs_CreateVerilogPio( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
 }
 int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
 {
-    Vec_Int_t * vBox;  Vec_Ptr_t * vRams, * vRam;
-    int i, k, iObj, iTerm, iFon, FormId, ActId;
+    Vec_Int_t * vBox2Obj = Vec_IntStart( Prs_NtkBoxNum(pNtk) );
+    Vec_Int_t * vBox;  Vec_Ptr_t * vAllRams, * vRam;
     int NameId, RangeId, Left, Right;
+    int i, k, iObj, iTerm, iFon, FormId, ActId;
     // map inputs
     Cba_NtkCleanMap( p );
     Cba_NtkForEachPi( p, iObj, i )
         Cba_NtkSetMap( p, Cba_ObjName(p, iObj), Cba_ObjFon0(p, iObj) );
+
+    // map wire names into their rangeID
+    Vec_IntForEachEntryTwo( &pNtk->vWires, &pNtk->vWiresR, NameId, RangeId, i )
+        Cba_NtkSetMap( p, NameId, -RangeId );
+    Vec_IntForEachEntryTwo( &pNtk->vOutputs, &pNtk->vOutputsR, NameId, RangeId, i )
+        Cba_NtkSetMap( p, NameId, -RangeId );
+
     // collect RAMs and create boxes
-    vRams = Prs_CreateDetectRams( pNtk );
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vRams, vRam, i )
+    vAllRams = Prs_CreateDetectRams( pNtk );
+    if ( vAllRams )
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vAllRams, vRam, i )
     {
+        char * pRamName = (char *)Vec_PtrEntry( vRam, 0 );
+        int MemSize = Abc_Ptr2Int( (char *)Vec_PtrEntry( vRam, 1 ) );
+        //char Buffer[1000]; sprintf( Buffer, "%s_box", pRamName );
+        //NameId = Cba_NtkNewStrId( p, Buffer ); 
+        NameId = Cba_NtkNewStrId( p, "%s_box", pRamName );
+        // create RAM object
+        iObj = Cba_ObjAlloc( p, CBA_BOX_RAMBOX, Vec_PtrSize(vRam)-2, 1 );
+        Cba_ObjSetName( p, iObj, NameId );
+        iFon = Cba_ObjFon0(p, iObj);
+        NameId = Cba_NtkNewStrId( p, pRamName ); 
+        Cba_FonSetName( p, iFon, NameId );
+        Prs_CreateRange( p, iFon, pNtk, NameId );
+        assert( Cba_FonLeft(p, iFon) <= MemSize-1 );
+        assert( Cba_FonRight(p, iFon) == 0 );
+        //Cba_VerificSaveLineFile( p, iObj, pNet->Linefile() );
+        // create write ports feeding into this object
+        Vec_PtrForEachEntryStart( Vec_Int_t *, vRam, vBox, k, 2 )
+        {
+            int iObjNew = Cba_ObjAlloc( p, CBA_BOX_RAMWC, 4, 1 );
+            int Line = Vec_IntPop( vBox );
+            Vec_IntWriteEntry( vBox2Obj, Line, iObjNew );
+            if ( Prs_BoxName(pNtk, Line) )
+                Cba_ObjSetName( p, iObjNew, Prs_BoxName(pNtk, Line) );
+            //Cba_VerificSaveLineFile( p, iObjNew, pInst->Linefile() );
+            // connect output
+            iFon = Cba_ObjFon0(p, iObjNew);
+            Cba_FonSetLeft( p, iFon, MemSize-1 );
+            Cba_FonSetRight( p, iFon, 0 );
+            //sprintf( Buffer, "%s_wp%d", pRamName, k-2 );
+            //NameId = Cba_NtkNewStrId( p, Buffer ); 
+            NameId = Cba_NtkNewStrId( p, "%s_wp%d", pRamName, k-2 );
+            Cba_FonSetName( p, iFon, NameId );
+            Cba_NtkSetMap( p, NameId, iFon );
+            // connet to RAM object
+            Cba_ObjSetFinFon( p, iObj, (k++)-2, iFon );
+            Vec_IntFree( vBox );
+        }
+        Vec_PtrFree( vRam );
     }
-    Vec_VecFree( (Vec_Vec_t *)vRams );
+    Vec_PtrFreeP( &vAllRams );
+
     // create objects
     Prs_NtkForEachBox( pNtk, vBox, i )
     {
@@ -1262,6 +1418,8 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
             Cba_Ntk_t * pBox = NULL; int nInputs, nOutputs = 1;
             char ** pOutNames = NULL, * pNtkName = Prs_NtkStr(pNtk, Prs_BoxNtk(pNtk, i));
             Cba_ObjType_t Type = Prs_ManFindType( pNtkName, &nInputs, 1, &pOutNames );
+            if ( Type == CBA_BOX_RAMWC )
+                continue;
             if ( Type == CBA_OBJ_BOX )
             {
                 pBox = Cba_ManNtkFind( p->pDesign, pNtkName );
@@ -1276,11 +1434,23 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
             else if ( Type == CBA_BOX_ADD )
                 nOutputs = 2;
             else if ( Type == CBA_BOX_NMUX )
-                nInputs = 1 + (1 << atoi(pNtkName+strlen("wide_mux_")));
+            {
+                if ( !strncmp(pNtkName, "wide_mux_", strlen("wide_mux_")) )
+                    nInputs = 1 + (1 << atoi(pNtkName+strlen("wide_mux_")));
+                else if ( !strncmp(pNtkName, "Mux_", strlen("Mux_")) )
+                    nInputs = 1 + (1 << atoi(pNtkName+strlen("Mux_")));
+                else assert( 0 );
+            }
             else if ( Type == CBA_BOX_SEL )
-                nInputs = 1 + atoi(pNtkName+strlen("wide_select_"));
+            {
+                if ( !strncmp(pNtkName, "wide_select_", strlen("wide_select_")) )
+                    nInputs = 1 + atoi(pNtkName+strlen("wide_select_"));
+                else if ( !strncmp(pNtkName, "Select_", strlen("Select_")) )
+                    nInputs = 1 + atoi(pNtkName+strlen("Select_"));
+                else assert( 0 );
+            }
             else if ( (Type == CBA_BOX_DFFRS || Type == CBA_BOX_LATCHRS) && !strncmp(pNtkName, "wide_", strlen("wide_")) && !Prs_CreateFlopSetReset(p, pNtk, vBox, NULL, NULL, NULL, NULL) )
-                Type = CBA_BOX_CATIN, nInputs = atoi(pNtkName+strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_")), nOutputs = 1;
+                nInputs = atoi(pNtkName+strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_")), nOutputs = 1, Type = CBA_BOX_CATIN;
             // create object
             iObj = Cba_ObjAlloc( p, Type, nInputs, nOutputs );
             if ( pBox ) Cba_ObjSetFunc( p, iObj, Cba_NtkId(pBox) );
@@ -1300,46 +1470,23 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                     Prs_CreateSignalOut( p, iFon, pNtk, ActId );
                 }
         }
+        Vec_IntWriteEntry( vBox2Obj, i, iObj );
         if ( Prs_BoxName(pNtk, i) )
             Cba_ObjSetName( p, iObj, Prs_BoxName(pNtk, i) );
+        //Cba_VerificSaveLineFile( p, iObj, pInst->Linefile() );
     }
 
-    // add wire ranges 
-    Vec_IntForEachEntryTwo( &pNtk->vWires, &pNtk->vWiresR, NameId, RangeId, i )
-    {
-        iFon = Prs_CreateVerilogFindFon( p, NameId ); // direct name
-        if ( iFon == 0 || RangeId == 0 ) // unused wire or 1-bit wire (default)
-            continue;
-        Prs_NtkParseRange( pNtk, RangeId, &Left, &Right );
-        Cba_FonSetLeft( p, iFon, Left );
-        Cba_FonSetRight( p, iFon, Right );
-    }
-    Vec_IntForEachEntryTwo( &pNtk->vOutputs, &pNtk->vOutputsR, NameId, RangeId, i )
-    {
-        iFon = Prs_CreateVerilogFindFon( p, NameId ); // direct name
-        if ( iFon == 0 || RangeId == 0 ) // unused wire or 1-bit wire (default)
-            continue;
-        Prs_NtkParseRange( pNtk, RangeId, &Left, &Right );
-        Cba_FonSetLeft( p, iFon, Left );
-        Cba_FonSetRight( p, iFon, Right );
-    }
-
-    // set cat-out ranges
-    Cba_NtkForEachObj( p, iObj )
-        if ( Cba_ObjType(p, iObj) == CBA_BOX_CATOUT )
-        {
-            int nBits = 0;
-            Cba_ObjForEachFon( p, iObj, iFon, k )
-                nBits += Cba_FonRange(p, iFon);
-            iFon = Cba_ObjFinFon( p, iObj, 0 );
-            Cba_FonSetLeft ( p, iFon, nBits-1 );
-            Cba_FonSetRight( p, iFon, 0 );
-        }
-
     // connect objects
     Prs_NtkForEachBox( pNtk, vBox, i )
     {
-        iObj = Cba_NtkPiNum(p) + Cba_NtkPoNum(p) + i + 1;
+//        char * pInstName = NULL;
+//        if ( Prs_BoxName(pNtk, i) )
+//            pInstName = Prs_NtkStr(pNtk, Prs_BoxName(pNtk, i));
+        if ( pNtk->iModuleName == 291 && i == 0 )
+        {
+            int s = 0;
+        }
+        iObj = Vec_IntEntry( vBox2Obj, i );
         if ( Prs_BoxIsNode(pNtk, i) ) // node
         {
             Vec_IntForEachEntryDoubleStart( vBox, FormId, ActId, k, 2 )
@@ -1354,23 +1501,6 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
             int nInputs = -1;
             char ** pInNames = NULL, * pNtkName = Prs_NtkStr(pNtk, Prs_BoxNtk(pNtk, i));
             Cba_ObjType_t Type = Prs_ManFindType( pNtkName, &nInputs, 0, &pInNames );
-            assert( Type == Cba_ObjType(p, iObj) || CBA_BOX_CATIN == Cba_ObjType(p, iObj) );
-            // mark PI objects
-            Cba_NtkCleanMap2( p );
-            if ( Type == CBA_OBJ_BOX )
-            {
-                Cba_Ntk_t * pBox = Cba_ObjNtk(p, iObj);
-                assert( Cba_NtkPiNum(pBox) == Cba_ObjFinNum(p, iObj) );
-                assert( Cba_NtkPoNum(pBox) == Cba_ObjFonNum(p, iObj) );
-                Cba_NtkForEachPi( pBox, iTerm, k )
-                    Cba_NtkSetMap2( p, Cba_ObjName(pBox, iTerm), k+1 );
-            }
-            else
-            {
-                assert( nInputs >= 0 );
-                for ( k = 0; k < nInputs; k++ )
-                    Cba_NtkSetMap2( p, Cba_NtkStrId(p, pInNames[k]), k+1 );
-            }
             if ( (Type == CBA_BOX_DFFRS || Type == CBA_BOX_LATCHRS) && !strncmp(pNtkName, "wide_", strlen("wide_")) )
             {
                 int IndexSet = -1, IndexRst = -1,  iBitSet = -1, iBitRst = -1;
@@ -1383,30 +1513,34 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                 }
                 else
                 {
-                    int Width = atoi( pNtkName + strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_") );
+                    int w, Width = atoi( pNtkName + strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_") );
                     assert( Cba_ObjType(p, iObj) == CBA_BOX_CATIN );
-                    for ( i = 0; i < Width; i++ )
+                    // prepare inputs
+                    assert( nInputs >= 0 );
+                    Cba_NtkCleanMap2( p );
+                    for ( k = 0; k < nInputs; k++ )
+                        Cba_NtkSetMap2( p, Cba_NtkStrId(p, pInNames[k]), k+1 );
+                    // create bit-level objects
+                    for ( w = 0; w < Width; w++ )
                     {
                         // create bit-level flop
                         int iObjNew = Cba_ObjAlloc( p, Type, 4, 1 );
                         if ( Prs_BoxName(pNtk, i) )
                         {
-                            char Buffer[1000];  sprintf( Buffer, "%s[%d]", Prs_NtkStr(pNtk, Prs_BoxName(pNtk, i)), i );
-                            NameId = Cba_NtkNewStrId( p, Buffer ); 
+                            NameId = Cba_NtkNewStrId( p, "%s[%d]", Prs_NtkStr(pNtk, Prs_BoxName(pNtk, i)), w );
                             Cba_ObjSetName( p, iObjNew, NameId );
                         }
                         //Cba_VerificSaveLineFile( p, iObjNew, pInst->Linefile() );
                         // set output fon
                         iFon = Cba_ObjFon0(p, iObjNew);
                         {
-                            char Buffer[1000];  sprintf( Buffer, "%s[%d]", Cba_FonNameStr(p, Cba_ObjFon0(p, iObj)), i );
-                            NameId = Cba_NtkNewStrId( p, Buffer ); 
+                            NameId = Cba_NtkNewStrId( p, "%s[%d]", Cba_FonNameStr(p, Cba_ObjFon0(p, iObj)), w );
                             Cba_FonSetName( p, iFon, NameId );
                         }
                         // no need to map this name because it may be produced elsewhere
                         //Cba_NtkSetMap( p, NameId, iFon );
                         // add the flop
-                        Cba_ObjSetFinFon( p, iObj, Width-1-i, iFon );
+                        Cba_ObjSetFinFon( p, iObj, Width-1-w, iFon );
                         // create bit-level flops
                         Vec_IntForEachEntryDouble( vBox, FormId, ActId, k )
                             if ( Cba_NtkGetMap2(p, FormId) )
@@ -1415,24 +1549,41 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                                 iFon = Prs_CreateSignalIn( p, pNtk, ActId );  assert( iFon );
                                 // create bit-select node for data/set/reset (but not for clock)
                                 if ( Index < 3 ) // not clock
-                                {
-                                    int iObjNew2 = Prs_CreateSlice( p, iFon, pNtk, 1, 0 );
-                                    //Cba_VerificSaveLineFile( p, iObjNew, pInst->Linefile() );
-                                    iFon = Cba_ObjFon0( p, iObjNew2 );
-                                }
+                                    iFon = Prs_CreateSlice( p, iFon, pNtk, 0, 0 );
                                 Cba_ObjSetFinFon( p, iObjNew, Index, iFon );
                             }
                     }
                     continue;
                 }
             }
+            assert( Type == Cba_ObjType(p, iObj) );
+            //assert( nInputs == -1 || nInputs == Cba_ObjFinNum(p, iObj) );
+            // mark PI objects
+            Cba_NtkCleanMap2( p );
+            if ( Type == CBA_OBJ_BOX )
+            {
+                Cba_Ntk_t * pBox = Cba_ObjNtk(p, iObj);
+                assert( Cba_NtkPiNum(pBox) == Cba_ObjFinNum(p, iObj) );
+                assert( Cba_NtkPoNum(pBox) == Cba_ObjFonNum(p, iObj) );
+                Cba_NtkForEachPi( pBox, iTerm, k )
+                    Cba_NtkSetMap2( p, Cba_ObjName(pBox, iTerm), k+1 );
+            }
+            else
+            {
+                assert( nInputs >= 0 );
+                for ( k = 0; k < nInputs; k++ )
+                    Cba_NtkSetMap2( p, Cba_NtkStrId(p, pInNames[k]), k+1 );
+            }
             // connect box fins
             Vec_IntForEachEntryDouble( vBox, FormId, ActId, k )
                 if ( Cba_NtkGetMap2(p, FormId) )
                 {
+                    int Index = Cba_NtkGetMap2(p, FormId)-1;
+                    int nBits = Cba_ObjFinNum(p, iObj);
+                    assert( Index < nBits );
                     iFon = Prs_CreateSignalIn( p, pNtk, ActId );
                     if ( iFon )
-                        Cba_ObjSetFinFon( p, iObj, Cba_NtkGetMap2(p, FormId)-1, iFon );
+                        Cba_ObjSetFinFon( p, iObj, Index, iFon );
                 }
             // special cases
             if ( Type == CBA_BOX_NMUX || Type == CBA_BOX_SEL )
@@ -1441,9 +1592,22 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                 int nBits  = Cba_FonRange( p, FonCat );
                 int nParts = Cba_ObjFinNum(p, iObj) - 1;
                 int Slice  = nBits / nParts;
-                assert( Cba_ObjFinNum(p, iObj) > 2 );
+                int nFins = Cba_ObjFinNum(p, iObj);
+                assert( Cba_ObjFinNum(p, iObj) >= 2 );
                 assert( Slice * nParts == nBits );
+                assert( nFins == 1 + nParts );
                 Cba_ObjCleanFinFon( p, iObj, 1 );
+                // create buffer for the constant
+                if ( FonCat < 0 ) 
+                {
+                    int iObjNew = Cba_ObjAlloc( p, CBA_BOX_BUF, 1, 1 );
+                    Cba_ObjSetFinFon( p, iObjNew, 0, FonCat );
+                    FonCat = Cba_ObjFon0( p, iObjNew );
+                    NameId = Cba_NtkNewStrId( p, "_buf_const_%d", iObjNew );
+                    Cba_FonSetName( p, FonCat, NameId );
+                    Cba_FonSetLeft( p, FonCat, nBits-1 );
+                    Cba_FonSetRight( p, FonCat, 0 );
+                }
                 for ( k = 0; k < nParts; k++ )
                 {
 //                    iFon = Prs_CreateSlice( p, FonCat, pNtk, (nParts-1-k)*Slice+Slice-1, (nParts-1-k)*Slice );
@@ -1453,6 +1617,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
             }
         }
     }
+    Vec_IntFree( vBox2Obj );
     // connect outputs
     Vec_IntForEachEntryTwo( &pNtk->vOutputs, &pNtk->vOutputsR, NameId, RangeId, i )
     {
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index 3ac9fdd7..b628ab9e 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -193,14 +193,19 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
 void Cba_ManCreatePrimMap( char ** pMap )
 {
     memset( pMap, 0, sizeof(char *) * CBA_BOX_LAST );
+
+    pMap[ CBA_BOX_SLICE  ] = "sli";
+    pMap[ CBA_BOX_CATIN  ] = "icc";
+    pMap[ CBA_BOX_CATOUT ] = "occ";
+
     pMap[ CBA_BOX_BUF    ] = "";
     pMap[ CBA_BOX_INV    ] = "~";
     pMap[ CBA_BOX_AND    ] = "&"; 
-    pMap[ CBA_BOX_NAND   ] = "~&"; 
+    pMap[ CBA_BOX_NAND   ] = "&"; 
     pMap[ CBA_BOX_OR     ] = "|"; 
-    pMap[ CBA_BOX_NOR    ] = "~|"; 
+    pMap[ CBA_BOX_NOR    ] = "|"; 
     pMap[ CBA_BOX_XOR    ] = "^"; 
-    pMap[ CBA_BOX_XNOR   ] = "~^"; 
+    pMap[ CBA_BOX_XNOR   ] = "^"; 
     pMap[ CBA_BOX_SHARP  ] = "&"; 
     pMap[ CBA_BOX_SHARPL ] = "&"; 
     pMap[ CBA_BOX_MUX    ] = "?"; 
@@ -218,12 +223,12 @@ void Cba_ManCreatePrimMap( char ** pMap )
     pMap[ CBA_BOX_LNOR   ] = NULL; 
     pMap[ CBA_BOX_LXOR   ] = "^^"; 
     pMap[ CBA_BOX_LXNOR  ] = NULL; 
-    pMap[ CBA_BOX_NMUX   ] = NULL; 
-    pMap[ CBA_BOX_SEL    ] = NULL; 
+    pMap[ CBA_BOX_NMUX   ] = "nmux"; 
+    pMap[ CBA_BOX_SEL    ] = "sel"; 
     pMap[ CBA_BOX_PSEL   ] = NULL; 
     pMap[ CBA_BOX_ENC    ] = NULL; 
     pMap[ CBA_BOX_PENC   ] = NULL; 
-    pMap[ CBA_BOX_DEC    ] = NULL; 
+    pMap[ CBA_BOX_DEC    ] = "dec"; 
     pMap[ CBA_BOX_EDEC   ] = NULL; 
     pMap[ CBA_BOX_ADD    ] = "+"; 
     pMap[ CBA_BOX_SUB    ] = "-"; 
@@ -242,39 +247,23 @@ void Cba_ManCreatePrimMap( char ** pMap )
     pMap[ CBA_BOX_NEQU   ] = "!="; 
     pMap[ CBA_BOX_SHIL   ] = "<<"; 
     pMap[ CBA_BOX_SHIR   ] = ">>"; 
-    pMap[ CBA_BOX_ROTL   ] = NULL; 
-    pMap[ CBA_BOX_ROTR   ] = NULL; 
+    pMap[ CBA_BOX_ROTL   ] = "rotL"; 
+    pMap[ CBA_BOX_ROTR   ] = "rotR"; 
+
+    pMap[ CBA_BOX_TRI    ] = "tri";
+    pMap[ CBA_BOX_RAM    ] = "ram";
+    pMap[ CBA_BOX_RAMR   ] = "ramR";
+    pMap[ CBA_BOX_RAMW   ] = "ramW";
+    pMap[ CBA_BOX_RAMWC  ] = "ramWC";
+    pMap[ CBA_BOX_RAMBOX ] = "ramBox";
+
+    pMap[ CBA_BOX_LATCH  ] = "lat";
+    pMap[ CBA_BOX_LATCHRS] = "latrs";
+    pMap[ CBA_BOX_DFF    ] = "dff";
+    pMap[ CBA_BOX_DFFRS  ] = "dffrs";
 }
 
 
-#ifdef WIN32
-#define vsnprintf _vsnprintf
-#endif
-
-#include <stdio.h>
-
-//extern int vsnprintf(char * s, size_t n, const char * format, va_list arg);
-
-static inline void Vec_StrPrintF( Vec_Str_t * p, const char * format, ... )
-{
-    va_list args;
-    char * pBuffer;
-    int nBuffer, nSize = 1000; 
-    va_start( args, format );
-    Vec_StrGrow( p, Vec_StrSize(p) + nSize );
-    pBuffer = Vec_StrArray(p) + Vec_StrSize(p);
-    nBuffer = vsnprintf( pBuffer, nSize, format, args );
-    if ( nBuffer > nSize )
-    {
-        Vec_StrGrow( p, Vec_StrSize(p) + nBuffer + nSize );
-        pBuffer = Vec_StrArray(p) + Vec_StrSize(p);
-        nSize = vsnprintf( pBuffer, nBuffer, format, args );
-        assert( nSize == nBuffer );
-    }
-    p->nSize += nBuffer;
-    va_end( args );
-}
-
 
 static inline int Cba_NameIsLegalInVerilog( char * pName )
 {
@@ -303,19 +292,24 @@ static inline char * Cba_NameLegal( char * pName )
 }
 char * Cba_ObjGetName( Cba_Ntk_t * p, int i )
 {
-    int fLegalize = 1;
-    char * pName = Cba_ObjNameStr(p, i); assert( pName );
-    return fLegalize ? Cba_NameLegal(pName) : pName;
+    char * pName = Cba_ObjNameStr(p, i);
+    if ( pName == NULL )
+        return pName;
+    if ( Cba_NameIsLegalInVerilog(pName) )
+        return pName;
+    return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "\\%s ", pName );
 }
 char * Cba_FonGetName( Cba_Ntk_t * p, int i )
 {
-    int fLegalize = 1;
-    char * pName = Cba_FonNameStr(p, i); assert( pName );
-    return fLegalize ? Cba_NameLegal(pName) : pName;
+    char * pName = Cba_FonNameStr(p, i);
+    if ( pName == NULL )
+        return pName;
+    if ( Cba_NameIsLegalInVerilog(pName) )
+        return pName;
+    return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "\\%s ", pName );
 }
 
 
-
 void Cba_ManWriteFonRange( Cba_Ntk_t * p, int iFon )
 {
     Vec_Str_t * vStr = &p->pDesign->vOut;
@@ -421,11 +415,7 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
         Vec_StrPrintStr( vStr, Cba_ObjIsPi(p, iObj) ? "input " : "output " );
         Cba_ManWriteFonRange( p, Cba_ObjIsPi(p, iObj) ? Cba_ObjFon0(p, iObj) : Cba_ObjFinFon(p, iObj, 0) );
         Vec_StrPrintStr( vStr, Cba_ObjGetName(p, iObj) );
-//        Vec_StrPush( vStr, ';' );
-//        for ( k = Vec_StrSize(vStr); k < Offset + 40; k++ )
-//            Vec_StrPush( vStr, ' ' );
         Vec_StrPrintF( vStr, ";%*s", Offset + 40 - Vec_StrSize(vStr), "" );
-
         Cba_ManWriteLineFile( p, iObj, FileAttr, LineAttr );
         Vec_StrPush( vStr, '\n' );
     }
@@ -433,6 +423,8 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
     // write objects
     Cba_NtkForEachBox( p, iObj )
     {
+//        char * pNameNtk = Cba_NtkName(p);
+//        char * pNameInst = Cba_ObjGetName(p, iObj);
         int Type = Cba_ObjType(p, iObj);
         if ( Cba_ObjIsSlice(p, iObj) )
             continue;
@@ -813,12 +805,17 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             }
             else if ( Cba_NtkTypeName(p, Type) ) // binary operation
             {
+                int fCompl = (Type == CBA_BOX_NAND || Type == CBA_BOX_NOR || Type == CBA_BOX_XNOR);
                 Vec_StrPush( vStr, ' ' );
+                if ( fCompl )
+                    Vec_StrPrintStr( vStr, "!(" );
                 Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );
                 Vec_StrPush( vStr, ' ' );
                 Vec_StrPrintStr( vStr, Cba_NtkTypeName(p, Type) );
                 Vec_StrPush( vStr, ' ' );
                 Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 1), fInlineConcat, 0 );
+                if ( fCompl )
+                    Vec_StrPrintStr( vStr, ")" );
             }
             else // unknown
             {
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 5cf351d4..96380a44 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -81,6 +81,7 @@
 #include <stdarg.h>
 #include <stdlib.h>
 #include <assert.h>
+#include <stdio.h>
 
 ////////////////////////////////////////////////////////////////////////
 ///                         NAMESPACES                               ///
diff --git a/src/misc/util/utilNam.c b/src/misc/util/utilNam.c
index 3be805aa..49a3ae6a 100644
--- a/src/misc/util/utilNam.c
+++ b/src/misc/util/utilNam.c
@@ -45,20 +45,22 @@ struct Abc_Nam_t_
     int              iHandle;      // the current free handle
     char *           pStore;       // storage for name objects
     // internal number mappings
-    Vec_Int_t *      vInt2Handle;  // mapping integers into handles
-    Vec_Int_t *      vInt2Next;    // mapping integers into nexts
+    Vec_Int_t        vInt2Handle;  // mapping integers into handles
+    Vec_Int_t        vInt2Next;    // mapping integers into nexts
     // hash table for names
     int *            pBins;        // the hash table bins 
     int              nBins;        // the number of bins 
     // manager recycling
     int              nRefs;        // reference counter for the manager
+    // internal buffer
+    Vec_Str_t        vBuffer;      
 };
 
 static inline char * Abc_NamHandleToStr( Abc_Nam_t * p, int h )        { return (char *)(p->pStore + h);                         }
-static inline int    Abc_NamIntToHandle( Abc_Nam_t * p, int i )        { return Vec_IntEntry(p->vInt2Handle, i);                 }
+static inline int    Abc_NamIntToHandle( Abc_Nam_t * p, int i )        { return Vec_IntEntry(&p->vInt2Handle, i);                }
 static inline char * Abc_NamIntToStr( Abc_Nam_t * p, int i )           { return Abc_NamHandleToStr(p, Abc_NamIntToHandle(p,i));  }
-static inline int    Abc_NamIntToNext( Abc_Nam_t * p, int i )          { return Vec_IntEntry(p->vInt2Next, i);                   }
-static inline int *  Abc_NamIntToNextP( Abc_Nam_t * p, int i )         { return Vec_IntEntryP(p->vInt2Next, i);                  }
+static inline int    Abc_NamIntToNext( Abc_Nam_t * p, int i )          { return Vec_IntEntry(&p->vInt2Next, i);                  }
+static inline int *  Abc_NamIntToNextP( Abc_Nam_t * p, int i )         { return Vec_IntEntryP(&p->vInt2Next, i);                 }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -86,8 +88,8 @@ Abc_Nam_t * Abc_NamStart( int nObjs, int nAveSize )
     p->nBins       = Abc_PrimeCudd( nObjs );
     p->pBins       = ABC_CALLOC( int, p->nBins );
     // 0th object is unused
-    p->vInt2Handle = Vec_IntAlloc( nObjs );  Vec_IntPush( p->vInt2Handle, -1 );
-    p->vInt2Next   = Vec_IntAlloc( nObjs );  Vec_IntPush( p->vInt2Next,   -1 );
+    Vec_IntGrow( &p->vInt2Handle, nObjs );  Vec_IntPush( &p->vInt2Handle, -1 );
+    Vec_IntGrow( &p->vInt2Next,   nObjs );  Vec_IntPush( &p->vInt2Next,   -1 );
     p->iHandle     = 4;
     memset( p->pStore, 0, 4 );
 //Abc_Print( 1, "Starting nam with %d bins.\n", p->nBins );
@@ -110,8 +112,9 @@ Abc_Nam_t * Abc_NamStart( int nObjs, int nAveSize )
 void Abc_NamStop( Abc_Nam_t * p )
 {
 //Abc_Print( 1, "Starting nam with %d bins.\n", p->nBins );
-    Vec_IntFree( p->vInt2Handle );
-    Vec_IntFree( p->vInt2Next );
+    Vec_StrErase( &p->vBuffer );
+    Vec_IntErase( &p->vInt2Handle );
+    Vec_IntErase( &p->vInt2Next );
     ABC_FREE( p->pStore );
     ABC_FREE( p->pBins );
     ABC_FREE( p );
@@ -130,10 +133,13 @@ void Abc_NamStop( Abc_Nam_t * p )
 ***********************************************************************/
 void Abc_NamPrint( Abc_Nam_t * p )
 {
-    int h, i;
-    Vec_IntForEachEntryStart( p->vInt2Handle, h, i, 1 )
-        Abc_Print( 1, "%d=\n%s\n", i, Abc_NamHandleToStr(p, h) );
+    int h, i, Counter = 0;
+    Vec_IntForEachEntryStart( &p->vInt2Handle, h, i, 1 )
+        if ( Abc_NamHandleToStr(p, h)[0] == '[' )
+            Abc_Print( 1, "%s ",  Abc_NamHandleToStr(p, h) ), Counter++;
+//            Abc_Print( 1, "%d=\n%s\n", i, Abc_NamHandleToStr(p, h) );
 //    Abc_Print( 1, "\n" );
+    printf( "  %d\n", Counter );
 }
 
 /**Function*************************************************************
@@ -185,7 +191,7 @@ void Abc_NamDeref( Abc_Nam_t * p )
 ***********************************************************************/
 int Abc_NamObjNumMax( Abc_Nam_t * p )
 {
-    return Vec_IntSize(p->vInt2Handle);
+    return Vec_IntSize(&p->vInt2Handle);
 }
 
 /**Function*************************************************************
@@ -204,7 +210,7 @@ int Abc_NamMemUsed( Abc_Nam_t * p )
     if ( p == NULL )
         return 0;
     return sizeof(Abc_Nam_t) + p->iHandle + sizeof(int) * p->nBins + 
-        sizeof(int) * (p->vInt2Handle->nSize + p->vInt2Next->nSize);
+        sizeof(int) * (p->vInt2Handle.nSize + p->vInt2Next.nSize);
 }
 
 /**Function*************************************************************
@@ -223,7 +229,7 @@ int Abc_NamMemAlloc( Abc_Nam_t * p )
     if ( p == NULL )
         return 0;
     return sizeof(Abc_Nam_t) + p->nStore + sizeof(int) * p->nBins + 
-        sizeof(int) * (p->vInt2Handle->nCap + p->vInt2Next->nCap);
+        sizeof(int) * (p->vInt2Handle.nCap + p->vInt2Next.nCap);
 }
 
 /**Function*************************************************************
@@ -328,8 +334,7 @@ static inline int * Abc_NamStrHashFind( Abc_Nam_t * p, const char * pStr, const
 ***********************************************************************/
 void Abc_NamStrHashResize( Abc_Nam_t * p )
 {
-    Vec_Int_t * vInt2HandleOld;
-    char * pThis;
+    Vec_Int_t vInt2HandleOld;  char * pThis; 
     int * piPlace, * pBinsOld, iHandleOld, i;//, clk = Abc_Clock();
     assert( p->pBins != NULL );
 //    Abc_Print( 1, "Resizing names manager hash table from %6d to %6d. ", p->nBins, Abc_PrimeCudd( 3 * p->nBins ) );
@@ -339,21 +344,22 @@ void Abc_NamStrHashResize( Abc_Nam_t * p )
     p->pBins = ABC_CALLOC( int, p->nBins );
     // replace the handles array
     vInt2HandleOld = p->vInt2Handle;
-    p->vInt2Handle = Vec_IntAlloc( 2 * Vec_IntSize(vInt2HandleOld) ); 
-    Vec_IntPush( p->vInt2Handle, -1 );
-    Vec_IntClear( p->vInt2Next );    Vec_IntPush( p->vInt2Next, -1 );
+    Vec_IntZero( &p->vInt2Handle );
+    Vec_IntGrow( &p->vInt2Handle, 2 * Vec_IntSize(&vInt2HandleOld) ); 
+    Vec_IntPush( &p->vInt2Handle, -1 );
+    Vec_IntClear( &p->vInt2Next );    Vec_IntPush( &p->vInt2Next, -1 );
     // rehash the entries from the old table
-    Vec_IntForEachEntryStart( vInt2HandleOld, iHandleOld, i, 1 )
+    Vec_IntForEachEntryStart( &vInt2HandleOld, iHandleOld, i, 1 )
     {
         pThis   = Abc_NamHandleToStr( p, iHandleOld );
         piPlace = Abc_NamStrHashFind( p, pThis, NULL );
         assert( *piPlace == 0 );
-        *piPlace = Vec_IntSize( p->vInt2Handle );
-        assert( Vec_IntSize( p->vInt2Handle ) == i );
-        Vec_IntPush( p->vInt2Handle, iHandleOld );
-        Vec_IntPush( p->vInt2Next,   0 );
+        *piPlace = Vec_IntSize( &p->vInt2Handle );
+        assert( Vec_IntSize( &p->vInt2Handle ) == i );
+        Vec_IntPush( &p->vInt2Handle, iHandleOld );
+        Vec_IntPush( &p->vInt2Next,   0 );
     }
-    Vec_IntFree( vInt2HandleOld );
+    Vec_IntErase( &vInt2HandleOld );
     ABC_FREE( pBinsOld );
 //    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
@@ -418,15 +424,15 @@ int Abc_NamStrFindOrAdd( Abc_Nam_t * p, char * pStr, int * pfFound )
     }
     assert( p->nStore >= iHandleNew );
     // create new handle
-    *piPlace = Vec_IntSize( p->vInt2Handle );
+    *piPlace = Vec_IntSize( &p->vInt2Handle );
     strcpy( Abc_NamHandleToStr( p, p->iHandle ), pStr );
-    Vec_IntPush( p->vInt2Handle, p->iHandle );
-    Vec_IntPush( p->vInt2Next, 0 );
+    Vec_IntPush( &p->vInt2Handle, p->iHandle );
+    Vec_IntPush( &p->vInt2Next, 0 );
     p->iHandle = iHandleNew;
     // extend the hash table
-    if ( Vec_IntSize(p->vInt2Handle) > 2 * p->nBins )
+    if ( Vec_IntSize(&p->vInt2Handle) > 2 * p->nBins )
         Abc_NamStrHashResize( p );
-    return Vec_IntSize(p->vInt2Handle) - 1;
+    return Vec_IntSize(&p->vInt2Handle) - 1;
 }
 int Abc_NamStrFindOrAddLim( Abc_Nam_t * p, char * pStr, char * pLim, int * pfFound )
 {
@@ -452,17 +458,32 @@ int Abc_NamStrFindOrAddLim( Abc_Nam_t * p, char * pStr, char * pLim, int * pfFou
     }
     assert( p->nStore >= iHandleNew );
     // create new handle
-    *piPlace = Vec_IntSize( p->vInt2Handle );
+    *piPlace = Vec_IntSize( &p->vInt2Handle );
     pStore = Abc_NamHandleToStr( p, p->iHandle );
     strncpy( pStore, pStr, pLim - pStr );
     pStore[pLim - pStr] = 0;
-    Vec_IntPush( p->vInt2Handle, p->iHandle );
-    Vec_IntPush( p->vInt2Next, 0 );
+    Vec_IntPush( &p->vInt2Handle, p->iHandle );
+    Vec_IntPush( &p->vInt2Next, 0 );
     p->iHandle = iHandleNew;
     // extend the hash table
-    if ( Vec_IntSize(p->vInt2Handle) > 2 * p->nBins )
+    if ( Vec_IntSize(&p->vInt2Handle) > 2 * p->nBins )
         Abc_NamStrHashResize( p );
-    return Vec_IntSize(p->vInt2Handle) - 1;
+    return Vec_IntSize(&p->vInt2Handle) - 1;
+}
+int Abc_NamStrFindOrAddF( Abc_Nam_t * p, const char * format, ...  )
+{
+    int nAdded, nSize = 1000; 
+    va_list args;  va_start( args, format );
+    Vec_StrGrow( &p->vBuffer, Vec_StrSize(&p->vBuffer) + nSize );
+    nAdded = vsnprintf( Vec_StrLimit(&p->vBuffer), nSize, format, args );
+    if ( nAdded > nSize )
+    {
+        Vec_StrGrow( &p->vBuffer, Vec_StrSize(&p->vBuffer) + nAdded + nSize );
+        nSize = vsnprintf( Vec_StrLimit(&p->vBuffer), nAdded, format, args );
+        assert( nSize == nAdded );
+    }
+    va_end( args );
+    return Abc_NamStrFindOrAddLim( p, Vec_StrLimit(&p->vBuffer), Vec_StrLimit(&p->vBuffer) + nAdded, NULL );
 }
 
 /**Function*************************************************************
@@ -483,6 +504,23 @@ char * Abc_NamStr( Abc_Nam_t * p, int NameId )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns internal buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Abc_NamBuffer( Abc_Nam_t * p )
+{
+    Vec_StrClear(&p->vBuffer);
+    return &p->vBuffer;
+}
+
+/**Function*************************************************************
+
   Synopsis    [For each ID of the first manager, gives ID of the second one.]
 
   Description []
@@ -500,7 +538,7 @@ Vec_Int_t * Abc_NamComputeIdMap( Abc_Nam_t * p1, Abc_Nam_t * p2 )
     if ( p1 == p2 )
         return Vec_IntStartNatural( Abc_NamObjNumMax(p1) );
     vMap = Vec_IntStart( Abc_NamObjNumMax(p1) );
-    Vec_IntForEachEntryStart( p1->vInt2Handle, iHandle1, i, 1 )
+    Vec_IntForEachEntryStart( &p1->vInt2Handle, iHandle1, i, 1 )
     {
         pThis = Abc_NamHandleToStr( p1, iHandle1 );
         piPlace = Abc_NamStrHashFind( p2, pThis, NULL );
diff --git a/src/misc/util/utilNam.h b/src/misc/util/utilNam.h
index 86802802..8083a566 100644
--- a/src/misc/util/utilNam.h
+++ b/src/misc/util/utilNam.h
@@ -62,7 +62,9 @@ extern int             Abc_NamStrFind( Abc_Nam_t * p, char * pStr );
 extern int             Abc_NamStrFindLim( Abc_Nam_t * p, char * pStr, char * pLim );
 extern int             Abc_NamStrFindOrAdd( Abc_Nam_t * p, char * pStr, int * pfFound );
 extern int             Abc_NamStrFindOrAddLim( Abc_Nam_t * p, char * pStr, char * pLim, int * pfFound );
+extern int             Abc_NamStrFindOrAddF( Abc_Nam_t * p, const char * format, ...  );
 extern char *          Abc_NamStr( Abc_Nam_t * p, int id );
+extern Vec_Str_t *     Abc_NamBuffer( Abc_Nam_t * p );
 extern Vec_Int_t *     Abc_NamComputeIdMap( Abc_Nam_t * p1, Abc_Nam_t * p2 );
 extern int             Abc_NamReportCommon( Vec_Int_t * vNameIds1, Abc_Nam_t * p1, Abc_Nam_t * p2 );
 extern char *          Abc_NamReportUnique( Vec_Int_t * vNameIds1, Abc_Nam_t * p1, Abc_Nam_t * p2 );
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 63be43d5..04cd5da8 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -283,6 +283,10 @@ static inline char * Vec_StrArray( Vec_Str_t * p )
 {
     return p->pArray;
 }
+static inline char * Vec_StrLimit( Vec_Str_t * p )
+{
+    return p->pArray + p->nSize;
+}
 
 /**Function*************************************************************
 
@@ -299,6 +303,10 @@ static inline int Vec_StrSize( Vec_Str_t * p )
 {
     return p->nSize;
 }
+static inline void Vec_StrSetSize( Vec_Str_t * p, int nSize )
+{
+    p->nSize = nSize;
+}
 
 /**Function*************************************************************
 
@@ -668,6 +676,39 @@ static inline void Vec_StrPrintStr( Vec_Str_t * p, const char * pStr )
         Vec_StrPush( p, pStr[i] );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#ifdef WIN32
+#define vsnprintf _vsnprintf
+#endif
+
+static inline char * Vec_StrPrintF( Vec_Str_t * p, const char * format, ... )
+{
+    int nAdded, nSize = 1000; 
+    va_list args;  va_start( args, format );
+    Vec_StrGrow( p, Vec_StrSize(p) + nSize );
+    nAdded = vsnprintf( Vec_StrLimit(p), nSize, format, args );
+    if ( nAdded > nSize )
+    {
+        Vec_StrGrow( p, Vec_StrSize(p) + nAdded + nSize );
+        nSize = vsnprintf( Vec_StrLimit(p), nAdded, format, args );
+        assert( nSize == nAdded );
+    }
+    p->nSize += nAdded;
+    va_end( args );
+    return Vec_StrLimit(p) - nAdded;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Appends the string to the char vector.]