Several improvements to CBA data-structure.

8 files changed, 629 insertions, 266 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 4043943e..716eaf43 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -120,6 +120,15 @@ typedef enum {
 } Cba_ObjType_t; 
 
 
+// name types
+typedef enum { 
+    CBA_NAME_BIN = 0,        // 0:  binary ID real
+    CBA_NAME_WORD,           // 1:  word-level ID real
+    CBA_NAME_INFO,           // 2:  word-level offset
+    CBA_NAME_INDEX,          // 3:  word-leveln index
+} Cba_NameType_t; 
+
+
 typedef struct Cba_Ntk_t_ Cba_Ntk_t;
 typedef struct Cba_Man_t_ Cba_Man_t;
 
@@ -136,12 +145,12 @@ struct Cba_Ntk_t_
     // interface
     Vec_Int_t    vInputs;  // inputs 
     Vec_Int_t    vOutputs; // outputs
+    Vec_Int_t    vInfo;    // input/output/wire info
     // object attributes
     Vec_Str_t    vType;    // types     
     Vec_Int_t    vFanin;   // fanin
     Vec_Int_t    vIndex;   // index
     Vec_Int_t    vName;    // original NameId or InstId
-    Vec_Int_t    vRange;   // range
     Vec_Int_t    vCopy;    // copy
     // other
     Vec_Int_t    vArray;
@@ -160,6 +169,7 @@ struct Cba_Man_t_
     int          nNtks;    // number of current networks
     Cba_Ntk_t *  pNtks;    // networks
     // user data
+    Vec_Str_t *  vOut;     
     Vec_Int_t    vBuf2RootNtk;
     Vec_Int_t    vBuf2RootObj;
     Vec_Int_t    vBuf2LeafNtk;
@@ -211,17 +221,27 @@ static inline Cba_Ntk_t *    Cba_NtkHostNtk( Cba_Ntk_t * p )                 { r
 static inline int            Cba_NtkHostObj( Cba_Ntk_t * p )                 { return p->iBoxObj;                                                                          }
 static inline void           Cba_NtkSetHost( Cba_Ntk_t * p, int n, int i )   { assert(p->iBoxNtk == -1); p->iBoxNtk = n; p->iBoxObj = i;                                   }
 
+static inline int            Cba_InfoRange( int Beg, int End )               { return End > Beg ? End - Beg + 1 : Beg - End + 1;                                           }
+static inline int            Cba_NtkInfoNum( Cba_Ntk_t * p )                 { return Vec_IntSize(&p->vInfo)/3;                                                            }
+static inline int            Cba_NtkInfoNumAlloc( Cba_Ntk_t * p )            { return Vec_IntCap(&p->vInfo)/3;                                                             }
+static inline int            Cba_NtkInfoType( Cba_Ntk_t * p, int i )         { return Abc_Lit2Att2(Vec_IntEntry(&p->vInfo, 3*i));                                          }
+static inline int            Cba_NtkInfoName( Cba_Ntk_t * p, int i )         { return Abc_Lit2Var2(Vec_IntEntry(&p->vInfo, 3*i));                                          }
+static inline int            Cba_NtkInfoBeg( Cba_Ntk_t * p, int i )          { return Vec_IntEntry(&p->vInfo, 3*i+1);                                                      }
+static inline int            Cba_NtkInfoEnd( Cba_Ntk_t * p, int i )          { return Vec_IntEntry(&p->vInfo, 3*i+2);                                                      }
+static inline int            Cba_NtkInfoRange( Cba_Ntk_t * p, int i )        { int* a = Vec_IntEntryP(&p->vInfo, 3*i); return a[1]>=0 ? Cba_InfoRange( a[1], a[2] ) : 1;   }
+static inline int            Cba_NtkInfoIndex( Cba_Ntk_t * p, int i, int j ) { int* a = Vec_IntEntryP(&p->vInfo, 3*i); assert(a[1]>=0); return a[1]<a[2] ? a[1]+j : a[1]-j;}
+static inline void           Cba_NtkAddInfo( Cba_Ntk_t * p,int i,int b,int e){ Vec_IntPush(&p->vInfo, i); Vec_IntPushTwo(&p->vInfo, b, e);                                 }
+static inline void           Cba_NtkSetInfoName( Cba_Ntk_t * p, int i, int n){ Vec_IntWriteEntry( &p->vInfo, 3*i, n );                                                     }
+
 static inline void           Cba_NtkStartNames( Cba_Ntk_t * p )              { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vName,  Cba_NtkObjNumAlloc(p),  0);          }
-static inline void           Cba_NtkStartRanges( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vRange, Cba_NtkObjNumAlloc(p),  0);          }
 static inline void           Cba_NtkStartCopies( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vCopy,  Cba_NtkObjNumAlloc(p), -1);          }
 static inline void           Cba_NtkFreeNames( Cba_Ntk_t * p )               { Vec_IntErase(&p->vName);                                                                    }
-static inline void           Cba_NtkFreeRanges( Cba_Ntk_t * p )              { Vec_IntErase(&p->vRange);                                                                   }
 static inline void           Cba_NtkFreeCopies( Cba_Ntk_t * p )              { Vec_IntErase(&p->vCopy);                                                                    }
 static inline int            Cba_NtkHasNames( Cba_Ntk_t * p )                { return p->vName.pArray != NULL;                                                             }
-static inline int            Cba_NtkHasRanges( Cba_Ntk_t * p )               { return p->vRange.pArray != NULL;                                                            }
 static inline int            Cba_NtkHasCopies( Cba_Ntk_t * p )               { return p->vCopy.pArray != NULL;                                                             }
 
 static inline int            Cba_TypeIsBox( Cba_ObjType_t Type )             { return Type >= CBA_OBJ_BOX && Type < CBA_BOX_UNKNOWN;                                       }
+static inline Cba_NameType_t Cba_NameType( int n )                           { assert( n ); return (Cba_NameType_t)Abc_Lit2Att2( n );                                      }
 
 static inline Cba_ObjType_t  Cba_ObjType( Cba_Ntk_t * p, int i )             { return (Cba_ObjType_t)Vec_StrEntry(&p->vType, i);                                           }
 static inline int            Cba_ObjIsPi( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_PI;                                                     }
@@ -243,14 +263,13 @@ static inline int            Cba_ObjIndex( Cba_Ntk_t * p, int i )            { a
 static inline int            Cba_ObjFaninTwo( Cba_Ntk_t * p, int i )         { return Cba_ObjFanin(p, Cba_ObjFanin(p, i));                                                 }
 static inline int            Cba_ObjNameInt( Cba_Ntk_t * p, int i )          { assert(!Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vName, i);                              }
 static inline int            Cba_ObjName( Cba_Ntk_t * p, int i )             { return Cba_ObjIsCo(p, i) ? Cba_ObjNameInt(p, Cba_ObjFanin(p,i)) : Cba_ObjNameInt(p, i);     }
-static inline int            Cba_ObjRange( Cba_Ntk_t * p, int i )            { return Vec_IntEntry(&p->vRange, i);                                                         }
+static inline Cba_NameType_t Cba_ObjNameType( Cba_Ntk_t * p, int i )         { assert(!Cba_ObjIsCo(p, i)); return Cba_NameType( Cba_ObjName(p, i) );                       }
+static inline int            Cba_ObjNameId( Cba_Ntk_t * p, int i )           { assert(!Cba_ObjIsCo(p, i)); return Abc_Lit2Var2( Cba_ObjName(p, i) );                       }
+static inline char *         Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { assert(Cba_ObjNameType(p, i) <= CBA_NAME_WORD); return Cba_NtkStr(p, Cba_ObjNameId(p, i));  }
 static inline int            Cba_ObjCopy( Cba_Ntk_t * p, int i )             { return Vec_IntEntry(&p->vCopy, i);                                                          }
-static inline char *         Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { return Cba_NtkStr(p, Cba_ObjName(p, i));                                                    }
-static inline char *         Cba_ObjRangeStr( Cba_Ntk_t * p, int i )         { return Cba_NtkStr(p, Cba_ObjRange(p, i));                                                   }
 static inline void           Cba_ObjSetFanin( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjFanin(p, i) == -1 && Cba_ObjIsCo(p, i)); Vec_IntWriteEntry( &p->vFanin, i, x);}
 static inline void           Cba_ObjSetIndex( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIndex(p, i) == -1); Vec_IntWriteEntry( &p->vIndex, i, x );                    }
 static inline void           Cba_ObjSetName( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjName(p, i) == 0 && !Cba_ObjIsCo(p, i)); Vec_IntWriteEntry( &p->vName, i, x ); }
-static inline void           Cba_ObjSetRange( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjRange(p, i) == 0);  Vec_IntWriteEntry( &p->vRange, i, x );                    }
 static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1);  Vec_IntWriteEntry( &p->vCopy,  i, x );                    }
 
 static inline int            Cba_BoxBiNum( Cba_Ntk_t * p, int i )            { int s = i-1; assert(Cba_ObjIsBox(p, i)); while (--i >= 0               && Cba_ObjIsBi(p, i)); return s - i;  }
@@ -312,6 +331,80 @@ static inline int Cba_NtkNameRanges( char * pName, int * pRanges, char * pSymbs
     pSymbs[nSigs] = Symb, pRanges[nSigs++] = Num;
     return nSigs;
 }
