Improvements to Cba data-structure.

3 files changed, 323 insertions, 461 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 85ba50cb..351c0b6e 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -74,6 +74,7 @@ typedef enum {
     CBA_BOX_RXOR,
     CBA_BOX_RXNOR,
 
+    CBA_BOX_LNOT,
     CBA_BOX_LAND,
     CBA_BOX_LNAND,
     CBA_BOX_LOR,
@@ -95,7 +96,7 @@ typedef enum {
     CBA_BOX_DIV,
     CBA_BOX_MOD,
     CBA_BOX_REM,
-    CBA_OBJ_POW,
+    CBA_BOX_POW,
     CBA_BOX_MIN,
     CBA_BOX_ABS,
 
@@ -185,14 +186,16 @@ struct Cba_Man_t_
     char *       pName;    // design name
     char *       pSpec;    // spec file name
     Abc_Nam_t *  pStrs;    // string manager
+    Abc_Nam_t *  pCons;    // constant manager
     Abc_Nam_t *  pMods;    // module name manager
     char *       pTypeNames[CBA_BOX_LAST];
     // internal data
     int          iRoot;    // root network
     Vec_Ptr_t    vNtks;    // networks
     // user data
-    Vec_Str_t *  vOut;     
-    Vec_Str_t *  vOut2;     
+    Vec_Str_t    vOut;     
+    Vec_Str_t    vOut2;     
+    void *       pMioLib;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -209,16 +212,24 @@ 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 * 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_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->pCons, i);                                                             }
+static inline int            Cba_ManConstId( Cba_Man_t * p, char * pStr )    { return Abc_NamStrFind(p->pCons, pStr);                                                      }
+static inline int            Cba_ManConstIdMax( Cba_Man_t * p )              { return Abc_NamObjNumMax(p->pCons) + 1;                                                      }
 
 static inline Cba_Man_t *    Cba_NtkMan( Cba_Ntk_t * p )                     { return p->pDesign;                                                                          }
 static inline Cba_Ntk_t *    Cba_NtkNtk( Cba_Ntk_t * p, int i )              { return Cba_ManNtk(p->pDesign, i);                                                           }
 static inline int            Cba_NtkId( Cba_Ntk_t * p )                      { return p->Id;                                                                               }
 static inline int            Cba_NtkPi( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vInputs, i);                                                        }
 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 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 int            Cba_NtkNameId( Cba_Ntk_t * p )                  { return p->NameId;                                                                           }
 static inline char *         Cba_NtkName( Cba_Ntk_t * p )                    { return Cba_NtkStr(p, p->NameId);                                                            }
 static inline char *         Cba_NtkTypeName( Cba_Ntk_t * p, int Type )      { return p->pDesign->pTypeNames[Type];                                                        }
@@ -231,6 +242,7 @@ static inline int            Cba_NtkPoNum( Cba_Ntk_t * p )                   { r
 static inline int            Cba_NtkPioNum( Cba_Ntk_t * p )                  { return Cba_NtkPiNum(p) + Cba_NtkPoNum(p);                                                   }
 static inline int            Cba_NtkPiNumAlloc( Cba_Ntk_t * p )              { return Vec_IntCap(&p->vInputs);                                                             }
 static inline int            Cba_NtkPoNumAlloc( Cba_Ntk_t * p )              { return Vec_IntCap(&p->vOutputs);                                                            }
+static inline int            Cba_NtkPioOrderNum( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vOrder);                                                             }
 static inline int            Cba_NtkObjNum( Cba_Ntk_t * p )                  { return Vec_StrSize(&p->vObjType)-1;                                                         }
 static inline int            Cba_NtkObjNumAlloc( Cba_Ntk_t * p )             { return Vec_StrCap(&p->vObjType)-1;                                                          }
 static inline int            Cba_NtkFinNum( Cba_Ntk_t * p )                  { return Vec_IntSize(&p->vFinFon)-1;                                                          }
@@ -289,6 +301,8 @@ static inline Cba_ObjType_t  Cba_ObjType( Cba_Ntk_t * p, int i )             { a
 static inline void           Cba_ObjCleanType( Cba_Ntk_t * p, int i )        { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)CBA_OBJ_NONE );                      }
 static inline int            Cba_TypeIsBox( Cba_ObjType_t Type )             { return Type >= CBA_OBJ_BOX && Type < CBA_BOX_LAST;                                          }
 static inline int            Cba_TypeIsSeq( Cba_ObjType_t Type )             { return Type >= CBA_BOX_RAM && Type <= CBA_BOX_DFFRS;                                        }
+static inline int            Cba_TypeIsUnary( Cba_ObjType_t Type )           { return Type == CBA_BOX_BUF || Type == CBA_BOX_INV || Type == CBA_BOX_LNOT || Type == CBA_BOX_MIN || (Type >= CBA_BOX_RAND && Type <= CBA_BOX_RXNOR);  }
+static inline int            Cba_TypeIsMux( Cba_ObjType_t Type )             { return Type == CBA_BOX_MUX || Type == CBA_BOX_NMUX || Type == CBA_BOX_SEL || Type == CBA_BOX_PSEL;  }
 
 static inline int            Cba_ObjIsPi( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_PI;                                                     }
 static inline int            Cba_ObjIsPo( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_PO;                                                     }
@@ -297,6 +311,9 @@ static inline int            Cba_ObjIsBox( Cba_Ntk_t * p, int i )            { r
 static inline int            Cba_ObjIsBoxUser( Cba_Ntk_t * p, int i )        { return Cba_ObjType(p, i) == CBA_OBJ_BOX;                                                    }
 static inline int            Cba_ObjIsBoxPrim( Cba_Ntk_t * p, int i )        { return Cba_ObjType(p, i) >  CBA_OBJ_BOX && Cba_ObjType(p, i) < CBA_BOX_LAST;                }
 static inline int            Cba_ObjIsGate( Cba_Ntk_t * p, int i )           { return Cba_ObjType(p, i) == CBA_BOX_GATE;                                                   }
+static inline int            Cba_ObjIsSlice( Cba_Ntk_t * p, int i )          { return Cba_ObjType(p, i) == CBA_BOX_SLICE;                                                  }
+static inline int            Cba_ObjIsConcat( Cba_Ntk_t * p, int i )         { return Cba_ObjType(p, i) == CBA_BOX_CONCAT;                                                 }
+static inline int            Cba_ObjIsUnary( Cba_Ntk_t * p, int i )          { return Cba_TypeIsUnary(Cba_ObjType(p, i));                                                  }
 
 static inline int            Cba_ObjFin0( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntEntry(&p->vObjFin0, i);                                          }
 static inline int            Cba_ObjFon0( Cba_Ntk_t * p, int i )             { assert(i>0); return Vec_IntEntry(&p->vObjFon0, i);                                          }
@@ -312,6 +329,7 @@ static inline char *         Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { a
 static inline int            Cba_ObjAttr( Cba_Ntk_t * p, int i )             { assert(i>=0); return Cba_NtkHasObjAttrs(p) ? Vec_IntGetEntry(&p->vObjAttr, i) : 0;          }
 static inline int            Cba_ObjAttrSize( Cba_Ntk_t * p, int i )         { assert(i>=0); return Cba_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Cba_ObjAttr(p, i)) : 0; }
 static inline int *          Cba_ObjAttrArray( Cba_Ntk_t * p, int i )        { assert(i>=0); return Cba_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Cba_ObjAttr(p, i)+1) : NULL; }
