Improvements to Cba data-structure.

6 files changed, 192 insertions, 201 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index bf060652..ab99514c 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -28,6 +28,7 @@
 #include "aig/gia/gia.h"
 #include "misc/extra/extra.h"
 #include "misc/util/utilNam.h"
+#include "misc/vec/vecHash.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -141,68 +142,67 @@ typedef struct Cba_Man_t_ Cba_Man_t;
 // network
 struct Cba_Ntk_t_
 {
-    Cba_Man_t *  pDesign;  // design
-    int          Id;       // network ID
-    int          NameId;   // name ID 
-    int          iCopy;    // copy module
-    unsigned     Mark : 1; // visit mark 
-    unsigned     fComb: 1; // the network is combinational
-    unsigned     fSeq : 1; // the network is sequential
+    Cba_Man_t *     pDesign;  // design
+    int             Id;       // network ID
+    int             NameId;   // name ID 
+    int             iCopy;    // copy module
+    unsigned        Mark : 1; // visit mark 
+    unsigned        fComb: 1; // the network is combinational
+    unsigned        fSeq : 1; // the network is sequential
     // interface
-    Vec_Int_t    vInputs;  // inputs 
-    Vec_Int_t    vOutputs; // outputs
-    Vec_Int_t    vOrder;   // order
-    Vec_Int_t    vSeq;     // sequential objects
+    Vec_Int_t       vInputs;  // inputs 
+    Vec_Int_t       vOutputs; // outputs
+    Vec_Int_t       vOrder;   // order
+    Vec_Int_t       vSeq;     // sequential objects
     // stucture
-    Vec_Str_t    vObjType; // type     
-    Vec_Int_t    vObjFin0; // fanins
-    Vec_Int_t    vObjFon0; // outputs
-    Vec_Int_t    vFinFon;  // fons
-    Vec_Int_t    vFonObj;  // object
+    Vec_Str_t       vObjType; // type     
+    Vec_Int_t       vObjFin0; // fanins
+    Vec_Int_t       vObjFon0; // outputs
+    Vec_Int_t       vFinFon;  // fons
+    Vec_Int_t       vFonObj;  // object
     // optional
-    Vec_Int_t    vObjCopy; // copy
-    Vec_Int_t    vObjFunc; // function
-    Vec_Int_t    vObjName; // name
-    Vec_Int_t    vObjAttr; // attribute offset
-    Vec_Int_t    vAttrSto; // attribute storage
-    Vec_Int_t    vFonCopy; // copy
-    Vec_Int_t    vFonName; // name
-    Vec_Int_t    vFonRange;// range
-    Vec_Int_t    vFonLeft; // left
-    Vec_Int_t    vFonRight;// right
-    Vec_Int_t    vFonPrev; // fanout: prev fon
-    Vec_Int_t    vFonNext; // fanout: next fon
-    Vec_Int_t    vFinFon0; // fanout: first fon
-    Vec_Int_t    vFinObj;  // object
-    Vec_Int_t    vNtkObjs; // instances
+    Vec_Int_t       vObjCopy; // copy
+    Vec_Int_t       vObjFunc; // function
+    Vec_Int_t       vObjName; // name
+    Vec_Int_t       vObjAttr; // attribute offset
+    Vec_Int_t       vAttrSto; // attribute storage
+    Vec_Int_t       vFonCopy; // copy
+    Vec_Int_t       vFonName; // name
+    Vec_Int_t       vFonRange;// range
+    Vec_Int_t       vFonPrev; // fanout: prev fon
+    Vec_Int_t       vFonNext; // fanout: next fon
+    Vec_Int_t       vFinFon0; // fanout: first fon
+    Vec_Int_t       vFinObj;  // object
+    Vec_Int_t       vNtkObjs; // instances
     // other
-    Vec_Ptr_t *  vOther;   // various data
-    Vec_Int_t    vArray0;
-    Vec_Int_t    vArray1;
+    Vec_Ptr_t *     vOther;   // various data
+    Vec_Int_t       vArray0;
+    Vec_Int_t       vArray1;
 };
 
 // design
 struct Cba_Man_t_
 {
     // design names
-    char *       pName;    // design name
-    char *       pSpec;    // spec file name
-    Abc_Nam_t *  pStrs;    // string manager
-    Abc_Nam_t *  pFuns;    // constant manager
-    Abc_Nam_t *  pMods;    // module name manager
-    Vec_Int_t    vNameMap; // mapping names
-    Vec_Int_t    vNameMap2;// mapping names
-    Vec_Int_t    vUsed;    // used map entries
-    Vec_Int_t    vUsed2;   // used map entries
-    char *       pTypeNames[CBA_BOX_LAST];
+    char *          pName;    // design name
+    char *          pSpec;    // spec file name
+    Abc_Nam_t *     pStrs;    // string manager
+    Abc_Nam_t *     pFuns;    // constant manager
+    Abc_Nam_t *     pMods;    // module name manager
+    Hash_IntMan_t * vHash; // variable ranges
+    Vec_Int_t       vNameMap; // mapping names
+    Vec_Int_t       vNameMap2;// mapping names
+    Vec_Int_t       vUsed;    // used map entries
+    Vec_Int_t       vUsed2;   // used map entries
+    char *          pTypeNames[CBA_BOX_LAST];
     // internal data
-    int          iRoot;    // root network
-    Vec_Ptr_t    vNtks;    // networks
+    int             iRoot;    // root network
+    Vec_Ptr_t       vNtks;    // networks
     // user data
-    int          nOpens;
-    Vec_Str_t    vOut;     
-    Vec_Str_t    vOut2;     
-    void *       pMioLib;
+    int             nOpens;
+    Vec_Str_t       vOut;     
+    Vec_Str_t       vOut2;     
+    void *          pMioLib;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -242,6 +242,10 @@ static inline char *         Cba_NtkTypeName( Cba_Ntk_t * p, int Type )      { r
 static inline int            Cba_NtkCopy( Cba_Ntk_t * p )                    { return p->iCopy;                                                                            }
 static inline Cba_Ntk_t *    Cba_NtkCopyNtk(Cba_Man_t * pNew, Cba_Ntk_t * p) { return Cba_ManNtk(pNew, Cba_NtkCopy(p));                                                    }
 static inline void           Cba_NtkSetCopy( Cba_Ntk_t * p, int i )          { assert(p->iCopy == 0); p->iCopy = i;                                                        }
+static inline int            Cba_NtkHashRange( Cba_Ntk_t * p, int l, int r ) { return Hash_Int2ManInsert( p->pDesign->vHash, l, r, 0 );                                    }
+static inline int            Cba_NtkRangeLeft( Cba_Ntk_t * p, int h )        { return h ? Hash_IntObjData0( p->pDesign->vHash, h ) : 0;                                    }
+static inline int            Cba_NtkRangeRight( Cba_Ntk_t * p, int h )       { return h ? Hash_IntObjData1( p->pDesign->vHash, h ) : 0;                                    }
+static inline int            Cba_NtkRangeSize( Cba_Ntk_t * p, int h )        { int l = Cba_NtkRangeLeft(p, h), r = Cba_NtkRangeRight(p, h); return 1 + (l > r ? l-r : r-l);}
 
 static inline int            Cba_NtkPiNum( Cba_Ntk_t * p )                   { return Vec_IntSize(&p->vInputs);                                                            }
 static inline int            Cba_NtkPoNum( Cba_Ntk_t * p )                   { return Vec_IntSize(&p->vOutputs);                                                           }
@@ -268,8 +272,6 @@ static inline void           Cba_NtkCleanObjAttrs( Cba_Ntk_t * p )           { V
 static inline void           Cba_NtkCleanFonCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonCopy, Vec_IntCap(&p->vFonObj),   0);        }
 static inline void           Cba_NtkCleanFonNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonName, Vec_IntCap(&p->vFonObj),   0);        }
 static inline void           Cba_NtkCleanFonRanges( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonRange,Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFonLefts( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonLeft, Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFonRights( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonRight,Vec_IntCap(&p->vFonObj),   0);        }
 static inline void           Cba_NtkCleanFonPrevs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonPrev, Vec_IntCap(&p->vFonObj),   0);        }
 static inline void           Cba_NtkCleanFonNexts( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonNext, Vec_IntCap(&p->vFonObj),   0);        }
 static inline void           Cba_NtkCleanFinFon0( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinFon0, Vec_IntCap(&p->vFinFon),   0);        }