+static inline void Cba_NtkReadRangesPrim( char * pName, Vec_Int_t * vRanges, int fPo )
+{
+    char * pTemp; int Last, Num = 0;
+    assert( !strncmp(pName, "ABC", 3) );
+    for ( pTemp = pName; *pTemp && !Cba_CharIsDigit(*pTemp); pTemp++ );
+    assert( Cba_CharIsDigit(*pTemp) );
+    Vec_IntClear( vRanges );
+    for ( ; *pTemp; pTemp++ )
+    {
+        if ( Cba_CharIsDigit(*pTemp) )
+            Num = 10 * Num + *pTemp - '0';
+        else
+            Vec_IntPush( vRanges, Num ), Num = 0;
+    }
+    assert( Num > 0 );
+    Vec_IntPush( vRanges, Num );
+    Last = Vec_IntPop(vRanges);
+    if ( !fPo )
+        return;
+    if ( !strncmp(pName, "ABCADD", 6) )
+        Vec_IntFillTwo( vRanges, 2, Last - 1, 1 );
+    else
+        Vec_IntFill( vRanges, 1, Last );
+}
+static inline int Cba_NtkReadRangesUser( Cba_Ntk_t * p, Vec_Int_t * vRanges, int fPo )
+{
+    int Count = 0;
+    assert( fPo == 0 || fPo == 1 );
+    if ( Cba_NtkInfoNum(p) == 0 )
+    {
+        if ( vRanges )
+            Vec_IntFill( vRanges, fPo ? Cba_NtkPoNum(p) : Cba_NtkPiNum(p), 1 );
+        Count = fPo ? Cba_NtkPoNum(p) : Cba_NtkPiNum(p);
+    }
+    else
+    {
+        int Value, Beg, End, k;
+        if ( vRanges )
+            Vec_IntClear( vRanges );
+        Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
+            if ( Abc_Lit2Att2(Value) == (fPo ? 2 : 1) )
+            {
+                if ( vRanges )
+                    Vec_IntPush( vRanges, Cba_InfoRange(Beg, End) );
+                Count += Cba_InfoRange(Beg, End);
+            }
+    }
+    return Count;
+}
+static inline int Cba_ObjGetRange( Cba_Ntk_t * p, int iObj, int * pBeg, int * pEnd )
+{
+    int i, Beg, End, iNameId = Cba_ObjName(p, iObj);
+    if ( pBeg ) *pBeg = -1;
+    if ( pEnd ) *pEnd = -1;
+    if ( Cba_NameType(iNameId) == CBA_NAME_BIN )
+        return 1;
+    if ( Cba_NameType(iNameId) == CBA_NAME_WORD )
+    {
+        if ( pBeg ) *pBeg = 0;
+        for ( i = 0; iObj + i + 1 < Cba_NtkObjNum(p); i++ )
+            if ( !Cba_ObjIsCi(p, iObj + i + 1) || Cba_ObjNameType(p, iObj + i + 1) != CBA_NAME_INDEX )
+                break;
+        if ( pEnd ) *pEnd = i;
+        return i + 1;
+    }
+    assert( Cba_NameType(iNameId) == CBA_NAME_INFO );
+    Beg = Cba_NtkInfoBeg( p, Abc_Lit2Var2(iNameId) );
+    End = Cba_NtkInfoEnd( p, Abc_Lit2Var2(iNameId) );
+    assert( Beg >= 0 );
+    if ( pBeg ) *pBeg = Beg;
+    if ( pEnd ) *pEnd = End;
+    return Cba_InfoRange( Beg, End );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -331,10 +424,10 @@ static inline int Cba_NtkNameRanges( char * pName, int * pRanges, char * pSymbs
 #define Cba_NtkForEachPoDriver( p, iObj, i )                                    \
     for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_ObjFanin(p, Cba_NtkPo(p, i))), 1); i++ ) 
 
-#define Cba_NtkForEachObj( p, i )                                         \
+#define Cba_NtkForEachObj( p, i )  if ( !Cba_ObjType(p, i) ) {} else      \
     for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) 
 #define Cba_NtkForEachObjType( p, Type, i )                               \
-    for ( i = 0; (i < Cba_NtkObjNum(p))  && (((Type) = Cba_ObjType(p, i)), 1); i++ ) 
+    for ( i = 0; (i < Cba_NtkObjNum(p))  && (((Type) = Cba_ObjType(p, i)), 1); i++ ) if ( !Type ) {} else
 
 #define Cba_NtkForEachBox( p, i )                                         \
     for ( i = 0; (i < Cba_NtkObjNum(p)); i++ ) if ( !Cba_ObjIsBox(p, i) ) {} else
@@ -399,8 +492,6 @@ static inline int Cba_ObjDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p, int i )
     int iObj = Cba_ObjAlloc( pNew, Cba_ObjType(p, i), Cba_ObjIsBox(p, i) ? Cba_BoxNtkId(p, i) : -1 );
     if ( Cba_NtkHasNames(p) && Cba_NtkHasNames(pNew) && !Cba_ObjIsCo(p, i) ) 
         Cba_ObjSetName( pNew, iObj, Cba_ObjName(p, i) );
-    if ( Cba_NtkHasRanges(p) && Cba_NtkHasRanges(pNew) ) 
-        Cba_ObjSetRange( pNew, iObj, Cba_ObjRange(p, i) );
     Cba_ObjSetCopy( p, i, iObj );
     return iObj;
 }
@@ -420,6 +511,8 @@ static inline int Cba_BoxDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p, int iBox )
     Cba_BoxForEachBiReverse( p, iBox, iTerm, i )
         Cba_ObjDup( pNew, p, iTerm );
     iBoxNew = Cba_ObjDup( pNew, p, iBox );
+    if ( Cba_NtkHasNames(p) && Cba_NtkHasNames(pNew) && Cba_ObjName(p, iBox) ) 
+        Cba_ObjSetName( pNew, iBoxNew, Cba_ObjName(p, iBox) );
     if ( Cba_BoxNtk(p, iBox) )
         Cba_BoxSetNtkId( pNew, iBoxNew, Cba_NtkCopy(Cba_BoxNtk(p, iBox)) );
     Cba_BoxForEachBo( p, iBox, iTerm, i )
@@ -430,6 +523,28 @@ static inline int Cba_BoxDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p, int iBox )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrPrint( Vec_Str_t * p, int fInt )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( fInt )
+            printf( "%d ", (int)p->pArray[i] );
+        else
+            printf( "%c ", p->pArray[i] );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Network APIs.]
 
   Description []
@@ -465,6 +580,8 @@ static inline void Cba_NtkDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
     int i, iObj;
     assert( pNew != p );
     Cba_NtkAlloc( pNew, Cba_NtkNameId(p), Cba_NtkPiNum(p), Cba_NtkPoNum(p), Cba_NtkObjNum(p) );
+    if ( Vec_IntSize(&p->vInfo) )
+        Vec_IntAppend( &pNew->vInfo, &p->vInfo );
     Cba_NtkStartCopies( p );
     if ( Cba_NtkHasNames(p) )
         Cba_NtkStartNames( pNew );
@@ -484,6 +601,8 @@ static inline void Cba_NtkDupUserBoxes( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
     int i, iObj;
     assert( pNew != p );
     Cba_NtkAlloc( pNew, Cba_NtkNameId(p), Cba_NtkPiNum(p), Cba_NtkPoNum(p), Cba_NtkObjNum(p) + 3*Cba_NtkCoNum(p) );
+    if ( Vec_IntSize(&p->vInfo) )
+        Vec_IntAppend( &pNew->vInfo, &p->vInfo );
     Cba_NtkStartCopies( p );
     Cba_NtkForEachPi( p, iObj, i )
         Cba_ObjDup( pNew, p, iObj );
@@ -505,8 +624,11 @@ static inline void Cba_NtkMoveNames( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
     Cba_NtkForEachPi( p, iObj, i )
         Cba_ObjSetName( pNew, Cba_ObjCopy(p, iObj), Cba_ObjName(p, iObj) );
     Cba_NtkForEachBoxUser( p, iBox )
+    {
+        Cba_ObjSetName( pNew, Cba_ObjCopy(p, iBox), Cba_ObjName(p, iBox) );
         Cba_BoxForEachBo( p, iBox, iObj, i )
             Cba_ObjSetName( pNew, Cba_ObjCopy(p, iObj), Cba_ObjName(p, iObj) );
+    }
     Cba_NtkForEachBoxUser( p, iBox )
         Cba_BoxForEachBi( p, iBox, iObj, i )
             if ( !Cba_ObjName(pNew, Cba_ObjFanin(pNew, Cba_ObjCopy(p, iObj))) )
@@ -520,11 +642,11 @@ static inline void Cba_NtkFree( Cba_Ntk_t * p )
 {
     Vec_IntErase( &p->vInputs );
     Vec_IntErase( &p->vOutputs );
+    Vec_IntErase( &p->vInfo );
     Vec_StrErase( &p->vType );
     Vec_IntErase( &p->vFanin );    
     Vec_IntErase( &p->vIndex );
     Vec_IntErase( &p->vName );    
-    Vec_IntErase( &p->vRange );    
     Vec_IntErase( &p->vCopy );    
     Vec_IntErase( &p->vArray );    
 }
@@ -533,11 +655,11 @@ static inline int Cba_NtkMemory( Cba_Ntk_t * p )
     int nMem = sizeof(Cba_Ntk_t);
     nMem += Vec_IntMemory(&p->vInputs);
     nMem += Vec_IntMemory(&p->vOutputs);
+    nMem += Vec_IntMemory(&p->vInfo);
     nMem += Vec_StrMemory(&p->vType);
     nMem += Vec_IntMemory(&p->vFanin);
     nMem += Vec_IntMemory(&p->vIndex);
     nMem += Vec_IntMemory(&p->vName);
-    nMem += Vec_IntMemory(&p->vRange);
     nMem += Vec_IntMemory(&p->vCopy);
     return nMem;
 }
@@ -569,6 +691,39 @@ static inline void Cba_NtkDeriveIndex( Cba_Ntk_t * p )
             Cba_ObjSetIndex( p, iTerm, i );
     }
 }
