Improvements to Cba data-structure.

7 files changed, 1581 insertions, 280 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index c0e0d91d..0086d031 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -42,112 +42,111 @@ ABC_NAMESPACE_HEADER_START
 
 // network objects
 typedef enum { 
-    CBA_OBJ_NONE = 0,  // 0:  unused
-    CBA_OBJ_PI,        // 1:  input
-    CBA_OBJ_PO,        // 2:  output
-    CBA_OBJ_BOX,       // 3:  box
-
-    CBA_BOX_SLICE,  
-    CBA_BOX_CATIN,  
-    CBA_BOX_CATOUT,  
-
-    CBA_BOX_CF,  
-    CBA_BOX_CT,  
-    CBA_BOX_CX,  
-    CBA_BOX_CZ,  
-
-    CBA_BOX_BUF,  
-    CBA_BOX_INV,  
-    CBA_BOX_AND,  
-    CBA_BOX_NAND, 
-    CBA_BOX_OR,   
-    CBA_BOX_NOR,  
-    CBA_BOX_XOR,  
-    CBA_BOX_XNOR, 
-    CBA_BOX_SHARP,
-    CBA_BOX_SHARPL,
-    CBA_BOX_MUX,  
-    CBA_BOX_MAJ,  
-
-    CBA_BOX_ABC,
-    CBA_BOX_BA,
-    CBA_BOX_BO,
-    CBA_BOX_BX,
-    CBA_BOX_BN,
-    CBA_BOX_BAO,
-    CBA_BOX_BOA,
-
-    CBA_BOX_RAND,
-    CBA_BOX_RNAND,
-    CBA_BOX_ROR,
-    CBA_BOX_RNOR,
-    CBA_BOX_RXOR,
-    CBA_BOX_RXNOR,
-
-    CBA_BOX_LNOT,
-    CBA_BOX_LAND,
-    CBA_BOX_LNAND,
-    CBA_BOX_LOR,
-    CBA_BOX_LNOR,
-    CBA_BOX_LXOR,
-    CBA_BOX_LXNOR,
-
-    CBA_BOX_NMUX,  
-    CBA_BOX_SEL,
-    CBA_BOX_PSEL,
-    CBA_BOX_ENC,
-    CBA_BOX_PENC,
-    CBA_BOX_DEC,
-    CBA_BOX_EDEC,
-
-    CBA_BOX_ADD,
-    CBA_BOX_SUB,
-    CBA_BOX_MUL,
-    CBA_BOX_SMUL,
-    CBA_BOX_DIV,
-    CBA_BOX_MOD,
-    CBA_BOX_REM,
-    CBA_BOX_POW,
-    CBA_BOX_MIN,
-    CBA_BOX_SQRT,
-    CBA_BOX_ABS,
-
-    CBA_BOX_SLTHAN,
-    CBA_BOX_LTHAN,
-    CBA_BOX_LETHAN,
-    CBA_BOX_METHAN,
-    CBA_BOX_MTHAN,
-    CBA_BOX_EQU,
-    CBA_BOX_NEQU,
-
-    CBA_BOX_SHIL,
-    CBA_BOX_SHIR,
-    CBA_BOX_SHILA,
-    CBA_BOX_SHIRA,
-    CBA_BOX_ROTL,
-    CBA_BOX_ROTR,
-
-    CBA_BOX_NODE,  
-    CBA_BOX_LUT,  
-    CBA_BOX_GATE,  
-    CBA_BOX_ASSIGN,  
-
-    CBA_BOX_TRI,
-    CBA_BOX_RAM,
-    CBA_BOX_RAMR,
-    CBA_BOX_RAMW,
-    CBA_BOX_RAMWC,
-    CBA_BOX_RAML,
-    CBA_BOX_RAMS,
-    CBA_BOX_RAMBOX,
-
-    CBA_BOX_LATCH,
-    CBA_BOX_LATCHRS,
-    CBA_BOX_DFF,
-    CBA_BOX_DFFCPL,
-    CBA_BOX_DFFRS,
-
-    CBA_BOX_LAST   // 67
+    CBA_OBJ_NONE = 0,  // 00:  unused
+    CBA_OBJ_PI,        // 01:  input
+    CBA_OBJ_PO,        // 02:  output
+    CBA_OBJ_BOX,       // 03:  box
+
+    CBA_BOX_CF,        // 04: 
+    CBA_BOX_CT,        // 05:   
+    CBA_BOX_CX,        // 06:   
+    CBA_BOX_CZ,        // 07:  
+
+    CBA_BOX_BUF,       // 08:    
+    CBA_BOX_INV,       // 09:    
+    CBA_BOX_AND,       // 10:    
+    CBA_BOX_NAND,      // 11:   
+    CBA_BOX_OR,        // 12:     
+    CBA_BOX_NOR,       // 13:    
+    CBA_BOX_XOR,       // 14:    
+    CBA_BOX_XNOR,      // 15:   
+    CBA_BOX_SHARP,     // 16:  
+    CBA_BOX_SHARPL,    // 17:  
+    CBA_BOX_MUX,       // 18:    
+    CBA_BOX_MAJ,       // 19:    
+
+    CBA_BOX_ABC,       // 20:
+    CBA_BOX_BA,        // 21:
+    CBA_BOX_BO,        // 22:
+    CBA_BOX_BX,        // 23:
+    CBA_BOX_BN,        // 24:
+    CBA_BOX_BAO,       // 25:
+    CBA_BOX_BOA,       // 26:
+
+    CBA_BOX_RAND,      // 27:
+    CBA_BOX_RNAND,     // 28:
+    CBA_BOX_ROR,       // 29:
+    CBA_BOX_RNOR,      // 30:
+    CBA_BOX_RXOR,      // 31:
+    CBA_BOX_RXNOR,     // 32:
+
+    CBA_BOX_LNOT,      // 33
+    CBA_BOX_LAND,      // 34:
+    CBA_BOX_LNAND,     // 35:
+    CBA_BOX_LOR,       // 36:
+    CBA_BOX_LNOR,      // 37:
+    CBA_BOX_LXOR,      // 38:
+    CBA_BOX_LXNOR,     // 39:
+
+    CBA_BOX_NMUX,      // 40:  
+    CBA_BOX_SEL,       // 41:
+    CBA_BOX_PSEL,      // 42:
+    CBA_BOX_ENC,       // 43:
+    CBA_BOX_PENC,      // 44:
+    CBA_BOX_DEC,       // 45:
+    CBA_BOX_EDEC,      // 46:
+
+    CBA_BOX_ADD,       // 47:
+    CBA_BOX_SUB,       // 48:
+    CBA_BOX_MUL,       // 49:
+    CBA_BOX_SMUL,      // 50:
+    CBA_BOX_DIV,       // 51:
+    CBA_BOX_MOD,       // 52:
+    CBA_BOX_REM,       // 53:
+    CBA_BOX_POW,       // 54:
+    CBA_BOX_MIN,       // 55:
+    CBA_BOX_SQRT,      // 56:
+    CBA_BOX_ABS,       // 57:
+
+    CBA_BOX_SLTHAN,    // 58:
+    CBA_BOX_LTHAN,     // 59:
+    CBA_BOX_LETHAN,    // 60:
+    CBA_BOX_METHAN,    // 61:
+    CBA_BOX_MTHAN,     // 62:
+    CBA_BOX_EQU,       // 63:
+    CBA_BOX_NEQU,      // 64:
+
+    CBA_BOX_SHIL,      // 65:
+    CBA_BOX_SHIR,      // 66:
+    CBA_BOX_SHILA,     // 67:
+    CBA_BOX_SHIRA,     // 68:
+    CBA_BOX_ROTL,      // 69:
+    CBA_BOX_ROTR,      // 70:
+
+    CBA_BOX_NODE,      // 71:  
+    CBA_BOX_LUT,       // 72: 
+    CBA_BOX_GATE,      // 73:  
+    CBA_BOX_TABLE,     // 74:  
+
+    CBA_BOX_TRI,       // 75:
+    CBA_BOX_RAM,       // 76:
+    CBA_BOX_RAMR,      // 77:
+    CBA_BOX_RAMW,      // 78:
+    CBA_BOX_RAMWC,     // 79:
+    CBA_BOX_RAML,      // 80:
+    CBA_BOX_RAMS,      // 81:
+    CBA_BOX_RAMBOX,    // 82:
+
+    CBA_BOX_LATCH,     // 83:
+    CBA_BOX_LATCHRS,   // 84:
+    CBA_BOX_DFF,       // 85:
+    CBA_BOX_DFFCPL,    // 86:
+    CBA_BOX_DFFRS,     // 87:
+
+    CBA_BOX_SLICE,     // 88:
+    CBA_BOX_CONCAT,    // 89: 
+
+    CBA_BOX_LAST       // 90
 } Cba_ObjType_t; 
 
 
@@ -190,6 +189,7 @@ struct Cba_Ntk_t_
     Vec_Int_t       vFinFon0; // fanout: first fon
     Vec_Int_t       vFinObj;  // object
     Vec_Int_t       vNtkObjs; // instances
+    Vec_Int_t       vFonBits; // fon mapping into AIG nodes
     // other
     Vec_Ptr_t *     vOther;   // various data
     Vec_Int_t       vArray0;
@@ -211,6 +211,8 @@ struct Cba_Man_t_
     Vec_Int_t       vUsed;    // used map entries
     Vec_Int_t       vUsed2;   // used map entries
     char *          pTypeNames[CBA_BOX_LAST];
+    int             nObjs[CBA_BOX_LAST]; // counter of objects of each type
+    int             nAnds[CBA_BOX_LAST]; // counter of AND gates after blasting
     // internal data
     int             iRoot;    // root network
     Vec_Ptr_t       vNtks;    // networks
@@ -332,8 +334,7 @@ static inline int            Cba_ObjIsBoxUser( Cba_Ntk_t * p, int i )        { r
 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_ObjIsCatIn( Cba_Ntk_t * p, int i )          { return Cba_ObjType(p, i) == CBA_BOX_CATIN;                                                  }
-static inline int            Cba_ObjIsCatOut( Cba_Ntk_t * p, int i )         { return Cba_ObjType(p, i) == CBA_BOX_CATOUT;                                                 }
+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);                                          }
@@ -375,16 +376,18 @@ static inline int            Cba_FonIsReal( int f )                          { r
 static inline int            Cba_FonIsConst( int f )                         { return f < 0;                             }
 static inline int            Cba_FonConst( int f )                           { assert(Cba_FonIsConst(f)); return -f-1;   }
 static inline int            Cba_FonFromConst( int c )                       { assert(c >= 0); return -c-1;              }
-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_FonConstRangeSize( Cba_Ntk_t * p, int f )   { assert(Cba_FonIsConst(f)); return atoi(Cba_NtkConst(p, Cba_FonConst(f)));                   }
+static inline int            Cba_FonConstSigned( Cba_Ntk_t * p, int f )      { assert(Cba_FonIsConst(f)); return strchr(Cba_NtkConst(p, Cba_FonConst(f)), 's') != NULL;    }
 
 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_FonRange( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Abc_Lit2Var(Vec_IntGetEntry(&p->vFonRange, f)):0;    }
-static inline int            Cba_FonSigned( Cba_Ntk_t * p, int f )           { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Abc_LitIsCompl(Vec_IntGetEntry(&p->vFonRange, f)):0; }
+static inline int            Cba_FonRangeId( Cba_Ntk_t * p, int f )          { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Vec_IntGetEntry(&p->vFonRange, f):0;}
+static inline int            Cba_FonRange( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Abc_Lit2Var( Cba_FonRangeId(p, f) );                       }
 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 int            Cba_FonSigned( Cba_Ntk_t * p, int f )           { return Cba_FonIsConst(f) ? Cba_FonConstSigned(p, f) : Abc_LitIsCompl(Cba_FonRangeId(p, f)); }
+static inline int            Cba_FonRangeSize( Cba_Ntk_t * p, int f )        { return Cba_FonIsConst(f) ? Cba_FonConstRangeSize(p, f):Cba_NtkRangeSize(p, Cba_FonRange(p, f)); }
 static inline void           Cba_FonSetRangeSign( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, f, x);                  }
-static inline void           Cba_FonSetRange( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, Abc_Var2Lit(f,0), x);       }
+static inline void           Cba_FonSetRange( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, f, Abc_Var2Lit(x,0));       }
 static inline void           Cba_FonHashRange( Cba_Ntk_t * p, int f, int l, int r ) { Cba_FonSetRange( p, f, Cba_NtkHashRange(p, l, r) );                                  }
 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); }
@@ -398,6 +401,11 @@ static inline int            Cba_FonNtkId( Cba_Ntk_t * p, int f )            { a
 static inline Cba_Ntk_t *    Cba_FonNtk( Cba_Ntk_t * p, int f )              { assert(Cba_FonIsReal(f)); return Cba_ObjNtk( p, Cba_FonObj(p, f) );                         }
 
 static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i, int k )     { assert(i>0); return Cba_FonObj( p, Cba_ObjFinFon(p, i, k) );                                }
+static inline int            Cba_ObjLeft( Cba_Ntk_t * p, int i )             { return Cba_FonLeft( p, Cba_ObjFon0(p, i) );                                                 }
+static inline int            Cba_ObjRight( Cba_Ntk_t * p, int i )            { return Cba_FonRight( p, Cba_ObjFon0(p, i) );                                                }
+static inline int            Cba_ObjRangeSize( Cba_Ntk_t * p, int i )        { return Cba_FonRangeSize( p, Cba_ObjFon0(p, i) );                                            }
+static inline int            Cba_ObjSigned( Cba_Ntk_t * p, int i )           { return Cba_FonSigned( p, Cba_ObjFon0(p, i) );                                               }
+static inline int            Cba_ObjSign( Cba_Ntk_t * p, int i )             { return Abc_Var2Lit( Cba_FonRangeSize(p, i), Cba_ObjSigned(p, i) );                          }
 
 ////////////////////////////////////////////////////////////////////////
 ///                          ITERATORS                               ///
@@ -435,10 +443,12 @@ static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i, int k )     { a
 #define Cba_NtkForEachBoxPrim( p, i )                                     \
     for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Cba_ObjIsBoxPrim(p, i) ) {} else
 
+#define Cba_NtkForEachFon( p, i )                                         \
+    for ( i = 1; i < Vec_IntSize(&p->vFonObj); i++ )
 #define Cba_NtkForEachFinFon( p, iFon, iFin )                             \
-    for ( iFin = 0; iFin < Vec_IntSize(&p->vFinFon) && (((iFon) = Vec_IntEntry(&p->vFinFon, iFin)), 1); iFin++ ) if ( !iFon ) {} else   
+    for ( iFin = 1; iFin < Vec_IntSize(&p->vFinFon) && (((iFon) = Vec_IntEntry(&p->vFinFon, iFin)), 1); iFin++ ) if ( !iFon ) {} else   
 #define Cba_NtkForEachFonName( p, NameId, iFon )                          \