@@ -282,8 +284,6 @@ static inline int            Cba_NtkHasObjAttrs( Cba_Ntk_t * p )             { r
 static inline int            Cba_NtkHasFonCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonCopy) > 0; }
 static inline int            Cba_NtkHasFonNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonName) > 0; }
 static inline int            Cba_NtkHasFonRanges( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonRange)> 0; }
-static inline int            Cba_NtkHasFonLefts( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonLeft) > 0; }
-static inline int            Cba_NtkHasFonRights( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonRight)> 0; }
 static inline int            Cba_NtkHasFonPrevs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonPrev) > 0; }
 static inline int            Cba_NtkHasFonNexts( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonNext) > 0; }
 static inline int            Cba_NtkHasFinFon0( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinFon0) > 0; }
@@ -296,8 +296,6 @@ static inline void           Cba_NtkFreeObjAttrs( Cba_Ntk_t * p )            { V
 static inline void           Cba_NtkFreeFonCopies( Cba_Ntk_t * p )           { Vec_IntErase(&p->vFonCopy);   }
 static inline void           Cba_NtkFreeFonNames( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonName);   }
 static inline void           Cba_NtkFreeFonRanges( Cba_Ntk_t * p )           { Vec_IntErase(&p->vFonRange);  }
-static inline void           Cba_NtkFreeFonLefts( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonLeft);   }
-static inline void           Cba_NtkFreeFonRights( Cba_Ntk_t * p )           { Vec_IntErase(&p->vFonRight);  }
 static inline void           Cba_NtkFreeFonPrevs( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonPrev);   }
 static inline void           Cba_NtkFreeFonNexts( Cba_Ntk_t * p )            { Vec_IntErase(&p->vFonNext);   }
 static inline void           Cba_NtkFreeFinFon0( Cba_Ntk_t * p )             { Vec_IntErase(&p->vFinFon0);   }
@@ -364,11 +362,11 @@ static inline int            Cba_FonFromConst( int c )                       { a
 static inline int            Cba_FonConstRange( Cba_Ntk_t * p, int f )       { assert(Cba_FonIsConst(f)); return atoi(Cba_NtkConst(p, Cba_FonConst(f)));                   }
 
 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, r; if (Cba_FonIsConst(f)) return Cba_FonConstRange(p, f); 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_FonRange( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Vec_IntGetEntry(&p->vFonRange, f):0;}
+static inline int            Cba_FonLeft( Cba_Ntk_t * p, int f )             { return Cba_NtkRangeLeft(p, Cba_FonRange(p, f));                                             }
+static inline int            Cba_FonRight( Cba_Ntk_t * p, int f )            { return Cba_NtkRangeRight(p, Cba_FonRange(p, f));                                            }
+static inline int            Cba_FonRangeSize( Cba_Ntk_t * p, int f )        { return Cba_FonIsConst(f) ? Cba_FonConstRange(p, f):Cba_NtkRangeSize(p, Cba_FonRange(p, f)); }
+static inline void           Cba_FonSetRange( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, 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 );                        }
@@ -535,8 +533,6 @@ static inline void Cba_NtkFree( Cba_Ntk_t * p )
     Vec_IntErase( &p->vFonCopy );    
     Vec_IntErase( &p->vFonName );    
     Vec_IntErase( &p->vFonRange );    
-    Vec_IntErase( &p->vFonLeft );    
-    Vec_IntErase( &p->vFonRight );    
     Vec_IntErase( &p->vFonPrev );    
     Vec_IntErase( &p->vFonNext );    
     Vec_IntErase( &p->vFinFon0 );    
@@ -720,8 +716,6 @@ static inline void Cba_NtkDupAttrs( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
     // transfer fon attributes
     Vec_IntRemapArray( &p->vFonCopy, &p->vFonName,  &pNew->vFonName,  Cba_NtkFonNum(pNew) + 1 );
     Vec_IntRemapArray( &p->vFonCopy, &p->vFonRange, &pNew->vFonRange, Cba_NtkFonNum(pNew) + 1 );
-    Vec_IntRemapArray( &p->vFonCopy, &p->vFonLeft,  &pNew->vFonLeft,  Cba_NtkFonNum(pNew) + 1 );
-    Vec_IntRemapArray( &p->vFonCopy, &p->vFonRight, &pNew->vFonRight, Cba_NtkFonNum(pNew) + 1 );
     // duplicate attributes
     Vec_IntAppend( &pNew->vAttrSto, &p->vAttrSto );
     pNew->vOther = p->vOther ? (Vec_Ptr_t *)Vec_VecDup( (Vec_Vec_t *)p->vOther ) : NULL;
@@ -749,8 +743,6 @@ static inline int Cba_NtkMemory( Cba_Ntk_t * p )
     nMem += (int)Vec_IntMemory(&p->vFonCopy );  
     nMem += (int)Vec_IntMemory(&p->vFonName );  
     nMem += (int)Vec_IntMemory(&p->vFonRange ); 
-    nMem += (int)Vec_IntMemory(&p->vFonLeft );  
-    nMem += (int)Vec_IntMemory(&p->vFonRight ); 
     nMem += (int)Vec_IntMemory(&p->vFonPrev );  
     nMem += (int)Vec_IntMemory(&p->vFonNext );  
     nMem += (int)Vec_IntMemory(&p->vFinFon0 );  
@@ -804,7 +796,7 @@ 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 * pFuns, Abc_Nam_t * pMods )
+static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t * pStrs, Abc_Nam_t * pFuns, Abc_Nam_t * pMods, Hash_IntMan_t * vHash )
 {
     Cba_Man_t * pNew = ABC_CALLOC( Cba_Man_t, 1 );
     pNew->pName = Extra_FileDesignName( pFileName );
@@ -812,6 +804,7 @@ static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t *
     pNew->pStrs = pStrs ? pStrs : Abc_NamStart( 1000, 24 );
     pNew->pFuns = pFuns ? pFuns : Abc_NamStart( 100, 24 );
     pNew->pMods = pMods ? pMods : Abc_NamStart( 100, 24 );
+    pNew->vHash = vHash ? vHash : Hash_IntManStart( 1000 );
     if ( pFuns == NULL )
     {
         Abc_NamStrFindOrAdd(pNew->pFuns, "1\'b0", NULL);
@@ -819,6 +812,8 @@ static inline Cba_Man_t * Cba_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t *
         Abc_NamStrFindOrAdd(pNew->pFuns, "1\'bx", NULL);
         Abc_NamStrFindOrAdd(pNew->pFuns, "1\'bz", NULL);
     }
+//    if ( vHash == NULL )
+//        Hash_Int2ManInsert( pNew->vHash, 0, 0, 0 );
     Vec_PtrGrow( &pNew->vNtks,  nNtks+1 ); Vec_PtrPush( &pNew->vNtks, NULL );
     // set default root module
     pNew->iRoot = 1;
@@ -831,7 +826,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_NamRef(p->pFuns), Abc_NamStart(100, 24) );
+    Cba_Man_t * pNew = Cba_ManAlloc( p->pSpec, Cba_ManNtkNum(p), Abc_NamRef(p->pStrs), Abc_NamRef(p->pFuns), Abc_NamStart(100, 24), Hash_IntManRef(p->vHash) );
     Cba_ManDupTypeNames( pNew, p );
     Cba_ManForEachNtk( p, pNtk, i )
     {
@@ -860,6 +855,7 @@ static inline void Cba_ManFree( Cba_Man_t * p )
     Abc_NamDeref( p->pStrs );
     Abc_NamDeref( p->pFuns );
     Abc_NamDeref( p->pMods );
+    Hash_IntManDeref( p->vHash );
     Vec_IntErase( &p->vNameMap );
     Vec_IntErase( &p->vUsed );
     Vec_IntErase( &p->vNameMap2 );
@@ -1054,6 +1050,7 @@ extern void          Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * p );
 extern void          Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p );
 /*=== cbaWriteVer.c ==========================================================*/
 extern void          Cba_ManCreatePrimMap( char ** pMap );
+extern char *        Cba_ManGetSliceName( Cba_Ntk_t * p, int iFon, int Left, int Right );
 extern void          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
 extern void          Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p, int fInlineConcat );
 
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 752744f1..f15df89a 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -489,7 +489,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_NamRef(p->pFuns), Abc_NamStart(100, 24) );
+    Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamRef(p->pFuns), Abc_NamStart(100, 24), Hash_IntManRef(p->vHash) );
     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;
@@ -660,7 +660,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_NamRef(p->pFuns), Abc_NamStart(100, 24) );
+    Cba_Man_t * pNew  = Cba_ManAlloc( p->pSpec, 1, Abc_NamRef(p->pStrs), Abc_NamRef(p->pFuns), Abc_NamStart(100, 24), Hash_IntManRef(p->vHash) );
     Cba_Ntk_t * pRoot = Cba_ManRoot( p ), * pRootNew;
     Vec_Int_t * vFonIns = Cba_NtkCollectInFons( pRoot, vObjs );
     Vec_Int_t * vFonOuts = Cba_NtkCollectOutFons( pRoot, vObjs );