+static inline void Cba_NtkPrint( Cba_Ntk_t * p )
+{
+    int i, Type, Value, Beg, End;
+    printf( "Interface (%d):\n", Cba_NtkInfoNum(p) );
+    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, i )
+    {
+        printf( "%6d : ", i );
+        printf( "Type =%3d  ", Cba_NtkInfoType(p, i/3) );
+        if ( Beg >= 0 )
+            printf( "[%d:%d]   ", End, Beg );
+        else
+            printf( "        " );
+        printf( "Name =%3d   ", Cba_NtkInfoName(p, i/3) );
+        if ( Cba_NtkInfoName(p, i/3) )
+            printf( "%s", Cba_NtkStr( p, Cba_NtkInfoName(p, i/3) ) );
+        printf( "\n" );
+    }
+    printf( "Objects (%d):\n", Cba_NtkObjNum(p) );
+    Cba_NtkForEachObjType( p, Type, i )
+    {
+        printf( "%6d : ", i );
+        printf( "Type =%3d  ", Type );
+        if ( Cba_ObjIsCo(p, i) )
+            printf( "Fanin =%6d  ", Cba_ObjFanin(p, i) );
+        else if ( Cba_NtkHasNames(p) && Cba_ObjName(p, i) )
+        {
+            printf( "Name  =%6d(%d)  ", Cba_ObjNameId(p, i), Cba_ObjNameType(p, i) );
+            if ( Cba_ObjNameType(p, i) <= CBA_NAME_WORD )
+                printf( "%s", Cba_ObjNameStr(p, i) );
+        }
+        printf( "\n" );
+    }
+}
 
 
 /**Function*************************************************************
@@ -831,6 +986,7 @@ extern Cba_Man_t * Cba_ManReadCba( char * pFileName );
 extern void        Cba_ManWriteCba( char * pFileName, Cba_Man_t * p );
 /*=== cbaNtk.c ===============================================================*/
 extern void        Cba_ManAssignInternNames( Cba_Man_t * p );
+extern void        Cba_ManAssignInternWordNames( Cba_Man_t * p );
 extern Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p );
 /*=== cbaPtr.c ===============================================================*/
 extern void        Cba_PtrFree( Vec_Ptr_t * vDes );
diff --git a/src/base/cba/cbaCba.c b/src/base/cba/cbaCba.c
index 83912edf..f7e7d2ba 100644
--- a/src/base/cba/cbaCba.c
+++ b/src/base/cba/cbaCba.c
@@ -50,9 +50,9 @@ int CbaManReadCbaLine( Vec_Str_t * vOut, int * pPos, char * pBuffer, char * pLim
     *pBuffer = 0;
     return pBuffer < pLimit;
 }
-int CbaManReadCbaNameAndNums( char * pBuffer, int * Num1, int * Num2, int * Num3 )
+int CbaManReadCbaNameAndNums( char * pBuffer, int * Num1, int * Num2, int * Num3, int * Num4 )
 {
-    *Num1 = *Num2 = *Num3 = -1;
+    *Num1 = *Num2 = *Num3 = *Num4 = -1;
     // read name
     while ( *pBuffer && *pBuffer != ' ' )
         pBuffer++;
@@ -76,6 +76,13 @@ int CbaManReadCbaNameAndNums( char * pBuffer, int * Num1, int * Num2, int * Num3
     // read Num3
     assert( *pBuffer == ' ' );
     *Num3 = atoi(++pBuffer);
+    while ( *pBuffer && *pBuffer != ' ' )
+        pBuffer++;
+    if ( !*pBuffer )
+        return 1;
+    // read Num4
+    assert( *pBuffer == ' ' );
+    *Num4 = atoi(++pBuffer);
     return 1;
 }
 void Cba_ManReadCbaVecStr( Vec_Str_t * vOut, int * pPos, Vec_Str_t * p, int nSize )
@@ -97,6 +104,7 @@ void Cba_ManReadCbaNtk( Vec_Str_t * vOut, int * pPos, Cba_Ntk_t * pNtk )
     int i, Type;
     Cba_ManReadCbaVecStr( vOut, pPos, &pNtk->vType,      Cba_NtkObjNumAlloc(pNtk) );
     Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vFanin, 4 * Cba_NtkObjNumAlloc(pNtk) );
+    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vInfo, 12 * Cba_NtkInfoNumAlloc(pNtk) );
     Cba_NtkForEachObjType( pNtk, Type, i )
     {
         if ( Type == CBA_OBJ_PI )
@@ -107,17 +115,18 @@ void Cba_ManReadCbaNtk( Vec_Str_t * vOut, int * pPos, Cba_Ntk_t * pNtk )
     assert( Cba_NtkPiNum(pNtk)  == Cba_NtkPiNumAlloc(pNtk) );
     assert( Cba_NtkPoNum(pNtk)  == Cba_NtkPoNumAlloc(pNtk) );
     assert( Cba_NtkObjNum(pNtk) == Cba_NtkObjNumAlloc(pNtk) );
+    assert( Cba_NtkInfoNum(pNtk) == Cba_NtkInfoNumAlloc(pNtk) );
 }
 Cba_Man_t * Cba_ManReadCbaInt( Vec_Str_t * vOut )
 {
     Cba_Man_t * p;
     Cba_Ntk_t * pNtk;
     char Buffer[1000] = "#"; 
-    int i, NameId, Pos = 0, nNtks, nPrims, Num1, Num2, Num3;
+    int i, NameId, Pos = 0, nNtks, nPrims, Num1, Num2, Num3, Num4;
     while ( Buffer[0] == '#' )
         if ( !CbaManReadCbaLine(vOut, &Pos, Buffer, Buffer+1000) )
             return NULL;
-    if ( !CbaManReadCbaNameAndNums(Buffer, &nNtks, &nPrims, &Num3) )
+    if ( !CbaManReadCbaNameAndNums(Buffer, &nNtks, &nPrims, &Num3, &Num4) )
         return NULL;
     // start manager
     assert( nNtks > 0 && nPrims > 0 );
@@ -130,7 +139,7 @@ Cba_Man_t * Cba_ManReadCbaInt( Vec_Str_t * vOut )
             Cba_ManFree( p );
             return NULL;
         }
-        if ( !CbaManReadCbaNameAndNums(Buffer, &Num1, &Num2, &Num3) )
+        if ( !CbaManReadCbaNameAndNums(Buffer, &Num1, &Num2, &Num3, &Num4) )
         {
             Cba_ManFree( p );
             return NULL;
@@ -138,6 +147,7 @@ Cba_Man_t * Cba_ManReadCbaInt( Vec_Str_t * vOut )
         assert( Num1 > 0 && Num2 > 0 && Num3 > 0 );
         NameId = Abc_NamStrFindOrAdd( p->pStrs, Buffer, NULL );
         Cba_NtkAlloc( pNtk, NameId, Num1, Num2, Num3 );
+        Vec_IntFill( &pNtk->vInfo, 3 * Num4, -1 );
     }
     // read networks
     Cba_ManForEachNtk( p, pNtk, i )
@@ -201,8 +211,9 @@ Cba_Man_t * Cba_ManReadCba( char * pFileName )
 ***********************************************************************/
 void Cba_ManWriteCbaNtk( Vec_Str_t * vOut, Cba_Ntk_t * pNtk )
 {
-    Vec_StrPushBuffer( vOut, (char *)Vec_StrArray(&pNtk->vType),      Cba_NtkObjNum(pNtk) );
-    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vFanin), 4 * Cba_NtkObjNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_StrArray(&pNtk->vType),       Cba_NtkObjNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vFanin),  4 * Cba_NtkObjNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vInfo),  12 * Cba_NtkInfoNum(pNtk) );
 }
 void Cba_ManWriteCbaInt( Vec_Str_t * vOut, Cba_Man_t * p )
 {
@@ -215,7 +226,8 @@ void Cba_ManWriteCbaInt( Vec_Str_t * vOut, Cba_Man_t * p )
     Vec_StrPrintStr( vOut, Buffer );
     Cba_ManForEachNtk( p, pNtk, i )
     {
-        sprintf( Buffer, "%s %d %d %d \n", Cba_NtkName(pNtk), Cba_NtkPiNum(pNtk), Cba_NtkPoNum(pNtk), Cba_NtkObjNum(pNtk) );
+        sprintf( Buffer, "%s %d %d %d %d \n", Cba_NtkName(pNtk), 
+            Cba_NtkPiNum(pNtk), Cba_NtkPoNum(pNtk), Cba_NtkObjNum(pNtk), Cba_NtkInfoNum(pNtk) );
         Vec_StrPrintStr( vOut, Buffer );
     }
     Cba_ManForEachNtk( p, pNtk, i )
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 2c9d8492..f24ff589 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -32,7 +32,116 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Assigns word-level names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_ManAssignInternTwo( Cba_Ntk_t * p, int iNum, Vec_Int_t * vMap )
+{
+    char Buffer[16];
+    int i = 0, NameId, nDigits;
+    do
+    {
+        nDigits = Abc_Base10Log( Cba_NtkObjNum(p) );
+        if ( i == 0 )
+            sprintf( Buffer, "%s%0*d", "n", nDigits, iNum );
+        else
+            sprintf( Buffer, "%s%0*d_%d", "n", nDigits, iNum, ++i );
+        NameId = Abc_NamStrFindOrAdd( p->pDesign->pStrs, Buffer, NULL );
+    }
+    while ( Vec_IntEntry(vMap, NameId) );
+    Vec_IntWriteEntry( vMap, NameId, iNum );
+    return NameId;
+}
+void Cba_ManPrepareBitNames( Cba_Ntk_t * p, Vec_Int_t * vMap, int * pnNames, Vec_Int_t * vRanges, Vec_Int_t * vNames )
+{
+    int n = 0, i, k, Range;
+    Vec_IntClear( vNames );
+    Vec_IntForEachEntry( vRanges, Range, i )
+    {
+        assert( Range > 0 );
+        if ( Range == 1 )
+            Vec_IntPush( vNames, Abc_Var2Lit2( Cba_ManAssignInternTwo(p, (*pnNames)++, vMap), CBA_NAME_BIN ) );
+        else
+        {
+            Vec_IntPush( vNames, Abc_Var2Lit2( Cba_ManAssignInternTwo(p, (*pnNames)++, vMap), CBA_NAME_WORD ) );
+            for ( k = 1; k < Range; k++ )
+                Vec_IntPush( vNames, Abc_Var2Lit2( k, CBA_NAME_INDEX ) );
+        }
+    }
+}
+void Cba_ManAssignInternWordNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t * vRanges, Vec_Int_t * vNames )
+{
+    int k, n = 0, iObj, iTerm, nNames = 1;
+    assert( Cba_NtkReadRangesUser(p, NULL, 0) == Cba_NtkPiNum(p) );
+    assert( Cba_NtkReadRangesUser(p, NULL, 1) == Cba_NtkPoNum(p) );
+    // start names
+    assert( !Cba_NtkHasNames(p) );
+    Cba_NtkStartNames(p);
+    // derive PI names
+    Cba_NtkReadRangesUser( p, vRanges, 0 );
+    Cba_ManPrepareBitNames( p, vMap, &nNames, vRanges, vNames );
+    assert( Vec_IntSize(vNames) == Cba_NtkPiNum(p) );
+    Cba_NtkForEachPi( p, iObj, k )
+    {
+        Cba_ObjSetName( p, iObj, Vec_IntEntry(vNames, k) );
+        if ( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD ) // works only if the PIs are before POs
+            Cba_NtkSetInfoName( p, n++, Abc_Var2Lit2(Cba_ObjNameId(p, iObj), 1) );
+    }
+    assert( n == Vec_IntSize(vRanges) );
+    // derive box output names
+    Cba_NtkForEachBox( p, iObj )
+    {
+        if ( Cba_ObjIsBoxUser(p, iObj) )
+            Cba_NtkReadRangesUser( Cba_BoxNtk(p, iObj), vRanges, 1 );
+        else if ( Cba_BoxNtkId(p, iObj) )
+            Cba_NtkReadRangesPrim( Cba_BoxNtkName(p, iObj), vRanges, 1 );
+        else assert( 0 );
+        Cba_ManPrepareBitNames( p, vMap, &nNames, vRanges, vNames );
+        assert( Vec_IntSize(vNames) == Cba_BoxBoNum(p, iObj) );
+        Cba_BoxForEachBo( p, iObj, iTerm, k )
+            Cba_ObjSetName( p, iTerm, Vec_IntEntry(vNames, k) );
+    }
+    // mark PO names
+    Cba_NtkReadRangesUser( p, vRanges, 1 );
+    Cba_NtkForEachPo( p, iObj, k )
+        if ( Cba_ObjNameType(p, Cba_ObjFanin(p, iObj)) <= CBA_NAME_WORD ) // works only if the PIs are before POs
+            Cba_NtkSetInfoName( p, n++, Abc_Var2Lit2(Cba_ObjNameId(p, Cba_ObjFanin(p, iObj)), 2) );
+    assert( n == Cba_NtkInfoNum(p) );
+    // unmark all names
+    Cba_NtkForEachPi( p, iObj, k )
+        if ( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD )
+            Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
+    Cba_NtkForEachBox( p, iObj )
+        Cba_BoxForEachBo( p, iObj, iTerm, k )
+            if ( Cba_ObjNameType(p, iTerm) <= CBA_NAME_WORD )
+                Vec_IntWriteEntry( vMap, Cba_ObjName(p, iTerm), 0 );
+    printf( "Generated %d word-level names.\n", nNames-1 );
+//    Vec_IntPrint( &p->vName );
+//    Vec_IntPrint( &p->vInfo );
+}
+void Cba_ManAssignInternWordNames( Cba_Man_t * p )
+{
+    Vec_Int_t * vMap = Vec_IntStart( Cba_ManObjNum(p) );
+    Vec_Int_t * vRanges = Vec_IntAlloc( 1000 );
+    Vec_Int_t * vNames = Vec_IntAlloc( 1000 );
+    Cba_Ntk_t * pNtk; int i;
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_ManAssignInternWordNamesNtk( pNtk, vMap, vRanges, vNames );
+    Vec_IntFree( vMap );
+    Vec_IntFree( vRanges );
+    Vec_IntFree( vNames );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns bit-level names.]
 
   Description []
                