-    for ( iFon = 0; iFon < Vec_IntSize(&p->vFonName) && (((NameId) = Vec_IntEntry(&p->vFonName, iFon)), 1); iFon++ ) if ( !NameId ) {} else   
+    for ( iFon = 1; iFon < Vec_IntSize(&p->vFonName) && (((NameId) = Vec_IntEntry(&p->vFonName, iFon)), 1); iFon++ ) if ( !NameId ) {} else   
 
 #define Cba_ObjForEachFin( p, iObj, iFin, k )                             \
     for ( k = 0, iFin = Cba_ObjFin0(p, iObj); iFin < Cba_ObjFin0(p, iObj+1); iFin++, k++ )
@@ -557,6 +567,7 @@ static inline void Cba_NtkFree( Cba_Ntk_t * p )
     Vec_IntErase( &p->vFinFon0 );    
     Vec_IntErase( &p->vFinObj );    
     Vec_IntErase( &p->vNtkObjs );    
+    Vec_IntErase( &p->vFonBits );    
     // other
     Vec_IntErase( &p->vArray0 );    
     Vec_IntErase( &p->vArray1 );    
@@ -779,6 +790,7 @@ static inline int Cba_NtkMemory( Cba_Ntk_t * p )
     nMem += (int)Vec_IntMemory(&p->vFinFon0 );  
     nMem += (int)Vec_IntMemory(&p->vFinObj );   
     nMem += (int)Vec_IntMemory(&p->vNtkObjs );  
+    nMem += (int)Vec_IntMemory(&p->vFonBits );  
     // other
     nMem += (int)Vec_IntMemory(&p->vArray1 );
     nMem += (int)Vec_IntMemory(&p->vArray1 );
@@ -1035,7 +1047,7 @@ static inline void Cba_ManPrintStats( Cba_Man_t * p, int nModules, int fVerbose
 
 
 /*=== cbaBlast.c =============================================================*/
-extern Gia_Man_t *   Cba_ManBlast( Cba_Man_t * p, int fBarBufs, int fVerbose );
+extern Gia_Man_t *   Cba_ManBlast( Cba_Man_t * p, int fBarBufs, int fSeq, int fVerbose );
 extern Cba_Man_t *   Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia );
 extern Cba_Man_t *   Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc );
 /*=== cbaCba.c ===============================================================*/
@@ -1043,8 +1055,10 @@ extern Cba_Man_t *   Cba_ManReadCba( char * pFileName );
 extern void          Cba_ManWriteCba( char * pFileName, Cba_Man_t * p );
 /*=== cbaCom.c ===============================================================*/
 /*=== cbaNtk.c ===============================================================*/
+extern void          Cba_NtkPrintStatsFull( Cba_Ntk_t * p, int fDistrib, int fVerbose );
+extern void          Cba_NtkPrintNodes( Cba_Ntk_t * p, int Type );
+extern void          Cba_NtkPrintDistribOld( Cba_Ntk_t * p );
 extern void          Cba_ManPrintDistrib( Cba_Man_t * p );
-extern void          Cba_NtkPrintDistrib( Cba_Ntk_t * p );
 //extern void           Cba_ManPrepareTypeNames( Cba_Man_t * p );
 extern void          Cba_NtkObjOrder( Cba_Ntk_t * p, Vec_Int_t * vObjs, Vec_Int_t * vNameIds );
 extern int           Cba_NtkCiFonNum( Cba_Ntk_t * p );
@@ -1057,9 +1071,11 @@ extern Cba_Man_t *   Cba_ManExtractGroup( Cba_Man_t * p, Vec_Int_t * vObjs );
 extern Cba_Man_t *   Cba_ManDeriveFromGia( Gia_Man_t * pGia, int fUseXor );
 extern Cba_Man_t *   Cba_ManInsertGroup( Cba_Man_t * p, Vec_Int_t * vObjs, Cba_Ntk_t * pSyn );
 /*=== cbaReadBlif.c ==========================================================*/
+extern Cba_Man_t *   Prs_ManBuildCbaBlif( char * pFileName, Vec_Ptr_t * vDes );
 extern void          Prs_ManReadBlifTest( char * pFileName );
 extern Cba_Man_t *   Cba_ManReadBlif( char * pFileName );
 /*=== cbaReadVer.c ===========================================================*/