@@ -743,7 +743,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, NULL );
+    Cba_Man_t * p = Cba_ManAlloc( pGia->pSpec, 1, NULL, 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;
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
index cfe1f06d..9fe1f33d 100644
--- a/src/base/cba/cbaPrs.h
+++ b/src/base/cba/cbaPrs.h
@@ -52,32 +52,33 @@ typedef struct Prs_Ntk_t_ Prs_Ntk_t;
 struct Prs_Ntk_t_
 {
     // general info
-    int          iModuleName;
-    unsigned     fMapped : 1;
-    unsigned     fSlices : 1;
-    unsigned     fHasC0s : 1;
-    unsigned     fHasC1s : 1;
-    unsigned     fHasCXs : 1;
-    unsigned     fHasCZs : 1;
-    Abc_Nam_t *  pStrs;
-    Abc_Nam_t *  pFuns;
+    int             iModuleName;
+    unsigned        fMapped : 1;
+    unsigned        fSlices : 1;
+    unsigned        fHasC0s : 1;
+    unsigned        fHasC1s : 1;
+    unsigned        fHasCXs : 1;
+    unsigned        fHasCZs : 1;
+    Abc_Nam_t *     pStrs;
+    Abc_Nam_t *     pFuns;
+    Hash_IntMan_t * vHash;
     // interface
-    Vec_Int_t    vOrder;     // order of signals
+    Vec_Int_t       vOrder;     // order of signals
     // signal names
-    Vec_Int_t    vInouts;    // inouts 
-    Vec_Int_t    vInputs;    // inputs 
-    Vec_Int_t    vOutputs;   // outputs
-    Vec_Int_t    vWires;     // wires  
+    Vec_Int_t       vInouts;    // inouts 
+    Vec_Int_t       vInputs;    // inputs 
+    Vec_Int_t       vOutputs;   // outputs
+    Vec_Int_t       vWires;     // wires  
     // signal ranges
-    Vec_Int_t    vInoutsR;   // inouts 
-    Vec_Int_t    vInputsR;   // inputs 
-    Vec_Int_t    vOutputsR;  // outputs
-    Vec_Int_t    vWiresR;    // wires  
+    Vec_Int_t       vInoutsR;   // inouts 
+    Vec_Int_t       vInputsR;   // inputs 
+    Vec_Int_t       vOutputsR;  // outputs
+    Vec_Int_t       vWiresR;    // wires  
     // slices/concatenations/objects
-    Vec_Int_t    vSlices;    // NameId + RangeId
-    Vec_Int_t    vConcats;   // array of NameId/SliceId/ConstId
-    Vec_Int_t    vBoxes;     // ModuleId + InstId + array of pairs {FormNameId, ActSignalId(NameId/SliceId/ConstId/ConcatId)}
-    Vec_Int_t    vObjs;      // box handles
+    Vec_Int_t       vSlices;    // NameId + RangeId
+    Vec_Int_t       vConcats;   // array of NameId/SliceId/ConstId
+    Vec_Int_t       vBoxes;     // ModuleId + InstId + array of pairs {FormNameId, ActSignalId(NameId/SliceId/ConstId/ConcatId)}
+    Vec_Int_t       vObjs;      // box handles
 };
 
 // parser
@@ -85,24 +86,25 @@ typedef struct Prs_Man_t_ Prs_Man_t;
 struct Prs_Man_t_
 {
     // input data
-    char *       pName;       // file name
-    char *       pBuffer;     // file contents
-    char *       pLimit;      // end of file
-    char *       pCur;        // current position
-    Abc_Nam_t *  pStrs;       // string manager
-    Abc_Nam_t *  pFuns;       // cover manager
-    Prs_Ntk_t *  pNtk;        // current network
-    Vec_Ptr_t *  vNtks;       // input networks
+    char *          pName;       // file name
+    char *          pBuffer;     // file contents
+    char *          pLimit;      // end of file
+    char *          pCur;        // current position
+    Abc_Nam_t *     pStrs;       // string manager
+    Abc_Nam_t *     pFuns;       // cover manager
+    Hash_IntMan_t * vHash;       // variable ranges
+    Prs_Ntk_t *     pNtk;        // current network
+    Vec_Ptr_t *     vNtks;       // input networks
     // temporary data
-    Vec_Str_t    vCover;      // one SOP cover
-    Vec_Int_t    vTemp;       // array of tokens
-    Vec_Int_t    vTemp2;      // array of tokens
+    Vec_Str_t       vCover;      // one SOP cover
+    Vec_Int_t       vTemp;       // array of tokens
+    Vec_Int_t       vTemp2;      // array of tokens
     // statistics
-    Vec_Int_t    vKnown;
-    Vec_Int_t    vFailed;
-    Vec_Int_t    vSucceeded;
+    Vec_Int_t       vKnown;
+    Vec_Int_t       vFailed;
+    Vec_Int_t       vSucceeded;
     // error handling
-    int          fUsingTemp2; // vTemp2 is in use
+    int             fUsingTemp2; // vTemp2 is in use
     char ErrorStr[1000];      // error
 };
 
@@ -188,6 +190,7 @@ static inline void Prs_ManInitializeNtk( Prs_Man_t * p, int iName, int fSlices )
     p->pNtk->fSlices = fSlices;
     p->pNtk->pStrs = Abc_NamRef( p->pStrs );
     p->pNtk->pFuns = Abc_NamRef( p->pFuns );
+    p->pNtk->vHash = Hash_IntManRef( p->vHash );
     Vec_PtrPush( p->vNtks, p->pNtk );
 }
 static inline void Prs_ManFinalizeNtk( Prs_Man_t * p )
@@ -229,16 +232,6 @@ static inline void Prs_NtkAddBox( Prs_Ntk_t * p, int ModName, int InstName, Vec_
     Vec_IntPush( &p->vBoxes, InstName );
     Vec_IntAppend( &p->vBoxes, vTemp );
 }
-
-// parsing range
-static inline void Prs_NtkParseRange( Prs_Ntk_t * p, int RangeId, int * pLeft, int * pRight )
-{
-    char * pRange = Prs_NtkStr(p, RangeId);
-    char * pPivot = strchr( pRange, ':' ); 
-    *pLeft  = atoi(pRange + 1);
-    *pRight = pPivot ? atoi(pPivot + 1) : *pLeft;
-}
-
 static inline char * Prs_ManLoadFile( char * pFileName, char ** ppLimit )
 {
     char * pBuffer;
@@ -280,6 +273,8 @@ static inline Prs_Man_t * Prs_ManAlloc( char * pFileName )
     p->pStrs   = Abc_NamStart( 1000, 24 );
     p->pFuns   = Abc_NamStart( 100, 24 );
     p->vNtks   = Vec_PtrAlloc( 100 );
+    p->vHash   = Hash_IntManStart( 1000 );
+//    Hash_Int2ManInsert( p->vHash, 0, 0, 0 );
     return p;
 }
 
@@ -287,6 +282,7 @@ static inline void Prs_NtkFree( Prs_Ntk_t * p )
 {
     if ( p->pStrs ) Abc_NamDeref( p->pStrs );
     if ( p->pFuns ) Abc_NamDeref( p->pFuns );
+    if ( p->vHash ) Hash_IntManDeref( p->vHash );
     Vec_IntErase( &p->vOrder );
     Vec_IntErase( &p->vInouts );
     Vec_IntErase( &p->vInputs );
@@ -315,6 +311,7 @@ static inline void Prs_ManFree( Prs_Man_t * p )
 {
     if ( p->pStrs ) Abc_NamDeref( p->pStrs );
     if ( p->pFuns ) Abc_NamDeref( p->pFuns );
+    if ( p->vHash ) Hash_IntManDeref( p->vHash );
     if ( p->vNtks ) Prs_ManVecFree( p->vNtks );
     // temporary
     Vec_StrErase( &p->vCover );
@@ -424,6 +421,7 @@ static inline char * Ptr_TypeToName( Cba_ObjType_t Type )
     if ( Type == CBA_BOX_MAJ )   return "maj";
     if ( Type == CBA_BOX_SHARP ) return "sharp";
     if ( Type == CBA_BOX_SHARPL) return "sharpl";
+    if ( Type == CBA_BOX_TRI)    return "bufifl";
     assert( 0 );
     return "???";
 }
diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c
index bf0aad5b..fff98413 100644
--- a/src/base/cba/cbaReadBlif.c
+++ b/src/base/cba/cbaReadBlif.c
@@ -592,7 +592,7 @@ Cba_Man_t * Prs_ManBuildCbaBlif( char * pFileName, Vec_Ptr_t * vDes )
     Abc_Nam_t * pStrs = Abc_NamRef(pPrsRoot->pStrs);
     Abc_Nam_t * pFuns = Abc_NamRef(pPrsRoot->pFuns);
     Abc_Nam_t * pMods = Abc_NamStart( 100, 24 );
-    Cba_Man_t * p = Cba_ManAlloc( pFileName, Vec_PtrSize(vDes), pStrs, pFuns, pMods );
+    Cba_Man_t * p = Cba_ManAlloc( pFileName, Vec_PtrSize(vDes), pStrs, pFuns, pMods, NULL );
     // initialize networks
     Vec_PtrForEachEntry( Prs_Ntk_t *, vDes, pPrsNtk, i )
     {
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index 32cd1b59..d1c3ee58 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -492,28 +492,29 @@ static inline int Prs_ManReadConstant( Prs_Man_t * p )
 }
 static inline int Prs_ManReadRange( Prs_Man_t * p )
 {
+    int Left, Right;
     assert( Prs_ManIsChar(p, '[') );
-    Vec_StrClear( &p->vCover );
-    Vec_StrPush( &p->vCover, *p->pCur++ );
+    p->pCur++;
     if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 3.", 0);
     if ( !Prs_ManIsDigit(p) )               return Prs_ManErrorSet(p, "Cannot read digit in range specification.", 0);
-    while ( Prs_ManIsDigit(p) )
-        Vec_StrPush( &p->vCover, *p->pCur++ );
+    Left = Right = atoi(p->pCur);
+    while ( Prs_ManIsDigit(p) ) 
+        p->pCur++;
     if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 4.", 0);
     if ( Prs_ManIsChar(p, ':') )
     {
-        Vec_StrPush( &p->vCover, *p->pCur++ );
+        p->pCur++;
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 5.", 0);
         if ( !Prs_ManIsDigit(p) )           return Prs_ManErrorSet(p, "Cannot read digit in range specification.", 0);
-        while ( Prs_ManIsDigit(p) )
-            Vec_StrPush( &p->vCover, *p->pCur++ );
+        Right = atoi(p->pCur);
+        while ( Prs_ManIsDigit(p) ) 
+            p->pCur++;
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 6.", 0);
     }
     if ( !Prs_ManIsChar(p, ']') )           return Prs_ManErrorSet(p, "Cannot read closing brace in range specification.", 0);
-    Vec_StrPush( &p->vCover, *p->pCur++ );
-    Vec_StrPush( &p->vCover, '\0' );
+    p->pCur++;
     if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 6a.", 0);
-    return Abc_NamStrFindOrAdd( p->pStrs, Vec_StrArray(&p->vCover), NULL );
+    return Hash_Int2ManInsert( p->vHash, Left, Right, 0 );
 }
 static inline int Prs_ManReadConcat( Prs_Man_t * p, Vec_Int_t * vTemp2 )
 {
@@ -784,10 +785,11 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
         return 1;
     while ( 1 )
     {
+        int fEscape = Prs_ManIsChar(p, '\\');
         int iName = Prs_ManReadName( p );
         if ( iName == 0 )                       return Prs_ManErrorSet(p, "Error number 31.", 0);
         if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 32.", 0);
-        if ( iName >= PRS_VER_INPUT && iName <= PRS_VER_INOUT ) // declaration
+        if ( iName >= PRS_VER_INPUT && iName <= PRS_VER_INOUT && !fEscape ) // declaration
         {
             iType = iName;
             if ( Prs_ManIsChar(p, '[') )
@@ -983,8 +985,7 @@ void Prs_ManReadVerilogTest( char * pFileName )
     printf( "Memory = %.2f MB. ", 1.0*Prs_ManMemory(vPrs)/(1<<20) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     Prs_ManWriteVerilog( Extra_FileNameGenericAppend(pFileName, "_out.v"), vPrs );
-
-    Abc_NamPrint( Prs_ManNameMan(vPrs) );
+//    Abc_NamPrint( Prs_ManNameMan(vPrs) );
     Prs_ManVecFree( vPrs );
 }
 
@@ -1007,17 +1008,12 @@ int Prs_CreateVerilogFindFon( Cba_Ntk_t * p, int NameId )
     printf( "Network \"%s\": Signal \"%s\" is not driven.\n", Cba_NtkName(p), Cba_NtkStr(p, NameId) );
     return 0;
 }
-int Prs_CreateSlice( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Left, int Right )
+int Prs_CreateSlice( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Range )
 {
-    char Buffer[1000];
     int iObj, iFonNew, NameId;
     assert( Cba_FonIsReal(iFon) );
-    if ( Left != Right )
-        sprintf( Buffer, "%s[%d:%d]", Cba_FonNameStr(p, iFon), Left, Right );
-    else
-        sprintf( Buffer, "%s[%d]", Cba_FonNameStr(p, iFon), Right );
     // check existing slice
-    NameId = Cba_NtkNewStrId( p, Buffer );
+    NameId = Cba_NtkNewStrId( p, Cba_ManGetSliceName(p, iFon, Cba_NtkRangeLeft(p, Range), Cba_NtkRangeRight(p, Range)) );
     iFonNew = Cba_NtkGetMap( p, NameId );
     if ( iFonNew )
         return iFonNew;
@@ -1026,8 +1022,7 @@ int Prs_CreateSlice( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Left, int Ri
     Cba_ObjSetName( p, iObj, NameId );
     Cba_ObjSetFinFon( p, iObj, 0, iFon );
     iFonNew = Cba_ObjFon0(p, iObj);
-    Cba_FonSetLeft( p, iFonNew, Abc_AbsInt(Left-Right) );
-    Cba_FonSetRight( p, iFonNew, 0 );
+    Cba_FonSetRange( p, iFonNew, Range );
     Cba_FonSetName( p, iFonNew, NameId );
     Cba_NtkSetMap( p, NameId, iFonNew );
     return iFonNew;        
@@ -1052,16 +1047,15 @@ int Prs_CreateCatIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Con )
         if ( iFon )
             Cba_ObjSetFinFon( p, iObj, i, iFon );
         if ( iFon )
-            nBits += Cba_FonRange( p, iFon );
+            nBits += Cba_FonRangeSize( p, iFon );
     }
     iFon = Cba_ObjFon0(p, iObj);
-    Cba_FonSetLeft( p, iFon, nBits-1 );
-    Cba_FonSetRight( p, iFon, 0 );
+    Cba_FonSetRange( p, iFon, Cba_NtkHashRange(p, nBits-1, 0) );
     return Cba_ObjFon0(p, iObj);
 }
 int Prs_CreateSignalIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Sig )
 {
-    int Left, Right, iFon, Value = Abc_Lit2Var2( Sig );
+    int iFon, Value = Abc_Lit2Var2( Sig );
     Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
     if ( !Sig ) return 0;
     if ( Type == CBA_PRS_NAME )
@@ -1073,30 +1067,27 @@ int Prs_CreateSignalIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Sig )
         iFon =  Prs_CreateVerilogFindFon( p, Cba_NtkNewStrId(p, Prs_NtkStr(pNtk, Prs_SliceName(pNtk, Value))) );
         if ( !iFon )
             return 0;
-        Prs_NtkParseRange( pNtk, Prs_SliceRange(pNtk, Value), &Left, &Right );
-        return Prs_CreateSlice( p, iFon, pNtk, Left, Right );
+        return Prs_CreateSlice( p, iFon, pNtk, Prs_SliceRange(pNtk, Value) );
     }
     assert( Type == CBA_PRS_CONCAT );
     return Prs_CreateCatIn( p, pNtk, Value );
 }
 int Prs_CreateRange( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int NameId )
 {
-    int Left, Right, RangeId = -Cba_NtkGetMap(p, NameId);
+    int RangeId = -Cba_NtkGetMap(p, NameId);
     if ( RangeId < 0 ) // this variable is already created
-        return Cba_FonRange( p, -RangeId );
+        return Cba_FonRangeSize( p, -RangeId );
     Cba_NtkUnsetMap( p, NameId );
     Cba_NtkSetMap( p, NameId, iFon );
     if ( RangeId == 0 )
         return 1;
     assert( RangeId > 0 );
-    Prs_NtkParseRange( pNtk, RangeId, &Left, &Right );
-    Cba_FonSetLeft( p, iFon, Left );
-    Cba_FonSetRight( p, iFon, Right );
-    return Cba_FonRange( p, iFon );
+    Cba_FonSetRange( p, iFon, RangeId );
+    return Cba_FonRangeSize( p, iFon );
 }
 int Prs_CreateCatOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Con )
 {
-    int i, Sig, iObj, iFonNew, NameId, Left, Right, nBits = 0;
+    int i, Sig, iObj, iFonNew, NameId, nBits = 0;
     Vec_Int_t * vSigs = Prs_CatSignals(pNtk, Con); char * pSigName;
     NameId = Cba_NtkNewStrId( p, "_occ%d_", iFon );
     Cba_FonSetName( p, iFon, NameId );
@@ -1119,24 +1110,22 @@ int Prs_CreateCatOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Con )
         }
         else if ( Type == CBA_PRS_SLICE )
         {
-            Prs_NtkParseRange( pNtk, Prs_SliceRange(pNtk, Value), &Left, &Right );
             pSigName = Prs_NtkStr(pNtk, Prs_SliceName(pNtk, Value));
             NameId = Cba_NtkNewStrId( p, pSigName );
             Cba_FonSetName( p, iFonNew, NameId );
             Prs_CreateRange( p, iFonNew, pNtk, NameId );
             // create slice of this concat
-            Prs_CreateSlice( p, iFonNew, pNtk, Left, Right );
-            nBits += Abc_AbsInt(Left-Right)+1;
+            Prs_CreateSlice( p, iFonNew, pNtk, Prs_SliceRange(pNtk, Value) );
+            nBits += Cba_NtkRangeSize( p, Prs_SliceRange(pNtk, Value) );
         }
         else assert( 0 );
     }
-    Cba_FonSetLeft( p, iFon, nBits-1 );
-    Cba_FonSetRight( p, iFon, 0 );
+    Cba_FonSetRange( p, iFon, Cba_NtkHashRange(p, nBits-1, 0) );
     return iObj;
 }
 void Prs_CreateSignalOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Sig )
 {
-    int iObj, NameId, Left, Right, Value = Abc_Lit2Var2( Sig );
+    int iObj, NameId, Value = Abc_Lit2Var2( Sig );
     Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
     if ( !Sig ) return;
     if ( Type == CBA_PRS_NAME )
@@ -1149,7 +1138,6 @@ void Prs_CreateSignalOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Sig )
     if ( Type == CBA_PRS_SLICE )
     {
         char * pSigName = Prs_NtkStr(pNtk, Prs_SliceName(pNtk, Value));
-        Prs_NtkParseRange( pNtk, Prs_SliceRange(pNtk, Value), &Left, &Right );
         // create buffer
         iObj = Cba_ObjAlloc( p, CBA_BOX_BUF, 1, 1 );
         Cba_ObjSetFinFon( p, iObj, 0, iFon );
@@ -1158,7 +1146,7 @@ void Prs_CreateSignalOut( Cba_Ntk_t * p, int iFon, Prs_Ntk_t * pNtk, int Sig )
         Cba_FonSetName( p, iFon, NameId );
         Prs_CreateRange( p, iFon, pNtk, NameId );
         // create slice of this concat
-        Prs_CreateSlice( p, iFon, pNtk, Left, Right );
+        Prs_CreateSlice( p, iFon, pNtk, Prs_SliceRange(pNtk, Value) );
         return;
     }
     assert( Type == CBA_PRS_CONCAT );
@@ -1302,12 +1290,11 @@ Vec_Ptr_t * Prs_CreateDetectRams( Prs_Ntk_t * pNtk )
 }
 void Prs_CreateVerilogPio( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
 {
-    int i, NameId, RangeId, Left, Right, iObj, iFon;
+    int i, NameId, RangeId, iObj, iFon;
     Cba_NtkCleanObjFuncs( p );
     Cba_NtkCleanObjNames( p );
     Cba_NtkCleanFonNames( p );
-    Cba_NtkCleanFonLefts( p );
-    Cba_NtkCleanFonRights( p );
+    Cba_NtkCleanFonRanges( p );
     // create inputs
     Cba_NtkCleanMap( p );
     assert( Vec_IntSize(&pNtk->vInouts) == 0 );
@@ -1316,12 +1303,7 @@ void Prs_CreateVerilogPio( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
         iObj = Cba_ObjAlloc( p, CBA_OBJ_PI, 0, 1 );
         Cba_ObjSetName( p, iObj, NameId ); // direct name
         iFon = Cba_ObjFon0(p, iObj);
-        if ( RangeId )
-        {
-            Prs_NtkParseRange( pNtk, RangeId, &Left, &Right );
-            Cba_FonSetLeft( p, iFon, Left );
-            Cba_FonSetRight( p, iFon, Right );
-        }
+        Cba_FonSetRange( p, iFon, RangeId );
         Cba_FonSetName( p, iFon, NameId );
         Cba_NtkSetMap( p, NameId, iObj );
     }
@@ -1344,8 +1326,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
 {
     Vec_Int_t * vBox2Obj = Vec_IntStart( Prs_NtkBoxNum(pNtk) );
     Vec_Int_t * vBox;  Vec_Ptr_t * vAllRams, * vRam;
-    int NameId, RangeId, Left, Right;
-    int i, k, iObj, iTerm, iFon, FormId, ActId;
+    int i, k, iObj, iTerm, iFon, FormId, ActId, RangeId, NameId;
     // map inputs
     Cba_NtkCleanMap( p );
     Cba_NtkForEachPi( p, iObj, i )
@@ -1388,8 +1369,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
             //Cba_VerificSaveLineFile( p, iObjNew, pInst->Linefile() );
             // connect output
             iFon = Cba_ObjFon0(p, iObjNew);
-            Cba_FonSetLeft( p, iFon, MemSize-1 );
-            Cba_FonSetRight( p, iFon, 0 );
+            Cba_FonSetRange( p, iFon, Cba_NtkHashRange(p, MemSize-1, 0) );
             //sprintf( Buffer, "%s_wp%d", pRamName, k-2 );
             //NameId = Cba_NtkNewStrId( p, Buffer ); 
             NameId = Cba_NtkNewStrId( p, "%s_wp%d", pRamName, k-2 );
@@ -1482,10 +1462,10 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
 //        char * pInstName = NULL;
 //        if ( Prs_BoxName(pNtk, i) )
 //            pInstName = Prs_NtkStr(pNtk, Prs_BoxName(pNtk, i));
-        if ( pNtk->iModuleName == 291 && i == 0 )
-        {
-            int s = 0;
-        }
+//        if ( pNtk->iModuleName == 291 && i == 0 )
+//        {
+//            int s = 0;
+//        }
         iObj = Vec_IntEntry( vBox2Obj, i );
         if ( Prs_BoxIsNode(pNtk, i) ) // node
         {
@@ -1549,7 +1529,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                                 iFon = Prs_CreateSignalIn( p, pNtk, ActId );  assert( iFon );
                                 // create bit-select node for data/set/reset (but not for clock)
                                 if ( Index < 3 ) // not clock
-                                    iFon = Prs_CreateSlice( p, iFon, pNtk, 0, 0 );
+                                    iFon = Prs_CreateSlice( p, iFon, pNtk, 0 );
                                 Cba_ObjSetFinFon( p, iObjNew, Index, iFon );
                             }
                     }
@@ -1589,7 +1569,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
             if ( Type == CBA_BOX_NMUX || Type == CBA_BOX_SEL )
             {
                 int FonCat = Cba_ObjFinFon( p, iObj, 1 );
-                int nBits  = Cba_FonRange( p, FonCat );
+                int nBits  = Cba_FonRangeSize( p, FonCat );
                 int nParts = Cba_ObjFinNum(p, iObj) - 1;
                 int Slice  = nBits / nParts;
                 int nFins = Cba_ObjFinNum(p, iObj);
@@ -1605,13 +1585,12 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                     FonCat = Cba_ObjFon0( p, iObjNew );
                     NameId = Cba_NtkNewStrId( p, "_buf_const_%d", iObjNew );
                     Cba_FonSetName( p, FonCat, NameId );
-                    Cba_FonSetLeft( p, FonCat, nBits-1 );
-                    Cba_FonSetRight( p, FonCat, 0 );
+                    Cba_FonSetRange( p, FonCat, Cba_NtkHashRange(p, nBits-1, 0) );
                 }
                 for ( k = 0; k < nParts; k++ )
                 {
-//                    iFon = Prs_CreateSlice( p, FonCat, pNtk, (nParts-1-k)*Slice+Slice-1, (nParts-1-k)*Slice );
-                    iFon = Prs_CreateSlice( p, FonCat, pNtk, k*Slice+Slice-1, k*Slice );
+//                    iFon = Prs_CreateSlice( p, FonCat, pNtk, Cba_NtkHashRange(p, (nParts-1-k)*Slice+Slice-1, (nParts-1-k)*Slice) );
+                    iFon = Prs_CreateSlice( p, FonCat, pNtk, Cba_NtkHashRange(p, k*Slice+Slice-1, k*Slice) );
                     Cba_ObjSetFinFon( p, iObj, k+1, iFon );
                 }
             }
@@ -1629,9 +1608,8 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
         Cba_ObjSetFinFon( p, iObj, 0, iFon );
         if ( RangeId )
         {
-            Prs_NtkParseRange( pNtk, RangeId, &Left, &Right );
-            assert( Left  == Cba_FonLeft(p, iFon) );
-            assert( Right == Cba_FonRight(p, iFon) );
+            assert( Cba_NtkRangeLeft(p, RangeId)  == Cba_FonLeft(p, iFon) );
+            assert( Cba_NtkRangeRight(p, RangeId) == Cba_FonRight(p, iFon) );
         }
     }
     return 0;
@@ -1644,7 +1622,7 @@ Cba_Man_t * Prs_ManBuildCbaVerilog( char * pFileName, Vec_Ptr_t * vDes )
     Abc_Nam_t * pStrs = Abc_NamRef(pPrsRoot->pStrs);
     Abc_Nam_t * pFuns = Abc_NamRef(pPrsRoot->pFuns);
     Abc_Nam_t * pMods = Abc_NamStart( 100, 24 );
-    Cba_Man_t * p = Cba_ManAlloc( pFileName, Vec_PtrSize(vDes), pStrs, pFuns, pMods );
+    Cba_Man_t * p = Cba_ManAlloc( pFileName, Vec_PtrSize(vDes), pStrs, pFuns, pMods, Hash_IntManRef(pPrsRoot->vHash) );
     // initialize networks
     Vec_PtrForEachEntry( Prs_Ntk_t *, vDes, pPrsNtk, i )
     {
@@ -1655,7 +1633,7 @@ Cba_Man_t * Prs_ManBuildCbaVerilog( char * pFileName, Vec_Ptr_t * vDes )
     // create networks
     Vec_PtrForEachEntry( Prs_Ntk_t *, vDes, pPrsNtk, i )
     {
-        printf( "Elaboration module \"%s\"...\n", Prs_NtkName(pPrsNtk) );
+        printf( "Building module \"%s\"...\n", Prs_NtkName(pPrsNtk) );
         fError = Prs_CreateVerilogNtk( Cba_ManNtk(p, i+1), pPrsNtk );
         if ( fError )
             break;
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index b628ab9e..f5a97083 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -112,6 +112,7 @@ static void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p )
     Prs_NtkForEachBox( p, vBox, i )
     {
         Cba_ObjType_t NtkId = Prs_BoxNtk(p, i);
+        char * pNtkName = Prs_NtkStr(p, Prs_BoxName(p, i));
         if ( NtkId == CBA_BOX_MUX )
             Prs_ManWriteVerilogMux( pFile, p, vBox );
         else if ( Prs_BoxIsNode(p, i) ) // node   ------- check order of fanins
@@ -304,16 +305,31 @@ char * Cba_FonGetName( Cba_Ntk_t * p, int i )
     char * pName = Cba_FonNameStr(p, i);
     if ( pName == NULL )
         return pName;
+    if ( Cba_ObjType(p, Cba_FonObj(p, i)) == CBA_BOX_SLICE )
+        return pName;
     if ( Cba_NameIsLegalInVerilog(pName) )
         return pName;
     return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "\\%s ", pName );
 }
-
+char * Cba_ManGetSliceName( Cba_Ntk_t * p, int iFon, int Left, int Right )
+{
+    char * pName = Cba_FonNameStr(p, iFon);
+    if ( Cba_NameIsLegalInVerilog(pName) )
+        if ( Left == Right )
+            return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "%s[%d]", pName, Right );
+        else
+            return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "%s[%d:%d]", pName, Left, Right );
+    else
+        if ( Left == Right )
+            return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "\\%s [%d]", pName, Right );
+        else
+            return Vec_StrPrintF( Abc_NamBuffer(Cba_NtkNam(p)), "\\%s [%d:%d]", pName, Left, Right );
+}
 
 void Cba_ManWriteFonRange( Cba_Ntk_t * p, int iFon )
 {
     Vec_Str_t * vStr = &p->pDesign->vOut;
-    if ( Cba_FonIsConst(iFon) || (Cba_FonRange(p, iFon) == 1 && Cba_FonRight(p, iFon) == 0) )
+    if ( Cba_FonIsConst(iFon) || (Cba_FonRangeSize(p, iFon) == 1 && Cba_FonRight(p, iFon) == 0) )
         return;
     Vec_StrPrintF( vStr, "[%d:%d] ", Cba_FonLeft(p, iFon), Cba_FonRight(p, iFon) );
 
@@ -329,7 +345,7 @@ void Cba_ManWriteFonName( Cba_Ntk_t * p, int iFon, int fInlineConcat, int fInput
         Cba_ManWriteCatIn( p, Cba_FonObj(p, iFon) );
     else
     {
-        int Range = fInput ? Cba_FonRange( p, iFon ) : 0;
+        int Range = fInput ? Cba_FonRangeSize( p, iFon ) : 0;
         if ( fInput && Range > 1 )
             Vec_StrPush( vStr, '{' );
         Vec_StrPrintStr( vStr, Cba_FonIsConst(iFon) ? Cba_NtkConst(p, Cba_FonConst(iFon)) : Cba_FonGetName(p, iFon) );
@@ -590,8 +606,8 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
         {
             int iFonIn   = Cba_ObjFinFon(p, iObj, 0);
             int iFonOut  = Cba_ObjFon0(p, iObj);
-            int nBitsIn  = Cba_FonRange(p, iFonIn);
-            int nBitsOut = Cba_FonRange(p, iFonOut);
+            int nBitsIn  = Cba_FonRangeSize(p, iFonIn);
+            int nBitsOut = Cba_FonRangeSize(p, iFonOut);
             assert( (1 << nBitsIn) == nBitsOut );
             // function [15:0] res;
             Vec_StrPrintStr( vStr, "  function " );
@@ -606,12 +622,14 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             // casez (i)
             Vec_StrPrintStr( vStr, "    casez(i)\n" );
             // 2'b00: res = 4'b0001;
-            Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
+            for ( i = 0; i < (1 << nBitsIn); i++ )
             {
-                Vec_StrPrintF( vStr, "      %d\'b: ", nBitsIn );
+                Vec_StrPrintF( vStr, "      %d\'b", nBitsIn );
+                for ( k = nBitsIn-1; k >= 0; k-- )
+                    Vec_StrPrintNum( vStr, (i >> k) & 1 );
                 Vec_StrPrintStr( vStr, ": _func_" );
                 Cba_ManWriteFonName( p, iFonOut, 0, 0 );
-                Vec_StrPrintF( vStr, " = %d\'b%*d;\n", nBitsOut, nBitsOut, 0 );
+                Vec_StrPrintF( vStr, " = %d\'b%0*d;\n", nBitsOut, nBitsOut, 0 );
                 Vec_StrWriteEntry( vStr, Vec_StrSize(vStr) - i - 3, '1' );
             }
             Vec_StrPrintStr( vStr, "    endcase\n" );
@@ -639,8 +657,8 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             int iFonSet  = Cba_ObjFinFon(p, iObj, 1);
             int iFonRst  = Cba_ObjFinFon(p, iObj, 2);
             int iFonC    = Cba_ObjFinFon(p, iObj, 3);
-            int Range    = Cba_FonRange( p, iFonQ );
-            assert( Cba_FonRange(p, iFonSet) == 1 && Cba_FonRange(p, iFonRst) == 1 );
+            int Range    = Cba_FonRangeSize( p, iFonQ );
+            assert( Cba_FonRangeSize(p, iFonSet) == 1 && Cba_FonRangeSize(p, iFonRst) == 1 );
             // reg    [3:0] Q;
             Vec_StrPrintStr( vStr, "  reg " );
             Cba_ManWriteFonRange( p, iFonQ );