@@ -45,8 +154,10 @@ int Cba_ManSetInternOne( Cba_Ntk_t * p, int iTerm, Vec_Int_t * vMap )
 {
     if ( !Cba_ObjName(p, iTerm) )
         return 1;
-    assert( Vec_IntEntry(vMap, Cba_ObjName(p, iTerm)) == 0 );
-    Vec_IntWriteEntry( vMap, Cba_ObjName(p, iTerm), iTerm+1 );
+    if ( Cba_ObjNameType(p, iTerm) > CBA_NAME_WORD )
+        return 0;
+    assert( Vec_IntEntry(vMap, Cba_ObjNameId(p, iTerm)) == 0 );
+    Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iTerm), iTerm+1 );
     return 0;
 }
 int Cba_ManAssignInternOne( Cba_Ntk_t * p, int iTerm, Vec_Int_t * vMap )
@@ -59,19 +170,20 @@ int Cba_ManAssignInternOne( Cba_Ntk_t * p, int iTerm, Vec_Int_t * vMap )
     {
         nDigits = Abc_Base10Log( Cba_NtkObjNum(p) );
         if ( i == 0 )
-            sprintf( Buffer, "%s%0*d", "_n_", nDigits, iTerm );
+            sprintf( Buffer, "%s%0*d", "n", nDigits, iTerm );
         else
-            sprintf( Buffer, "%s%0*d_%d", "_n_", nDigits, iTerm, ++i );
+            sprintf( Buffer, "%s%0*d_%d", "n", nDigits, iTerm, ++i );
         NameId = Abc_NamStrFindOrAdd( p->pDesign->pStrs, Buffer, NULL );
     }
     while ( Vec_IntEntry(vMap, NameId) );
-    Cba_ObjSetName( p, iTerm, NameId );
+    Cba_ObjSetName( p, iTerm, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
     Vec_IntWriteEntry( vMap, NameId, iTerm+1 );
     return 1;
 }
 void Cba_ManAssignInternNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap )
 {
     int i, iObj, iTerm, nNameless = 0;
+//    Vec_IntPrint( &p->vName );
     if ( !Cba_NtkHasNames(p) )
         Cba_NtkStartNames(p);
     // set all names
@@ -95,10 +207,12 @@ void Cba_ManAssignInternNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap )
     }
     // unmark all names
     Cba_NtkForEachPi( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
+        if ( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD )
+            Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 );
     Cba_NtkForEachBox( p, iObj )
         Cba_BoxForEachBo( p, iObj, iTerm, i )
-            Vec_IntWriteEntry( vMap, Cba_ObjName(p, iTerm), 0 );
+            if ( Cba_ObjNameType(p, iTerm) <= CBA_NAME_WORD )
+                Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iTerm), 0 );
 }
 void Cba_ManAssignInternNames( Cba_Man_t * p )
 {
diff --git a/src/base/cba/cbaPrsBuild.c b/src/base/cba/cbaPrsBuild.c
index ab014518..e3e51c1c 100644
--- a/src/base/cba/cbaPrsBuild.c
+++ b/src/base/cba/cbaPrsBuild.c
@@ -186,7 +186,7 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
         if ( Vec_IntEntry(vMap, NameId) != -1 )
             printf( "Primary inputs %d and %d have the same name.\n", Vec_IntEntry(vMap, NameId), i );
         iObj = Cba_ObjAlloc( pNew, CBA_OBJ_PI, -1 );
-        Cba_ObjSetName( pNew, iObj, NameId );
+        Cba_ObjSetName( pNew, iObj, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
         Vec_IntWriteEntry( vMap, NameId, iObj );
     }
     // create box outputs
@@ -198,20 +198,20 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
             if ( pNtkBox == NULL )
             {
                 iObj = Cba_BoxAlloc( pNew, CBA_BOX_GATE, Vec_IntSize(vSigs)/2-1, 1, Prs_BoxNtk(pNtk, iBox) + 1 ); // +1 to map NtkId into gate name
-                Cba_ObjSetName( pNew, iObj, Prs_BoxName(pNtk, iBox) );
+                Cba_ObjSetName( pNew, iObj, Abc_Var2Lit2(Prs_BoxName(pNtk, iBox), CBA_NAME_BIN) );
                 // consider box output 
                 NameId = Vec_IntEntryLast( vSigs );
                 NameId = Prs_NtkSigName( pNtk, NameId );
                 if ( Vec_IntEntry(vMap, NameId) != -1 )
                     printf( "Box output name %d is already driven.\n", NameId );
                 iTerm = Cba_BoxBo( pNew, iObj, 0 );
-                Cba_ObjSetName( pNew, iTerm, NameId );
+                Cba_ObjSetName( pNew, iTerm, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
                 Vec_IntWriteEntry( vMap, NameId, iTerm );
             }
             else
             {
                 iObj = Cba_BoxAlloc( pNew, CBA_OBJ_BOX, Prs_NtkPiNum(pNtkBox), Prs_NtkPoNum(pNtkBox), Prs_BoxNtk(pNtk, iBox) );
-                Cba_ObjSetName( pNew, iObj, Prs_BoxName(pNtk, iBox) );
+                Cba_ObjSetName( pNew, iObj, Abc_Var2Lit2(Prs_BoxName(pNtk, iBox), CBA_NAME_BIN) );
                 Cba_NtkSetHost( Cba_ManNtk(pNew->pDesign, Prs_BoxNtk(pNtk, iBox)), Cba_NtkId(pNew), iObj );
                 Vec_IntForEachEntry( vSigs, Index, i )
                 {
@@ -225,7 +225,7 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
                     if ( Vec_IntEntry(vMap, NameId) != -1 )
                         printf( "Box output name %d is already driven.\n", NameId );
                     iTerm = Cba_BoxBo( pNew, iObj, Index - Prs_NtkPiNum(pNtkBox) );
-                    Cba_ObjSetName( pNew, iTerm, NameId );
+                    Cba_ObjSetName( pNew, iTerm, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
                     Vec_IntWriteEntry( vMap, NameId, iTerm );
                 }
             }
@@ -241,7 +241,7 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
             if ( Vec_IntEntry(vMap, NameId) != -1 )
                 printf( "Node output name %d is already driven.\n", NameId );
             iTerm = Cba_BoxBo( pNew, iObj, 0 );
-            Cba_ObjSetName( pNew, iTerm, NameId );
+            Cba_ObjSetName( pNew, iTerm, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
             Vec_IntWriteEntry( vMap, NameId, iTerm );
             // remember box
             Vec_IntPush( vBoxes, iObj );
@@ -269,7 +269,6 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
                         nNonDriven++;
                     }
                     Cba_ObjSetFanin( pNew, iTerm, Vec_IntEntry(vMap, NameId) );
-                    //Cba_ObjSetName( pNew, iTerm, NameId );
                 }
             }
             else
@@ -291,7 +290,6 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
                         nNonDriven++;
                     }
                     Cba_ObjSetFanin( pNew, iTerm, Vec_IntEntry(vMap, NameId) );
-                    //Cba_ObjSetName( pNew, iTerm, NameId );
                 }
             }
         }
@@ -312,7 +310,6 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
                     nNonDriven++;
                 }
                 Cba_ObjSetFanin( pNew, iTerm, Vec_IntEntry(vMap, NameId) );
-                //Cba_ObjSetName( pNew, iTerm, NameId );
             }
         }
     // add fanins for primary outputs
@@ -326,13 +323,13 @@ void Prs_ManBuildNtk( Cba_Ntk_t * pNew, Vec_Ptr_t * vDes, Prs_Ntk_t * pNtk, Vec_
             nNonDriven++;
         }
     Prs_NtkForEachPo( pNtk, NameId, i )
-    {
         iObj = Cba_ObjAlloc( pNew, CBA_OBJ_PO, Vec_IntEntry(vMap, NameId) );
-        //Cba_ObjSetName( pNew, iObj, NameId );
-    }
     if ( nNonDriven )
         printf( "Module %s has %d non-driven nets (for example, %s).\n", Prs_NtkName(pNtk), nNonDriven, Prs_NtkStr(pNtk, iNonDriven) );
     Prs_ManCleanMap( pNtk, vMap );
+    // setup info
+    Vec_IntForEachEntry( &pNtk->vOrder, NameId, i )
+        Cba_NtkAddInfo( pNew, NameId, -1, -1 );
 }
 
 /**Function*************************************************************
@@ -364,6 +361,7 @@ Cba_Man_t * Prs_ManBuildCba( char * pFileName, Vec_Ptr_t * vDes )
     assert( Vec_IntCountEntry(vMap, -1) == Vec_IntSize(vMap) );
     Vec_IntFree( vMap );
     Vec_IntFree( vTmp );
+//    Vec_StrPrint( &Cba_ManNtk(pNew, 0)->vType, 1 );
     return pNew;
 }
 
diff --git a/src/base/cba/cbaPtrAbc.c b/src/base/cba/cbaPtrAbc.c
index af9c8f7d..60fdcb02 100644
--- a/src/base/cba/cbaPtrAbc.c
+++ b/src/base/cba/cbaPtrAbc.c
@@ -290,8 +290,9 @@ int Cba_NtkDeriveFromPtr( Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Int_t * vMap,
         if ( Vec_IntGetEntryFull(vMap, NameId) != -1 )
             { printf( "PI with name \"%s\" is not unique module \"%s\".\n", pName, pModuleName ); return 0; }
         iObj = Cba_ObjAlloc( pNtk, CBA_OBJ_PI, -1 );
-        Cba_ObjSetName( pNtk, iObj, NameId );
+        Cba_ObjSetName( pNtk, iObj, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
         Vec_IntSetEntryFull( vMap, NameId, iObj );
+        Cba_NtkAddInfo( pNtk, Abc_Var2Lit2(NameId, 1), -1, -1 );
     }
     // map driven NameIds into their ObjIds for BOs
     Vec_IntClear( vBox2Id );
@@ -307,14 +308,14 @@ int Cba_NtkDeriveFromPtr( Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Int_t * vMap,
         iObj = Cba_BoxAlloc( pNtk, Ptr_NameToType(pBoxNtk), nInputs, nOutputs, NtkId );
         if ( NtkId >= 0 )
             Cba_NtkSetHost( Cba_ManNtk(pNtk->pDesign, NtkId), Cba_NtkId(pNtk), iObj );
-        Cba_ObjSetName( pNtk, iObj, Abc_NamStrFindOrAdd(pNtk->pDesign->pStrs, pBoxName, NULL) );
+        Cba_ObjSetName( pNtk, iObj, Abc_Var2Lit2(Abc_NamStrFindOrAdd(pNtk->pDesign->pStrs, pBoxName, NULL), CBA_NAME_BIN) );
         Cba_BoxForEachBo( pNtk, iObj, iTerm, k )
         {
             pName = (char *)Vec_PtrEntry( vBox, Vec_PtrSize(vBox) - 2*(nOutputs - k) + 1 );
             NameId = Abc_NamStrFindOrAdd( pNtk->pDesign->pStrs, pName, NULL );
             if ( Vec_IntGetEntryFull(vMap, NameId) != -1 )
                 { printf( "Signal \"%s\" has multiple drivers in module \"%s\".\n", pName, pModuleName ); return 0; }
-            Cba_ObjSetName( pNtk, iTerm, NameId );
+            Cba_ObjSetName( pNtk, iTerm, Abc_Var2Lit2(NameId, CBA_NAME_BIN) );
             Vec_IntSetEntryFull( vMap, NameId, iTerm );
         }
         Vec_IntPush( vBox2Id, iObj );
@@ -331,7 +332,6 @@ int Cba_NtkDeriveFromPtr( Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Int_t * vMap,
             if ( Vec_IntGetEntryFull(vMap, NameId) == -1 )
                 printf( "Signal \"%s\" in not driven in module \"%s\".\n", pName, pModuleName );
             Cba_ObjSetFanin( pNtk, iTerm, Vec_IntGetEntryFull(vMap, NameId) );
-            //Cba_ObjSetName( pNtk, iTerm, NameId );
         }
     }
     // connect POs
@@ -341,7 +341,7 @@ int Cba_NtkDeriveFromPtr( Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Int_t * vMap,
         if ( Vec_IntGetEntryFull(vMap, NameId) == -1 )
             printf( "PO with name \"%s\" in not driven in module \"%s\".\n", pName, pModuleName );
         iObj = Cba_ObjAlloc( pNtk, CBA_OBJ_PO, Vec_IntGetEntryFull(vMap, NameId) );
-        //Cba_ObjSetName( pNtk, iObj, NameId );
+        Cba_NtkAddInfo( pNtk, Abc_Var2Lit2(NameId, 2), -1, -1 );
     }
     // update map
     Cba_NtkForEachCi( pNtk, iObj )
diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c
index 0dafc16f..0cadfd7b 100644
--- a/src/base/cba/cbaReadBlif.c
+++ b/src/base/cba/cbaReadBlif.c
@@ -144,12 +144,15 @@ static inline int Prs_ManReadName( Prs_Man_t * p )
         return 0;
     return Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur, NULL );
 }
-static inline int Prs_ManReadList( Prs_Man_t * p )
+static inline int Prs_ManReadList( Prs_Man_t * p, Vec_Int_t * vOrder, int Type )
 {
     int iToken;
     Vec_IntClear( &p->vTemp );
     while ( (iToken = Prs_ManReadName(p)) )
+    {
         Vec_IntPush( &p->vTemp, iToken );
+        Vec_IntPush( vOrder, Abc_Var2Lit2(iToken, Type) );
+    }
     if ( Vec_IntSize(&p->vTemp) == 0 )                return Prs_ManErrorSet(p, "Signal list is empty.", 1);
     return 0;
 }
@@ -201,7 +204,7 @@ static inline int Prs_ManReadCube( Prs_Man_t * p )
     Prs_ManSkipSpaces( p );
     if ( Prs_ManIsChar(p, '\n') )
     {
-        if ( Vec_StrSize(&p->vCover) != 1 )            return Prs_ManErrorSet(p, "Cannot read cube.", 1);
+        if ( Vec_StrSize(&p->vCover) != 1 )           return Prs_ManErrorSet(p, "Cannot read cube.", 1);
         // fix single literal cube by adding space
         Vec_StrPush( &p->vCover, Vec_StrEntry(&p->vCover,0) );
         Vec_StrWriteEntry( &p->vCover, 0, ' ' );
@@ -221,7 +224,8 @@ static inline void Prs_ManSaveCover( Prs_Man_t * p )
     int iToken;
     assert( Vec_StrSize(&p->vCover) > 0 );
     Vec_StrPush( &p->vCover, '\0' );
-    iToken = Abc_NamStrFindOrAdd( p->pStrs, Vec_StrArray(&p->vCover), NULL );
+    //iToken = Abc_NamStrFindOrAdd( p->pStrs, Vec_StrArray(&p->vCover), NULL );
+    iToken = Ptr_SopToType( Vec_StrArray(&p->vCover) );
     Vec_StrClear( &p->vCover );
     // set the cover to the module of this box
     assert( Prs_BoxNtk(p->pNtk, Prs_NtkBoxNum(p->pNtk)-1) == 1 ); // default const 0
@@ -241,19 +245,19 @@ static inline void Prs_ManSaveCover( Prs_Man_t * p )
 ***********************************************************************/
 static inline int Prs_ManReadInouts( Prs_Man_t * p )
 {
-    if ( Prs_ManReadList(p) )    return 1;
+    if ( Prs_ManReadList(p, &p->pNtk->vOrder, 3) )    return 1;
     Vec_IntAppend( &p->pNtk->vInouts, &p->vTemp );
     return 0;
 }
 static inline int Prs_ManReadInputs( Prs_Man_t * p )
 {
-    if ( Prs_ManReadList(p) )    return 1;
+    if ( Prs_ManReadList(p, &p->pNtk->vOrder, 1) )    return 1;
     Vec_IntAppend( &p->pNtk->vInputs, &p->vTemp );
     return 0;
 }
 static inline int Prs_ManReadOutputs( Prs_Man_t * p )
 {
-    if ( Prs_ManReadList(p) )    return 1;
+    if ( Prs_ManReadList(p, &p->pNtk->vOrder, 2) )    return 1;
     Vec_IntAppend( &p->pNtk->vOutputs, &p->vTemp );
     return 0;
 }
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index 97c355b6..312a4471 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -30,11 +30,11 @@ ABC_NAMESPACE_IMPL_START
 // Verilog keywords
 typedef enum { 
     PRS_VER_NONE = 0,  // 0:  unused
-    PRS_VER_MODULE,    // 1:  module
-    PRS_VER_INOUT,     // 2:  inout
-    PRS_VER_INPUT,     // 3:  input
-    PRS_VER_OUTPUT,    // 4:  output
-    PRS_VER_WIRE,      // 5:  wire
+    PRS_VER_INPUT,     // 1:  input
+    PRS_VER_OUTPUT,    // 2:  output
+    PRS_VER_INOUT,     // 3:  inout
+    PRS_VER_WIRE,      // 4:  wire
+    PRS_VER_MODULE,    // 5:  module
     PRS_VER_ASSIGN,    // 6:  assign
     PRS_VER_REG,       // 7:  reg
     PRS_VER_ALWAYS,    // 8:  always
@@ -47,11 +47,11 @@ typedef enum {
 
 const char * s_VerTypes[PRS_VER_UNKNOWN+1] = {
     NULL,              // 0:  unused
-    "module",          // 1:  module
-    "inout",           // 2:  inout
-    "input",           // 3:  input
-    "output",          // 4:  output
-    "wire",            // 5:  wire
+    "input",           // 1:  input
+    "output",          // 2:  output
+    "inout",           // 3:  inout
+    "wire",            // 4:  wire
+    "module",          // 5:  module
     "assign",          // 6:  assign
     "reg",             // 7:  reg
     "always",          // 8:  always
@@ -476,17 +476,19 @@ static inline int Prs_ManReadSignalList2( Prs_Man_t * p, Vec_Int_t * vTemp )
 ***********************************************************************/
 static inline int Prs_ManReadDeclaration( Prs_Man_t * p, int Type )
 {
-    int i, Sig, RangeId = 0;
-    Vec_Int_t * vSigs[4]  = { &p->pNtk->vInouts,  &p->pNtk->vInputs,  &p->pNtk->vOutputs,  &p->pNtk->vWires };
-    Vec_Int_t * vSigsR[4] = { &p->pNtk->vInoutsR, &p->pNtk->vInputsR, &p->pNtk->vOutputsR, &p->pNtk->vWiresR };
-    assert( Type >= PRS_VER_INOUT && Type <= PRS_VER_WIRE );
+    int i, NameId, RangeId = 0;
+    Vec_Int_t * vNames[4]  = { &p->pNtk->vInputs,  &p->pNtk->vOutputs,  &p->pNtk->vInouts,  &p->pNtk->vWires };
+    Vec_Int_t * vNamesR[4] = { &p->pNtk->vInputsR, &p->pNtk->vOutputsR, &p->pNtk->vInoutsR, &p->pNtk->vWiresR };
+    assert( Type >= PRS_VER_INPUT && Type <= PRS_VER_WIRE );
     if ( Prs_ManUtilSkipSpaces(p) )                                   return 0;
     if ( Prs_ManIsChar(p, '[') && !(RangeId = Prs_ManReadRange(p)) )  return 0;
     if ( !Prs_ManReadNameList( p, &p->vTemp, ';' ) )                  return 0;
-    Vec_IntForEachEntry( &p->vTemp, Sig, i )
+    Vec_IntForEachEntry( &p->vTemp, NameId, i )
     {
-        Vec_IntPush( vSigs[Type - PRS_VER_INOUT], Sig );
-        Vec_IntPush( vSigsR[Type - PRS_VER_INOUT], RangeId );
+        Vec_IntPush( vNames[Type - PRS_VER_INPUT], NameId );
+        Vec_IntPush( vNamesR[Type - PRS_VER_INPUT], RangeId );
+        if ( Type < PRS_VER_WIRE )
+            Vec_IntPush( &p->pNtk->vOrder, Abc_Var2Lit2(NameId, Type) );
     }
     return 1;
 }
@@ -592,8 +594,8 @@ static inline int Prs_ManReadInstance( Prs_Man_t * p, int Func )
 static inline int Prs_ManReadArguments( Prs_Man_t * p )
 {
     int iRange = 0, iType = -1;
-    Vec_Int_t * vSigs[3]  = { &p->pNtk->vInouts,  &p->pNtk->vInputs,  &p->pNtk->vOutputs };
-    Vec_Int_t * vSigsR[3] = { &p->pNtk->vInoutsR, &p->pNtk->vInputsR, &p->pNtk->vOutputsR };
+    Vec_Int_t * vSigs[3]  = { &p->pNtk->vInputs,  &p->pNtk->vOutputs,  &p->pNtk->vInouts  };
+    Vec_Int_t * vSigsR[3] = { &p->pNtk->vInputsR, &p->pNtk->vOutputsR, &p->pNtk->vInoutsR };
     assert( Prs_ManIsChar(p, '(') );
     p->pCur++;
     if ( Prs_ManUtilSkipSpaces(p) )             return 0;
@@ -602,7 +604,7 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
         int iName = Prs_ManReadName( p );
         if ( iName == 0 )                       return 0;
         if ( Prs_ManUtilSkipSpaces(p) )         return 0;
-        if ( iName >= PRS_VER_INOUT && iName <= PRS_VER_OUTPUT ) // declaration
+        if ( iName >= PRS_VER_INPUT && iName <= PRS_VER_INOUT ) // declaration
         {
             iType = iName;
             if ( Prs_ManIsChar(p, '[') )
@@ -611,13 +613,15 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
                 if ( iRange == 0 )              return 0;
                 if ( Prs_ManUtilSkipSpaces(p) ) return 0;
             }
+            iName = Prs_ManReadName( p );
+            if ( iName == 0 )                   return 0;
         }
         if ( iType > 0 )
         {
-            Vec_IntPush( vSigs[iType - PRS_VER_INOUT], iName );
-            Vec_IntPush( vSigsR[iType - PRS_VER_INOUT], iRange );
+            Vec_IntPush( vSigs[iType - PRS_VER_INPUT], iName );
+            Vec_IntPush( vSigsR[iType - PRS_VER_INPUT], iRange );
+            Vec_IntPush( &p->pNtk->vOrder, Abc_Var2Lit2(iName, iType) );
         }
-        Vec_IntPush( &p->pNtk->vOrder, iName );
         if ( Prs_ManIsChar(p, ')') )
             break;
         if ( !Prs_ManIsChar(p, ',') )           return Prs_ManErrorSet(p, "Expecting comma in the instance.", 0);
@@ -673,7 +677,7 @@ static inline int Prs_ManReadModule( Prs_Man_t * p )
             Prs_ManFinalizeNtk( p );
             return 1;
         }
-        if ( iToken >= PRS_VER_INOUT && iToken <= PRS_VER_WIRE ) // declaration
+        if ( iToken >= PRS_VER_INPUT && iToken <= PRS_VER_WIRE ) // declaration
             Status = Prs_ManReadDeclaration( p, iToken );
         else if ( iToken == PRS_VER_REG || iToken == PRS_VER_DEFPARAM ) // unsupported keywords
             Status = Prs_ManUtilSkipUntil( p, ';' );
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index c375301d..0480d75d 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -182,7 +182,7 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
 
 /**Function*************************************************************
 
-  Synopsis    [Collect all nodes names used that are not inputs/outputs.]
+  Synopsis    [Writing word-level Verilog.]
 
   Description []
                
@@ -191,234 +191,309 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Cba_NtkCollectWires( Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t * vWires )
+void Cba_ManWriteRange( Cba_Ntk_t * p, int Beg, int End )
 {
-    int i, k, iTerm, iObj, NameId;
-    Vec_IntClear( vWires );
-    Cba_NtkForEachPi( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 1 );
-    Cba_NtkForEachPo( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 1 );
-    Cba_NtkForEachBox( p, iObj )
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    Vec_StrPrintStr( vStr, "[" );
+    Vec_StrPrintNum( vStr, End );
+    Vec_StrPrintStr( vStr, ":" );
+    Vec_StrPrintNum( vStr, Beg );
+    Vec_StrPrintStr( vStr, "]" );
+}
+void Cba_ManWriteLit( Cba_Ntk_t * p, int NameId, int iBit )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    Vec_StrPrintStr( vStr, Cba_NtkStr(p, NameId) );
+    if ( iBit == -1 )
+        return;
+    Vec_StrPrintStr( vStr, "[" );
+    Vec_StrPrintNum( vStr, iBit );
+    Vec_StrPrintStr( vStr, "]" );
+}
+void Cba_ManWriteSig( Cba_Ntk_t * p, int iObj )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    int iNameId = Cba_ObjName(p, iObj);
+    if ( Cba_NameType(iNameId) == CBA_NAME_BIN )
+        Cba_ManWriteLit( p, Abc_Lit2Var2(iNameId), -1 );
+    else if ( Cba_NameType(iNameId) == CBA_NAME_WORD )
+        Cba_ManWriteLit( p, Abc_Lit2Var2(iNameId), 0 );
+    else if ( Cba_NameType(iNameId) == CBA_NAME_INDEX )
     {
-        Cba_BoxForEachBi( p, iObj, iTerm, k )
-        {
-            NameId = Cba_ObjName( p, iTerm );
-            if ( Vec_IntEntry(vMap, NameId) == 0 )
-            {
-                Vec_IntWriteEntry( vMap, NameId, 1 );
-                Vec_IntPush( vWires, iTerm );
-            }
-        }
-        Cba_BoxForEachBo( p, iObj, iTerm, k )
+        int iBit = Abc_Lit2Var2(iNameId);
+        iNameId = Cba_ObjName(p, iObj - iBit);
+        if ( Cba_NameType(iNameId) == CBA_NAME_WORD )
+            Cba_ManWriteLit( p, Abc_Lit2Var2(iNameId), iBit );
+        else if ( Cba_NameType(iNameId) == CBA_NAME_INFO )
+            Cba_ManWriteLit( p, Cba_NtkInfoName(p, Abc_Lit2Var2(iNameId)), Cba_NtkInfoIndex(p, Abc_Lit2Var2(iNameId), iBit) );
+        else assert( 0 );
+    }
+    else if ( Cba_NameType(iNameId) == CBA_NAME_INFO )
+        Cba_ManWriteLit( p, Cba_NtkInfoName(p, Abc_Lit2Var2(iNameId)), Cba_NtkInfoIndex(p, Abc_Lit2Var2(iNameId), 0) );
+    else assert( 0 );
+}
+void Cba_ManWriteConcat( Cba_Ntk_t * p, int iStart, int nObjs )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut; int i;
+    assert( nObjs >= 1 );
+    if ( nObjs == 1 )
+        Cba_ManWriteSig( p, iStart );
+    else
+    {
+        Vec_StrPrintStr( vStr, "{" );
+        for ( i = nObjs - 1; i >= 0; i-- )
         {
-            NameId = Cba_ObjName( p, iTerm );
-            if ( Vec_IntEntry(vMap, NameId) == 0 )
-            {
-                Vec_IntWriteEntry( vMap, NameId, 1 );
-                Vec_IntPush( vWires, iTerm );
-            }
+            Vec_StrPrintStr( vStr, i < nObjs - 1 ? ", " : "" );
+            if ( Cba_ObjIsBo(p, iStart) )
+                Cba_ManWriteSig( p, iStart + i );
+            else if ( Cba_ObjIsBi(p, iStart) )
+                Cba_ManWriteSig( p, Cba_ObjFanin(p, iStart - i) );
+            else assert( 0 );
         }
+        Vec_StrPrintStr( vStr, "}" );
     }
-    Cba_NtkForEachPi( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
-    Cba_NtkForEachPo( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
-    Vec_IntForEachEntry( vWires, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
-    //Vec_IntSort( vWires, 0 );
-    return vWires;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_ManWriteVerilogArray2( FILE * pFile, Cba_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
+void Cba_ManWriteGate( Cba_Ntk_t * p, int iObj )
 {
-    int i, iFanin;
-    fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iObj), (Vec_IntSize(vFanins) == 0) ? "" : ", " );
-    Vec_IntForEachEntry( vFanins, iFanin, i )
-        fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iFanin), (i == Vec_IntSize(vFanins) - 1) ? "" : ", " );
+    Vec_Str_t * vStr = p->pDesign->vOut; int iTerm, k;
+    char * pGateName = Abc_NamStr(p->pDesign->pMods, Cba_BoxNtkId(p, iObj));
+    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen( Abc_FrameGetGlobalFrame() );
+    Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pGateName, NULL );
+    Vec_StrPrintStr( vStr, "  " );
+    Vec_StrPrintStr( vStr, pGateName );
+    Vec_StrPrintStr( vStr, " (" );
+    Cba_BoxForEachBi( p, iObj, iTerm, k )
+    {
+        Vec_StrPrintStr( vStr, k ? ", ." : "." );
+        Vec_StrPrintStr( vStr, Mio_GateReadPinName(pGate, k) );
+        Vec_StrPrintStr( vStr, "(" );
+        Cba_ManWriteSig( p, iTerm );
+        Vec_StrPrintStr( vStr, ")" );
+    }
+    Cba_BoxForEachBo( p, iObj, iTerm, k )
+    {
+        Vec_StrPrintStr( vStr, Cba_BoxBiNum(p, iObj) ? ", ." : "." );
+        Vec_StrPrintStr( vStr, Mio_GateReadOutName(pGate) );
+        Vec_StrPrintStr( vStr, "(" );
+        Cba_ManWriteSig( p, iTerm );
+        Vec_StrPrintStr( vStr, ")" );
+    }
+    Vec_StrPrintStr( vStr, " );\n" );
 }
-void Cba_ManWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p )
+void Cba_ManWriteAssign( Cba_Ntk_t * p, int iObj )
 {
-    int i, k, iTerm;
-    Cba_NtkForEachBox( p, i ) // .subckt/.gate/box (formal/actual binding) 
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    Cba_ObjType_t Type = Cba_ObjType(p, iObj);
+    int nInputs = Cba_BoxBiNum(p, iObj);
+    int nOutputs = Cba_BoxBoNum(p, iObj);
+    assert( nOutputs == 1 );
+    Vec_StrPrintStr( vStr, "  assign " );
+    Cba_ManWriteSig( p, iObj + 1 );
+    Vec_StrPrintStr( vStr, " = " );
+    if ( nInputs == 0 )
+    {
+        if ( Type == CBA_BOX_CF )
+            Vec_StrPrintStr( vStr, "1\'b0" );
+        else if ( Type == CBA_BOX_CT )
+            Vec_StrPrintStr( vStr, "1\'b1" );
+        else if ( Type == CBA_BOX_CX )
+            Vec_StrPrintStr( vStr, "1\'bx" );
+        else if ( Type == CBA_BOX_CZ )
+            Vec_StrPrintStr( vStr, "1\'bz" );
+        else assert( 0 );       
+    }
+    else if ( nInputs == 1 )
     {
-        if ( Cba_ObjIsBoxUser(p, i) )
+        if ( Type == CBA_BOX_INV )
+            Vec_StrPrintStr( vStr, "~" );
+        else assert( Type == CBA_BOX_BUF );
+        Cba_ManWriteSig( p, iObj - 1 );
+    }
+    else if ( nInputs == 2 )
+    {
+        if ( Type == CBA_BOX_XNOR )
         {
-            Cba_Ntk_t * pModel = Cba_BoxNtk( p, i );
-            fprintf( pFile, "  %s %s (", Cba_NtkName(pModel), Cba_ObjNameStr(p, i) ? Cba_ObjNameStr(p, i) : "" );
-            Cba_NtkForEachPi( pModel, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", k ? ", " : "", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_BoxBi(p, i, k)) );
-            Cba_NtkForEachPo( pModel, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", Cba_NtkPiNum(pModel) ? ", " : "", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_BoxBo(p, i, k)) );
-            fprintf( pFile, ");\n" );
+            Vec_StrPrintStr( vStr, "~" );
+            Type = CBA_BOX_XOR;
         }
-        else if ( Cba_ObjIsGate(p, i) )
+        Cba_ManWriteSig( p, iObj - 1 );
+        if ( Type == CBA_BOX_AND )
+            Vec_StrPrintStr( vStr, " & " );
+        else if ( Type == CBA_BOX_OR )
+            Vec_StrPrintStr( vStr, " | " );
+        else if ( Type == CBA_BOX_XOR )
+            Vec_StrPrintStr( vStr, " ^ " );
+        else assert( 0 );
+        Cba_ManWriteSig( p, iObj - 2 );
+    }
+    Vec_StrPrintStr( vStr, ";\n" );
+}
+void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    int iObj, k, i, o;
+    Cba_NtkForEachBox( p, iObj ) // .subckt/.gate/box (formal/actual binding) 
+    {
+        Cba_Ntk_t * pModel = NULL;
+        char * pName = NULL;
+        // write mapped
+        if ( Cba_ObjIsGate(p, iObj) )
         {
-            char * pGateName = Abc_NamStr(p->pDesign->pMods, Cba_BoxNtkId(p, i));
-            Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen( Abc_FrameGetGlobalFrame() );
-            Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pGateName, NULL );
-            fprintf( pFile, "  %s (", pGateName );
-            Cba_BoxForEachBi( p, i, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", k ? ", " : "", Mio_GateReadPinName(pGate, k), Cba_ObjNameStr(p, iTerm) );
-            Cba_BoxForEachBo( p, i, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", Cba_BoxBiNum(p, i) ? ", " : "", Mio_GateReadOutName(pGate), Cba_ObjNameStr(p, iTerm) );
-            fprintf( pFile, ");\n" );
+            Cba_ManWriteGate( p, iObj );
+            continue;
         }
-/*
-        else if ( Cba_BoxNtkId(p, i) )
+        // write primitives as assign-statements
+        if ( Cba_BoxNtkName(p, iObj) == NULL )
         {
-            int pRanges[8]; char pSymbs[8];
-            char * pName = Cba_BoxNtkName(p, i);
-            int nSigs = Cba_NtkNameRanges( pName, pRanges, pSymbs );
-            int s, k, iTerm, nInputs = 0;
-            fprintf( pFile, "  %s ( ", pName );
-            for ( s = 0; s < nSigs-1; s++ )
-            {
-                fprintf( pFile, "%s.%c(", nInputs ? ", " : "", pSymbs[s] );
-                if ( pRanges[s] == 1 )
-                {
-                    iTerm = Cba_BoxBi(p, i, nInputs++);
-                    fprintf( pFile, "%s", Cba_ObjNameStr(p, iTerm) );
-                }
-                else
-                {
-                    assert( pRanges[s] > 1 );
-                    fprintf( pFile, "{" );
-                    for ( k = 0; k < pRanges[s]; k++ )
-                    {
-                        iTerm = Cba_BoxBi(p, i, nInputs++);
-                        fprintf( pFile, "%s%s", k ? ", " : "", Cba_ObjNameStr(p, iTerm) );
-                    }
-                    fprintf( pFile, "}" );
-                }
-                fprintf( pFile, ")" );
-            }
-            assert( nInputs == Cba_BoxBiNum(p, i) );
-            fprintf( pFile, "%s.%c(", nInputs ? ", " : "", pSymbs[nSigs-1] );
-            if ( pRanges[nSigs-1] == 1 )
-            {
-                iTerm = Cba_BoxBo(p, i, 0);
-                fprintf( pFile, "%s", Cba_ObjNameStr(p, iTerm) );
-            }
-            else
+            Cba_ManWriteAssign( p, iObj );
+            continue;
+        }
+
+        // write header
+        if ( Cba_ObjIsBoxUser(p, iObj) )
+            pModel = Cba_BoxNtk( p, iObj );
+        else if ( Cba_BoxNtkId(p, iObj) )
+            pName = Cba_BoxNtkName(p, iObj);
+        else assert( 0 );
+        Vec_StrPrintStr( vStr, "  " );
+        Vec_StrPrintStr( vStr, pModel ? Cba_NtkName(pModel) : pName );
+        Vec_StrPrintStr( vStr, " " );
+        Vec_StrPrintStr( vStr, Cba_ObjName(p, iObj) ? Cba_ObjNameStr(p, iObj) : ""  );
+
+        // write arguments
+        i = o = 0;
+        Vec_StrPrintStr( vStr, " (" );
+        if ( pModel )
+        {
+            int Value, Beg, End, Range;
+            assert( Cba_NtkInfoNum(pModel) );
+            Vec_IntForEachEntryTriple( &pModel->vInfo, Value, Beg, End, k )
             {
-                assert( pRanges[nSigs-1] > 1 );
-                fprintf( pFile, "{" );
-                for ( k = 0; k < pRanges[nSigs-1]; k++ )
-                {
-                    iTerm = Cba_BoxBo(p, i, k);
-                    fprintf( pFile, "%s%s", k ? ", " : "", Cba_ObjNameStr(p, iTerm) );
-                }
-                fprintf( pFile, "}" );
+                int NameId = Abc_Lit2Var2( Value );
+                int Type = Abc_Lit2Att2( Value );
+                Vec_StrPrintStr( vStr, k ? ", ." : "." );
+                Vec_StrPrintStr( vStr, Cba_NtkStr(p, NameId) );
+                Vec_StrPrintStr( vStr, "(" );
+                Range = Cba_InfoRange( Beg, End );
+                assert( Range > 0 );
+                if ( Type == 1 )
+                    Cba_ManWriteConcat( p, Cba_BoxBi(p, iObj, i), Range ), i += Range;
+                else if ( Type == 2 )
+                    Cba_ManWriteConcat( p, Cba_BoxBo(p, iObj, o), Range ), o += Range;
+                else assert( 0 );
+                Vec_StrPrintStr( vStr, ")" );
             }
-            fprintf( pFile, ") );\n" );
         }
-*/
         else
         {
-            Cba_ObjType_t Type = Cba_ObjType( p, i );
-            int nInputs = Cba_BoxBiNum(p, i);
-            fprintf( pFile, "  %s (", Ptr_TypeToName(Type) );
-            Cba_BoxForEachBo( p, i, iTerm, k )
-                fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iTerm), nInputs ? ", " : "" );
-            Cba_BoxForEachBi( p, i, iTerm, k )
-                fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iTerm), k < nInputs - 1 ? ", " : "" );
-            fprintf( pFile, ");\n" );
+            int pRanges[8]; char pSymbs[8];
+            int nSigs = Cba_NtkNameRanges( pName, pRanges, pSymbs );
+            for ( k = 0; k < nSigs; k++ )
+            {
+                Vec_StrPrintStr( vStr, k ? ", ." : "." );
+                Vec_StrPush( vStr, pSymbs[k] );
+                Vec_StrPrintStr( vStr, "(" );
+                if ( k < nSigs - 1 )
+                    Cba_ManWriteConcat( p, Cba_BoxBi(p, iObj, i), pRanges[k] ), i += pRanges[k];
+                else 
+                    Cba_ManWriteConcat( p, Cba_BoxBo(p, iObj, o), pRanges[k] ), o += pRanges[k];
+                Vec_StrPrintStr( vStr, ")" );
+            }
         }
