Several improvements to CBA data-structure.

5 files changed, 334 insertions, 211 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index c9dd98b7..33030f35 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -131,10 +131,10 @@ typedef enum {
 
 // 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_NAME_BIN = 0,        // 0:  binary variable
+    CBA_NAME_WORD,           // 1:  first bit of word-level variable
+    CBA_NAME_INFO,           // 2:  first bit of special variable
+    CBA_NAME_INDEX,          // 3:  index of word-level variable
 } Cba_NameType_t; 
 
 
@@ -273,6 +273,7 @@ static inline int            Cba_ObjIsCi( Cba_Ntk_t * p, int i )             { r
 static inline int            Cba_ObjIsCo( Cba_Ntk_t * p, int i )             { return Cba_ObjIsPo(p, i) || Cba_ObjIsBi(p, i);                                              }
 static inline int            Cba_ObjIsCio( Cba_Ntk_t * p, int i )            { return Cba_ObjType(p, i) < CBA_OBJ_BOX;                                                     }
 static inline int            Cba_ObjIsConst( Cba_Ntk_t * p, int i )          { return Cba_ObjType(p, i) >= CBA_BOX_CF && Cba_ObjType(p, i) <= CBA_BOX_CZ;                  }
+static inline int            Cba_ObjIsConstBin( Cba_Ntk_t * p, int i )       { return Cba_ObjType(p, i) == CBA_BOX_CF || Cba_ObjType(p, i) == CBA_BOX_CT;                  }
 
 static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vFanin, i);                              }
 static inline int            Cba_ObjIndex( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsCio(p, i)); return Vec_IntEntry(&p->vIndex, i);                             }
@@ -291,7 +292,7 @@ static inline void           Cba_ObjSetFanin( Cba_Ntk_t * p, int i, int x )  { a
 static inline void           Cba_ObjSetIndex( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIndex(p, i) == -1); Vec_IntSetEntry( &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_IntSetEntry( &p->vName, i, x );   }
 static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1);  Vec_IntSetEntry( &p->vCopy,  i, x );                      }
-static inline int            Cba_ObjGetConst( Cba_Ntk_t * p, int i )         { int f = Cba_ObjFanin(p, i); return Cba_ObjIsBo(p, f) && Cba_ObjIsConst(p, f-1) ? -Cba_ObjType(p, f-1) : 0;   }
+static inline int            Cba_ObjGetConst( Cba_Ntk_t * p, int i )         { assert(Cba_ObjIsCi(p, i)); return Cba_ObjIsBo(p, i) && Cba_ObjIsConst(p, i-1) ? Cba_ObjType(p, i-1) : 0;              }
 
 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;  }
 static inline int            Cba_BoxBoNum( Cba_Ntk_t * p, int i )            { int s = i+1; assert(Cba_ObjIsBox(p, i)); while (++i < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, i)); return i - s;  }
@@ -403,32 +404,19 @@ static inline int Cba_NtkReadRangesUser( Cba_Ntk_t * p, Vec_Int_t * vRanges, int
     }
     return Count;
 }
-static inline int Cba_ObjGetRange( Cba_Ntk_t * p, int iObj, int * pBeg, int * pEnd )
+static inline int Cba_ObjGetRange( Cba_Ntk_t * p, int iObj )
 {
-    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 );
+    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;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cba/cbaCba.c b/src/base/cba/cbaCba.c
index f7e7d2ba..d7bcb562 100644
--- a/src/base/cba/cbaCba.c
+++ b/src/base/cba/cbaCba.c
@@ -144,7 +144,7 @@ Cba_Man_t * Cba_ManReadCbaInt( Vec_Str_t * vOut )
             Cba_ManFree( p );
             return NULL;
         }
-        assert( Num1 > 0 && Num2 > 0 && Num3 > 0 );
+        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 );
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 15aacd2e..f899488f 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -102,24 +102,21 @@ void Cba_ManDeriveFanout( Cba_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cba_ManAssignInternTwo( Cba_Ntk_t * p, int iNum, Vec_Int_t * vMap )
+int Cba_ManAssignInternTwo( Cba_Ntk_t * p, int iNum, int nDigits, int fPis, Vec_Int_t * vMap )
 {
-    char Buffer[16];
-    int i = 0, NameId, nDigits;
-    do
+    char Buffer[16]; int i, NameId = 0;
+    for ( i = 0; !NameId || Vec_IntEntry(vMap, NameId); i++ )
     {
-        nDigits = Abc_Base10Log( Cba_NtkObjNum(p) );
         if ( i == 0 )
-            sprintf( Buffer, "%s%0*d", "n", nDigits, iNum );
+            sprintf( Buffer, "%s%0*d", fPis ? "i" : "n", nDigits, iNum );
         else
-            sprintf( Buffer, "%s%0*d_%d", "n", nDigits, iNum, ++i );
+            sprintf( Buffer, "%s%0*d_%d", fPis ? "i" : "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 )
+void Cba_ManPrepareBitNames( Cba_Ntk_t * p, Vec_Int_t * vMap, int * pnNames, int nDigits, int fPis, Vec_Int_t * vRanges, Vec_Int_t * vNames )
 {
     int i, k, Range;
     Vec_IntClear( vNames );
@@ -127,18 +124,40 @@ void Cba_ManPrepareBitNames( Cba_Ntk_t * p, Vec_Int_t * vMap, int * pnNames, Vec
     {
         assert( Range > 0 );
         if ( Range == 1 )
-            Vec_IntPush( vNames, Abc_Var2Lit2( Cba_ManAssignInternTwo(p, (*pnNames)++, vMap), CBA_NAME_BIN ) );
+            Vec_IntPush( vNames, Abc_Var2Lit2( Cba_ManAssignInternTwo(p, (*pnNames)++, nDigits, fPis, vMap), CBA_NAME_BIN ) );
         else
         {
-            Vec_IntPush( vNames, Abc_Var2Lit2( Cba_ManAssignInternTwo(p, (*pnNames)++, vMap), CBA_NAME_WORD ) );
+            Vec_IntPush( vNames, Abc_Var2Lit2( Cba_ManAssignInternTwo(p, (*pnNames)++, nDigits, fPis, 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 Cba_ManAssignCountNames( Cba_Ntk_t * p )
+{
+    int iBox, Counter = 1;
+    Vec_Int_t * vRanges = &p->pDesign->pNtks->vArray;
+    Cba_NtkReadRangesUser( p, vRanges, 0 );
+    Counter += Vec_IntSize(vRanges);
+    Cba_NtkReadRangesUser( p, vRanges, 1 );
+    Counter += Vec_IntSize(vRanges);
+    Cba_NtkForEachBox( p, iBox )
+    {
+        if ( Cba_ObjIsBoxUser(p, iBox) )
+            Cba_NtkReadRangesUser( Cba_BoxNtk(p, iBox), vRanges, 1 );
+        else if ( Cba_BoxNtkId(p, iBox) )
+            Cba_NtkReadRangesPrim( Cba_BoxNtkName(p, iBox), vRanges, 1 );
+        else assert( 0 );
+        Counter += Vec_IntSize(vRanges);
+    }
+    return Counter;
+}
+void Cba_ManAssignInternWordNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap )
 {
-    int k, n = 0, iObj, iTerm, nNames = 1;
+    Vec_Int_t * vRanges = &p->pDesign->pNtks->vArray;
+    Vec_Int_t * vNames  = &p->pDesign->pNtks->vArray2;
+    int k, nPis = 0, nPos = 0, iObj, iTerm, nNames = 1;
+    int nDigits = Abc_Base10Log( Cba_ManAssignCountNames(p) );
     assert( Cba_NtkReadRangesUser(p, NULL, 0) == Cba_NtkPiNum(p) );
     assert( Cba_NtkReadRangesUser(p, NULL, 1) == Cba_NtkPoNum(p) );
     // start names
@@ -146,15 +165,10 @@ void Cba_ManAssignInternWordNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t
     Cba_NtkStartNames(p);
     // derive PI names
     Cba_NtkReadRangesUser( p, vRanges, 0 );
-    Cba_ManPrepareBitNames( p, vMap, &nNames, vRanges, vNames );
+    Cba_ManPrepareBitNames( p, vMap, &nNames, nDigits, 1, 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 )
     {
@@ -163,25 +177,43 @@ void Cba_ManAssignInternWordNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t
         else if ( Cba_BoxNtkId(p, iObj) )
             Cba_NtkReadRangesPrim( Cba_BoxNtkName(p, iObj), vRanges, 1 );
         else assert( 0 );
-        Cba_ManPrepareBitNames( p, vMap, &nNames, vRanges, vNames );
+        Cba_ManPrepareBitNames( p, vMap, &nNames, nDigits, 0, 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) );
+    // transfer names to the interface
+//    Cba_NtkReadRangesUser( p, vRanges, 1 );
+    for ( k = 0; k < Cba_NtkInfoNum(p); k++ )
+    {
+        char * pName = Cba_NtkName(p);
+        if ( Cba_NtkInfoType(p, k) == 1 ) // PI
+        {
+            iObj = Cba_NtkPi(p, nPis);
+            assert( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD );
+            Cba_NtkSetInfoName( p, k, Abc_Var2Lit2(Cba_ObjNameId(p, iObj), 1) );
+            nPis += Cba_NtkInfoRange(p, k);
+        }
+        else if ( Cba_NtkInfoType(p, k) == 2 ) // PO
+        {
+            iObj = Cba_NtkPo(p, nPos);
+            iObj = Cba_ObjFanin(p, iObj);
+            assert( Cba_ObjNameType(p, iObj) <= CBA_NAME_WORD );
+            Cba_NtkSetInfoName( p, k, Abc_Var2Lit2(Cba_ObjNameId(p, iObj), 2) );
+            nPos += Cba_NtkInfoRange(p, k);
+        }
+        else assert( 0 );
+    }
+    assert( nPis == Cba_NtkPiNum(p) );
+    assert( nPos == Cba_NtkPoNum(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 );
+            Vec_IntWriteEntry( vMap, Cba_ObjNameId(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 );
+                Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iTerm), 0 );
     printf( "Generated %d word-level names.\n", nNames-1 );
 //    Vec_IntPrint( &p->vName );
 //    Vec_IntPrint( &p->vInfo );
@@ -189,14 +221,10 @@ void Cba_ManAssignInternWordNamesNtk( Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t
 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 );
+        Cba_ManAssignInternWordNamesNtk( pNtk, vMap );
     Vec_IntFree( vMap );
-    Vec_IntFree( vRanges );
-    Vec_IntFree( vNames );
 }
 
 
@@ -470,10 +498,10 @@ Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p )
     {
         Cba_NtkStartNames( pRootNew );
         Cba_NtkForEachPi( pRoot, iObj, i )
-            Cba_ObjSetName( pRootNew, Cba_NtkPi(pRootNew, i), Cba_ObjName(pRoot, iObj) );
+            Cba_ObjSetName( pRootNew, Cba_NtkPi(pRootNew, i), Cba_ObjNameId(pRoot, iObj) );
         Cba_NtkForEachPoDriver( pRoot, iObj, i )
             if ( !Cba_ObjIsPi(pRoot, iObj) )
-                Cba_ObjSetName( pRootNew, Cba_ObjCopy(pRoot, iObj), Cba_ObjName(pRoot, iObj) );
+                Cba_ObjSetName( pRootNew, Cba_ObjCopy(pRoot, iObj), Cba_ObjNameId(pRoot, iObj) );
     }
     return pNew;
 }
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index 16051a43..5bf42759 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -191,152 +191,194 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
   SeeAlso     []
 
 ***********************************************************************/
+void Cba_ManWriteVar( Cba_Ntk_t * p, int RealName )
+{
+    Vec_StrPrintStr( p->pDesign->vOut, Cba_NtkStr(p, RealName) );
+}
 void Cba_ManWriteRange( Cba_Ntk_t * p, int Beg, int End )
 {
     Vec_Str_t * vStr = p->pDesign->vOut;
     Vec_StrPrintStr( vStr, "[" );
-    Vec_StrPrintNum( vStr, End );
-    Vec_StrPrintStr( vStr, ":" );
+    if ( End >= 0 )
+    {
+        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 )
+void Cba_ManWriteConstBit( Cba_Ntk_t * p, int iObj, int fHead )
 {
     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, "]" );
+    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 );
 }
-void Cba_ManWriteSig( Cba_Ntk_t * p, int iObj )
+int Cba_ManFindRealNameId( Cba_Ntk_t * p, int iObj )
 {
-    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 )
-    {
-        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 );
+    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);
 }
-/*
-void Cba_ManWriteSlices( Cba_Ntk_t * p, Vec_Int_t * vSigs )
+int Cba_ManFindRealIndex( Cba_Ntk_t * p, int iObj )
 {
-    int Entry, NameId, Beg, End, j;
-    Vec_Str_t * vStr = p->pDesign->vOut; 
-    Vec_StrClear( vStr );
-    Vec_StrPrintStr( vStr, "{" );
-    Vec_IntForEachEntry( vSigs, NameId, Beg )
+    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;
+}
+void Cba_ManWriteSig( Cba_Ntk_t * p, int iObj )
+{
+    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 );
+    else
     {
-        if ( Vec_StrEntryLast(vStr) != '{' )
-            Vec_StrPrintStr( vStr, ", " );
-        if ( NameId < 0 ) // constant
-        {
-            Vec_IntForEachEntryStart( vSigs, Entry, End, Beg+1 )
-                if ( Entry >= 0 )
-                    break;
-            Vec_StrPrintNum( vStr, End - Beg );
-            Vec_StrPrintStr( vStr, "b\'" );
-            Vec_IntForEachEntryStartStop( vSigs, NameId, j, Beg, End )
-            {
-                if ( -NameId == CBA_BOX_CF )
-                    Vec_StrPush( vStr, '0' );
-                else if ( -NameId == CBA_BOX_CT )
-                    Vec_StrPush( vStr, '1' );
-                else if ( -NameId == CBA_BOX_CX )
-                    Vec_StrPush( vStr, 'x' );
-                else if ( -NameId == CBA_BOX_CZ )
-                    Vec_StrPush( vStr, 'z' );
-                else assert( 0 );
-            }
-        }
-        else if ( Cba_NameType(NameId) == CBA_NAME_BIN ) // bin
-        {
-            Cba_ManWriteLit( p, Abc_Lit2Var2(NameId), -1 );
-        }
-        else if ( Cba_NameType(NameId) == CBA_NAME_WORD || Cba_NameType(NameId) == CBA_NAME_INDEX ) // word
+        int NameId = Cba_ObjName(p, iObj);
+        if ( Cba_NameType(NameId) == CBA_NAME_BIN )
+            Cba_ManWriteVar( p, Abc_Lit2Var2(NameId) );
+        else
         {
-            Vec_IntForEachEntryStart( vSigs, Entry, End, Beg+1 )
-                if ( Cba_NameType(Entry) != CBA_NAME_INDEX )
-                    break;
-            // the whole word is there
-            if ( Cba_NameType(NameId) == CBA_NAME_WORD && Cba_ObjGetRange(p, 0) == End - Beg )
-                Cba_ManWriteLit( p, Abc_Lit2Var2(NameId), -1 );
-            else if ( End - Beg == 1 )
-                Cba_ManWriteLit( p, Abc_Lit2Var2(NameId), Beg );
-            else
-            {
-                Cba_ManWriteLit( p, Abc_Lit2Var2(NameId), -1 );
-                Cba_ManWriteRange( p, Beg, End-1 );
-            }
+            Cba_ManWriteVar( p, Cba_ManFindRealNameId(p, iObj) );
+            Cba_ManWriteRange( p, Cba_ManFindRealIndex(p, iObj), -1 );
         }
-        else assert( 0 );
     }
-    Vec_StrPrintStr( vStr, "}" );
-    Vec_StrReverseOrder( vStr );
-    Vec_StrPush( vStr, '\0' );
+}
+void Cba_ManWriteConstant( Cba_Ntk_t * p, int iObj )
+{
 }
 void Cba_ManWriteConcat( Cba_Ntk_t * p, int iStart, int nObjs )
 {
-    Vec_Str_t * vStr = p->pDesign->vOut; int i;
+    Vec_Str_t * vStr = p->pDesign->vOut; 
     assert( nObjs >= 1 );
     if ( nObjs == 1 )
+    {
         Cba_ManWriteSig( p, iStart );
-    else
+        return;
+    }
+    Vec_StrPrintStr( vStr, "{" );
+    if ( Cba_ObjIsBo(p, iStart) ) // box output
     {
-        // collect fanins
-        Vec_IntClear( &p->vArray );
-        for ( i = 0; i < nObjs; i++ )
+        int i;
+        for ( i = iStart + nObjs - 1; i >= iStart; i-- )
         {
-            if ( Cba_ObjIsBo(p, iStart) )
-                Vec_IntPush( &p->vArray, iStart + i );
-            else if ( Cba_ObjIsBi(p, iStart) )
-            {
-                int iFanin = Cba_ObjFanin(p, iStart - i);
-                int Const  = Cba_ObjGetConst(p, iFanin);
-                Vec_IntPush( &p->vArray, Const ? Const : Cba_ObjName(p, iFanin) );
-            }
-            else assert( 0 );
+            if ( Cba_ObjNameType(p, i) == CBA_NAME_INDEX )
+                continue;
+            if ( Vec_StrEntryLast(vStr) != '{' )
+                Vec_StrPrintStr( vStr, ", " );
+            Cba_ManWriteVar( p, Cba_ManFindRealNameId(p, i) );
         }
-        ABC_SWAP( Vec_Str_t *, p->pDesign->vOut, p->pDesign->vOut2 );
-        Cba_ManWriteSlices( p, &p->vArray );
-        ABC_SWAP( Vec_Str_t *, p->pDesign->vOut, p->pDesign->vOut2 );
-        Vec_StrAppend( vStr, Vec_StrArray(p->pDesign->vOut2) );
     }
-}
-*/
-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
+    else if ( Cba_ObjIsBi(p, iStart) ) // box input
     {
-        Vec_StrPrintStr( vStr, "{" );
-        for ( i = nObjs - 1; i >= 0; i-- )
+        int e, b, k, NameId;
+        for ( e = iStart - nObjs + 1; e <= iStart; )
         {
-            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 );
+            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, "}" );
     }
+    else assert( 0 );
+    Vec_StrPrintStr( vStr, "}" );
 }
 void Cba_ManWriteGate( Cba_Ntk_t * p, int iObj )
 {
@@ -363,7 +405,7 @@ void Cba_ManWriteGate( Cba_Ntk_t * p, int iObj )
         Cba_ManWriteSig( p, iTerm );
         Vec_StrPrintStr( vStr, ")" );
     }
-    Vec_StrPrintStr( vStr, " );\n" );
+    Vec_StrPrintStr( vStr, ");\n" );
 }
 void Cba_ManWriteAssign( Cba_Ntk_t * p, int iObj )
 {
@@ -416,11 +458,14 @@ void Cba_ManWriteAssign( Cba_Ntk_t * p, int iObj )
 void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
 {
     Vec_Str_t * vStr = p->pDesign->vOut;
-    int iObj, k, i, o;
+    int iObj, k, i, o, StartPos;
     Cba_NtkForEachBox( p, iObj ) // .subckt/.gate/box (formal/actual binding) 
     {
         Cba_Ntk_t * pModel = NULL;
         char * pName = NULL;
+        // skip constants
+        if ( Cba_ObjIsConst(p, iObj) )
+            continue;
         // write mapped
         if ( Cba_ObjIsGate(p, iObj) )
         {
@@ -433,18 +478,17 @@ void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
             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 );
+        StartPos = Vec_StrSize(vStr);
         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, " (" );
@@ -456,7 +500,13 @@ void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
             {
                 int NameId = Abc_Lit2Var2( Value );
                 int Type = Abc_Lit2Att2( Value );
-                Vec_StrPrintStr( vStr, k ? ", ." : "." );
+                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 );
@@ -469,13 +519,19 @@ void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
                 Vec_StrPrintStr( vStr, ")" );
             }
         }
-        else
+        else 
         {
             int pRanges[8]; char pSymbs[8];
             int nSigs = Cba_NtkNameRanges( pName, pRanges, pSymbs );
             for ( k = 0; k < nSigs; k++ )
             {
-                Vec_StrPrintStr( vStr, k ? ", ." : "." );
+                Vec_StrPrintStr( vStr, k ? ", " : "" );
+                if ( Vec_StrSize(vStr) > StartPos + 70 )
+                {
+                    StartPos = Vec_StrSize(vStr);
+                    Vec_StrPrintStr( vStr, "\n    " );
+                }
+                Vec_StrPrintStr( vStr, "." );
                 Vec_StrPush( vStr, pSymbs[k] );
                 Vec_StrPrintStr( vStr, "(" );
                 if ( k < nSigs - 1 )
@@ -485,7 +541,7 @@ void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
                 Vec_StrPrintStr( vStr, ")" );
             }
         }
-        Vec_StrPrintStr( vStr, " );\n" );
+        Vec_StrPrintStr( vStr, ");\n" );
         assert( i == Cba_BoxBiNum(p, iObj) );
         assert( o == Cba_BoxBoNum(p, iObj) );
     }
@@ -494,19 +550,25 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p )
 {
     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) );
+    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 ? ", " : "" );
-        Vec_StrPrintStr( vStr, Cba_NtkStr(p, Abc_Lit2Var2(Value)) );
+        if ( Vec_StrSize(vStr) > StartPos + 70 )
+        {
+            StartPos = Vec_StrSize(vStr);
+            Vec_StrPrintStr( vStr, "\n    " );
+        }
+        Cba_ManWriteVar( p, Abc_Lit2Var2(Value) );
     }
     Vec_StrPrintStr( vStr, "\n  );\n" );
     // write inputs/outputs
@@ -517,37 +579,48 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p )
         Vec_StrPrintStr( vStr, pKeyword[Abc_Lit2Att2(Value)] );
         if ( Beg >= 0 )
             Cba_ManWriteRange( p, Beg, End );
-        Vec_StrPrintStr( vStr, Cba_NtkStr(p, Abc_Lit2Var2(Value)) );
+        Cba_ManWriteVar( 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 )
+    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 )
         {
-            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) );
+            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" );
         }
-    // write bit-level wires
-    Length = 7;
-    Vec_StrPrintStr( vStr, "  wire " );
+    // check if there are any wires left
+    fHaveWires = 0;
     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" );
+    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" );
+    }
+    Vec_StrPrintStr( vStr, "\n" );
     // write objects
     Cba_ManWriteVerilogBoxes( p );
     Vec_StrPrintStr( vStr, "endmodule\n\n" );
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 51bd887e..479045f9 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -2532,6 +2532,40 @@ void Extra_NpnTest()
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_NtkPrintBin( word * pT, int nBits )
+{
+    int i;
+    for ( i = nBits - 1; i >= 0; i-- )
+        printf( "%d", (*pT >> (word)i) & 1 );
+}
+void Extra_NtkPowerTest()
+{
+    int i, j, k, n = 4;
+    for ( i = 0; i < (1<<n); i++ )
+    for ( j = 0; j < (1<<n); j++ )
+    {
+        word t = (word)i;
+        for ( k = 1; k < j; k++ )
+            t *= (word)i;
+        Extra_NtkPrintBin( (word *)&i, n );
+        Extra_NtkPrintBin( (word *)&j, n );
+        printf( " " );
+        Extra_NtkPrintBin( (word *)&t, 64 );
+        printf( "\n" );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////