+extern Cba_Man_t *   Prs_ManBuildCbaVerilog( char * pFileName, Vec_Ptr_t * vDes );
 extern void          Prs_ManReadVerilogTest( char * pFileName );
 extern Cba_Man_t *   Cba_ManReadVerilog( char * pFileName );
 /*=== cbaWriteBlif.c =========================================================*/
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index 70298b47..f91887ee 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -36,6 +36,540 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Helper functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_NtkPrepareBits( Cba_Ntk_t * p )
+{
+    int i, nBits = 0;
+    Cba_NtkCleanFonCopies( p );
+    Cba_NtkForEachFon( p, i )
+    {
+        Cba_FonSetCopy( p, i, nBits );
+        nBits += Cba_FonRangeSize( p, i );
+    }
+    return nBits;
+}
+int * Cba_VecCopy( Vec_Int_t * vOut, int * pArray, int nSize )
+{
+    int i; Vec_IntClear( vOut );
+    for( i = 0; i < nSize; i++) 
+        Vec_IntPush( vOut, pArray[i] );
+    return Vec_IntArray( vOut );
+}
+int Cba_ReadHexDigit( char HexChar )
+{
+    if ( HexChar >= '0' && HexChar <= '9' )
+        return HexChar - '0';
+    if ( HexChar >= 'A' && HexChar <= 'F' )
+        return HexChar - 'A' + 10;
+    if ( HexChar >= 'a' && HexChar <= 'f' )
+        return HexChar - 'a' + 10;
+    assert( 0 ); // not a hexadecimal symbol
+    return -1; // return value which makes no sense
+}
+void Cba_BlastConst( Cba_Ntk_t * p, Vec_Int_t * vOut, int iFon, int nTotal, int fSigned )
+{
+    char * pConst = Cba_NtkConst(p, Cba_FonConst(iFon));
+    char * pLimit = pConst + strlen(pConst);
+    int i, Number, nBits = atoi( pConst );
+    assert( nBits <= nTotal );
+    while ( *pConst >= '0' && *pConst <= '9' )
+        pConst++;
+    assert( *pConst == '\'' );
+    pConst++;
+    if ( *pConst == 's' ) // assume signedness is already used in setting fSigned
+        pConst++;
+    Vec_IntClear( vOut );
+    if ( *pConst == 'b' )
+    {
+        while ( --pLimit > pConst )
+            Vec_IntPush( vOut, *pLimit == '0' ? 0 : 1 );
+    }
+    else if ( *pConst == 'h' )
+    {
+        while ( --pLimit > pConst )
+        {
+            Number = Cba_ReadHexDigit( *pLimit );
+            for ( i = 0; i < 4; i++ )
+                Vec_IntPush( vOut, (Number >> i) & 1 );
+        }
+        if ( Vec_IntSize(vOut) > nTotal )
+            Vec_IntShrink( vOut, nTotal );
+    }
+    else if ( *pConst == 'd' )
+    {
+        Number = atoi( pConst+1 );
+        assert( Number <= 0x7FFFFFFF );
+        for ( i = 0; i < 32; i++ )
+            Vec_IntPush( vOut, (Number >> i) & 1 );
+        if ( Vec_IntSize(vOut) > nTotal )
+            Vec_IntShrink( vOut, nTotal );
+    }
+    else assert( 0 );
+    if ( fSigned && Vec_IntSize(vOut) < nTotal )
+        Vec_IntFillExtra( vOut, nTotal - Vec_IntSize(vOut), Vec_IntEntryLast(vOut) );
+}
+int * Cba_VecLoadFanins( Cba_Ntk_t * p, Vec_Int_t * vOut, int iFon, int * pFanins, int nFanins, int nTotal, int fSigned )
+{
+    assert( nFanins <= nTotal );
+    if ( Cba_FonIsReal(iFon) )
+    {
+        int i, Fill = fSigned ? pFanins[nFanins-1] : 0;
+        Vec_IntClear( vOut );
+        for( i = 0; i < nTotal; i++) 
+            Vec_IntPush( vOut, i < nFanins ? pFanins[i] : Fill );
+    }
+    else if ( Cba_FonIsConst(iFon) )
+        Cba_BlastConst( p, vOut, iFon, nTotal, fSigned );
+    else if ( iFon == 0 ) // undriven input
+        Vec_IntFill( vOut, nTotal, 0 );
+    else assert( 0 );
+    assert( Vec_IntSize(vOut) == nTotal );
+    return Vec_IntArray( vOut );
+}
+int Cba_NtkMuxTree_rec( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData, int Shift )
+{
+    int iLit0, iLit1;
+    if ( nCtrl == 0 )
+        return Vec_IntEntry( vData, Shift );
+    iLit0 = Cba_NtkMuxTree_rec( pNew, pCtrl, nCtrl-1, vData, Shift );
+    iLit1 = Cba_NtkMuxTree_rec( pNew, pCtrl, nCtrl-1, vData, Shift + (1<<(nCtrl-1)) );
+    return Gia_ManHashMux( pNew, pCtrl[nCtrl-1], iLit1, iLit0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Bit blasting for specific operations.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
+{
+    int * pRes = Cba_VecCopy( vRes, pNum, nNum );
+    int Fill = fSticky ? pNum[nNum-1] : 0;
+    int i, j, fShort = 0;
+    if ( nShift > 32 )
+        nShift = 32;
+    assert( nShift <= 32 );
+    for( i = 0; i < nShift; i++ ) 
+        for( j = 0; j < nNum - fSticky; j++ ) 
+        {
+            if( fShort || j + (1<<i) >= nNum ) 
+            {
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], Fill, pRes[j] );
+                if ( (1<<i) > nNum ) 
+                    fShort = 1;
+            } 
+            else 
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], pRes[j+(1<<i)], pRes[j] );
+        }
+}
+void Cba_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
+{
+    int * pRes = Cba_VecCopy( vRes, pNum, nNum );
+    int Fill = fSticky ? pNum[0] : 0;
+    int i, j, fShort = 0;
+    if ( nShift > 32 )
+        nShift = 32;
+    assert( nShift <= 32 );
+    for( i = 0; i < nShift; i++ ) 
+        for( j = nNum-1; j >= fSticky; j-- ) 
+        {
+            if( fShort || (1<<i) > j ) 
+            {
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], Fill, pRes[j] );
+                if ( (1<<i) > nNum ) 
+                    fShort = 1;
+            } 
+            else 
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], pRes[j-(1<<i)], pRes[j] );
+        }
+}
+void Cba_BlastRotateRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, Vec_Int_t * vRes )
+{
+    int * pRes = Cba_VecCopy( vRes, pNum, nNum );
+    int i, j, * pTemp = ABC_ALLOC( int, nNum );
+    assert( nShift <= 32 );
+    for( i = 0; i < nShift; i++, pRes = Cba_VecCopy(vRes, pTemp, nNum) ) 
+        for( j = 0; j < nNum; j++ ) 
+            pTemp[j] = Gia_ManHashMux( pNew, pShift[i], pRes[(j+(1<<i))%nNum], pRes[j] );
+    ABC_FREE( pTemp );
+}
+void Cba_BlastRotateLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, Vec_Int_t * vRes )
+{
+    int * pRes = Cba_VecCopy( vRes, pNum, nNum );
+    int i, j, * pTemp = ABC_ALLOC( int, nNum );
+    assert( nShift <= 32 );
+    for( i = 0; i < nShift; i++, pRes = Cba_VecCopy(vRes, pTemp, nNum) ) 
+        for( j = 0; j < nNum; j++ ) 
+        {
+            int move = (j >= (1<<i)) ? (j-(1<<i))%nNum : (nNum - (((1<<i)-j)%nNum)) % nNum;
+            pTemp[j] = Gia_ManHashMux( pNew, pShift[i], pRes[move], pRes[j] );
+//            pTemp[j] = Gia_ManHashMux( pNew, pShift[i], pRes[((unsigned)(nNum-(1<<i)+j))%nNum], pRes[j] );
+        }
+    ABC_FREE( pTemp );
+}
+int Cba_BlastReduction( Gia_Man_t * pNew, int * pFans, int nFans, int Type )
+{
+    if ( Type == CBA_BOX_RAND )
+    {
+        int k, iLit = 1;
+        for ( k = 0; k < nFans; k++ )
+            iLit = Gia_ManHashAnd( pNew, iLit, pFans[k] );
+        return iLit;
+    }
+    if ( Type == CBA_BOX_ROR )
+    {
+        int k, iLit = 0;
+        for ( k = 0; k < nFans; k++ )
+            iLit = Gia_ManHashOr( pNew, iLit, pFans[k] );
+        return iLit;
+    }
+    if ( Type == CBA_BOX_RXOR )
+    {
+        int k, iLit = 0;
+        for ( k = 0; k < nFans; k++ )
+            iLit = Gia_ManHashXor( pNew, iLit, pFans[k] );
+        return iLit;
+    }
+    assert( 0 );
+    return -1;
+}
+int Cba_BlastLess2( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
+{
+    int k, iKnown = 0, iRes = 0;
+    for ( k = nBits - 1; k >= 0; k-- )
+    {
+        iRes   = Gia_ManHashMux( pNew, iKnown, iRes, Gia_ManHashAnd(pNew, Abc_LitNot(pArg0[k]), pArg1[k]) );
+        iKnown = Gia_ManHashOr( pNew, iKnown, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) );
+        if ( iKnown == 1 )
+            break;
+    }
+    return iRes;
+}
+void Cba_BlastLess_rec( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits, int * pYes, int * pNo )
+{
+    if ( nBits > 1 )
+    {
+        int Yes = Gia_ManHashAnd( pNew, Abc_LitNot(pArg0[nBits-1]), pArg1[nBits-1] ), YesR;
+        int No  = Gia_ManHashAnd( pNew, Abc_LitNot(pArg1[nBits-1]), pArg0[nBits-1] ), NoR;
+        if ( Yes == 1 || No == 1 )
+        {
+            *pYes = Yes;
+            *pNo  = No;
+            return;
+        }
+        Cba_BlastLess_rec( pNew, pArg0, pArg1, nBits-1, &YesR, &NoR );
+        *pYes = Gia_ManHashOr( pNew, Yes, Gia_ManHashAnd(pNew, Abc_LitNot(No),  YesR) );
+        *pNo  = Gia_ManHashOr( pNew, No,  Gia_ManHashAnd(pNew, Abc_LitNot(Yes), NoR ) );
+        return;
+    }
+    assert( nBits == 1 );
+    *pYes = Gia_ManHashAnd( pNew, Abc_LitNot(pArg0[0]), pArg1[0] );
+    *pNo  = Gia_ManHashAnd( pNew, Abc_LitNot(pArg1[0]), pArg0[0] );
+}
+int Cba_BlastLess( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
+{
+    int Yes, No;
+    if ( nBits == 0 )
+        return 0;
+    Cba_BlastLess_rec( pNew, pArg0, pArg1, nBits, &Yes, &No );
+    return Yes;
+}
+int Cba_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
+{
+    int iDiffSign = Gia_ManHashXor( pNew, pArg0[nBits-1], pArg1[nBits-1] );
+    return Gia_ManHashMux( pNew, iDiffSign, pArg0[nBits-1], Cba_BlastLess(pNew, pArg0, pArg1, nBits-1) );
+}
+void Cba_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
+{
+    int Xor  = Gia_ManHashXor(pNew, a, b);
+    int And1 = Gia_ManHashAnd(pNew, a, b);
+    int And2 = Gia_ManHashAnd(pNew, c, Xor);
+    *ps      = Gia_ManHashXor(pNew, c, Xor);
+    *pc      = Gia_ManHashOr (pNew, And1, And2);
+}
+int Cba_BlastAdder( Gia_Man_t * pNew, int Carry, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
+{
+    int b;
+    for ( b = 0; b < nBits; b++ )
+        Cba_BlastFullAdder( pNew, pAdd0[b], pAdd1[b], Carry, &Carry, &pAdd0[b] );
+    return Carry;
+}
+void Cba_BlastSubtract( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
+{
+    int b, Carry = 1;
+    for ( b = 0; b < nBits; b++ )
+        Cba_BlastFullAdder( pNew, pAdd0[b], Abc_LitNot(pAdd1[b]), Carry, &Carry, &pAdd0[b] );
+}
+void Cba_BlastMinus( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vRes )
+{
+    int * pRes  = Cba_VecCopy( vRes, pNum, nNum );
+    int i, invert = 0;
+    for ( i = 0; i < nNum; i++ )
+    {
+        pRes[i] = Gia_ManHashMux( pNew, invert, Abc_LitNot(pRes[i]), pRes[i] );
+        invert = Gia_ManHashOr( pNew, invert, pNum[i] );    
+    }
+}
+void Cba_BlastMultiplier2( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits, Vec_Int_t * vTemp, Vec_Int_t * vRes )
+{
+    int i, j;
+    Vec_IntFill( vRes, nBits, 0 );
+    for ( i = 0; i < nBits; i++ )
+    {
+        Vec_IntFill( vTemp, i, 0 );
+        for ( j = 0; Vec_IntSize(vTemp) < nBits; j++ )
+            Vec_IntPush( vTemp, Gia_ManHashAnd(pNew, pArg0[j], pArg1[i]) );
+        assert( Vec_IntSize(vTemp) == nBits );
+        Cba_BlastAdder( pNew, 0, Vec_IntArray(vRes), Vec_IntArray(vTemp), nBits );
+    }
+}
+void Cba_BlastFullAdderCtrl( Gia_Man_t * pNew, int a, int ac, int b, int c, int * pc, int * ps, int fNeg )
+{
+    int And  = Abc_LitNotCond( Gia_ManHashAnd(pNew, a, ac), fNeg );
+    Cba_BlastFullAdder( pNew, And, b, c, pc, ps );
+}
+void Cba_BlastFullAdderSubtr( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps, int fSub )
+{
+    Cba_BlastFullAdder( pNew, Gia_ManHashXor(pNew, a, fSub), b, c, pc, ps );
+}
+void Cba_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int fSigned )
+{
+    int * pRes, * pArgC, * pArgS, a, b, Carry = fSigned;
+    assert( nArgA > 0 && nArgB > 0 );
+    assert( fSigned == 0 || fSigned == 1 );
+    // prepare result
+    Vec_IntFill( vRes, nArgA + nArgB, 0 );
+    pRes = Vec_IntArray( vRes );
+    // prepare intermediate storage
+    Vec_IntFill( vTemp, 2 * nArgA, 0 );
+    pArgC = Vec_IntArray( vTemp );
+    pArgS = pArgC + nArgA;
+    // create matrix
+    for ( b = 0; b < nArgB; b++ )
+        for ( a = 0; a < nArgA; a++ )
+            Cba_BlastFullAdderCtrl( pNew, pArgA[a], pArgB[b], pArgS[a], pArgC[a], 
+                &pArgC[a], a ? &pArgS[a-1] : &pRes[b], fSigned && ((a+1 == nArgA) ^ (b+1 == nArgB)) );
+    // final addition
+    pArgS[nArgA-1] = fSigned;
+    for ( a = 0; a < nArgA; a++ )
+        Cba_BlastFullAdderCtrl( pNew, 1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], 0 );
+}
+void Cba_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
+{
+    int * pRes  = Cba_VecCopy( vRes, pNum, nNum );
+    int * pQuo  = ABC_ALLOC( int, nNum );
+    int * pTemp = ABC_ALLOC( int, nNum );
+    int i, j, known, borrow, y_bit, top_bit;
+    assert( nNum == nDiv );
+    for ( j = nNum - 1; j >= 0; j-- ) 
+    {
+        known = 0;
+        for ( i = nNum - 1; i > nNum - 1 - j; i-- ) 
+        {
+            known = Gia_ManHashOr( pNew, known, pDiv[i] );
+            if( known == 1 ) 
+                break;
+        }
+        pQuo[j] = known;
+        for ( i = nNum - 1; i >= 0; i-- ) 
+        {
+            if ( known == 1 ) 
+                break;
+            y_bit = (i >= j) ? pDiv[i-j] : 0;
+            pQuo[j] = Gia_ManHashMux( pNew, known, pQuo[j], Gia_ManHashAnd( pNew, y_bit, Abc_LitNot(pRes[i]) ) );
+            known = Gia_ManHashOr( pNew, known, Gia_ManHashXor(pNew, y_bit, pRes[i]));
+        }
+        pQuo[j] = Abc_LitNot(pQuo[j]);
+        if ( pQuo[j] == 0 )
+            continue;
+        borrow = 0;
+        for ( i = 0; i < nNum; i++ ) 
+        {
+            top_bit  = Gia_ManHashMux( pNew, borrow, Abc_LitNot(pRes[i]), pRes[i] );
+            y_bit    = (i >= j) ? pDiv[i-j] : 0;
+            borrow   = Gia_ManHashMux( pNew, pRes[i], Gia_ManHashAnd(pNew, borrow, y_bit), Gia_ManHashOr(pNew, borrow, y_bit) );
+            pTemp[i] = Gia_ManHashXor( pNew, top_bit, y_bit );
+        }
+        if ( pQuo[j] == 1 ) 
+            Cba_VecCopy( vRes, pTemp, nNum );
+        else 
+            for( i = 0; i < nNum; i++ ) 
+                pRes[i] = Gia_ManHashMux( pNew, pQuo[j], pTemp[i], pRes[i] );
+    }
+    ABC_FREE( pTemp );
+    if ( fQuo )
+        Cba_VecCopy( vRes, pQuo, nNum );
+    ABC_FREE( pQuo );
+}
+// non-restoring divider
+void Cba_BlastDivider2( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
+{
+    int i, * pRes  = Vec_IntArray(vRes);
+    int k, * pQuo  = ABC_ALLOC( int, nNum );
+    assert( nNum > 0 && nDiv > 0 );
+    assert( Vec_IntSize(vRes) < nNum + nDiv );
+    for ( i = 0; i < nNum + nDiv; i++ )
+        pRes[i] = i < nNum ? pNum[i] : 0;
+    for ( i = nNum-1; i >= 0; i-- )
+    {
+        int Cntrl = i == nNum-1 ? 1 : pQuo[i+1];
+        int Carry = Cntrl;
+        for ( k = 0; k <= nDiv; k++ )
+            Cba_BlastFullAdderSubtr( pNew, k < nDiv ? pDiv[k] : 0, pRes[i+k], Carry, &Carry, &pRes[i+k], Cntrl );
+        pQuo[i] = Abc_LitNot(pRes[i+nDiv]);
+    }
+    if ( fQuo )
+        Cba_VecCopy( vRes, pQuo, nNum );
+    else
+    {
+        int Carry = 0, Temp;
+        for ( k = 0; k < nDiv; k++ )
+        {
+            Cba_BlastFullAdder( pNew, pDiv[k], pRes[k], Carry, &Carry, &Temp );
+            pRes[k] = Gia_ManHashMux( pNew, pQuo[0], pRes[k], Temp );
+        }
+        Vec_IntShrink( vRes, nDiv );
+    }
+    ABC_FREE( pQuo );
+}
+void Cba_BlastDividerSigned( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
+{
+    Vec_Int_t * vNum   = Vec_IntAlloc( nNum );
+    Vec_Int_t * vDiv   = Vec_IntAlloc( nDiv );
+    Vec_Int_t * vRes00 = Vec_IntAlloc( nNum + nDiv );
+    Vec_Int_t * vRes01 = Vec_IntAlloc( nNum + nDiv );
+    Vec_Int_t * vRes10 = Vec_IntAlloc( nNum + nDiv );
+    Vec_Int_t * vRes11 = Vec_IntAlloc( nNum + nDiv );
+    Vec_Int_t * vRes2  = Vec_IntAlloc( nNum );
+    int k, iDiffSign   = Gia_ManHashXor( pNew, pNum[nNum-1], pDiv[nDiv-1] );
+    Cba_BlastMinus( pNew, pNum, nNum, vNum );
+    Cba_BlastMinus( pNew, pDiv, nDiv, vDiv );
+    Cba_BlastDivider( pNew,               pNum, nNum,               pDiv, nDiv, fQuo, vRes00 );
+    Cba_BlastDivider( pNew,               pNum, nNum, Vec_IntArray(vDiv), nDiv, fQuo, vRes01 );
+    Cba_BlastDivider( pNew, Vec_IntArray(vNum), nNum,               pDiv, nDiv, fQuo, vRes10 );
+    Cba_BlastDivider( pNew, Vec_IntArray(vNum), nNum, Vec_IntArray(vDiv), nDiv, fQuo, vRes11 );
+    Vec_IntClear( vRes );
+    for ( k = 0; k < nNum; k++ )
+    {
+        int Data0 =  Gia_ManHashMux( pNew, pDiv[nDiv-1], Vec_IntEntry(vRes01,k), Vec_IntEntry(vRes00,k) );
+        int Data1 =  Gia_ManHashMux( pNew, pDiv[nDiv-1], Vec_IntEntry(vRes11,k), Vec_IntEntry(vRes10,k) );
+        Vec_IntPush( vRes, Gia_ManHashMux(pNew, pNum[nNum-1], Data1, Data0) );
+    }
+    Cba_BlastMinus( pNew, Vec_IntArray(vRes), nNum, vRes2 );
+    for ( k = 0; k < nNum; k++ )
+        Vec_IntWriteEntry( vRes, k, Gia_ManHashMux(pNew, fQuo ? iDiffSign : pNum[nNum-1], Vec_IntEntry(vRes2,k), Vec_IntEntry(vRes,k)) );
+    Vec_IntFree( vNum );
+    Vec_IntFree( vDiv );
+    Vec_IntFree( vRes00 );
+    Vec_IntFree( vRes01 );
+    Vec_IntFree( vRes10 );
+    Vec_IntFree( vRes11 );
+    Vec_IntFree( vRes2 );
+    assert( Vec_IntSize(vRes) == nNum );
+}
+void Cba_BlastZeroCondition( Gia_Man_t * pNew, int * pDiv, int nDiv, Vec_Int_t * vRes )
+{
+    int i, Entry, iLit = Cba_BlastReduction( pNew, pDiv, nDiv, CBA_BOX_ROR );
+    Vec_IntForEachEntry( vRes, Entry, i )
+        Vec_IntWriteEntry( vRes, i, Gia_ManHashAnd(pNew, iLit, Entry) );
+}
+void Cba_BlastTable( Gia_Man_t * pNew, word * pTable, int * pFans, int nFans, int nOuts, Vec_Int_t * vRes )
+{
+    extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+    Vec_Int_t * vMemory = Vec_IntAlloc( 0 );
+    Vec_Int_t vLeaves = { nFans, nFans, pFans };
+    word * pTruth = ABC_ALLOC( word, Abc_TtWordNum(nFans) );
+    int o, i, m, iLit, nMints = (1 << nFans);
+    Vec_IntClear( vRes );
+    for ( o = 0; o < nOuts; o++ )
+    {
+        // derive truth table
+        memset( pTruth, 0, sizeof(word) * Abc_TtWordNum(nFans) );
+        for ( m = 0; m < nMints; m++ )
+            for ( i = 0; i < nFans; i++ )
+                if ( Abc_TtGetBit( pTable, m * nFans + i ) )
+                    Abc_TtSetBit( pTruth, m );
+        // implement truth table
+        if ( nFans < 6 )
+            pTruth[0] = Abc_Tt6Stretch( pTruth[0], nFans );
+        iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, nFans, vMemory, &vLeaves, 1 );
+        Vec_IntPush( vRes, iLit );
+    }
+    Vec_IntFree( vMemory );
+    ABC_FREE( pTruth );
+}
+void Cba_BlastPower( Gia_Man_t * pNew, int * pNum, int nNum, int * pExp, int nExp, Vec_Int_t * vTemp, Vec_Int_t * vRes )
+{
+    Vec_Int_t * vDegrees = Vec_IntAlloc( 2*nNum );
+    Vec_Int_t * vResTemp = Vec_IntAlloc( 2*nNum );
+    int i, * pDegrees = NULL, * pRes = Vec_IntArray(vRes);
+    int k, * pResTemp = Vec_IntArray(vResTemp);
+    Vec_IntFill( vRes, nNum, 0 );
+    Vec_IntWriteEntry( vRes, 0, 1 );
+    for ( i = 0; i < nExp; i++ )
+    {
+        if ( i == 0 )
+            pDegrees = Cba_VecCopy( vDegrees, pNum, nNum );
+        else
+        {
+            Cba_BlastMultiplier2( pNew, pDegrees, pDegrees, nNum, vTemp, vResTemp );
+            pDegrees = Cba_VecCopy( vDegrees, pResTemp, nNum );
+        }
+        Cba_BlastMultiplier2( pNew, pRes, pDegrees, nNum, vTemp, vResTemp );
+        for ( k = 0; k < nNum; k++ )
+            pRes[k] = Gia_ManHashMux( pNew, pExp[i], pResTemp[k], pRes[k] );
+    }
+    Vec_IntFree( vResTemp );
+    Vec_IntFree( vDegrees );
+}
+void Cba_BlastSqrt( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp, Vec_Int_t * vRes )
+{
+    int * pRes, * pSum, * pSumP;
+    int i, k, Carry = -1;
+    assert( nNum % 2 == 0 );
+    Vec_IntFill( vRes, nNum/2, 0 );
+    Vec_IntFill( vTmp, 2*nNum, 0 );
+    pRes = Vec_IntArray( vRes );
+    pSum = Vec_IntArray( vTmp );
+    pSumP = pSum + nNum;
+    for ( i = 0; i < nNum/2; i++ )
+    {
+        pSumP[0] = pNum[nNum-2*i-2];
+        pSumP[1] = pNum[nNum-2*i-1];
+        for ( k = 0; k < i+1; k++ )
+            pSumP[k+2] = pSum[k];
+        for ( k = 0; k < i + 3; k++ )
+        {
+            if ( k >= 2 && k < i + 2 ) // middle ones
+                Cba_BlastFullAdder( pNew, pSumP[k], Abc_LitNot(pRes[i-k+1]), Carry, &Carry, &pSum[k] );
+            else
+                Cba_BlastFullAdder( pNew, pSumP[k], Abc_LitNot(k ? Carry:1), 1,     &Carry, &pSum[k] );
+            if ( k == 0 || k > i )
+                Carry = Abc_LitNot(Carry);
+        }
+        pRes[i] = Abc_LitNot(Carry);
+        for ( k = 0; k < i + 3; k++ )
+            pSum[k] = Gia_ManHashMux( pNew, pRes[i], pSum[k], pSumP[k] );
+    }
+    Vec_IntReverseOrder( vRes );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -45,9 +579,452 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cba_ManBlast( Cba_Man_t * p, int fBarBufs, int fVerbose )
+Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq )
 {
-    return NULL;
+    int fVerbose = 0;
+    int fUseOldMultiplierBlasting = 0;
+    Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
+    Vec_Int_t * vTemp0, * vTemp1, * vTemp2, * vRes;
+    Vec_Str_t * vInit = fSeq ? Vec_StrAlloc(100) : NULL;
+    Vec_Int_t * vBits = &p->vFonBits;
+    int nBits = Cba_NtkPrepareBits( p );
+    int * pFans0, * pFans1, * pFans2;
+    int nRange, nRange0, nRange1, nRange2;
+    int Type, iFon, iFon0, iFon1, iFon2, fSigned01;
+    int i, k, b, iFin, iObj, iLit, nAndPrev;
+    Vec_IntClear( vBits );
+    Vec_IntGrow( vBits, nBits );
+    vTemp0 = Vec_IntAlloc( 1000 );
+    vTemp1 = Vec_IntAlloc( 1000 );
+    vTemp2 = Vec_IntAlloc( 1000 );
+    vRes   = Vec_IntAlloc( 1000 );
+    // clean AND-gate counters
+    memset( p->pDesign->nAnds, 0, sizeof(int) * CBA_BOX_LAST );
+    // create AIG manager
+    pNew = Gia_ManStart( 5 * Cba_NtkObjNum(p) + 1000 );
+    pNew->pName = Abc_UtilStrsav( Cba_ManName(p->pDesign) );
+    Gia_ManHashAlloc( pNew );
+    // blast in the topological order
+    Cba_NtkForEachObj( p, i )
+    {
+        Type = Cba_ObjType(p, i);
+        if ( Type == CBA_OBJ_PO )
+            continue;
+        assert( Vec_IntSize(vBits) == Cba_FonCopy(p, Cba_ObjFon0(p, i)) );
+        nRange = Cba_ObjRangeSize(p, i); assert( nRange > 0 );
+        if ( Cba_ObjIsPi(p, i) || Cba_ObjIsSeq(p, i) )
+        {
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vBits, Gia_ManAppendCi(pNew) );
+            assert( Type == CBA_BOX_DFFCPL || Cba_ObjFonNum(p, i) == 1 );
+            continue;
+        }
+        assert( Cba_ObjFinNum(p, i) > 0 );
+        iFon0     = Cba_ObjFinNum(p, i) > 0 ? Cba_ObjFinFon(p, i, 0) : -1;
+        iFon1     = Cba_ObjFinNum(p, i) > 1 ? Cba_ObjFinFon(p, i, 1) : -1;
+        iFon2     = Cba_ObjFinNum(p, i) > 2 ? Cba_ObjFinFon(p, i, 2) : -1;
+        nRange0   = Cba_ObjFinNum(p, i) > 0 ? Cba_FonRangeSize(p, iFon0) : -1; 
+        nRange1   = Cba_ObjFinNum(p, i) > 1 ? Cba_FonRangeSize(p, iFon1) : -1; 
+        nRange2   = Cba_ObjFinNum(p, i) > 2 ? Cba_FonRangeSize(p, iFon2) : -1; 
+        pFans0    = (Cba_ObjFinNum(p, i) > 0 && Cba_FonIsReal(iFon0)) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFon0) ) : NULL;
+        pFans1    = (Cba_ObjFinNum(p, i) > 1 && Cba_FonIsReal(iFon1)) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFon1) ) : NULL;
+        pFans2    = (Cba_ObjFinNum(p, i) > 2 && Cba_FonIsReal(iFon2)) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFon2) ) : NULL;
+        fSigned01 = (Cba_ObjFinNum(p, i) > 1 && Cba_FonSigned(p, iFon0) && Cba_FonSigned(p, iFon1));
+        nAndPrev  = Gia_ManAndNum(pNew);
+        Vec_IntClear( vRes );
+        if ( Type == CBA_BOX_SLICE )
+        {
+            int Left   = Cba_ObjLeft( p, i );
+            int Right  = Cba_ObjRight( p, i );
+            int Left0  = Cba_FonLeft( p, iFon0 );
+            int Right0 = Cba_FonRight( p, iFon0 );
+            if ( Left > Right )
+            {
+                assert( Left0 > Right0 );
+                for ( k = Right; k <= Left; k++ )
+                    Vec_IntPush( vRes, pFans0[k - Right0] );
+            }
+            else
+            {
+                assert( Left < Right && Left0 < Right0 );
+                for ( k = Right; k >= Left; k-- )
+                    Vec_IntPush( vRes, pFans0[k - Right0] );
+            }
+        }
+        else if ( Type == CBA_BOX_CONCAT )
+        {
+            int iFinT, iFonT, nTotal = 0;
+            Cba_ObjForEachFinFon( p, i, iFinT, iFonT, k )
+                nTotal += Cba_FonRangeSize( p, iFonT );
+            assert( nRange == nTotal );
+            Cba_ObjForEachFinFon( p, i, iFinT, iFonT, k )
+            {
+                nRange0 = Cba_FonRangeSize( p, iFonT );
+                pFans0  = Cba_FonIsReal(iFonT) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFonT) ) : NULL;
+                pFans0  = Cba_VecLoadFanins( p, vTemp0, iFonT, pFans0, nRange0, nRange0, Cba_FonSigned(p, iFonT) );
+                for ( b = 0; b < nRange0; b++ )
+                    Vec_IntPush( vRes, pFans0[b] );
+            }
+        }
+        else if ( Type == CBA_BOX_BUF )
+        {
+            int nRangeMax = Abc_MaxInt( nRange0, nRange );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, Cba_FonSigned(p, iFon0) );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vRes, pArg0[k] );
+        }
+        else if ( Type >= CBA_BOX_CF && Type <= CBA_BOX_CZ )
+        {
+            assert( 0 );
+            //word * pTruth = (word *)Cba_ObjFanins(p, i);
+            //for ( k = 0; k < nRange; k++ )
+            //    Vec_IntPush( vRes, Abc_TtGetBit(pTruth, k) );
+        }
+        else if ( Type == CBA_BOX_MUX || Type == CBA_BOX_NMUX )
+        {
+            // It is strange and disturbing that Verilog standard treats these statements differently:
+            // Statement 1:   
+            //     assign o = i ? b : a;
+            // Statement 2:
+            //     always @( i or a or b )
+            //       begin
+            //         case ( i )
+            //           0 : o = a ;
+            //           1 : o = b ;
+            //         endcase
+            //       end
+            // If a is signed and b is unsigned,  Statement 1 does not sign-extend a, while Statement 2 does.
+            // The signedness of o does not matter.
+            //
+            // Below we (somewhat arbitrarily) distinguish these two by assuming that 
+            // Statement 1 has three fanins, while Statement 2 has more than three fanins.
+            //
+            int iFinT, iFonT, fSigned = 1;
+            assert( nRange0 >= 1 && Cba_ObjFinNum(p, i) >= 3 );
+            assert( 1 + (1 << nRange0) == Cba_ObjFinNum(p, i) );
+            Cba_ObjForEachFinFon( p, i, iFinT, iFonT, k )
+                if ( k > 0 )
+                    fSigned &= Cba_FonSigned(p, iFonT);
+            for ( b = 0; b < nRange; b++ )
+            {
+                Vec_IntClear( vTemp0 );
+                Cba_ObjForEachFinFon( p, i, iFinT, iFonT, k )
+                    if ( k > 0 )
+                    {
+                        nRange1 = Cba_FonRangeSize( p, iFonT );
+                        pFans1  = Cba_FonIsReal(iFonT) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFonT) ) : NULL;
+                        if ( Cba_ObjFinNum(p, i) == 3 ) // Statement 1
+                            Vec_IntPush( vTemp0, k < nRange1 ? pFans1[k] : (fSigned? pFans1[nRange1-1] : 0) );
+                        else // Statement 2
+                            Vec_IntPush( vTemp0, k < nRange1 ? pFans1[k] : (Cba_FonSigned(p, iFonT)? pFans1[nRange1-1] : 0) );
+                    }
+                Vec_IntPush( vRes, Cba_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) );
+            }
+        }
+        else if ( Type == CBA_BOX_SHIR || Type == CBA_BOX_SHIRA ||
+                  Type == CBA_BOX_SHIL || Type == CBA_BOX_SHILA )
+        {
+            int nRangeMax = Abc_MaxInt( nRange, nRange0 );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, Cba_FonSigned(p, iFon0) );
+            if ( Type == CBA_BOX_SHIR || Type == CBA_BOX_SHIRA )
+                Cba_BlastShiftRight( pNew, pArg0, nRangeMax, pFans1, nRange1, Cba_FonSigned(p, iFon0) && Type == CBA_BOX_SHIRA, vRes );
+            else
+                Cba_BlastShiftLeft( pNew, pArg0, nRangeMax, pFans1, nRange1, 0, vRes );
+            Vec_IntShrink( vRes, nRange );
+        }
+        else if ( Type == CBA_BOX_ROTR )
+        {
+            assert( nRange0 == nRange );
+            Cba_BlastRotateRight( pNew, pFans0, nRange0, pFans1, nRange1, vRes );
+        }
+        else if ( Type == CBA_BOX_ROTL )
+        {
+            assert( nRange0 == nRange );
+            Cba_BlastRotateLeft( pNew, pFans0, nRange0, pFans1, nRange1, vRes );
+        }
+        else if ( Type == CBA_BOX_INV )
+        {
+            int nRangeMax = Abc_MaxInt( nRange, nRange0 );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, Cba_FonSigned(p, iFon0) );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vRes, Abc_LitNot(pArg0[k]) );
+        }
+        else if ( Type == CBA_BOX_AND )
+        {
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vRes, Gia_ManHashAnd(pNew, pArg0[k], pArg1[k]) );
+        }
+        else if ( Type == CBA_BOX_OR )
+        {
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vRes, Gia_ManHashOr(pNew, pArg0[k], pArg1[k]) );
+        }
+        else if ( Type == CBA_BOX_XOR )
+        {
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vRes, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) );
+        }
+        else if ( Type == CBA_BOX_LNOT )
+        {
+            iLit = Cba_BlastReduction( pNew, pFans0, nRange0, CBA_BOX_ROR );
+            Vec_IntFill( vRes, 1, Abc_LitNot(iLit) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_LAND )
+        {
+            int iLit0 = Cba_BlastReduction( pNew, pFans0, nRange0, CBA_BOX_ROR );
+            int iLit1 = Cba_BlastReduction( pNew, pFans1, nRange1, CBA_BOX_ROR );
+            Vec_IntFill( vRes, 1, Gia_ManHashAnd(pNew, iLit0, iLit1) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_LOR )
+        {
+            int iLit0 = Cba_BlastReduction( pNew, pFans0, nRange0, CBA_BOX_ROR );
+            int iLit1 = Cba_BlastReduction( pNew, pFans1, nRange1, CBA_BOX_ROR );
+            Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, iLit0, iLit1) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_LXOR )
+        {
+            int iLit0 = Cba_BlastReduction( pNew, pFans0, nRange0, CBA_BOX_ROR );
+            int iLit1 = Cba_BlastReduction( pNew, pFans1, nRange1, CBA_BOX_ROR );
+            Vec_IntFill( vRes, 1, Gia_ManHashXor(pNew, iLit0, iLit1) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_EQU || Type == CBA_BOX_NEQU )
+        {
+            int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            for ( k = 0; k < nRangeMax; k++ )
+                iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) ); 
+            Vec_IntFill( vRes, 1, Abc_LitNotCond(iLit, Type == CBA_BOX_EQU) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_LTHAN || Type == CBA_BOX_METHAN ||
+                  Type == CBA_BOX_MTHAN || Type == CBA_BOX_LETHAN )
+        {
+            int nRangeMax = Abc_MaxInt( nRange0, nRange1 );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            int fSwap  = (Type == CBA_BOX_MTHAN  || Type == CBA_BOX_LETHAN);
+            int fCompl = (Type == CBA_BOX_METHAN || Type == CBA_BOX_LETHAN);
+            if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 );
+            if ( fSigned01 )
+                iLit = Cba_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax );
+            else
+                iLit = Cba_BlastLess( pNew, pArg0, pArg1, nRangeMax );
+            iLit = Abc_LitNotCond( iLit, fCompl );
+            Vec_IntFill( vRes, 1, iLit );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_RAND || Type == CBA_BOX_ROR || Type == CBA_BOX_RXOR )
+        {
+            Vec_IntPush( vRes, Cba_BlastReduction( pNew, pFans0, nRange0, Type ) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
+        else if ( Type == CBA_BOX_ADD ) 
+        {
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange1, nRange2) );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, 1, 1, 0 );
+            int * pArg1 = Cba_VecLoadFanins( p, vRes,   iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            int * pArg2 = Cba_VecLoadFanins( p, vTemp1, iFon2, pFans2, nRange2, nRangeMax, fSigned01 );
+            int Carry   = Cba_BlastAdder( pNew, pArg0[0], pArg1, pArg2, nRange ); // result is in pArg1 (vRes)
+            assert( nRange0 == 1 );
+            Vec_IntShrink( vRes, nRange );
+            Vec_IntPush( vRes, Carry );
+        }
+        else if ( Type == CBA_BOX_SUB ) 
+        {
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Cba_VecLoadFanins( p, vRes,   iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            int Carry = 0;
+            Cba_BlastSubtract( pNew, pArg0, pArg1, nRange ); // result is in pFan0 (vRes)
+            Vec_IntShrink( vRes, nRange );
+        }
+        else if ( Type == CBA_BOX_MUL )
+        {
+            if ( fUseOldMultiplierBlasting )
+            {
+                int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+                int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+                int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+                Cba_BlastMultiplier2( pNew, pArg0, pArg1, nRange, vTemp2, vRes );
+                Vec_IntShrink( vRes, nRange );
+            }
+            else
+            {
+                int nRangeMax = Abc_MaxInt(nRange0, nRange1);
+                int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+                int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+                Cba_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned01 );
+                if ( nRange > nRangeMax + nRangeMax )
+                    Vec_IntFillExtra( vRes, nRange, fSigned01 ? Vec_IntEntryLast(vRes) : 0 );
+                else
+                    Vec_IntShrink( vRes, nRange );
+                assert( Vec_IntSize(vRes) == nRange );
+            }
+        }
+        else if ( Type == CBA_BOX_DIV || Type == CBA_BOX_MOD )
+        {
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, fSigned01 );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRangeMax, fSigned01 );
+            if ( fSigned01 )
+                Cba_BlastDividerSigned( pNew, pArg0, nRangeMax, pArg1, nRangeMax, Type == CBA_BOX_DIV, vRes );
+            else
+                Cba_BlastDivider( pNew, pArg0, nRangeMax, pArg1, nRangeMax, Type == CBA_BOX_DIV, vRes );
+            Vec_IntShrink( vRes, nRange );
+            if ( Type == CBA_BOX_DIV )
+                Cba_BlastZeroCondition( pNew, pFans1, nRange1, vRes );
+        }
+        else if ( Type == CBA_BOX_MIN )
+        {
+            int nRangeMax = Abc_MaxInt( nRange0, nRange );
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, Cba_FonSigned(p, iFon0) );
+            Cba_BlastMinus( pNew, pArg0, nRangeMax, vRes );
+            Vec_IntShrink( vRes, nRange );
+        }
+        else if ( Type == CBA_BOX_POW )
+        {
+            int nRangeMax = Abc_MaxInt(nRange0, nRange);
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRangeMax, Cba_FonSigned(p, iFon0) );
+            int * pArg1 = Cba_VecLoadFanins( p, vTemp1, iFon1, pFans1, nRange1, nRange1,   Cba_FonSigned(p, iFon1) );
+            Cba_BlastPower( pNew, pArg0, nRangeMax, pArg1, nRange1, vTemp2, vRes );
+            Vec_IntShrink( vRes, nRange );
+        }
+        else if ( Type == CBA_BOX_SQRT )
+        {
+            int * pArg0 = Cba_VecLoadFanins( p, vTemp0, iFon0, pFans0, nRange0, nRange0 + (nRange0 & 1), 0 );
+            nRange0 += (nRange0 & 1);
+            Cba_BlastSqrt( pNew, pArg0, nRange0, vTemp2, vRes );
+            if ( nRange > Vec_IntSize(vRes) )
+                Vec_IntFillExtra( vRes, nRange, 0 );
+            else
+                Vec_IntShrink( vRes, nRange );
+        }
+        else if ( Type == CBA_BOX_TABLE )
+        {
+            assert( 0 );
+            //Cba_BlastTable( pNew, Cba_ObjTable(p, p, i), pFans0, nRange0, nRange, vRes );
+        }
+        else assert( 0 );
+        Vec_IntAppend( vBits, vRes );
+        p->pDesign->nAnds[Type] += Gia_ManAndNum(pNew) - nAndPrev;
+    }
+    assert( nBits == Vec_IntSize(vBits) );
+    p->pDesign->nAnds[0] = Gia_ManAndNum(pNew);
+    // create COs
+    Cba_NtkForEachPo( p, iObj, i )
+    {
+        Cba_ObjForEachFinFon( p, iObj, iFin, iFon, k )
+        {
+            nRange = Cba_FonRangeSize( p, iFon );
+            pFans0  = Cba_FonIsReal(iFon) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFon) ) : NULL;
+            pFans0  = Cba_VecLoadFanins( p, vTemp0, iFon, pFans0, nRange0, nRange0, Cba_FonSigned(p, iFon) );
+            for ( b = 0; b < nRange; b++ )
+                Gia_ManAppendCo( pNew, pFans0[b] );
+        }
+    }
+    Cba_NtkForEachBoxSeq( p, iObj, i )
+    {
+        if ( fSeq )
+        {
+            assert( Cba_ObjType(p, iObj) == CBA_BOX_DFFCPL );
+            iFon0 = Cba_ObjFinFon( p, iObj, 0 );
+            iFon1 = Cba_ObjFinFon( p, iObj, 1 );
+            nRange0 = Cba_FonRangeSize( p, iFon0 );
+            nRange1 = Cba_FonRangeSize( p, iFon1 );
+            assert( nRange0 == nRange1 );
+            Cba_ObjForEachFinFon( p, iObj, iFin, iFon, k )
+            {
+                nRange = Cba_FonRangeSize( p, iFon );
+                pFans0 = Cba_FonIsReal(iFon) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFon) ) : NULL;
+                pFans0 = Cba_VecLoadFanins( p, vTemp0, iFon, pFans0, nRange0, nRange0, Cba_FonSigned(p, iFon) );
+                if ( k == 0 )
+                {
+                    for ( b = 0; b < nRange; b++ )
+                        Gia_ManAppendCo( pNew, pFans0[b] );
+                }
+                else if ( k == 1 )
+                {
+                    for ( b = 0; b < nRange; b++ )
+                        if ( pFans0[b] == 0 )
+                            Vec_StrPush( vInit, '0' );
+                        else if ( pFans0[b] == 1 )
+                            Vec_StrPush( vInit, '1' );
+                        else
+                            Vec_StrPush( vInit, 'x' );
+                }
+                else break;
+            }
+        }
+        else // combinational
+        {
+            Cba_ObjForEachFinFon( p, iObj, iFin, iFon, k )
+            {
+                nRange = Cba_FonRangeSize( p, iFon );
+                pFans0  = Cba_FonIsReal(iFon) ? Vec_IntEntryP( vBits, Cba_FonCopy(p, iFon) ) : NULL;
+                pFans0  = Cba_VecLoadFanins( p, vTemp0, iFon, pFans0, nRange0, nRange0, Cba_FonSigned(p, iFon) );
+                for ( b = 0; b < nRange; b++ )
+                    Gia_ManAppendCo( pNew, pFans0[b] );
+            }
+        }
+    }
+    Vec_IntFree( vTemp0 );
+    Vec_IntFree( vTemp1 );
+    Vec_IntFree( vTemp2 );
+    Vec_IntFree( vRes );
+    // finalize AIG
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManDupRemapLiterals( vBits, pTemp );
+    Gia_ManStop( pTemp );
+    // transform AIG with init state
+    if ( fSeq )
+    {
+        Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) );
+        Vec_StrPush( vInit, '\0' );
+        pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 1 );
+        Gia_ManDupRemapLiterals( vBits, pTemp );
+        Gia_ManStop( pTemp );
+        Vec_StrFreeP( &vInit );
+    }
+    //Vec_IntErase( vBits );
+    //Vec_IntErase( &p->vCopies );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cba_ManBlast( Cba_Man_t * p, int fBarBufs, int fSeq, int fVerbose )
+{
+    return Cba_NtkBlast( Cba_ManRoot(p), fSeq );
 }
 
 /**Function*************************************************************
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index b01f0d4e..9605975a 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -34,6 +34,7 @@ static int  Cba_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Cba_CommandPut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Cba_CommandGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Cba_CommandClp      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Cba_CommandCec      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Cba_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -64,6 +65,7 @@ void Cba_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New word level", "@put",        Cba_CommandPut,       0 );
     Cmd_CommandAdd( pAbc, "New word level", "@get",        Cba_CommandGet,       0 );
     Cmd_CommandAdd( pAbc, "New word level", "@clp",        Cba_CommandClp,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@blast",      Cba_CommandBlast,     0 );
     Cmd_CommandAdd( pAbc, "New word level", "@cec",        Cba_CommandCec,       0 );
     Cmd_CommandAdd( pAbc, "New word level", "@test",       Cba_CommandTest,      0 );
 }
@@ -101,15 +103,18 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     Cba_Man_t * p = NULL;
     char * pFileName = NULL;
-    int c, fTest = 0, fVerbose = 0;
+    int c, fTest = 0, fDfs = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "tvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "tdvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 't':
             fTest ^= 1;
             break;
+        case 'd':
+            fDfs ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -159,12 +164,19 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Unrecognized input file extension.\n" );
         return 0;
     }
+    if ( fDfs )
+    {
+        Cba_Man_t * pTemp;
+        p = Cba_ManDup( pTemp = p, Cba_NtkCollectDfs );
+        Cba_ManFree( pTemp );
+    }
     Cba_AbcUpdateMan( pAbc, p );
     return 0;
 usage:
-    Abc_Print( -2, "usage: @read [-tvh] <file_name>\n" );
+    Abc_Print( -2, "usage: @read [-tdvh] <file_name>\n" );
     Abc_Print( -2, "\t         reads hierarchical design\n" );
     Abc_Print( -2, "\t-t     : toggle testing the parser [default = %s]\n", fTest? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle computing DFS ordering [default = %s]\n", fDfs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -259,9 +271,13 @@ usage:
 int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cba_Man_t * p = Cba_AbcGetMan(pAbc);
-    int c, nModules = 0, fVerbose  = 0;
+    int nModules     = 0;
+    int fShowMulti   = 0;
+    int fShowAdder   = 0;
+    int fDistrib     = 0;
+    int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mmadvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -276,6 +292,15 @@ int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nModules < 0 )
                 goto usage;
             break;
+        case 'm':
+            fShowMulti ^= 1;
+            break;
+        case 'a':
+            fShowAdder ^= 1;
+            break;
+        case 'd':
+            fDistrib ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -290,12 +315,24 @@ int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandPs(): There is no current design.\n" );
         return 0;
     }
-    Cba_ManPrintStats( p, nModules, fVerbose );
+    if ( nModules )
+    {
+        Cba_ManPrintStats( p, nModules, fVerbose );
+        return 0;
+    }
+    Cba_NtkPrintStatsFull( Cba_ManRoot(p), fDistrib, fVerbose );
+    if ( fShowMulti )
+        Cba_NtkPrintNodes( Cba_ManRoot(p), CBA_BOX_MUL );
+    if ( fShowAdder )
+        Cba_NtkPrintNodes( Cba_ManRoot(p), CBA_BOX_ADD );
     return 0;
 usage:
-    Abc_Print( -2, "usage: @ps [-M num] [-vh]\n" );
+    Abc_Print( -2, "usage: @ps [-M num] [-madvh]\n" );
     Abc_Print( -2, "\t         prints statistics\n" );
     Abc_Print( -2, "\t-M num : the number of first modules to report [default = %d]\n", nModules );
+    Abc_Print( -2, "\t-m     : toggle printing multipliers [default = %s]\n",         fShowMulti? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle printing adders [default = %s]\n",              fShowAdder? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle printing distrubition [default = %s]\n",        fDistrib? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -316,15 +353,18 @@ int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cba_Man_t * p = Cba_AbcGetMan(pAbc);
     Gia_Man_t * pGia = NULL;
-    int c, fBarBufs = 1, fVerbose  = 0;
+    int c, fBarBufs = 1, fSeq = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bsvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'b':
             fBarBufs ^= 1;
             break;
+        case 's':
+            fSeq ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -339,7 +379,7 @@ int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Cba_CommandPut(): There is no current design.\n" );
         return 0;
     }
-    pGia = Cba_ManBlast( p, fBarBufs, fVerbose );
+    pGia = Cba_ManBlast( p, fBarBufs, fSeq, fVerbose );
     if ( pGia == NULL )
     {
         Abc_Print( 1, "Cba_CommandPut(): Conversion to AIG has failed.\n" );
@@ -348,9 +388,10 @@ int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pGia );
     return 0;
 usage:
-    Abc_Print( -2, "usage: @put [-bvh]\n" );
+    Abc_Print( -2, "usage: @put [-bsvh]\n" );
     Abc_Print( -2, "\t         extracts AIG from the hierarchical design\n" );
     Abc_Print( -2, "\t-b     : toggle using barrier buffers [default = %s]\n", fBarBufs? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -479,6 +520,61 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pNew = NULL;
+    Cba_Man_t * p = Cba_AbcGetMan(pAbc);
+    int c, fSeq = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 's':
+            fSeq ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandBlast(): There is no current design.\n" );
+        return 0;
+    }
+    pNew = Cba_ManBlast( p, 0, fSeq, fVerbose );
+    if ( pNew == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandBlast(): Bit-blasting has failed.\n" );
+        return 0;
+    }
+    Abc_FrameUpdateGia( pAbc, pNew );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%blast [-svh]\n" );
+    Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
+    Abc_Print( -2, "\t-s     : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cba_Man_t * p = Cba_AbcGetMan(pAbc), * pTemp;
@@ -536,7 +632,7 @@ int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // extract AIG from the current design
-    pFirst = Cba_ManBlast( p, 0, 0 );
+    pFirst = Cba_ManBlast( p, 0, 0, 0 );
     if ( pFirst == NULL )
     {
         Abc_Print( -1, "Extracting AIG from the current design has failed.\n" );
@@ -551,7 +647,7 @@ int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "cba" )  )
         pTemp = Cba_ManReadCba( pFileName );
     else assert( 0 );
-    pSecond = Cba_ManBlast( pTemp, 0, 0 );
+    pSecond = Cba_ManBlast( pTemp, 0, 0, 0 );
     Cba_ManFree( pTemp );
     if ( pSecond == NULL )
     {
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 6c312e88..d5598c43 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include <math.h>
 #include "cba.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -32,6 +33,269 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Prints distribution of operator types.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WrdSelectSortCost2( word * pArray, int nSize, word * pCosts )
+{
+    int i, j, best_i;
+    for ( i = 0; i < nSize-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < nSize; j++ )
+            if ( pCosts[j] < pCosts[best_i] )
+                best_i = j;
+        ABC_SWAP( word, pArray[i], pArray[best_i] );
+        ABC_SWAP( word, pCosts[i], pCosts[best_i] );
+    }
+}
+static inline word Cba_NtkPrintDistribMakeSign( int s, int s0, int s1 )
+{
+    return ((word)s1 << 42) | ((word)s0 << 21) | (word)s;
+}
+static inline void Cba_NtkPrintDistribFromSign( word sss, int * s, int * s0, int * s1 )
+{
+    *s1 =  (int)(sss >> 42);  *s0 = (int)(sss >> 21) & 0x1FFFFF;  *s  =  (int)sss & 0x1FFFFF;
+}
+static inline void Cba_NtkPrintDistribAddOne( Vec_Ptr_t * vTypes, Vec_Ptr_t * vOccurs, int Type, word Sign )
+{
+    Vec_Wrd_t * vType  = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, Type );
+    Vec_Wrd_t * vOccur = (Vec_Wrd_t *)Vec_PtrEntry( vOccurs, Type );
+    word Entry; int i;
+    Vec_WrdForEachEntry( vType, Entry, i )
+        if ( Entry == Sign )
+        {
+            Vec_WrdAddToEntry( vOccur, i, 1 );
+            return;
+        }
+    Vec_WrdPush( vType, Sign );
+    Vec_WrdPush( vOccur, 1 );
+}
+void Cba_NtkPrintDistribSortOne( Vec_Ptr_t * vTypes, Vec_Ptr_t * vOccurs, int Type )
+{
+    Vec_Wrd_t * vType  = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, Type );
+    Vec_Wrd_t * vOccur = (Vec_Wrd_t *)Vec_PtrEntry( vOccurs, Type );
+    Vec_WrdSelectSortCost2( Vec_WrdArray(vType), Vec_WrdSize(vType), Vec_WrdArray(vOccur) );
+    Vec_WrdReverseOrder( vType );
+    Vec_WrdReverseOrder( vOccur );
+}
+void Cba_NtkPrintDistrib( Cba_Ntk_t * p, int fVerbose )
+{
+    Vec_Ptr_t * vTypes, * vOccurs;
+    Vec_Int_t * vAnds = Vec_IntStart( CBA_BOX_LAST );
+    int iRnObj = -1, nCountRange = 0;
+    int i, k, s, s0, s1, Type;  word Sign;
+    char * pTypeNames[CBA_BOX_LAST];
+    Cba_ManCreatePrimMap( pTypeNames );
+    // allocate statistics arrays
+    vTypes  = Vec_PtrStart( CBA_BOX_LAST );
+    vOccurs = Vec_PtrStart( CBA_BOX_LAST );
+    for ( i = 0; i < CBA_BOX_LAST; i++ )
+        Vec_PtrWriteEntry( vTypes, i, Vec_WrdAlloc(16) );
+    for ( i = 0; i < CBA_BOX_LAST; i++ )
+        Vec_PtrWriteEntry( vOccurs, i, Vec_WrdAlloc(16) );
+    // add nodes
+    Cba_NtkForEachObj( p, i )
+    {
+//        char * pName = Cba_ObjName(p, i);
+        Type = Cba_ObjType( p, i );
+        if ( Cba_ObjSign(p, i) > 0x1FFFFF )
+            printf( "Object %6d has range %d, which is reduced to %d in the statistics.\n", 
+                i, Cba_ObjRangeSize(p, i), Cba_ObjRangeSize(p, i) & 0xFFFFF );
+        if ( Cba_ObjLeft(p, i) && Cba_ObjRight(p, i) )
+        {
+            if ( iRnObj == -1 )
+                iRnObj = 1;
+            nCountRange++;
+        }
+        // 0-input types
+        if ( Cba_ObjIsPi(p, i) || (Type == CBA_BOX_BUF && Cba_FonIsConst(Cba_ObjFinFon(p, i, 0))) || Type == CBA_BOX_CONCAT )
+            Sign = Cba_NtkPrintDistribMakeSign( Cba_ObjSign(p, i), 0, 0 );
+        // 1-input types
+        else if ( Cba_TypeIsUnary(Type)  )
+            Sign = Cba_NtkPrintDistribMakeSign( Cba_ObjSign(p, i), Cba_ObjSign(p, Cba_ObjFinFon(p, i, 0)), 0 );
+        // 2-input types (including MUX)
+        else if ( Cba_ObjFinNum(p, i) == 1 )
+            Sign = Cba_NtkPrintDistribMakeSign( Cba_ObjSign(p, i), Cba_ObjSign(p, Cba_ObjFinFon(p, i, 0)), 0 );
+        else
+        {
+            assert( Cba_ObjFinNum(p, i) >= 2 );
+            Sign = Cba_NtkPrintDistribMakeSign( Cba_ObjSign(p, i), Cba_ObjSign(p, Cba_ObjFinFon(p, i, 0)), Cba_ObjSign(p, Cba_ObjFinFon(p, i, 1)) );
+        }
+        // add to storage
+        Cba_NtkPrintDistribAddOne( vTypes, vOccurs, Type, Sign );
+        // count the number of AIG nodes
+        if ( Type == CBA_BOX_MUX )
+            Vec_IntAddToEntry( vAnds, CBA_BOX_MUX,      3 * Cba_ObjRangeSize(p, i) * (Cba_ObjFinNum(p, i) - 2) );
+        else if ( Type == CBA_BOX_SHIR )      
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SHIR,  Abc_MinInt(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Abc_Base2Log(Cba_ObjRangeSize(p, i))) * 3 );
+        else if ( Type == CBA_BOX_SHIRA )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SHIRA, Cba_ObjRangeSize(p, i) * Abc_MinInt(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Abc_Base2Log(Cba_ObjRangeSize(p, i))) * 3 );
+        else if ( Type == CBA_BOX_SHIL )      
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SHIL,  Cba_ObjRangeSize(p, i) * Abc_MinInt(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Abc_Base2Log(Cba_ObjRangeSize(p, i))) * 3 );
+        else if ( Type == CBA_BOX_SHILA )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SHILA, Cba_ObjRangeSize(p, i) * Abc_MinInt(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Abc_Base2Log(Cba_ObjRangeSize(p, i))) * 3 );
+        else if ( Type == CBA_BOX_ROTR )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_ROTR,  Cba_ObjRangeSize(p, i) * Abc_MinInt(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Abc_Base2Log(Cba_ObjRangeSize(p, i))) * 3 );
+        else if ( Type == CBA_BOX_ROTL )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_ROTL,  Cba_ObjRangeSize(p, i) * Abc_MinInt(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Abc_Base2Log(Cba_ObjRangeSize(p, i))) * 3 );
+        else if ( Type == CBA_BOX_INV )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_INV, 0 );
+        else if ( Type == CBA_BOX_AND )      
+            Vec_IntAddToEntry( vAnds, CBA_BOX_AND,         Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) );
+        else if ( Type == CBA_BOX_OR )       
+            Vec_IntAddToEntry( vAnds, CBA_BOX_OR,          Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) );
+        else if ( Type == CBA_BOX_XOR )      
+            Vec_IntAddToEntry( vAnds, CBA_BOX_XOR,     3 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) );
+        else if ( Type == CBA_BOX_SLICE )   
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SLICE, 0 );
+        else if ( Type == CBA_BOX_CONCAT )   
+            Vec_IntAddToEntry( vAnds, CBA_BOX_CONCAT, 0 );
+        else if ( Type == CBA_BOX_LNOT )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_LNOT,        Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 1 );
+        else if ( Type == CBA_BOX_LAND )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_LAND,        Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) + Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 1)) - 1 );
+        else if ( Type == CBA_BOX_LOR )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_LOR,         Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) + Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 1)) - 1 );
+        else if ( Type == CBA_BOX_LXOR )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_LXOR,        Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) + Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 1)) + 1 );
+        else if ( Type == CBA_BOX_EQU )     
+            Vec_IntAddToEntry( vAnds, CBA_BOX_EQU,      4 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 1 );
+        else if ( Type == CBA_BOX_NEQU )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_NEQU,     4 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 1 );
+        else if ( Type == CBA_BOX_LTHAN )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_LTHAN,    6 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 6 );
+        else if ( Type == CBA_BOX_MTHAN )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_MTHAN,    6 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 6 );
+        else if ( Type == CBA_BOX_LETHAN ) 
+            Vec_IntAddToEntry( vAnds, CBA_BOX_LETHAN,   6 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 6 );
+        else if ( Type == CBA_BOX_METHAN ) 
+            Vec_IntAddToEntry( vAnds, CBA_BOX_METHAN,   6 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 6 );
+        else if ( Type == CBA_BOX_RAND )   
+            Vec_IntAddToEntry( vAnds, CBA_BOX_RAND,         Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 1 );
+        else if ( Type == CBA_BOX_ROR )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_ROR,          Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 1 );
+        else if ( Type == CBA_BOX_RXOR )   
+            Vec_IntAddToEntry( vAnds, CBA_BOX_RXOR,     3 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 3 );
+        else if ( Type == CBA_BOX_ADD )       
+            Vec_IntAddToEntry( vAnds, CBA_BOX_ADD,      9 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) );
+        else if ( Type == CBA_BOX_SUB )       
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SUB,      9 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) );
+        else if ( Type == CBA_BOX_MUL )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_MUL,      9 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 1)) );
+        else if ( Type == CBA_BOX_DIV )   
+            Vec_IntAddToEntry( vAnds, CBA_BOX_DIV,     13 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 19 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) + 10 );
+        else if ( Type == CBA_BOX_MOD )  
+            Vec_IntAddToEntry( vAnds, CBA_BOX_MOD,     13 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 7 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) - 2  );
+        else if ( Type == CBA_BOX_POW ) 
+            Vec_IntAddToEntry( vAnds, CBA_BOX_POW,     10 * (int)pow(Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)),Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0))) );
+        else if ( Type == CBA_BOX_MIN )   
+            Vec_IntAddToEntry( vAnds, CBA_BOX_MIN,      4 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) );
+        else if ( Type == CBA_BOX_SQRT )    
+            Vec_IntAddToEntry( vAnds, CBA_BOX_SQRT,    11 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) / 8 + 5 * Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)) / 2 - 5  );
+    }
+    if ( nCountRange )
+    {
+        printf( "Warning: %d objects of the design have non-zero-based ranges.\n", nCountRange );
+        printf( "In particular, object %6d with name \"%s\" has range %d=[%d:%d]\n", 
+            iRnObj, Cba_FonName(p, Cba_ObjFon0(p, iRnObj)), 
+            Cba_ObjRangeSize(p, iRnObj), Cba_ObjLeft(p, iRnObj), Cba_ObjRight(p, iRnObj) );
+    }
+    // print by occurrence
+    printf( "ID  :  name  occurrence    and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n" );
+    for ( i = 0; i < CBA_BOX_LAST; i++ )
+    {
+        Vec_Wrd_t * vType  = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, i );
+        Vec_Wrd_t * vOccur = (Vec_Wrd_t *)Vec_PtrEntry( vOccurs, i );
+        if ( p->pDesign->nObjs[i] == 0 )
+            continue;
+        printf( "%2d  :  %-8s  %6d%8d ", i, pTypeNames[i], p->pDesign->nObjs[i], Vec_IntEntry(vAnds, i) );
+        // sort by occurence
+        Cba_NtkPrintDistribSortOne( vTypes, vOccurs, i );
+        Vec_WrdForEachEntry( vType, Sign, k )
+        {
+            Cba_NtkPrintDistribFromSign( Sign, &s, &s0, &s1 );
+            if ( ((k % 6) == 5 && s1) || ((k % 8) == 7 && !s1) )
+                printf( "\n                                " );
+            printf( "(%d)", (int)Vec_WrdEntry( vOccur, k ) );
+            printf( "%s%d",      Abc_LitIsCompl(s)?"-":"",  Abc_Lit2Var(s) );
+            if ( s0 )
+                printf( "=%s%d", Abc_LitIsCompl(s0)?"-":"", Abc_Lit2Var(s0) );
+            if ( s1 )
+                printf( ".%s%d", Abc_LitIsCompl(s1)?"-":"", Abc_Lit2Var(s1) );
+            printf( " " );
+        }
+        printf( "\n" );
+    }
+    Vec_VecFree( (Vec_Vec_t *)vTypes );
+    Vec_VecFree( (Vec_Vec_t *)vOccurs );
+    Vec_IntFree( vAnds );
+}
+void Cba_NtkPrintNodes( Cba_Ntk_t * p, int Type )
+{
+    int i, iFon0, iFon1, Counter = 0;
+    char * pTypeNames[CBA_BOX_LAST];
+    Cba_ManCreatePrimMap( pTypeNames );
+    printf( "Operation %s\n", pTypeNames[Type] );
+    Cba_NtkForEachObj( p, i )
+    {
+        if ( (int)Type != Type )
+            continue;
+        iFon0 = Cba_ObjFinFon(p, i, 0);
+        iFon1 = Cba_ObjFinFon(p, i, 1);
+
+        printf( "%8d  :",      Counter++ );
+        printf( "%8d  :  ",    i );
+        printf( "%3d%s = ",    Cba_ObjRangeSize(p, i),                      Cba_ObjSigned(p, i) ? "s" : " " );
+        printf( "%3d%s  %s ",  Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 0)), Cba_ObjSigned(p, iFon0) ? "s" : " ", pTypeNames[Type] );
+        printf( "%3d%s ",      Cba_ObjRangeSize(p, Cba_ObjFinFon(p, i, 1)), Cba_ObjSigned(p, iFon1) ? "s" : " " );
+        printf( " :    " );
+        printf( "%-12s =  ",   Cba_ObjName(p, i) );
+        printf( "%-12s  %s  ", Cba_FonIsConst(iFon0) ? Cba_NtkConst(p, Cba_FonConst(iFon0)) : Cba_FonNameStr(p, iFon0), pTypeNames[Type] );
+        printf( "%-12s ",      Cba_FonIsConst(iFon1) ? Cba_NtkConst(p, Cba_FonConst(iFon1)) : Cba_FonNameStr(p, iFon1) );
+        printf( "\n" );
+    }
+}
+void Cba_NtkPrintStatsFull( Cba_Ntk_t * p, int fDistrib, int fVerbose )
+{
+    int i;
+    char * pTypeNames[CBA_BOX_LAST];
+    Cba_ManCreatePrimMap( pTypeNames );
+    printf( "%-20s : ",        Cba_NtkName(p) );
+    printf( "PI = %4d  ",      Cba_NtkPiNum(p) );
+    printf( "PO = %4d  ",      Cba_NtkPoNum(p) );
+    printf( "FF = %4d  ",      Cba_NtkBoxSeqNum(p) );
+    printf( "Obj = %6d  ",     Cba_NtkObjNum(p) );
+    printf( "Mem = %.3f MB",   1.0*Cba_NtkMemory(p)/(1<<20) );
+    printf( "\n" );
+    if ( fDistrib )
+    {
+        Cba_NtkPrintDistrib( p, fVerbose );
+        return;
+    }
+    if ( !fVerbose )
+        return;
+    printf( "Node type statistics:\n" );
+    for ( i = 1; i < CBA_BOX_LAST; i++ )
+    {
+        if ( !p->pDesign->nObjs[i] )
+            continue;
+        if ( p->pDesign->nAnds[0] && p->pDesign->nAnds[i] )
+            printf( "%2d  :  %-8s  %6d  %7.2f %%\n", i, pTypeNames[i], p->pDesign->nObjs[i], 100.0*p->pDesign->nAnds[i]/p->pDesign->nAnds[0] );
+        else
+            printf( "%2d  :  %-8s  %6d\n", i, pTypeNames[i], p->pDesign->nObjs[i] );
+    }
+}
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -63,7 +327,7 @@ void Cba_NtkPrintDistribStat( Cba_Ntk_t * p, int * pCounts, int * pUserCounts )
         if ( pUserCounts[i] )
             printf( "%-20s = %5d\n", Cba_NtkName(pNtk), pUserCounts[i] );
 }
-void Cba_NtkPrintDistrib( Cba_Ntk_t * p )
+void Cba_NtkPrintDistribOld( Cba_Ntk_t * p )
 {
     int pCounts[CBA_BOX_LAST] = {0};
     int * pUserCounts = ABC_CALLOC( int, Cba_ManNtkNum(p->pDesign) + 1 );
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
index 5183762d..6a259ccd 100644
--- a/src/base/cba/cbaPrs.h
+++ b/src/base/cba/cbaPrs.h
@@ -128,6 +128,7 @@ struct Prs_Man_t_
     Vec_Int_t       vFailed;
     Vec_Int_t       vSucceeded;
     // error handling
+    int             nOpens;      // open port counter
     int             fUsingTemp2; // vTemp2 is in use
     int             FuncNameId;  // temp value
     int             FuncRangeId; // temp value
@@ -226,10 +227,10 @@ static inline void Prs_ManFinalizeNtk( Prs_Man_t * p )
     p->pNtk = NULL;
 }
 
-static inline int Prs_NtkNewStrId( Prs_Ntk_t * pNtk, const char * format, ...  )
+static inline int Prs_ManNewStrId( Prs_Man_t * p, const char * format, ...  )
 {
-    Abc_Nam_t * p = pNtk->pStrs;
-    Vec_Str_t * vBuf = Abc_NamBuffer( p );
+    Abc_Nam_t * pStrs = p->pStrs;
+    Vec_Str_t * vBuf = Abc_NamBuffer( pStrs );
     int nAdded, nSize = 1000; 
     va_list args;   va_start( args, format );
     Vec_StrGrow( vBuf, Vec_StrSize(vBuf) + nSize );
@@ -241,7 +242,7 @@ static inline int Prs_NtkNewStrId( Prs_Ntk_t * pNtk, const char * format, ...  )
         assert( nSize == nAdded );
     }
     va_end( args );
-    return Abc_NamStrFindOrAddLim( p, Vec_StrLimit(vBuf), Vec_StrLimit(vBuf) + nAdded, NULL );
+    return Abc_NamStrFindOrAddLim( pStrs, Vec_StrLimit(vBuf), Vec_StrLimit(vBuf) + nAdded, NULL );
 }
 
 // parsing slice/concatentation/box
@@ -306,20 +307,22 @@ static inline char * Prs_ManLoadFile( char * pFileName, char ** ppLimit )
 static inline Prs_Man_t * Prs_ManAlloc( char * pFileName )
 {
     Prs_Man_t * p;
-    char * pBuffer, * pLimit;
-    pBuffer = Prs_ManLoadFile( pFileName, &pLimit );
-    if ( pBuffer == NULL )
-        return NULL;
     p = ABC_CALLOC( Prs_Man_t, 1 );
-    p->pName   = pFileName;
-    p->pBuffer = pBuffer;
-    p->pLimit  = pLimit;
-    p->pCur    = pBuffer;
-    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 );
+    if ( pFileName )
+    {
+        char * pBuffer, * pLimit;
+        pBuffer = Prs_ManLoadFile( pFileName, &pLimit );
+        if ( pBuffer == NULL )
+            return NULL;
+        p->pName   = pFileName;
+        p->pBuffer = pBuffer;
+        p->pLimit  = pLimit;
+        p->pCur    = pBuffer;
+    }
+    p->pStrs = Abc_NamStart( 1000, 24 );
+    p->pFuns = Abc_NamStart( 100, 24 );
+    p->vHash = Hash_IntManStart( 1000 );
+    p->vNtks = Vec_PtrAlloc( 100 );
     return p;
 }
 
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index a5bdb219..1cbf6b19 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -1449,7 +1449,7 @@ int Prs_CreateCatIn( Cba_Ntk_t * p, Prs_Ntk_t * pNtk, int Con )
     int i, Sig, iObj, iFon, NameId, nBits = 0;
     Vec_Int_t * vSigs = Prs_CatSignals(pNtk, Con);
     // create input concatenation
-    iObj = Cba_ObjAlloc( p, CBA_BOX_CATIN, Vec_IntSize(vSigs), 1 );
+    iObj = Cba_ObjAlloc( p, CBA_BOX_CONCAT, Vec_IntSize(vSigs), 1 );
     iFon = Cba_ObjFon0(p, iObj);
     //sprintf( Buffer, "_icc%d_", iObj );
     //NameId = Cba_NtkNewStrId( p, Buffer );
@@ -1501,46 +1501,6 @@ int Prs_CreateRange( Cba_Ntk_t * p, int iFon, int NameId )
     Cba_FonSetRangeSign( 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, nBits = 0;
-    Vec_Int_t * vSigs = Prs_CatSignals(pNtk, Con); char * pSigName;
-    NameId = Cba_NtkNewStrId( p, "_occ%d_", iFon );
-    Cba_FonSetName( p, iFon, NameId );
-    Cba_NtkSetMap( p, NameId, iFon );
-    // create output concatenation
-    iObj = Cba_ObjAlloc( p, CBA_BOX_CATOUT, 1, Vec_IntSize(vSigs) );
-    Cba_ObjSetFinFon( p, iObj, 0, iFon );
-    // set outputs
-    Vec_IntForEachEntry( vSigs, Sig, i )
-    {
-        int Value = Abc_Lit2Var2(Sig);
-        Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
-        iFonNew = Cba_ObjFon( p, iObj, Vec_IntSize(vSigs)-1-i );
-        if ( Type == CBA_PRS_NAME  )
-        {
-            pSigName = Prs_NtkStr(pNtk, Value);
-            NameId = Cba_NtkNewStrId( p, pSigName ); 
-            Cba_FonSetName( p, iFonNew, NameId );
-            nBits += Prs_CreateRange( p, iFonNew, NameId );
-        }
-        else if ( Type == CBA_PRS_SLICE )
-        {
-            pSigName = Prs_NtkStr(pNtk, Prs_SliceName(pNtk, Value));
-            NameId = Cba_NtkNewStrId( p, pSigName );
-            Cba_FonSetName( p, iFonNew, NameId );
-            Prs_CreateRange( p, iFonNew, NameId );
-            // create slice of this concat
-            Prs_CreateSlice( p, iFonNew, pNtk, Prs_SliceRange(pNtk, Value) );
-            nBits += Cba_NtkRangeSize( p, Prs_SliceRange(pNtk, Value) );
-        }
-        else assert( 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 i, iFonNew, NameOut, RangeOut, NameId, RangeId, RangeSize, nBits = 0; 
@@ -1656,7 +1616,7 @@ void Prs_CreateOutConcat( Cba_Ntk_t * p, int * pSlices, int nSlices )
         Prev = iFon;
     }
     // create new concatenation
-    iObj = Cba_ObjAlloc( p, CBA_BOX_CATIN, nParts, 1 );
+    iObj = Cba_ObjAlloc( p, CBA_BOX_CONCAT, nParts, 1 );
     iFon = Cba_ObjFon0(p, iObj);
     Cba_FonSetName( p, iFon, NameId );
     Prs_CreateRange( p, iFon, NameId );
@@ -1855,7 +1815,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 i, k, iObj, iTerm, iFon, FormId, ActId, RangeId, NameId;
+    int i, k, iObj, iTerm, iFon, FormId, ActId, RangeId, NameId, Type;
     // map inputs
     Cba_NtkCleanMap( p );
     Cba_NtkForEachPi( p, iObj, i )
@@ -1918,25 +1878,15 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
     {
         if ( Prs_BoxIsNode(pNtk, i) ) // node
         {
-            int Type = Prs_BoxNtk(pNtk, i);
-            int nSigs = Prs_BoxIONum( pNtk, i );
-/*
-            int NameId = Abc_Lit2Var2(Vec_IntEntry(vBox, 1));
-            char * pName = Cba_NtkStr( p, NameId );
-            if ( !strcmp(pName, "E_336717") )
-            {
-                int s = 0;
-            }
-*/
-            iObj = Cba_ObjAlloc( p, Type, nSigs-1, Type == CBA_BOX_ADD ? 2 : 1 );
+            Type = Prs_BoxNtk(pNtk, i);
+            iObj = Cba_ObjAlloc( p, Type, Prs_BoxIONum(pNtk, i)-1, Type == CBA_BOX_ADD ? 2 : 1 );
             Prs_CreateSignalOut( p, Cba_ObjFon0(p, iObj), pNtk, Vec_IntEntry(vBox, 1) ); // node output