+        Vec_StrPrintStr( vStr, " );\n" );
+        assert( i == Cba_BoxBiNum(p, iObj) );
+        assert( o == Cba_BoxBoNum(p, iObj) );
     }
 }
-void Cba_ManWriteVerilogSignals( FILE * pFile, Cba_Ntk_t * p, int SigType, int fNoRange, Vec_Int_t * vWires )
-{
-    int NameId, RangeId, i;
-    char * pSigNames[3]  = { "input", "output", "wire" }; 
-    Vec_Int_t * vSigs[3] = { &p->vInputs, &p->vOutputs, vWires };
-    if ( fNoRange )
-    {
-        Vec_IntForEachEntry( vSigs[SigType], NameId, i )
-            fprintf( pFile, "  %s %s;\n", pSigNames[SigType], SigType==3 ? Cba_NtkStr(p, NameId) : Cba_ObjNameStr(p, NameId) );
-    }
-    else
-    {
-        Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i )
-            fprintf( pFile, "  %s %s%s;\n", pSigNames[SigType], RangeId ? Cba_NtkStr(p, RangeId) : "", SigType==3 ? Cba_NtkStr(p, NameId) : Cba_ObjNameStr(p, NameId) );
-    }
-}
-void Cba_ManWriteVerilogSignalList( FILE * pFile, Cba_Ntk_t * p, int SigType, int fSkipComma, int fNoRange, Vec_Int_t * vWires )
-{
-    int NameId, RangeId, i;
-    Vec_Int_t * vSigs[3] = { &p->vInputs, &p->vOutputs, vWires };
-    if ( fNoRange )
-    {
-        Vec_IntForEachEntry( vSigs[SigType], NameId, i )
-            fprintf( pFile, "%s%s", Cba_ObjNameStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 1) ? "" : ", " );
-    }
-    else
-    {
-        Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i )
-            fprintf( pFile, "%s%s", Cba_ObjNameStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 2) ? "" : ", " );
-    }
-}
-void Cba_ManWriteVerilogNtk( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t * vWires )
+void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p )
 {
-    int s;
+    char * pKeyword[4] = { "wire ", "input ", "output ", "inout " };
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    int k, iObj, iTerm, Value, Beg, End, Length;
+    assert( Cba_NtkInfoNum(p) );
     assert( Vec_IntSize(&p->vFanin) == Cba_NtkObjNum(p) );
-    // collect wires
-    Cba_NtkCollectWires( p, vMap, vWires );
+//    Cba_NtkPrint( p );
     // write header
-    fprintf( pFile, "module %s (\n", Cba_NtkName(p) );
-    for ( s = 0; s < 2; s++ )
+    Vec_StrPrintStr( vStr, "module " );
+    Vec_StrPrintStr( vStr, Cba_NtkName(p) );
+    Vec_StrPrintStr( vStr, " (\n    " );
+    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
+    if ( Abc_Lit2Att2(Value) != 0 )
     {
-        fprintf( pFile, "    " );
-        Cba_ManWriteVerilogSignalList( pFile, p, s, s==1, 1, vWires );
-        fprintf( pFile, "\n" );
+        Vec_StrPrintStr( vStr, k ? ", " : "" );
+        Vec_StrPrintStr( vStr, Cba_NtkStr(p, Abc_Lit2Var2(Value)) );
     }
-    fprintf( pFile, "  );\n" );
-    // write declarations
-    for ( s = 0; s < 3; s++ )
-        Cba_ManWriteVerilogSignals( pFile, p, s, 1, vWires );
-    fprintf( pFile, "\n" );
+    Vec_StrPrintStr( vStr, "\n  );\n" );
+    // write inputs/outputs
+    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
+    if ( Abc_Lit2Att2(Value) != 0 )
+    {
+        Vec_StrPrintStr( vStr, "  " );
+        Vec_StrPrintStr( vStr, pKeyword[Abc_Lit2Att2(Value)] );
+        if ( Beg >= 0 )
+            Cba_ManWriteRange( p, Beg, End );
+        Vec_StrPrintStr( vStr, Cba_NtkStr(p, Abc_Lit2Var2(Value)) );
+        Vec_StrPrintStr( vStr, ";\n" );
+    }
+    Vec_StrPrintStr( vStr, "\n" );
+    // write word-level wires
+    Cba_NtkForEachBox( p, iObj )
+    Cba_BoxForEachBo( p, iObj, iTerm, k )
+        if ( Cba_NameType(Cba_ObjName(p, iTerm)) == CBA_NAME_WORD )
+        {
+            int Beg, End;
+            Cba_ObjGetRange( p, iTerm, &Beg, &End );
+            Vec_StrPrintStr( vStr, "  wire " );
+            Cba_ManWriteRange( p, Beg, End );
+            Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iTerm) );
+            Vec_StrPrintStr( vStr, ";\n" );
+        }
+    // write bit-level wires
+    Length = 7;
+    Vec_StrPrintStr( vStr, "  wire " );
+    Cba_NtkForEachBox( p, iObj )
+    Cba_BoxForEachBo( p, iObj, iTerm, k )
+        if ( Cba_NameType(Cba_ObjName(p, iTerm)) == CBA_NAME_BIN )
+        {
+            if ( Length > 72 )
+                Vec_StrPrintStr( vStr, ";\n  wire " ), Length = 7;
+            if ( Length > 7 )
+                Vec_StrPrintStr( vStr, ", " );
+            Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iTerm) ); 
+            Length += strlen(Cba_ObjNameStr(p, iTerm));
+        }
+    Vec_StrPrintStr( vStr, ";\n\n" );
     // write objects
-    Cba_ManWriteVerilogBoxes( pFile, p );
-    fprintf( pFile, "endmodule\n\n" );
+    Cba_ManWriteVerilogBoxes( p );
+    Vec_StrPrintStr( vStr, "endmodule\n\n" );
 }
 void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p )
 {
-    FILE * pFile;
-    Cba_Ntk_t * pNtk; 
-    Vec_Int_t * vMap, * vWires;
-    int i;
+    Cba_Ntk_t * pNtk; int i;
     // check the library
     if ( p->pMioLib && p->pMioLib != Abc_FrameReadLibGen() )
     {
         printf( "Genlib library used in the mapped design is not longer a current library.\n" );
         return;
     }
-    pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open output file \"%s\".\n", pFileName );
-        return;
-    }
-    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() );
+    // derive the stream
+    p->vOut = Vec_StrAlloc( 10000 );
     Cba_ManAssignInternNames( p );
-    vMap = Vec_IntStart( Abc_NamObjNumMax(p->pStrs) + 1 );
-    vWires = Vec_IntAlloc( 1000 );
     Cba_ManForEachNtk( p, pNtk, i )
-        Cba_ManWriteVerilogNtk( pFile, pNtk, vMap, vWires );
-    Vec_IntFree( vWires );
-    Vec_IntFree( vMap );
-    fclose( pFile );
+        Cba_ManWriteVerilogNtk( pNtk );
+    // dump into file
+    if ( p->vOut && Vec_StrSize(p->vOut) > 0 )
+    {
+        FILE * pFile = fopen( pFileName, "wb" );
+        if ( pFile == NULL )
+            printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        else
+        {
+            fwrite( Vec_StrArray(p->vOut), 1, Vec_StrSize(p->vOut), pFile );
+            fclose( pFile );
+        }
+    }
+    Vec_StrFreeP( &p->vOut );
 }