+static inline int            Cba_ObjAttrValue( Cba_Ntk_t * p, int i, int x ) { int k, s = Cba_ObjAttrSize(p, i), * a = Cba_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2)  if (a[k] == x) return a[k+1]; return 0; }
 
 static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x );                     }
 static inline void           Cba_ObjSetFunc( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjFunc(p, i) ==  0); Vec_IntSetEntry( &p->vObjFunc, i, x );                     }
@@ -338,6 +356,11 @@ static inline int            Cba_FonConst( int f )                           { a
 static inline int            Cba_FonFromConst( int c )                       { assert(c >= 0); return -c-1;              }
 
 static inline int            Cba_FonObj( Cba_Ntk_t * p, int f )              { return Cba_FonIsReal(f) ? Vec_IntEntry(&p->vFonObj, f) : 0;                                 }
+static inline int            Cba_FonLeft( Cba_Ntk_t * p, int f )             { return Cba_NtkHasFonLefts(p) ? Vec_IntEntry(&p->vFonLeft, f) : 0;                           }
+static inline int            Cba_FonRight( Cba_Ntk_t * p, int f )            { return Cba_NtkHasFonRights(p) ? Vec_IntEntry(&p->vFonRight, f) : 0;                         }
+static inline int            Cba_FonRange( Cba_Ntk_t * p, int f )            { int l = Cba_FonLeft(p, f), r = Cba_FonRight(p, f); return 1 + (l > r ? l-r : r-l);          }
+static inline void           Cba_FonSetLeft( Cba_Ntk_t * p, int f, int x )   { assert(Cba_NtkHasFonLefts(p));  Vec_IntSetEntry(&p->vFonLeft, f, x);                        }
+static inline void           Cba_FonSetRight( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRights(p)); Vec_IntSetEntry(&p->vFonRight, f, x);                       }
 static inline int            Cba_FonCopy( Cba_Ntk_t * p, int f )             { return Cba_FonIsReal(f) ? Vec_IntEntry(&p->vFonCopy, f) : f;                                }
 static inline void           Cba_FonSetCopy( Cba_Ntk_t * p, int f, int x )   { assert(Cba_FonIsReal(f)); assert(Cba_FonCopy(p, f) == 0); Vec_IntWriteEntry(&p->vFonCopy, f, x); }
 static inline int            Cba_FonName( Cba_Ntk_t * p, int f )             { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); return Vec_IntGetEntry( &p->vFonName, f );                        }
@@ -364,6 +387,8 @@ static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i, int k )     { a
     for ( i = 0; (i < Cba_NtkPoNum(p))  && (((iObj) = Cba_NtkPo(p, i)), 1); i++ ) 
 #define Cba_NtkForEachBoxSeq( p, iObj, i )                                \
     for ( i = 0; (i < Cba_NtkBoxSeqNum(p))  && (((iObj) = Cba_NtkBoxSeq(p, i)), 1); i++ ) 
+#define Cba_NtkForEachPioOrder( p, iObj, i )                              \
+    for ( i = 0; (i < Cba_NtkPioOrderNum(p))  && (((iObj) = Cba_NtkPioOrder(p, i)), 1); i++ ) 
 
 #define Cba_NtkForEachPiFon( p, iObj, iFon, i )                           \
     for ( i = 0; (i < Cba_NtkPiNum(p))  && (((iObj) = Cba_NtkPi(p, i)), 1)  && (((iFon) = Cba_ObjFon0(p, iObj)), 1); i++ ) 
@@ -554,7 +579,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_ManNewStrId_(p->pDesign, pPref, iFon, NULL) );
 }
 static inline void Cba_NtkMissingFonNames( Cba_Ntk_t * p, char * pPref )
 {
@@ -567,7 +592,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_ManNewStrId_(p->pDesign, pPref, iFon, NULL) );
 }
 static inline int Cba_NtkIsSeq( Cba_Ntk_t * p )
 {
@@ -657,6 +682,8 @@ static inline Cba_Ntk_t * Cba_NtkDupOrder( Cba_Man_t * pMan, Cba_Ntk_t * p, Vec_
 }
 static inline void Cba_NtkDupAttrs( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
 {
+//    Vec_IntRemapArray( &p->vObjCopy, &p->vOrder,    &pNew->vOrder,    Cba_NtkPioOrderNum(pNew) );
+//    Vec_IntRemapArray( &p->vObjCopy, &p->vSeq,      &pNew->vSeq,      Cba_NtkBoxSeqNum(pNew) );
     // transfer object attributes
     Vec_IntRemapArray( &p->vObjCopy, &p->vObjFunc,  &pNew->vObjFunc,  Cba_NtkObjNum(pNew) + 1 );
     Vec_IntRemapArray( &p->vObjCopy, &p->vObjName,  &pNew->vObjName,  Cba_NtkObjNum(pNew) + 1 );
@@ -748,13 +775,21 @@ static inline void Cba_NtkPrint( Cba_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t * pStrs, Abc_Nam_t * pMods )
+static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t * pStrs, Abc_Nam_t * pCons, Abc_Nam_t * pMods )
 {
     Cba_Man_t * pNew = ABC_CALLOC( Cba_Man_t, 1 );
     pNew->pName = Extra_FileDesignName( pFileName );
     pNew->pSpec = Abc_UtilStrsav( pFileName );
     pNew->pStrs = pStrs ? pStrs : Abc_NamStart( 1000, 24 );
-    pNew->pMods = pMods ? pMods : Abc_NamStart( 1000, 24 );
+    pNew->pCons = pCons ? pCons : Abc_NamStart( 100, 24 );
+    pNew->pMods = pMods ? pMods : Abc_NamStart( 100, 24 );
+    if ( pCons == NULL )
+    {
+        Abc_NamStrFindOrAdd(pNew->pCons, "1\'b0", NULL);
+        Abc_NamStrFindOrAdd(pNew->pCons, "1\'b1", NULL);
+        Abc_NamStrFindOrAdd(pNew->pCons, "1\'bx", NULL);
+        Abc_NamStrFindOrAdd(pNew->pCons, "1\'bz", NULL);
+    }
     Vec_PtrGrow( &pNew->vNtks,  nNtks+1 ); Vec_PtrPush( &pNew->vNtks, NULL );
     if ( nNtks == 1 ) pNew->iRoot = 1;
     return pNew;
@@ -766,7 +801,7 @@ static inline void Cba_ManDupTypeNames( Cba_Man_t * pNew, Cba_Man_t * p )
 static inline Cba_Man_t * Cba_ManDup( Cba_Man_t * p, Vec_Int_t*(* pFuncOrder)(Cba_Ntk_t*) )
 {
     Cba_Ntk_t * pNtk, * pNtkNew; int i;
-    Cba_Man_t * pNew = Cba_ManAlloc( p->pSpec, Cba_ManNtkNum(p), Abc_NamRef(p->pStrs), Abc_NamStart(100, 24) );
+    Cba_Man_t * pNew = Cba_ManAlloc( p->pSpec, Cba_ManNtkNum(p), Abc_NamRef(p->pStrs), Abc_NamRef(p->pCons), Abc_NamStart(100, 24) );
     Cba_ManDupTypeNames( pNew, p );
     Cba_ManForEachNtk( p, pNtk, i )
     {
@@ -793,13 +828,28 @@ static inline void Cba_ManFree( Cba_Man_t * p )
         Cba_NtkFree( pNtk );
     ABC_FREE( p->vNtks.pArray );
     Abc_NamDeref( p->pStrs );
+    Abc_NamDeref( p->pCons );
     Abc_NamDeref( p->pMods );
-    Vec_StrFreeP( &p->vOut );
-    Vec_StrFreeP( &p->vOut2 );
+    Vec_StrErase( &p->vOut );
+    Vec_StrErase( &p->vOut2 );
     ABC_FREE( p->pName );
     ABC_FREE( p->pSpec );
     ABC_FREE( p );
 }
+static inline int Cba_ManNewConstId( Cba_Man_t * p, Vec_Str_t * vBits ) 
+{ 
+    Vec_Str_t * vOut = &p->vOut; 
+    char Symb; int i; 
+    assert( Vec_StrSize(vBits) > 0 );
+    Vec_StrClear( vOut );
+    Vec_StrPrintNum( vOut, Vec_StrSize(vBits) );
+    Vec_StrPush( vOut, '\'' );
+    Vec_StrPush( vOut, 'b' );
+    Vec_StrForEachEntry( vBits, Symb, i )
+        Vec_StrPush( vOut, Symb );
+    Vec_StrPush( vOut, '\0' );
+    return Abc_NamStrFindOrAdd(p->pCons, Vec_StrArray(vOut), NULL);
+}
 static inline int Cba_ManMemory( Cba_Man_t * p )
 {
     Cba_Ntk_t * pNtk; int i;
@@ -807,6 +857,7 @@ static inline int Cba_ManMemory( Cba_Man_t * p )
     nMem += p->pName ? (int)strlen(p->pName) : 0;
     nMem += p->pSpec ? (int)strlen(p->pSpec) : 0;
     nMem += Abc_NamMemUsed(p->pStrs);
+    nMem += Abc_NamMemUsed(p->pCons);
     nMem += Abc_NamMemUsed(p->pMods);
     nMem += (int)Vec_PtrMemory(&p->vNtks);
     Cba_ManForEachNtk( p, pNtk, i )
@@ -906,8 +957,8 @@ extern Vec_Ptr_t *   Prs_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          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
-//extern void          Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fUseAssign );
+extern void          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
+extern void          Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fInlineConcat );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 1bc21e22..34bc4253 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -422,7 +422,7 @@ void Cba_NtkCollapse_rec( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vSigs, in
 }
 Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p, int TypeBuf )
 {
-    Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamStart(100, 24) );
+    Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamRef(p->pCons), Abc_NamStart(100, 24) );
     Cba_Ntk_t * pRoot = Cba_ManRoot( p ), * pRootNew;
     Vec_Int_t * vSigs = Vec_IntAlloc( 1000 );
     int i, iObj, iObjNew, iFon, nObjs = 0, nFins = 0, nFons = 0;
@@ -593,7 +593,7 @@ void Cba_ManExtractGroupInt( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vObjs,
 }
 Cba_Man_t * Cba_ManExtractGroup( Cba_Man_t * p, Vec_Int_t * vObjs )
 {
-    Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamStart(100, 24) );
+    Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamRef(p->pCons), Abc_NamStart(100, 24) );
     Cba_Ntk_t * pRoot = Cba_ManRoot( p ), * pRootNew;
     Vec_Int_t * vFonIns = Cba_NtkCollectInFons( pRoot, vObjs );
     Vec_Int_t * vFonOuts = Cba_NtkCollectOutFons( pRoot, vObjs );
@@ -676,7 +676,7 @@ static inline int Cba_NtkInsertGiaObj( Cba_Ntk_t * p, Gia_Man_t * pGia, int iObj
 }
 Cba_Man_t * Cba_ManDeriveFromGia( Gia_Man_t * pGia )
 {
-    Cba_Man_t * p = Cba_ManAlloc( pGia->pSpec, 1, NULL, NULL );
+    Cba_Man_t * p = Cba_ManAlloc( pGia->pSpec, 1, NULL, NULL, NULL );
     Cba_Ntk_t * pNtk = Cba_NtkAlloc( p, Abc_NamStrFindOrAdd(p->pStrs, pGia->pName, NULL), Gia_ManCiNum(pGia), Gia_ManCoNum(pGia), 1000, 2000, 2000 );
     Vec_Int_t * vLit2Fon = Vec_IntStartFull( 2*Gia_ManObjNum(pGia) );
     int i, iObj, iObjNew, NameId, iLit0, iFon0;
@@ -686,7 +686,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_ManNewStrId_(p, "i", i, NULL);
         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 +708,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_ManNewStrId_(p, "o", i, NULL);
         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/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index 58604eb1..228656d0 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -179,486 +179,301 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
 }
 
 
-#if 0
 
-/**Function*************************************************************
-
-  Synopsis    [Writing word-level Verilog.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
 
+/**Function*************************************************************
+  
+  Synopsis    []  
+  
+  Description []  
+                 
+  SideEffects []  
+  
+  SeeAlso     []  
+  
 ***********************************************************************/
-// compute range of a name (different from range of a multi-bit wire)
-static inline int Cba_ObjGetRange( Cba_Ntk_t * p, int iObj )
+void Cba_ManCreatePrimMap( char ** pMap )
 {
-    int i, NameId = Cba_ObjName(p, iObj);
-    assert( Cba_ObjIsCi(p, iObj) );
-//    if ( Cba_NameType(NameId) == CBA_NAME_INDEX )
-//        NameId = Cba_ObjName(p, iObj - Abc_Lit2Var2(NameId));
-    assert( Cba_NameType(NameId) == CBA_NAME_WORD || Cba_NameType(NameId) == CBA_NAME_INFO );
-    for ( i = iObj + 1; i < Cba_NtkObjNum(p); i++ )
-        if ( !Cba_ObjIsCi(p, i) || Cba_ObjNameType(p, i) != CBA_NAME_INDEX )
-            break;
-    return i - iObj;
+    memset( pMap, 0, sizeof(char *) * CBA_BOX_LAST );
+    pMap[ CBA_BOX_BUF    ] = "";
+    pMap[ CBA_BOX_INV    ] = "~";
+    pMap[ CBA_BOX_AND    ] = "&"; 
+    pMap[ CBA_BOX_NAND   ] = "~&"; 
+    pMap[ CBA_BOX_OR     ] = "|"; 
+    pMap[ CBA_BOX_NOR    ] = "~|"; 
+    pMap[ CBA_BOX_XOR    ] = "^"; 
+    pMap[ CBA_BOX_XNOR   ] = "~^"; 
+    pMap[ CBA_BOX_SHARP  ] = "&"; 
+    pMap[ CBA_BOX_SHARPL ] = "&"; 
+    pMap[ CBA_BOX_MUX    ] = "?"; 
+    pMap[ CBA_BOX_MAJ    ] = "maj"; 
+    pMap[ CBA_BOX_RAND   ] = "&"; 
+    pMap[ CBA_BOX_RNAND  ] = "~&"; 
+    pMap[ CBA_BOX_ROR    ] = "|"; 
+    pMap[ CBA_BOX_RNOR   ] = "~|"; 
+    pMap[ CBA_BOX_RXOR   ] = "^"; 
+    pMap[ CBA_BOX_RXNOR  ] = "~^"; 
+    pMap[ CBA_BOX_LNOT   ] = "!"; 
+    pMap[ CBA_BOX_LAND   ] = "&&"; 
+    pMap[ CBA_BOX_LNAND  ] = "!&&"; 
+    pMap[ CBA_BOX_LOR    ] = "||"; 
+    pMap[ CBA_BOX_LNOR   ] = "!||"; 
+    pMap[ CBA_BOX_LXOR   ] = "^^"; 
+    pMap[ CBA_BOX_LXNOR  ] = "!^^"; 
+    pMap[ CBA_BOX_NMUX   ] = "??"; 
+    pMap[ CBA_BOX_SEL    ] = "?|"; 
+    pMap[ CBA_BOX_PSEL   ] = "?%"; 
+    pMap[ CBA_BOX_ENC    ] = "enc"; 
+    pMap[ CBA_BOX_PENC   ] = "penc"; 
+    pMap[ CBA_BOX_DEC    ] = "dec"; 
+    pMap[ CBA_BOX_EDEC   ] = "edec"; 
+    pMap[ CBA_BOX_ADD    ] = "+"; 
+    pMap[ CBA_BOX_SUB    ] = "-"; 
+    pMap[ CBA_BOX_MUL    ] = "*"; 
+    pMap[ CBA_BOX_DIV    ] = "/"; 
+    pMap[ CBA_BOX_MOD    ] = "mod"; 
+    pMap[ CBA_BOX_REM    ] = "%%"; 
+    pMap[ CBA_BOX_POW    ] = "**"; 
+    pMap[ CBA_BOX_MIN    ] = "-"; 
+    pMap[ CBA_BOX_ABS    ] = "abs"; 
+    pMap[ CBA_BOX_LTHAN  ] = "<"; 
+    pMap[ CBA_BOX_LETHAN ] = "<="; 
+    pMap[ CBA_BOX_METHAN ] = ">="; 
+    pMap[ CBA_BOX_MTHAN  ] = ">"; 
+    pMap[ CBA_BOX_EQU    ] = "=="; 
+    pMap[ CBA_BOX_NEQU   ] = "!="; 
+    pMap[ CBA_BOX_SHIL   ] = "<<"; 
+    pMap[ CBA_BOX_SHIR   ] = ">>"; 
+    pMap[ CBA_BOX_ROTL   ] = "rotL"; 
+    pMap[ CBA_BOX_ROTR   ] = "rotR"; 
 }
 
-static inline void Cba_ManWriteVar( Cba_Ntk_t * p, int RealName )
-{
-    Vec_StrPrintStr( p->pDesign->vOut, Cba_NtkStr(p, RealName) );
-}
-static inline void Cba_ManWriteRange( Cba_Ntk_t * p, int Beg, int End )
-{
-    Vec_Str_t * vStr = p->pDesign->vOut;
-    Vec_StrPrintStr( vStr, "[" );
-    if ( End >= 0 )
-    {
-        Vec_StrPrintNum( vStr, End );
-        Vec_StrPrintStr( vStr, ":" );
-    }
-    Vec_StrPrintNum( vStr, Beg );
-    Vec_StrPrintStr( vStr, "]" );
-}
-static inline void Cba_ManWriteConstBit( Cba_Ntk_t * p, int iObj, int fHead )
-{
-    Vec_Str_t * vStr = p->pDesign->vOut;
-    int Const = Cba_ObjGetConst(p, iObj);
-    assert( Const );
-    if ( fHead )
-        Vec_StrPrintStr( vStr, "1\'b" );
-    if ( Const == CBA_BOX_CF )
-        Vec_StrPush( vStr, '0' );
-    else if ( Const == CBA_BOX_CT )
-        Vec_StrPush( vStr, '1' );
-    else if ( Const == CBA_BOX_CX )
-        Vec_StrPush( vStr, 'x' );
-    else if ( Const == CBA_BOX_CZ )
-        Vec_StrPush( vStr, 'z' );
-    else assert( 0 );
-}
-static inline int Cba_ManFindRealNameId( Cba_Ntk_t * p, int iObj )
+void Cba_ManWriteFonRange( Cba_Ntk_t * p, int iFon )
 {
-    int NameId = Cba_ObjName(p, iObj);
-    assert( Cba_ObjIsCi(p, iObj) );
-    if ( Cba_NameType(NameId) == CBA_NAME_INDEX )
-        NameId = Cba_ObjName(p, iObj - Abc_Lit2Var2(NameId));
-    if ( Cba_NameType(NameId) == CBA_NAME_INFO )
-        return Cba_NtkInfoName(p, Abc_Lit2Var2(NameId));
-    assert( Cba_NameType(NameId) == CBA_NAME_BIN || Cba_NameType(NameId) == CBA_NAME_WORD );
-    return Abc_Lit2Var2(NameId);
-}
-static inline int Cba_ManFindRealIndex( Cba_Ntk_t * p, int iObj )
-{
-    int iBit = 0, NameId = Cba_ObjName(p, iObj);
-    assert( Cba_ObjIsCi(p, iObj) );
-    assert( Cba_NameType(NameId) != CBA_NAME_BIN );
-    if ( Cba_NameType(NameId) == CBA_NAME_INDEX )
-        NameId = Cba_ObjName(p, iObj - (iBit = Abc_Lit2Var2(NameId)));
-    if ( Cba_NameType(NameId) == CBA_NAME_INFO )
-        return Cba_NtkInfoIndex(p, Abc_Lit2Var2(NameId), iBit);
-    assert( Cba_NameType(NameId) == CBA_NAME_WORD );
-    return iBit;
+    Vec_Str_t * vStr = &p->pDesign->vOut;
+    if ( Cba_FonIsConst(iFon) || Cba_FonRange(p, iFon) == 1 )
+        return;
+    Vec_StrPush( vStr, '[' );
+    Vec_StrPrintNum( vStr, Cba_FonLeft(p, iFon) );
+    Vec_StrPush( vStr, ':' );
+    Vec_StrPrintNum( vStr, Cba_FonRight(p, iFon) );
+    Vec_StrPush( vStr, ']' );
+    Vec_StrPush( vStr, ' ' );
 }
-static inline void Cba_ManWriteSig( Cba_Ntk_t * p, int iObj )
+void Cba_ManWriteFonName( Cba_Ntk_t * p, int iFon, int fInlineConcat )
 {
-    if ( Cba_ObjIsCo(p, iObj) )
-        iObj = Cba_ObjFanin(p, iObj);
-    assert( Cba_ObjIsCi(p, iObj) );
-    if ( Cba_ObjGetConst(p, iObj) )
-        Cba_ManWriteConstBit( p, iObj, 1 );
+    extern void Cba_ManWriteConcat( Cba_Ntk_t * p, int iObj );
+    Vec_Str_t * vStr = &p->pDesign->vOut;
+    if ( Cba_FonIsConst(iFon) )
+        Vec_StrPrintStr( vStr, Cba_NtkConst(p, Cba_FonConst(iFon)) );
+    else if ( fInlineConcat && Cba_ObjIsConcat(p, Cba_FonObj(p, iFon)) )
+        Cba_ManWriteConcat( p, Cba_FonObj(p, iFon) );
     else
-    {
-        int NameId = Cba_ObjName(p, iObj);
-        if ( Cba_NameType(NameId) == CBA_NAME_BIN )
-            Cba_ManWriteVar( p, Abc_Lit2Var2(NameId) );
-        else
-        {
-            Cba_ManWriteVar( p, Cba_ManFindRealNameId(p, iObj) );
-            Cba_ManWriteRange( p, Cba_ManFindRealIndex(p, iObj), -1 );
-        }
-    }
+        Vec_StrPrintStr( vStr, Cba_FonNameStr(p, iFon) );
 }
-static inline void Cba_ManWriteConcat( Cba_Ntk_t * p, int iStart, int nObjs )
+void Cba_ManWriteConcat( Cba_Ntk_t * p, int iObj )
 {
-    Vec_Str_t * vStr = p->pDesign->vOut; 
-    assert( nObjs >= 1 );
-    if ( nObjs == 1 )
-    {
-        Cba_ManWriteSig( p, iStart );
-        return;
-    }
-    Vec_StrPrintStr( vStr, "{" );
-    if ( Cba_ObjIsBo(p, iStart) ) // box output
-    {
-        int i;
-        for ( i = iStart + nObjs - 1; i >= iStart; i-- )
-        {
-            if ( Cba_ObjNameType(p, i) == CBA_NAME_INDEX )
-                continue;
-            if ( Vec_StrEntryLast(vStr) != '{' )
-                Vec_StrPrintStr( vStr, ", " );
-            Cba_ManWriteVar( p, Cba_ManFindRealNameId(p, i) );
-        }
-    }
-    else if ( Cba_ObjIsBi(p, iStart) ) // box input
+    int i, iFin, iFon;
+    Vec_Str_t * vStr = &p->pDesign->vOut;
+    assert( Cba_ObjIsConcat(p, iObj) );
+    Vec_StrPush( vStr, '{' );
+    Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
     {
-        int e, b, k, NameId;
-        for ( e = iStart - nObjs + 1; e <= iStart; )
-        {
-            if ( Vec_StrEntryLast(vStr) != '{' )
-                Vec_StrPrintStr( vStr, ", " );
-            // write constant
-            if ( Cba_ObjGetConst(p, Cba_ObjFanin(p, e)) )
-            {
-                int fBinary = Cba_ObjIsConstBin(p, Cba_ObjFanin(p, e)-1);                
-                for ( b = e + 1; b <= iStart; b++ )
-                {
-                    if ( !Cba_ObjGetConst(p, Cba_ObjFanin(p, b)) )
-                        break;
-                    if ( !Cba_ObjIsConstBin(p, Cba_ObjFanin(p, b)-1) )
-                        fBinary = 0;
-                }
-                Vec_StrPrintNum( vStr, b - e );
-                if ( fBinary && b - e > 8 ) // write hex if more than 8 bits
-                {
-                    int Digit = 0, nBits = ((b - e) & 3) ? (b - e) & 3 : 4;
-                    Vec_StrPrintStr( vStr, "\'h" );
-                    for ( k = e; k < b; k++ )
-                    {
-                        Digit = 2*Digit + Cba_ObjGetConst(p, Cba_ObjFanin(p, k)) - CBA_BOX_CF;
-                        assert( Digit < 16 );
-                        if ( --nBits == 0 )
-                        {
-                            Vec_StrPush( vStr, (char)(Digit < 10 ? '0' + Digit : 'a' + Digit - 10) );
-                            nBits = 4;
-                            Digit = 0;
-                        }
-                    }
-                    assert( nBits == 4 );
-                    assert( Digit == 0 );
-                }
-                else
-                {
-                    Vec_StrPrintStr( vStr, "\'b" );
-                    for ( k = e; k < b; k++ )
-                        Cba_ManWriteConstBit( p, Cba_ObjFanin(p, k), 0 );
-                }
-                e = b;
-                continue;
-            }
-            // try replication
-            for ( b = e + 1; b <= iStart; b++ )
-                if ( Cba_ObjFanin(p, b) != Cba_ObjFanin(p, e) )
-                    break;
-            if ( b > e + 2 ) // more than two
-            {
-                Vec_StrPrintNum( vStr, b - e );
-                Vec_StrPrintStr( vStr, "{" );
-                Cba_ManWriteSig( p, e );
-                Vec_StrPrintStr( vStr, "}" );
-                e = b;
-                continue;
-            }
-            NameId = Cba_ObjName(p, Cba_ObjFanin(p, e));
-            if ( Cba_NameType(NameId) == CBA_NAME_BIN )
-            {
-                Cba_ManWriteVar( p, Abc_Lit2Var2(NameId) );
-                e++;
-                continue;
-            }
-            // find end of the slice
-            for ( b = e + 1; b <= iStart; b++ )
-                if ( Cba_ObjFanin(p, e) - Cba_ObjFanin(p, b) != b - e )
-                    break;
-            // write signal name
-            Cba_ManWriteVar( p, Cba_ManFindRealNameId(p, Cba_ObjFanin(p, e)) );
-            if ( b == e + 1 ) // literal
-                Cba_ManWriteRange( p, Cba_ManFindRealIndex(p, Cba_ObjFanin(p, e)), -1 );
-            else // slice or complete variable
-            {
-                // consider first variable of the slice
-                int f = Cba_ObjFanin( p, b-1 );
-                assert( Cba_ObjNameType(p, f) != CBA_NAME_BIN );
-                if ( Cba_ObjNameType(p, f) == CBA_NAME_INDEX || Cba_ObjGetRange(p, f) != b - e ) // slice
-                    Cba_ManWriteRange( p, Cba_ManFindRealIndex(p, f), Cba_ManFindRealIndex(p, Cba_ObjFanin(p, e)) );
-                // else this is complete variable
-            }
-            e = b;
-        }
+        Vec_StrPrintStr( vStr, i ? ", " : "" );
+        Cba_ManWriteFonName( p, iFon, 1 );
     }
-    else assert( 0 );
-    Vec_StrPrintStr( vStr, "}" );
+    Vec_StrPush( vStr, '}' );
 }
-static inline void Cba_ManWriteGate( Cba_Ntk_t * p, int iObj )
+int Cba_ManWriteLineFile( Cba_Ntk_t * p, int iObj, int FileAttr, int LineAttr )
 {
-    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();
-    Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pGateName, NULL );
-    Vec_StrPrintStr( vStr, "  " );
-    Vec_StrPrintStr( vStr, pGateName );
-    Vec_StrPrintStr( vStr, " " );
-    Vec_StrPrintStr( vStr, Cba_ObjName(p, iObj) ? Cba_ObjNameStr(p, iObj) : "" );
-    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_Str_t * vStr = &p->pDesign->vOut;
+    int FileId = 0, LineId = 0;
+    if ( FileAttr && (FileId = Cba_ObjAttrValue(p, iObj, FileAttr)) )
     {
-        Vec_StrPrintStr( vStr, Cba_BoxBiNum(p, iObj) ? ", ." : "." );
-        Vec_StrPrintStr( vStr, Mio_GateReadOutName(pGate) );
-        Vec_StrPrintStr( vStr, "(" );
-        Cba_ManWriteSig( p, iTerm );
-        Vec_StrPrintStr( vStr, ")" );
+        LineId = Cba_ObjAttrValue(p, iObj, LineAttr);
+        Vec_StrPrintStr( vStr, "  // " );
+        Vec_StrPrintStr( vStr, Cba_NtkStr(p, FileId) );
+        Vec_StrPush( vStr, '(' );
+        Vec_StrPrintNum( vStr, LineId );
+        Vec_StrPush( vStr, ')' );
+        return 1;
     }
-    Vec_StrPrintStr( vStr, ");\n" );
+    return 0;
 }
-static inline void Cba_ManWriteAssign( Cba_Ntk_t * p, int iObj )
+void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
 {
-    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 )
+    Vec_Str_t * vStr = &p->pDesign->vOut;
+    int i, iObj, iFin, iFon, StartPos, Status;
+    int FileAttr = Cba_NtkStrId( p, "file" );
+    int LineAttr = Cba_NtkStrId( p, "line" );
+    int fUseNewLine = (int)(Cba_NtkPioNum(p) > 5);
+    // mark PO fons
+    Vec_Bit_t * vPoFons = Vec_BitStart( Cba_NtkFonNum(p)+1 );
+    Cba_NtkForEachPoDriverFon( p, iObj, iFon, i )
+        if ( Cba_FonIsReal(iFon) )
+            Vec_BitWriteEntry( vPoFons, iFon, 1 );
+    // write header
+    Vec_StrPrintStr( vStr, "module " );
+    Vec_StrPrintStr( vStr, Cba_NtkName(p) );
+    Vec_StrPrintStr( vStr, fUseNewLine ? " (\n    " : " ( " );
+    StartPos = Vec_StrSize(vStr);
+    Cba_NtkForEachPioOrder( p, iObj, i )
     {
-        if ( Type == CBA_BOX_INV )
-            Vec_StrPrintStr( vStr, "~" );
-        else assert( Type == CBA_BOX_BUF );
-        Cba_ManWriteSig( p, iObj - 1 );
+        Vec_StrPrintStr( vStr, i ? ", " : "" );
+        if ( Vec_StrSize(vStr) > StartPos + 70 )
+        {
+            StartPos = Vec_StrSize(vStr);
+            Vec_StrPrintStr( vStr, "\n    " );
+        }
+        Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iObj) );
     }
-    else if ( nInputs == 2 )
+    Vec_StrPrintStr( vStr, fUseNewLine ? "\n  );" : " );" );
+    Cba_ManWriteLineFile( p, 0, FileAttr, LineAttr );
+    Vec_StrPrintStr( vStr, fUseNewLine ? "\n" : "\n\n" );
+    // write inputs/outputs
+    Cba_NtkForEachPioOrder( p, iObj, i )
     {
-        if ( Type == CBA_BOX_NAND || Type == CBA_BOX_NOR || Type == CBA_BOX_XNOR || Type == CBA_BOX_SHARPL )
-            Vec_StrPrintStr( vStr, "~" );
-        Cba_ManWriteSig( p, iObj - 1 );
-        if ( Type == CBA_BOX_AND || Type == CBA_BOX_SHARPL )
-            Vec_StrPrintStr( vStr, " & " );
-        else if ( Type == CBA_BOX_SHARP || Type == CBA_BOX_NOR )
-            Vec_StrPrintStr( vStr, " & ~" );
-        else if ( Type == CBA_BOX_OR )
-            Vec_StrPrintStr( vStr, " | " );
-        else if ( Type == CBA_BOX_NAND )
-            Vec_StrPrintStr( vStr, " | ~" );
-        else if ( Type == CBA_BOX_XOR || Type == CBA_BOX_XNOR )
-            Vec_StrPrintStr( vStr, " ^ " );
-        else assert( 0 );
-        Cba_ManWriteSig( p, iObj - 2 );
+        Vec_StrPrintStr( vStr, "  " );
+        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_ObjNameStr(p, iObj) );
+        Vec_StrPush( vStr, ';' );
+        Cba_ManWriteLineFile( p, iObj, FileAttr, LineAttr );
+        Vec_StrPush( vStr, '\n' );
     }
-    Vec_StrPrintStr( vStr, ";\n" );
-}
-void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p, int fUseAssign )
-{
-    Vec_Str_t * vStr = p->pDesign->vOut;
-    int iObj, k, i, o, StartPos;
-    Cba_NtkForEachBox( p, iObj ) // .subckt/.gate/box (formal/actual binding) 
+    Vec_StrPrintStr( vStr, "\n" );
+    // write objects
+    Cba_NtkForEachBox( p, iObj )
     {
-        // skip constants
-        if ( Cba_ObjIsConst(p, iObj) )
+        if ( Cba_ObjIsSlice(p, iObj) )
             continue;
-        // write mapped
-        if ( Cba_ObjIsGate(p, iObj) )
-        {
-            Cba_ManWriteGate( p, iObj );
-            continue;
-        }
-        // write primitives as assign-statements
-        if ( !Cba_ObjIsBoxUser(p, iObj) && fUseAssign )
-        {
-            Cba_ManWriteAssign( p, iObj );
+        if ( fInlineConcat && Cba_ObjIsConcat(p, iObj) )
             continue;
-        }
-        // write header
-        StartPos = Vec_StrSize(vStr);
         if ( Cba_ObjIsBoxUser(p, iObj) )
         {
-            int Value, Beg, End, Range;
-            Cba_Ntk_t * pModel = Cba_BoxNtk( p, iObj );
+            Cba_Ntk_t * pNtk = Cba_ObjNtk(p, iObj);
+            // write output wire declarations
+            Cba_ObjForEachFon( p, iObj, iFon, i )
+            {
+                Vec_StrPrintStr( vStr, "  wire " );
+                Cba_ManWriteFonRange( p, iFon );
+                Cba_ManWriteFonName( p, iFon, 0 );
+                Vec_StrPrintStr( vStr, ";\n" );
+            }
+            // write box
             Vec_StrPrintStr( vStr, "  " );
-            Vec_StrPrintStr( vStr, Cba_NtkName(pModel) );
-            Vec_StrPrintStr( vStr, " " );
-            Vec_StrPrintStr( vStr, Cba_ObjName(p, iObj) ? Cba_ObjNameStr(p, iObj) : ""  );
-            Vec_StrPrintStr( vStr, " (" );
-            // write arguments
-            i = o = 0;
-            assert( Cba_NtkInfoNum(pModel) );
-            Vec_IntForEachEntryTriple( &pModel->vInfo, Value, Beg, End, k )
+            Vec_StrPrintStr( vStr, Cba_NtkName(pNtk) );
+            Vec_StrPush( vStr, ' ' );
+            if ( Cba_ObjName(p, iObj) )
+                Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iObj) ),
+                Vec_StrPush( vStr, ' ' );
+            // write input binding
+            Vec_StrPrintStr( vStr, "( " );
+            Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
             {
-                int NameId = Abc_Lit2Var2( Value );
-                int Type = Abc_Lit2Att2( Value );
-                Vec_StrPrintStr( vStr, k ? ", " : "" );
-                if ( Vec_StrSize(vStr) > StartPos + 70 )
-                {
-                    StartPos = Vec_StrSize(vStr);
-                    Vec_StrPrintStr( vStr, "\n    " );
-                }
-                Vec_StrPrintStr( vStr, "." );
-                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, ")" );
+                Vec_StrPrintStr( vStr, i ? ", " : "" );
+                Vec_StrPush( vStr, '.' );
+                Vec_StrPrintStr( vStr, Cba_ObjNameStr(pNtk, Cba_NtkPi(pNtk, i)) );
+                Vec_StrPush( vStr, '(' );
+                Cba_ManWriteFonName( p, iFon, fInlineConcat );
+                Vec_StrPush( vStr, ')' );
+            }
+            // write output binding
+            Cba_ObjForEachFon( p, iObj, iFon, i )
+            {
+                Vec_StrPrintStr( vStr, Cba_ObjFinNum(p, iObj) ? ", " : "" );
+                Vec_StrPush( vStr, '.' );
+                Vec_StrPrintStr( vStr, Cba_ObjNameStr(pNtk, Cba_NtkPo(pNtk, i)) );
+                Vec_StrPush( vStr, '(' );
+                Cba_ManWriteFonName( p, iFon, 0 );
+                Vec_StrPush( vStr, ')' );
             }
-            assert( i == Cba_BoxBiNum(p, iObj) );
-            assert( o == Cba_BoxBoNum(p, iObj) );
+            Vec_StrPrintStr( vStr, ");" );
         }
         else
         {
-            int iTerm, k, Range, iSig = 0;
-            Vec_Int_t * vBits = Cba_BoxCollectRanges( p, iObj );
-            char * pName = Cba_NtkGenerateName( p, Cba_ObjType(p, iObj), vBits );
-            char * pSymbs = Cba_ManPrimSymb( p->pDesign, Cba_ObjType(p, iObj) );
-            Vec_StrPrintStr( vStr, "  " );
-            Vec_StrPrintStr( vStr, pName );
-            Vec_StrPrintStr( vStr, " " );
-            Vec_StrPrintStr( vStr, Cba_ObjName(p, iObj) ? Cba_ObjNameStr(p, iObj) : ""  );
-            Vec_StrPrintStr( vStr, " (" );
-            // write inputs
-            Cba_BoxForEachBiMain( p, iObj, iTerm, k )
+            int Type = Cba_ObjType(p, iObj);
+            if ( Vec_BitEntry(vPoFons, Cba_ObjFon0(p, iObj)) )
+                Vec_StrPrintStr( vStr, "  assign " );
+            else
+            {
+                Vec_StrPrintStr( vStr, "  wire " );
+                Cba_ManWriteFonRange( p, Cba_ObjFon0(p, iObj) );
+            }
+            Cba_ManWriteFonName( p, Cba_ObjFon0(p, iObj), 0 );
+            Vec_StrPrintStr( vStr, " = " );
+            if ( Cba_ObjIsConcat(p, iObj) )
+                Cba_ManWriteConcat( p, iObj );
+            else if ( Type == CBA_BOX_MUX || Type == CBA_BOX_NMUX )
+            {
+                char * pSymb = Type == CBA_BOX_MUX ? " ? " : " ?? ";
+                Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
+                {
+                    Vec_StrPrintStr( vStr, i ? (i == 1 ? pSymb: " : ") : "" );
+                    Cba_ManWriteFonName( p, iFon, fInlineConcat );
+                }
+            }
+            else if ( Type == CBA_BOX_SEL || Type == CBA_BOX_PSEL )
             {
-                Range = Vec_IntEntry( vBits, iSig );
-                Vec_StrPrintStr( vStr, iSig ? ", " : "" );
-                if ( Vec_StrSize(vStr) > StartPos + 70 )
+                char * pSymb = Type == CBA_BOX_SEL ? " ?| " : " ?% ";
+                Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
                 {
-                    StartPos = Vec_StrSize(vStr);
-                    Vec_StrPrintStr( vStr, "\n    " );
+                    Vec_StrPrintStr( vStr, i ? (i == 1 ? pSymb: " : ") : "" );
+                    Cba_ManWriteFonName( p, iFon, fInlineConcat );
                 }
-                Vec_StrPrintStr( vStr, "." );
-                Vec_StrPush( vStr, pSymbs[iSig] );
-                Vec_StrPrintStr( vStr, "(" );
-                Cba_ManWriteConcat( p, iTerm, Range );
-                Vec_StrPrintStr( vStr, ")" );
-                iSig++;
             }
-            Cba_BoxForEachBoMain( p, iObj, iTerm, k )
+            else if ( Cba_TypeIsUnary(Type) )
+            {
+                Vec_StrPrintStr( vStr, Cba_NtkTypeName(p, Type) );
+                Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat );
+            }
+            else // binary operation
             {
-                Range = Vec_IntEntry( vBits, iSig );
-                Vec_StrPrintStr( vStr, iSig ? ", " : "" );
-                if ( Vec_StrSize(vStr) > StartPos + 70 )
+                Vec_StrPush( vStr, ' ' );
+                Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat );
+                Vec_StrPush( vStr, ' ' );
+                Vec_StrPrintStr( vStr, Cba_NtkTypeName(p, Type) );
+                Vec_StrPush( vStr, ' ' );
+                Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 1), fInlineConcat );
+                if ( Type == CBA_BOX_ADD )
                 {
-                    StartPos = Vec_StrSize(vStr);
-                    Vec_StrPrintStr( vStr, "\n    " );
+                    Vec_StrPush( vStr, ' ' );
+                    Vec_StrPrintStr( vStr, Cba_NtkTypeName(p, Type) );
+                    Vec_StrPush( vStr, ' ' );
+                    Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 2), fInlineConcat );
                 }
-                Vec_StrPrintStr( vStr, "." );
-                Vec_StrPush( vStr, pSymbs[iSig] );
-                Vec_StrPrintStr( vStr, "(" );
-                Cba_ManWriteConcat( p, iTerm, Range );
-                Vec_StrPrintStr( vStr, ")" );
-                iSig++;
             }
-            assert( iSig == Vec_IntSize(vBits) );
+            Vec_StrPush( vStr, ';' );
         }
-        Vec_StrPrintStr( vStr, ");\n" );
-    }
-}
-void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fUseAssign )
-{
-    char * pKeyword[4] = { "wire ", "input ", "output ", "inout " };
-    Vec_Str_t * vStr = p->pDesign->vOut;
-    int k, iObj, iTerm, Value, Beg, End, Length, fHaveWires, StartPos;
-//    assert( Cba_NtkInfoNum(p) );
-    assert( Vec_IntSize(&p->vFanin) == Cba_NtkObjNum(p) );
-//    Cba_NtkPrint( p );
-    // write header
-    Vec_StrPrintStr( vStr, "module " );
-    Vec_StrPrintStr( vStr, Cba_NtkName(p) );
-    Vec_StrPrintStr( vStr, " (\n    " );
-    StartPos = Vec_StrSize(vStr);
-    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
-    if ( Abc_Lit2Att2(Value) != 0 )
-    {
-        Vec_StrPrintStr( vStr, k ? ", " : "" );
-        if ( Vec_StrSize(vStr) > StartPos + 70 )
+        // write attributes
+        Status = Cba_ManWriteLineFile( p, iObj, FileAttr, LineAttr );
+        if ( !Cba_ObjIsBoxUser(p, iObj) && Cba_ObjName(p, iObj) )
         {
-            StartPos = Vec_StrSize(vStr);
-            Vec_StrPrintStr( vStr, "\n    " );
+            if ( !Status )
+                Vec_StrPrintStr( vStr, "  //" );
+            Vec_StrPrintStr( vStr, " name=" );
+            Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iObj) );
         }
-        Cba_ManWriteVar( p, Abc_Lit2Var2(Value) );
+        Vec_StrPush( vStr, '\n' );
     }
-    Vec_StrPrintStr( vStr, "\n  );\n" );
-    // write inputs/outputs
-    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
-    if ( Abc_Lit2Att2(Value) != 0 )
+    // write remaining outputs
+    Cba_NtkForEachPo( p, iObj, i )
     {
-        Vec_StrPrintStr( vStr, "  " );
-        Vec_StrPrintStr( vStr, pKeyword[Abc_Lit2Att2(Value)] );
-        if ( Beg >= 0 )
-            Cba_ManWriteRange( p, Beg, End );
-        Cba_ManWriteVar( p, Abc_Lit2Var2(Value) );
-        Vec_StrPrintStr( vStr, ";\n" );
-    }
-    Vec_StrPrintStr( vStr, "\n" );
-    // write word-level wires
-    Cba_NtkForEachBox( p, iObj )
-    if ( !Cba_ObjIsConst(p, iObj) )
-        Cba_BoxForEachBo( p, iObj, iTerm, k )
-        if ( Cba_ObjNameType(p, iTerm) == CBA_NAME_WORD || Cba_ObjNameType(p, iTerm) == CBA_NAME_INFO )
-        {
-            Vec_StrPrintStr( vStr, "  wire " );
-            Cba_ManWriteRange( p, Cba_ManFindRealIndex(p, iTerm), Cba_ManFindRealIndex(p, iTerm + Cba_ObjGetRange(p, iTerm) - 1) );
-            Cba_ManWriteVar( p, Cba_ManFindRealNameId(p, iTerm) );
-            Vec_StrPrintStr( vStr, ";\n" );
-        }
-    // check if there are any wires left
-    fHaveWires = 0;
-    Cba_NtkForEachBox( p, iObj )
-    if ( !Cba_ObjIsConst(p, iObj) )
-        Cba_BoxForEachBo( p, iObj, iTerm, k )
-        if ( Cba_ObjNameType(p, iTerm) == CBA_NAME_BIN )
-        { fHaveWires = 1; iObj = Cba_NtkObjNum(p); break; }
-    // write bit-level wires
-    if ( fHaveWires )
-    {
-        Length = 7;
-        Vec_StrPrintStr( vStr, "\n  wire " );
-        Cba_NtkForEachBox( p, iObj )
-        if ( !Cba_ObjIsConst(p, iObj) )
-            Cba_BoxForEachBo( p, iObj, iTerm, k )
-            if ( Cba_ObjNameType(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" );
+        iFon = Cba_ObjFinFon(p, iObj, 0);
+        if ( !Cba_FonIsConst(iFon) && Cba_FonName(p, iFon) == Cba_ObjName(p, iObj) ) // already written
+            continue;
+        Vec_StrPrintStr( vStr, "  assign " );
+        Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iObj) );
+        Vec_StrPrintStr( vStr, " = " );
+        Cba_ManWriteFonName( p, iFon, fInlineConcat );
+        Vec_StrPush( vStr, ';' );
+        Vec_StrPush( vStr, '\n' );
     }
     Vec_StrPrintStr( vStr, "\n" );
-    // write objects
-    Cba_ManWriteVerilogBoxes( p, fUseAssign );
     Vec_StrPrintStr( vStr, "endmodule\n\n" );
+    Vec_BitFree( vPoFons );
 }
-void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fUseAssign )
+void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fInlineConcat )
 {
     Cba_Ntk_t * pNtk; int i;
     // check the library
@@ -667,35 +482,31 @@ void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fUseAssign )
         printf( "Genlib library used in the mapped design is not longer a current library.\n" );
         return;
     }
+    Cba_ManCreatePrimMap( p->pTypeNames );
     // derive the stream
-    p->vOut = Vec_StrAlloc( 10000 );
-    p->vOut2 = Vec_StrAlloc( 1000 );
-    Vec_StrPrintStr( p->vOut, "// Design \"" );
-    Vec_StrPrintStr( p->vOut, Cba_ManName(p) );
-    Vec_StrPrintStr( p->vOut, "\" written via CBA package in ABC on " );
-    Vec_StrPrintStr( p->vOut, Extra_TimeStamp() );
-    Vec_StrPrintStr( p->vOut, "\n\n" );
-    Cba_ManAssignInternWordNames( p );
+    Vec_StrClear( &p->vOut );
+    Vec_StrClear( &p->vOut2 );
+    Vec_StrPrintStr( &p->vOut, "// Design \"" );
+    Vec_StrPrintStr( &p->vOut, Cba_ManName(p) );
+    Vec_StrPrintStr( &p->vOut, "\" written via CBA package in ABC on " );
+    Vec_StrPrintStr( &p->vOut, Extra_TimeStamp() );
+    Vec_StrPrintStr( &p->vOut, "\n\n" );
     Cba_ManForEachNtk( p, pNtk, i )
-        Cba_ManWriteVerilogNtk( pNtk, fUseAssign );
+        Cba_ManWriteVerilogNtk( pNtk, fInlineConcat );
     // dump into file
-    if ( p->vOut && Vec_StrSize(p->vOut) > 0 )
+    if ( 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 );
+            fwrite( Vec_StrArray(&p->vOut), 1, Vec_StrSize(&p->vOut), pFile );
             fclose( pFile );
         }
     }
-    Vec_StrFreeP( &p->vOut );
-    Vec_StrFreeP( &p->vOut2 );
 }
 
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////