-            //Cba_ObjSetFunc( p, iObj, FuncId );
         }
         else // box
         {
             Cba_Ntk_t * pBox = NULL; int nInputs, nOutputs = 1;
             char ** pOutNames = NULL, * pNtkName = Prs_NtkStr(pNtk, Prs_BoxNtk(pNtk, i));
-            Cba_ObjType_t Type = Prs_ManFindType( pNtkName, &nInputs, 1, &pOutNames );
+            Type = Prs_ManFindType( pNtkName, &nInputs, 1, &pOutNames );
             if ( Type == CBA_BOX_RAMWC )
                 continue;
             if ( Type == CBA_OBJ_BOX )
@@ -1969,7 +1919,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                 else assert( 0 );
             }
             else if ( (Type == CBA_BOX_DFFRS || Type == CBA_BOX_LATCHRS) && !strncmp(pNtkName, "wide_", strlen("wide_")) && !Prs_CreateFlopSetReset(p, pNtk, vBox, NULL, NULL, NULL, NULL) )
-                nInputs = atoi(pNtkName+strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_")), nOutputs = 1, Type = CBA_BOX_CATIN;
+                nInputs = atoi(pNtkName+strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_")), nOutputs = 1, Type = CBA_BOX_CONCAT;
             // create object
             iObj = Cba_ObjAlloc( p, Type, nInputs, nOutputs );
             if ( pBox ) Cba_ObjSetFunc( p, iObj, Cba_NtkId(pBox) );
@@ -2013,16 +1963,10 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
     // connect objects
     Prs_NtkForEachBox( pNtk, vBox, i )
     {
-//        char * pInstName = NULL;
-//        if ( Prs_BoxName(pNtk, i) )
-//            pInstName = Prs_NtkStr(pNtk, Prs_BoxName(pNtk, i));
-//        if ( pNtk->iModuleName == 291 && i == 0 )
-//        {
-//            int s = 0;
-//        }
         iObj = Vec_IntEntry( vBox2Obj, i );
         if ( Prs_BoxIsNode(pNtk, i) ) // node
         {
+            Type = Prs_BoxNtk(pNtk, i);
             Vec_IntForEachEntryDoubleStart( vBox, FormId, ActId, k, 2 )
             {
                 iFon = Prs_CreateSignalIn( p, pNtk, ActId );
@@ -2034,7 +1978,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
         {
             int nInputs = -1;
             char ** pInNames = NULL, * pNtkName = Prs_NtkStr(pNtk, Prs_BoxNtk(pNtk, i));
-            Cba_ObjType_t Type = Prs_ManFindType( pNtkName, &nInputs, 0, &pInNames );
+            Type = Prs_ManFindType( pNtkName, &nInputs, 0, &pInNames );
             if ( (Type == CBA_BOX_DFFRS || Type == CBA_BOX_LATCHRS) && !strncmp(pNtkName, "wide_", strlen("wide_")) )
             {
                 int IndexSet = -1, IndexRst = -1,  iBitSet = -1, iBitRst = -1;
@@ -2048,7 +1992,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                 else
                 {
                     int w, Width = atoi( pNtkName + strlen(Type == CBA_BOX_DFFRS ? "wide_dffrs_" : "wide_latchrs_") );
-                    assert( Cba_ObjType(p, iObj) == CBA_BOX_CATIN );
+                    assert( Cba_ObjType(p, iObj) == CBA_BOX_CONCAT );
                     // prepare inputs
                     assert( nInputs >= 0 );
                     Cba_NtkCleanMap2( p );
@@ -2149,6 +2093,14 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                 }
             }
         }
+        // if carry-in is not supplied, use constant 0
+        if ( Type == CBA_BOX_ADD && Cba_ObjFinFon(p, iObj, 0) == 0 )
+            Cba_ObjSetFinFon( p, iObj, 0, Cba_FonFromConst(1) );
+        // if set or reset are not supplied, use constant 0
+        if ( Type == CBA_BOX_DFFRS && Cba_ObjFinFon(p, iObj, 1) == 0 )
+            Cba_ObjSetFinFon( p, iObj, 1, Cba_FonFromConst(1) );
+        if ( Type == CBA_BOX_DFFRS && Cba_ObjFinFon(p, iObj, 2) == 0 )
+            Cba_ObjSetFinFon( p, iObj, 2, Cba_FonFromConst(1) );
     }
     Vec_IntFree( vBox2Obj );
     // connect outputs
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index cabc8111..c6f7b2ac 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -49,8 +49,7 @@ void Cba_ManCreatePrimMap( char ** pMap )
     memset( pMap, 0, sizeof(char *) * CBA_BOX_LAST );
 
     pMap[ CBA_BOX_SLICE  ] = "sli";
-    pMap[ CBA_BOX_CATIN  ] = "icc";
-    pMap[ CBA_BOX_CATOUT ] = "occ";
+    pMap[ CBA_BOX_CONCAT ] = "icc";
 
     pMap[ CBA_BOX_BUF    ] = "";
     pMap[ CBA_BOX_INV    ] = "~";
@@ -63,7 +62,7 @@ void Cba_ManCreatePrimMap( char ** pMap )
     pMap[ CBA_BOX_SHARP  ] = "&"; 
     pMap[ CBA_BOX_SHARPL ] = "&"; 
     pMap[ CBA_BOX_MUX    ] = "?"; 
-    pMap[ CBA_BOX_MAJ    ] = NULL; 
+    pMap[ CBA_BOX_MAJ    ] = "maj"; 
     pMap[ CBA_BOX_RAND   ] = "&"; 
     pMap[ CBA_BOX_RNAND  ] = "~&"; 
     pMap[ CBA_BOX_ROR    ] = "|"; 
@@ -72,18 +71,18 @@ void Cba_ManCreatePrimMap( char ** pMap )
     pMap[ CBA_BOX_RXNOR  ] = "~^"; 
     pMap[ CBA_BOX_LNOT   ] = "!"; 
     pMap[ CBA_BOX_LAND   ] = "&&"; 
-    pMap[ CBA_BOX_LNAND  ] = NULL; 
+    pMap[ CBA_BOX_LNAND  ] = "logic nand"; 
     pMap[ CBA_BOX_LOR    ] = "||"; 
-    pMap[ CBA_BOX_LNOR   ] = NULL; 
+    pMap[ CBA_BOX_LNOR   ] = "logic nor"; 
     pMap[ CBA_BOX_LXOR   ] = "^^"; 
-    pMap[ CBA_BOX_LXNOR  ] = NULL; 
+    pMap[ CBA_BOX_LXNOR  ] = "logic xnor"; 
     pMap[ CBA_BOX_NMUX   ] = "nmux"; 
     pMap[ CBA_BOX_SEL    ] = "sel"; 
-    pMap[ CBA_BOX_PSEL   ] = NULL; 
-    pMap[ CBA_BOX_ENC    ] = NULL; 
-    pMap[ CBA_BOX_PENC   ] = NULL; 
+    pMap[ CBA_BOX_PSEL   ] = "prio-select"; 
+    pMap[ CBA_BOX_ENC    ] = "enc"; 
+    pMap[ CBA_BOX_PENC   ] = "prio-enc"; 
     pMap[ CBA_BOX_DEC    ] = "dec"; 
-    pMap[ CBA_BOX_EDEC   ] = NULL; 
+    pMap[ CBA_BOX_EDEC   ] = "enable-dec"; 
     pMap[ CBA_BOX_ADD    ] = "+"; 
     pMap[ CBA_BOX_SUB    ] = "-"; 
     pMap[ CBA_BOX_MUL    ] = "*"; 
@@ -93,7 +92,7 @@ void Cba_ManCreatePrimMap( char ** pMap )
     pMap[ CBA_BOX_POW    ] = "**"; 
     pMap[ CBA_BOX_MIN    ] = "-"; 
     pMap[ CBA_BOX_SQRT   ] = "@"; 
-    pMap[ CBA_BOX_ABS    ] = NULL; 
+    pMap[ CBA_BOX_ABS    ] = "abs"; 
     pMap[ CBA_BOX_LTHAN  ] = "<"; 
     pMap[ CBA_BOX_LETHAN ] = "<="; 
     pMap[ CBA_BOX_METHAN ] = ">="; 
@@ -131,6 +130,33 @@ void Cba_ManCreatePrimMap( char ** pMap )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Prs_NameIsLegalInVerilog( char * pName, int NameId )
+{
+    // identifier ::= simple_identifier | escaped_identifier
+    // simple_identifier ::= [a-zA-Z_][a-zA-Z0-9_$]
+    // escaped_identifier ::= \ {Any_ASCII_character_except_white_space} white_space
+    // white_space ::= space | tab | newline
+    assert( pName != NULL && *pName != '\0' );
+    if ( *pName == '\\' )
+        return 1;
+    if ( NameId < 13 ) // see PRS_VER_UNKNOWN in cbaReadVer.c
+        return 0;
+    if ( (*pName < 'a' || *pName > 'z') && (*pName < 'A' || *pName > 'Z') && *pName != '_' )
+        return 0;
+    while ( *(++pName) )
+        if ( (*pName < 'a' || *pName > 'z') && (*pName < 'A' || *pName > 'Z') && (*pName < '0' || *pName > '9') && *pName != '_' && *pName != '$' ) 
+            return 0;
+    return 1;
+}
+char * Prs_ObjGetName( Prs_Ntk_t * p, int NameId )
+{
+    char * pName = Prs_NtkStr(p, NameId);
+    if ( pName == NULL )
+        return pName;
+    if ( Prs_NameIsLegalInVerilog(pName, NameId) )
+        return pName;
+    return Vec_StrPrintF( Abc_NamBuffer(p->pStrs), "\\%s ", pName );
+}
 static inline char * Prs_ManWriteRange( Prs_Ntk_t * p, int RangeId, int fSlice )
 {
     int Left  = RangeId ? Hash_IntObjData0( p->vHash, RangeId ) : 0;
@@ -153,11 +179,11 @@ static void Prs_ManWriteVerilogSignal( FILE * pFile, Prs_Ntk_t * p, int Sig )
     int Value = Abc_Lit2Var2( Sig );
     Prs_ManType_t Type = (Prs_ManType_t)Abc_Lit2Att2( Sig );
     if ( Type == CBA_PRS_NAME )
-        fprintf( pFile, "%s", Prs_NtkStr(p, Value) );
+        fprintf( pFile, "%s", Prs_ObjGetName(p, Value) );
     else if ( Type == CBA_PRS_CONST )
         fprintf( pFile, "%s", Prs_NtkConst(p, Value) );
     else if ( Type == CBA_PRS_SLICE )
-        fprintf( pFile, "%s%s", Prs_NtkStr(p, Prs_SliceName(p, Value)), Prs_ManWriteRange(p, Prs_SliceRange(p, Value), 1) );
+        fprintf( pFile, "%s%s", Prs_ObjGetName(p, Prs_SliceName(p, Value)), Prs_ManWriteRange(p, Prs_SliceRange(p, Value), 1) );
     else if ( Type == CBA_PRS_CONCAT )
         Prs_ManWriteVerilogConcat( pFile, p, Value );
     else assert( 0 );
@@ -182,7 +208,7 @@ static void Prs_ManWriteVerilogArray2( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t *
     Vec_IntForEachEntryDouble( vSigs, FormId, ActSig, i )
     {
         fprintf( pFile, "." );
-        fprintf( pFile, "%s", Prs_NtkStr(p, FormId) );
+        fprintf( pFile, "%s", Prs_ObjGetName(p, FormId) );
         fprintf( pFile, "(" );
         Prs_ManWriteVerilogSignal( pFile, p, ActSig );
         fprintf( pFile, ")%s", (i == Vec_IntSize(vSigs) - 2) ? "" : ", " );
@@ -208,8 +234,8 @@ static void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p, char ** pType
     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 )
+        //char * pNtkName = Prs_ObjGetName(p, Prs_BoxName(p, i));
+        if ( NtkId == CBA_BOX_MUX && Prs_BoxIsNode(p, i) )
             Prs_ManWriteVerilogMux( pFile, p, vBox );
         else if ( Prs_BoxIsNode(p, i) ) // node
         {
@@ -252,7 +278,7 @@ static void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p, char ** pType
         }
         else // box
         {
-            fprintf( pFile, "  %s %s ( ", Prs_NtkStr(p, NtkId), Prs_BoxName(p, i) ? Prs_NtkStr(p, Prs_BoxName(p, i)) : "" );
+            fprintf( pFile, "  %s %s ( ", Prs_ObjGetName(p, NtkId), Prs_BoxName(p, i) ? Prs_ObjGetName(p, Prs_BoxName(p, i)) : "" );
             Prs_ManWriteVerilogArray2( pFile, p, vBox );
             fprintf( pFile, " );\n" );
         }
@@ -267,19 +293,22 @@ static void Prs_ManWriteVerilogIos( FILE * pFile, Prs_Ntk_t * p, int SigType )
     if ( SigType == 3 )
         fprintf( pFile, "\n" );
     Vec_IntForEachEntryTwo( vSigs[SigType], vSigsR[SigType], NameId, RangeId, i )
-        fprintf( pFile, "  %s %s%s%s;\n", pSigNames[SigType], Abc_LitIsCompl(RangeId) ? "signed " : "", RangeId ? Prs_ManWriteRange(p, Abc_Lit2Var(RangeId), 0) : "", Prs_NtkStr(p, NameId) );
+    {
+        fprintf( pFile, "  %s %s%s", pSigNames[SigType], Abc_LitIsCompl(RangeId) ? "signed " : "", RangeId ? Prs_ManWriteRange(p, Abc_Lit2Var(RangeId), 0) : "" );
+        fprintf( pFile, "%s;\n", Prs_ObjGetName(p, NameId) );
+    }
 }
 static void Prs_ManWriteVerilogIoOrder( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vOrder )
 {
     int i, NameId;
     Vec_IntForEachEntry( vOrder, NameId, i )
-        fprintf( pFile, "%s%s", Prs_NtkStr(p, Abc_Lit2Var2(NameId)), i == Vec_IntSize(vOrder) - 1 ? "" : ", " );
+        fprintf( pFile, "%s%s", Prs_ObjGetName(p, Abc_Lit2Var2(NameId)), i == Vec_IntSize(vOrder) - 1 ? "" : ", " );
 }
 static void Prs_ManWriteVerilogNtk( FILE * pFile, Prs_Ntk_t * p, char ** pTypeNames )
 {
     int s;
     // write header
-    fprintf( pFile, "module %s (\n    ", Prs_NtkStr(p, p->iModuleName) );
+    fprintf( pFile, "module %s (\n    ", Prs_ObjGetName(p, p->iModuleName) );
     Prs_ManWriteVerilogIoOrder( pFile, p, &p->vOrder );
     fprintf( pFile, "\n  );\n" );
     // write declarations
@@ -377,13 +406,13 @@ void Cba_ManWriteFonRange( Cba_Ntk_t * p, int iFon )
 }
 void Cba_ManWriteFonName( Cba_Ntk_t * p, int iFon, int fInlineConcat, int fInput )
 {
-    extern void Cba_ManWriteCatIn( Cba_Ntk_t * p, int iObj );
+    extern void Cba_ManWriteConcat( Cba_Ntk_t * p, int iObj );
     Vec_Str_t * vStr = &p->pDesign->vOut;
     if ( !iFon || (!Cba_FonIsConst(iFon) && !Cba_FonName(p, iFon)) ) 
         Vec_StrPrintF( vStr, "Open_%d", Cba_NtkMan(p)->nOpens++ );
 //        Vec_StrPrintF( vStr, "1\'b0" );
-    else if ( fInlineConcat && !Cba_FonIsConst(iFon) && Cba_ObjIsCatIn(p, Cba_FonObj(p, iFon)) )
-        Cba_ManWriteCatIn( p, Cba_FonObj(p, iFon) );
+    else if ( fInlineConcat && !Cba_FonIsConst(iFon) && Cba_ObjIsConcat(p, Cba_FonObj(p, iFon)) )
+        Cba_ManWriteConcat( p, Cba_FonObj(p, iFon) );
     else
     {
         int Range = fInput ? Cba_FonRangeSize( p, iFon ) : 0;
@@ -394,11 +423,11 @@ void Cba_ManWriteFonName( Cba_Ntk_t * p, int iFon, int fInlineConcat, int fInput
             Vec_StrPush( vStr, '}' );
     }
 }
-void Cba_ManWriteCatIn( Cba_Ntk_t * p, int iObj )
+void Cba_ManWriteConcat( Cba_Ntk_t * p, int iObj )
 {
     int i, iFin, iFon;
     Vec_Str_t * vStr = &p->pDesign->vOut;
-    assert( Cba_ObjIsCatIn(p, iObj) );
+    assert( Cba_ObjIsConcat(p, iObj) );
     Vec_StrPush( vStr, '{' );
     Cba_ObjForEachFinFon( p, iObj, iFin, iFon, i )
     {
@@ -407,21 +436,6 @@ void Cba_ManWriteCatIn( Cba_Ntk_t * p, int iObj )
     }
     Vec_StrPush( vStr, '}' );
 }
-void Cba_ManWriteCatOut( Cba_Ntk_t * p, int iObj )
-{
-    int i, iFon;
-    Vec_Str_t * vStr = &p->pDesign->vOut;
-    assert( Cba_ObjIsCatOut(p, iObj) );
-    if ( Cba_ObjFonNum(p, iObj) > 1 )
-        Vec_StrPush( vStr, '{' );
-    Cba_ObjForEachFon( p, iObj, iFon, i )
-    {
-        Vec_StrPrintStr( vStr, i ? ", " : "" );
-        Cba_ManWriteFonName( p, iFon, 0, 0 );
-    }
-    if ( Cba_ObjFonNum(p, iObj) > 1 )
-        Vec_StrPush( vStr, '}' );
-}
 int Cba_ManWriteLineFile( Cba_Ntk_t * p, int iObj, int FileAttr, int LineAttr )
 {
     Vec_Str_t * vStr = &p->pDesign->vOut;
@@ -485,7 +499,7 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
         int Type = Cba_ObjType(p, iObj);
         if ( Cba_ObjIsSlice(p, iObj) )
             continue;
-        if ( fInlineConcat && Cba_ObjIsCatIn(p, iObj) )
+        if ( fInlineConcat && Cba_ObjIsConcat(p, iObj) )
             continue;
         if ( Cba_ObjIsBoxUser(p, iObj) )
         {
@@ -552,27 +566,6 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             Cba_ManWriteFonName( p, iFonOut, 0, 1 );
             Vec_StrPrintStr( vStr, ") );" );
         }
-        else if ( Type == CBA_BOX_CATOUT )
-        {
-            // write declarations
-            Cba_ObjForEachFon( p, iObj, iFon, i )
-            {
-                if ( !Cba_FonName(p, iFon) ) 
-                    continue;
-                if ( Vec_BitEntry(vPoFons, iFon) )
-                    continue;
-                Vec_StrPrintStr( vStr, "  wire " );
-                Cba_ManWriteFonRange( p, iFon );
-                Cba_ManWriteFonName( p, iFon, 0, 0 );
-                Vec_StrPrintStr( vStr, ";\n" );
-            }
-            // write output concatenation
-            Vec_StrPrintStr( vStr, "  assign " );
-            Cba_ManWriteCatOut( p, iObj );
-            Vec_StrPrintStr( vStr, " = " );
-            Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), 0, 0 );
-            Vec_StrPush( vStr, ';' );
-        }
         else if ( Type == CBA_BOX_NMUX || Type == CBA_BOX_SEL )
         {
             int fUseSel = Type == CBA_BOX_SEL;
@@ -878,8 +871,8 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             }
             Cba_ManWriteFonName( p, Cba_ObjFon0(p, iObj), 0, 0 );
             Vec_StrPrintStr( vStr, " = " );
-            if ( Cba_ObjIsCatIn(p, iObj) )
-                Cba_ManWriteCatIn( p, iObj );
+            if ( Cba_ObjIsConcat(p, iObj) )
+                Cba_ManWriteConcat( p, iObj );
             else if ( Type == CBA_BOX_MUX )
             {
                 Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );