New parser and framework.

24 files changed, 3294 insertions, 837 deletions

diff --git a/Makefile b/Makefile
index 7fe51673..532639d2 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@ PROG := abc
 MODULES := \
 	$(wildcard src/ext*) \
 	src/base/abc src/base/abci src/base/cmd src/base/io \
-	src/base/main src/base/ver src/base/wlc src/base/test \
+	src/base/main src/base/ver src/base/wlc src/base/cba src/base/test \
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse \
 	src/bdd/reo src/bdd/cas \
 	src/map/mapper src/map/mio src/map/super src/map/if \
diff --git a/abclib.dsp b/abclib.dsp
index a09acc7f..8a948629 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -770,6 +770,58 @@ SOURCE=.\src\base\wlc\wlcReadVer.c
 SOURCE=.\src\base\wlc\wlcWriteVer.c
 # End Source File
 # End Group
+# Begin Group "cba"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\cba\cba.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaBlast.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaBuild.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaCom.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaPrs.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaReadBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaReadVer.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaSimple.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaWriteBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cba\cbaWriteVer.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "bdd"
 
diff --git a/src/base/abc/abcHieGia.c b/src/base/abc/abcHieGia.c
index 1b5413e0..24166c8f 100644
--- a/src/base/abc/abcHieGia.c
+++ b/src/base/abc/abcHieGia.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "misc/util/utilNam.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -321,829 +320,6 @@ Gia_Man_t * Gia_ManFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
 }
 
 
-
-
-/*
-design = array containing design name (as the first entry in the array) followed by pointers to modules
-module = array containing module name (as the first entry in the array) followed by pointers to four arrays: 
-         {array of input names; array of output names; array of nodes; array of boxes}
-node   = array containing output name, followed by node type, followed by input names
-box    = array containing model name, instance name, followed by pairs of formal/actual names for each port
-*/
-
-
-/**Function*************************************************************
-
-  Synopsis    [Node type conversions.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-typedef enum { 
-    PTR_OBJ_NONE,    // 0: non-existent object
-    PTR_OBJ_CONST0,  // 1: constant node
-    PTR_OBJ_PI,      // 2: primary input
-    PTR_OBJ_PO,      // 3: primary output
-    PTR_OBJ_FAN,     // 4: box output
-    PTR_OBJ_FLOP,    // 5: flip-flop
-    PTR_OBJ_BOX,     // 6: box
-    PTR_OBJ_NODE,    // 7: logic node
-
-    PTR_OBJ_C0,      // 8: logic node
-    PTR_OBJ_C1,      // 9: logic node
-    PTR_OBJ_BUF,     // 0: logic node
-    PTR_OBJ_INV,     // 1: logic node
-    PTR_OBJ_AND,     // 2: logic node
-    PTR_OBJ_OR,      // 3: logic node
-    PTR_OBJ_XOR,     // 4: logic node
-    PTR_OBJ_NAND,    // 5: logic node
-    PTR_OBJ_NOR,     // 6: logic node
-    PTR_OBJ_XNOR,    // 7: logic node
-    PTR_OBJ_MUX,     // 8: logic node
-    PTR_OBJ_MAJ,     // 9: logic node
-
-    PTR_VOID         // 0: placeholder
-} Ptr_ObjType_t;
-
-char * Ptr_TypeToName( Ptr_ObjType_t Type )
-{
-    if ( Type == PTR_OBJ_BUF )   return "buf";
-    if ( Type == PTR_OBJ_INV )   return "not";
-    if ( Type == PTR_OBJ_AND )   return "and";
-    if ( Type == PTR_OBJ_OR )    return "or";
-    if ( Type == PTR_OBJ_XOR )   return "xor";
-    if ( Type == PTR_OBJ_XNOR )  return "xnor";
-    assert( 0 );
-    return "???";
-}
-char * Ptr_TypeToSop( Ptr_ObjType_t Type )
-{
-    if ( Type == PTR_OBJ_BUF )   return "1 1\n";
-    if ( Type == PTR_OBJ_INV )   return "0 1\n";
-    if ( Type == PTR_OBJ_AND )   return "11 1\n";
-    if ( Type == PTR_OBJ_OR )    return "00 0\n";
-    if ( Type == PTR_OBJ_XOR )   return "01 1\n10 1\n";
-    if ( Type == PTR_OBJ_XNOR )  return "00 1\n11 1\n";
-    assert( 0 );
-    return "???";
-}
-Ptr_ObjType_t Ptr_SopToType( char * pSop )
-{
-    if ( !strcmp(pSop, "1 1\n") )        return PTR_OBJ_BUF;
-    if ( !strcmp(pSop, "0 1\n") )        return PTR_OBJ_INV;
-    if ( !strcmp(pSop, "11 1\n") )       return PTR_OBJ_AND;
-    if ( !strcmp(pSop, "00 0\n") )       return PTR_OBJ_OR;
-    if ( !strcmp(pSop, "-1 1\n1- 1\n") ) return PTR_OBJ_OR;
-    if ( !strcmp(pSop, "1- 1\n-1 1\n") ) return PTR_OBJ_OR;
-    if ( !strcmp(pSop, "01 1\n10 1\n") ) return PTR_OBJ_XOR;
-    if ( !strcmp(pSop, "10 1\n01 1\n") ) return PTR_OBJ_XOR;
-    if ( !strcmp(pSop, "11 1\n00 1\n") ) return PTR_OBJ_XNOR;
-    if ( !strcmp(pSop, "00 1\n11 1\n") ) return PTR_OBJ_XNOR;
-    assert( 0 );
-    return PTR_OBJ_NONE;
-}
-Ptr_ObjType_t Ptr_HopToType( Abc_Obj_t * pObj )
-{
-    static word uTruth, uTruths6[3] = {
-        ABC_CONST(0xAAAAAAAAAAAAAAAA),
-        ABC_CONST(0xCCCCCCCCCCCCCCCC),
-        ABC_CONST(0xF0F0F0F0F0F0F0F0),
-    };
-    assert( Abc_ObjIsNode(pObj) );
-    uTruth = Hop_ManComputeTruth6( (Hop_Man_t *)Abc_ObjNtk(pObj)->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj) );
-    if ( uTruth ==  uTruths6[0] )                 return PTR_OBJ_BUF;
-    if ( uTruth == ~uTruths6[0] )                 return PTR_OBJ_INV;
-    if ( uTruth == (uTruths6[0] & uTruths6[1]) )  return PTR_OBJ_AND;
-    if ( uTruth == (uTruths6[0] | uTruths6[1]) )  return PTR_OBJ_OR;
-    if ( uTruth == (uTruths6[0] ^ uTruths6[1]) )  return PTR_OBJ_XOR;
-    if ( uTruth == (uTruths6[0] ^~uTruths6[1]) )  return PTR_OBJ_XNOR;
-    assert( 0 );
-    return PTR_OBJ_NONE;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dumping hierarchical Abc_Ntk_t in Ptr form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline char * Ptr_ObjName( Abc_Obj_t * pObj )
-{
-    if ( Abc_ObjIsNet(pObj) || Abc_ObjIsBox(pObj) )
-        return Abc_ObjName(pObj);
-    if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) )
-        return Ptr_ObjName(Abc_ObjFanout0(pObj));
-    if ( Abc_ObjIsCo(pObj) )
-        return Ptr_ObjName(Abc_ObjFanin0(pObj));
-    assert( 0 );
-    return NULL;
-}
-int Ptr_ManCheckArray( Vec_Ptr_t * vArray )
-{
-    if ( Vec_PtrSize(vArray) == 0 )
-        return 1;
-    if ( Abc_MaxInt(8, Vec_PtrSize(vArray)) == Vec_PtrCap(vArray) )
-        return 1;
-    assert( 0 );
-    return 0;
-}
-Vec_Ptr_t * Ptr_ManDumpNode( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pFanin; int i;
-    Vec_Ptr_t * vNode = Vec_PtrAlloc( 2 + Abc_ObjFaninNum(pObj) );
-    assert( Abc_ObjIsNode(pObj) );
-    Vec_PtrPush( vNode, Ptr_ObjName(pObj) );
-    Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_HopToType(pObj)) );
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-        Vec_PtrPush( vNode, Ptr_ObjName(pFanin) );
-    assert( Ptr_ManCheckArray(vNode) );
-    return vNode;
-}
-Vec_Ptr_t * Ptr_ManDumpNodes( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj; int i;
-    Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
-    Abc_NtkForEachNode( pNtk, pObj, i )
-        Vec_PtrPush( vNodes, Ptr_ManDumpNode(pObj) );
-    assert( Ptr_ManCheckArray(vNodes) );
-    return vNodes;
-}
-
-Vec_Ptr_t * Ptr_ManDumpBox( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pNext; int i;
-    Abc_Ntk_t * pModel = Abc_ObjModel(pObj);
-    Vec_Ptr_t * vBox = Vec_PtrAlloc( 2 + 2 * Abc_ObjFaninNum(pObj) + 2 * Abc_ObjFanoutNum(pObj) );
-    assert( Abc_ObjIsBox(pObj) );
-    Vec_PtrPush( vBox, Abc_NtkName(pModel) );
-    Vec_PtrPush( vBox, Ptr_ObjName(pObj) );
-    Abc_ObjForEachFanin( pObj, pNext, i )
-    {
-        Vec_PtrPush( vBox, Ptr_ObjName(Abc_NtkPi(pModel, i)) );
-        Vec_PtrPush( vBox, Ptr_ObjName(pNext) );
-    }
-    Abc_ObjForEachFanout( pObj, pNext, i )
-    {
-        Vec_PtrPush( vBox, Ptr_ObjName(Abc_NtkPo(pModel, i)) );
-        Vec_PtrPush( vBox, Ptr_ObjName(pNext) );
-    }
-    assert( Ptr_ManCheckArray(vBox) );
-    return vBox;
-}
-Vec_Ptr_t * Ptr_ManDumpBoxes( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj; int i;
-    Vec_Ptr_t * vBoxes = Vec_PtrAlloc( Abc_NtkBoxNum(pNtk) );
-    Abc_NtkForEachBox( pNtk, pObj, i )
-        Vec_PtrPush( vBoxes, Ptr_ManDumpBox(pObj) );
-    assert( Ptr_ManCheckArray(vBoxes) );
-    return vBoxes;
-}
-
-Vec_Ptr_t * Ptr_ManDumpInputs( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj; int i;
-    Vec_Ptr_t * vSigs = Vec_PtrAlloc( Abc_NtkPiNum(pNtk) );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        Vec_PtrPush( vSigs, Ptr_ObjName(pObj) );
-    assert( Ptr_ManCheckArray(vSigs) );
-    return vSigs;
-}
-Vec_Ptr_t * Ptr_ManDumpOutputs( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj; int i;
-    Vec_Ptr_t * vSigs = Vec_PtrAlloc( Abc_NtkPoNum(pNtk) );
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Vec_PtrPush( vSigs, Ptr_ObjName(pObj) );
-    assert( Ptr_ManCheckArray(vSigs) );
-    return vSigs;
-}
-Vec_Ptr_t * Ptr_ManDumpNtk( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vNtk = Vec_PtrAlloc( 5 );
-    Vec_PtrPush( vNtk, Abc_NtkName(pNtk) );
-    Vec_PtrPush( vNtk, Ptr_ManDumpInputs(pNtk) );
-    Vec_PtrPush( vNtk, Ptr_ManDumpOutputs(pNtk) );
-    Vec_PtrPush( vNtk, Ptr_ManDumpNodes(pNtk) );
-    Vec_PtrPush( vNtk, Ptr_ManDumpBoxes(pNtk) );
-    assert( Ptr_ManCheckArray(vNtk) );
-    return vNtk;
-}
-Vec_Ptr_t * Ptr_ManDumpDes( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vDes;
-    Abc_Ntk_t * pTemp; int i;
-    vDes = Vec_PtrAlloc( 1 + Vec_PtrSize(pNtk->pDesign->vModules) );
-    Vec_PtrPush( vDes, pNtk->pDesign->pName );
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
-        Vec_PtrPush( vDes, Ptr_ManDumpNtk(pTemp) );
-    assert( Ptr_ManCheckArray(vDes) );
-    return vDes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dumping Ptr into a Verilog file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ptr_ManDumpNodeToBlif( FILE * pFile, Vec_Ptr_t * vNode )
-{
-    char * pName;  int i;
-    fprintf( pFile, ".names" );
-    Vec_PtrForEachEntryStart( char *, vNode, pName, i, 2 )
-        fprintf( pFile, " %s", pName );
-    fprintf( pFile, " %s\n", (char *)Vec_PtrEntry(vNode, 0) );
-    fprintf( pFile, "%s", Ptr_TypeToSop( (Ptr_ObjType_t)Abc_Ptr2Int(Vec_PtrEntry(vNode, 1)) ) );
-}
-void Ptr_ManDumpNodesToBlif( FILE * pFile, Vec_Ptr_t * vNodes )
-{
-    Vec_Ptr_t * vNode; int i;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
-        Ptr_ManDumpNodeToBlif( pFile, vNode );
-}
-
-void Ptr_ManDumpBoxToBlif( FILE * pFile, Vec_Ptr_t * vBox )
-{
-    char * pName; int i;
-    fprintf( pFile, "%s", (char *)Vec_PtrEntry(vBox, 0) );
-    Vec_PtrForEachEntryStart( char *, vBox, pName, i, 2 )
-        fprintf( pFile, " %s=%s", pName, (char *)Vec_PtrEntry(vBox, i+1) ), i++;
-    fprintf( pFile, "\n" );
-}
-void Ptr_ManDumpBoxesToBlif( FILE * pFile, Vec_Ptr_t * vBoxes )
-{
-    Vec_Ptr_t * vBox; int i;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vBoxes, vBox, i )
-        Ptr_ManDumpBoxToBlif( pFile, vBox );
-}
-
-void Ptr_ManDumpSignalsToBlif( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
-{
-    char * pSig; int i;
-    Vec_PtrForEachEntry( char *, vSigs, pSig, i )
-        fprintf( pFile, " %s", pSig );
-}
-void Ptr_ManDumpModuleToBlif( FILE * pFile, Vec_Ptr_t * vNtk )
-{
-    fprintf( pFile, ".model %s\n", (char *)Vec_PtrEntry(vNtk, 0) );
-    fprintf( pFile, ".inputs" );
-    Ptr_ManDumpSignalsToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, ".outputs" );
-    Ptr_ManDumpSignalsToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
-    fprintf( pFile, "\n\n" );
-    Ptr_ManDumpNodesToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
-    fprintf( pFile, "\n" );
-    Ptr_ManDumpBoxesToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, ".end\n\n" );
-}
-void Ptr_ManDumpToBlif( char * pFileName, Vec_Ptr_t * vDes )
-{
-    FILE * pFile;
-    Vec_Ptr_t * vNtk; int i;
-    pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open output file \"%s\".\n", pFileName );
-        return;
-    }
-    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", (char *)Vec_PtrEntry(vDes, 0), Extra_TimeStamp() );
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Ptr_ManDumpModuleToBlif( pFile, vNtk );
-    fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Dumping Ptr into a Verilog file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ptr_ManDumpNodeToFile( FILE * pFile, Vec_Ptr_t * vNode )
-{
-    char * pName;  int i;
-    fprintf( pFile, "%s", Ptr_TypeToName( (Ptr_ObjType_t)Abc_Ptr2Int(Vec_PtrEntry(vNode, 1)) ) );
-    fprintf( pFile, "( %s", (char *)Vec_PtrEntry(vNode, 0) );
-    Vec_PtrForEachEntryStart( char *, vNode, pName, i, 2 )
-        fprintf( pFile, ", %s", pName );
-    fprintf( pFile, " );\n" );
-}
-void Ptr_ManDumpNodesToFile( FILE * pFile, Vec_Ptr_t * vNodes )
-{
-    Vec_Ptr_t * vNode; int i;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
-        Ptr_ManDumpNodeToFile( pFile, vNode );
-}
-
-void Ptr_ManDumpBoxToFile( FILE * pFile, Vec_Ptr_t * vBox )
-{
-    char * pName; int i;
-    fprintf( pFile, "%s %s (", (char *)Vec_PtrEntry(vBox, 0), (char *)Vec_PtrEntry(vBox, 1) );
-    Vec_PtrForEachEntryStart( char *, vBox, pName, i, 2 )
-        fprintf( pFile, " .%s(%s)%s", pName, (char *)Vec_PtrEntry(vBox, i+1), i >= Vec_PtrSize(vBox)-2 ? "" : "," ), i++;
-    fprintf( pFile, " );\n" );
-}
-void Ptr_ManDumpBoxesToFile( FILE * pFile, Vec_Ptr_t * vBoxes )
-{
-    Vec_Ptr_t * vBox; int i;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vBoxes, vBox, i )
-        Ptr_ManDumpBoxToFile( pFile, vBox );
-}
-
-void Ptr_ManDumpSignalsToFile( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
-{
-    char * pSig; int i;
-    Vec_PtrForEachEntry( char *, vSigs, pSig, i )
-        fprintf( pFile, " %s%s", pSig, (fSkipLastComma && i == Vec_PtrSize(vSigs)-1) ? "" : "," );
-}
-void Ptr_ManDumpModuleToFile( FILE * pFile, Vec_Ptr_t * vNtk )
-{
-    fprintf( pFile, "module %s\n", (char *)Vec_PtrEntry(vNtk, 0) );
-    fprintf( pFile, "(\n" );
-    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
-    fprintf( pFile, "\n" );
-    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
-    fprintf( pFile, "\n);\ninput" );
-    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 1 );
-    fprintf( pFile, ";\noutput" );
-    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
-    fprintf( pFile, ";\n\n" );
-    Ptr_ManDumpNodesToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
-    fprintf( pFile, "\n" );
-    Ptr_ManDumpBoxesToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
-    fprintf( pFile, "endmodule\n\n" );
-}
-void Ptr_ManDumpToFile( char * pFileName, Vec_Ptr_t * vDes )
-{
-    FILE * pFile;
-    Vec_Ptr_t * vNtk; int i;
-    pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open output file \"%s\".\n", pFileName );
-        return;
-    }
-    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", (char *)Vec_PtrEntry(vDes, 0), Extra_TimeStamp() );
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Ptr_ManDumpModuleToFile( pFile, vNtk );
-    fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count memory used by Ptr.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ptr_ManMemArray( Vec_Ptr_t * vArray )
-{
-    return (int)Vec_PtrMemory(vArray);
-}
-int Ptr_ManMemArrayArray( Vec_Ptr_t * vArrayArray )
-{
-    Vec_Ptr_t * vArray; int i, nBytes = 0;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vArrayArray, vArray, i )
-        nBytes += Ptr_ManMemArray(vArray);
-    return nBytes;
-}
-int Ptr_ManMemNtk( Vec_Ptr_t * vNtk )
-{
-    int nBytes = (int)Vec_PtrMemory(vNtk);
-    nBytes += Ptr_ManMemArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1) );
-    nBytes += Ptr_ManMemArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2) );
-    nBytes += Ptr_ManMemArrayArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
-    nBytes += Ptr_ManMemArrayArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
-    return nBytes;
-}
-int Ptr_ManMemDes( Vec_Ptr_t * vDes )
-{
-    Vec_Ptr_t * vNtk; int i, nBytes = (int)Vec_PtrMemory(vDes);
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        nBytes += Ptr_ManMemNtk(vNtk);
-    return nBytes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Free Ptr.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ptr_ManFreeNtk( Vec_Ptr_t * vNtk )
-{
-    Vec_PtrFree( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1) );
-    Vec_PtrFree( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2) );
-    Vec_VecFree( (Vec_Vec_t *)Vec_PtrEntry(vNtk, 3) );
-    Vec_VecFree( (Vec_Vec_t *)Vec_PtrEntry(vNtk, 4) );
-    Vec_PtrFree( vNtk );
-}
-void Ptr_ManFreeDes( Vec_Ptr_t * vDes )
-{
-    Vec_Ptr_t * vNtk; int i;
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Ptr_ManFreeNtk( vNtk );
-    Vec_PtrFree( vDes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count memory use used by Ptr.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ptr_ManExperiment( Abc_Ntk_t * pNtk )
-{
-    abctime clk = Abc_Clock();
-    Vec_Ptr_t * vDes = Ptr_ManDumpDes( pNtk );
-    printf( "Converting to Ptr:  Memory = %6.3f MB  ", 1.0*Ptr_ManMemDes(vDes)/(1<<20) );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    Ptr_ManDumpToFile( Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.v"), vDes );
-    printf( "Finished writing output file \"%s\".\n", Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.v") );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    Ptr_ManFreeDes( vDes );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Transform Ptr into Int.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ptr_ManDumpArrayToInt( Abc_Nam_t * pNames, Vec_Ptr_t * vVec, int fNode )
-{
-    char * pName; int i;
-    Vec_Int_t * vNew = Vec_IntAlloc( Vec_PtrSize(vVec) );
-    Vec_PtrForEachEntry( char *, vVec, pName, i )
-        Vec_IntPush( vNew, (fNode && i == 1) ? Abc_Ptr2Int(pName) : Abc_NamStrFind(pNames, pName) );
-    return vNew;
-}
-Vec_Ptr_t * Ptr_ManDumpArrarArrayToInt( Abc_Nam_t * pNames, Vec_Ptr_t * vNodes, int fNode )
-{
-    Vec_Ptr_t * vNode; int i;
-    Vec_Ptr_t * vNew = Vec_PtrAlloc( Vec_PtrSize(vNodes) );
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
-        Vec_PtrPush( vNew, Ptr_ManDumpArrayToInt(pNames, vNode, fNode) );
-    assert( Ptr_ManCheckArray(vNew) );
-    return vNew;
-}
-Vec_Ptr_t * Ptr_ManDumpNtkToInt( Abc_Nam_t * pNames, Vec_Ptr_t * vNtk, int i )
-{
-    Vec_Ptr_t * vNew   = Vec_PtrAlloc( 5 );
-    assert( Abc_NamStrFind(pNames, (char *)Vec_PtrEntry(vNtk, 0)) == i );
-    Vec_PtrPush( vNew, Abc_Int2Ptr(i) );
-    Vec_PtrPush( vNew, Ptr_ManDumpArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0) );
-    Vec_PtrPush( vNew, Ptr_ManDumpArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 0) );
-    Vec_PtrPush( vNew, Ptr_ManDumpArrarArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3), 1) );
-    Vec_PtrPush( vNew, Ptr_ManDumpArrarArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4), 0) );
-    assert( Ptr_ManCheckArray(vNew) );
-    return vNew;
-}
-Vec_Ptr_t * Ptr_ManDumpToInt( Vec_Ptr_t * vDes )
-{
-    Vec_Ptr_t * vNew = Vec_PtrAlloc( Vec_PtrSize(vDes) );
-    Vec_Ptr_t * vNtk; int i;
-    // create module names
-    Abc_Nam_t * pNames = Abc_NamStart( 1000, 20 );
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Abc_NamStrFind( pNames, (char *)Vec_PtrEntry(vNtk, 0) );
-    assert( i == Abc_NamObjNumMax(pNames) );
-    // create resulting array
-    Vec_PtrPush( vNew, pNames );
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Vec_PtrPush( vNew, Ptr_ManDumpNtkToInt(pNames, vNtk, i) );
-    assert( Ptr_ManCheckArray(vNew) );
-    return vNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Transform Ptr into Int.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-typedef struct Int_Des_t_ Int_Des_t;
-struct Int_Des_t_
-{
-    char *           pName;   // design name
-    Abc_Nam_t *      pNames;  // name manager
-    Vec_Ptr_t        vModels; // models
-};
-typedef struct Int_Obj_t_ Int_Obj_t;
-struct Int_Obj_t_
-{
-    int              iModel;
-    int              iFunc;
-    Vec_Wrd_t        vFanins;
-};
-typedef struct Int_Ntk_t_ Int_Ntk_t;
-struct Int_Ntk_t_
-{
-    int              iName;
-    int              nObjs;
-    Int_Des_t *      pMan;
-    Vec_Ptr_t        vInstances;
-    Vec_Wrd_t        vOutputs;
-    Vec_Int_t        vInputNames;
-    Vec_Int_t        vOutputNames;
-    Vec_Int_t *      vCopies;
-    Vec_Int_t *      vCopies2;
-};
-
-static inline char *      Int_DesName( Int_Des_t * p )       { return p->pName;                                     }
-static inline int         Int_DesNtkNum( Int_Des_t * p )     { return Vec_PtrSize( &p->vModels ) - 1;               }
-static inline Int_Ntk_t * Int_DesNtk( Int_Des_t * p, int i ) { return (Int_Ntk_t *)Vec_PtrEntry( &p->vModels, i );  }
-
-static inline char *      Int_NtkName( Int_Ntk_t * p )       { return Abc_NamStr( p->pMan->pNames, p->iName );      }
-static inline int         Int_NtkPiNum( Int_Ntk_t * p )      { return Vec_IntSize( &p->vInputNames );               }
-static inline int         Int_NtkPoNum( Int_Ntk_t * p )      { return Vec_IntSize( &p->vOutputNames );              }
-
-static inline int         Int_ObjInputNum( Int_Ntk_t * p, Int_Obj_t * pObj )  { return pObj->iModel ? Int_NtkPiNum(Int_DesNtk(p->pMan, pObj->iModel)) : Vec_WrdSize(&pObj->vFanins); }
-static inline int         Int_ObjOutputNum( Int_Ntk_t * p, Int_Obj_t * pObj ) { return pObj->iModel ? Int_NtkPoNum(Int_DesNtk(p->pMan, pObj->iModel)) : 1;                           }
-
-Int_Obj_t * Int_ObjAlloc( int nFanins )
-{
-    Int_Obj_t * p = (Int_Obj_t *)ABC_CALLOC( char, sizeof(Int_Obj_t) + sizeof(word) * nFanins );
-    p->vFanins.pArray = (word *)((char *)p + sizeof(Int_Obj_t));
-    p->vFanins.nCap = nFanins;
-    return p;
-}
-void Int_ObjFree( Int_Obj_t * p )
-{
-    ABC_FREE( p );
-}
-Int_Ntk_t * Int_NtkAlloc( Int_Des_t * pMan, int Id, int nPis, int nPos, int nInsts )
-{
-    Int_Ntk_t * p = ABC_CALLOC( Int_Ntk_t, 1 );
-    p->iName = Id;
-    p->nObjs = nPis + nInsts;
-    p->pMan  = pMan;
-    Vec_PtrGrow( &p->vInstances,   nInsts );
-    Vec_WrdGrow( &p->vOutputs,     nPos );
-    Vec_IntGrow( &p->vInputNames,  nPis );
-    Vec_IntGrow( &p->vOutputNames, nPos );
-    return p;
-}
-void Int_NtkFree( Int_Ntk_t * p )
-{
-    Int_Obj_t * pObj; int i;
-    Vec_PtrForEachEntry( Int_Obj_t *, &p->vInstances, pObj, i )
-        Int_ObjFree( pObj );
-    ABC_FREE( p->vInstances.pArray );
-    ABC_FREE( p->vOutputs.pArray );
-    ABC_FREE( p->vInputNames.pArray );
-    ABC_FREE( p->vOutputNames.pArray );
-    Vec_IntFreeP( &p->vCopies );
-    Vec_IntFreeP( &p->vCopies2 );
-    ABC_FREE( p );
-}
-Int_Des_t * Int_DesAlloc( char * pName, Abc_Nam_t * pNames, int nModels )
-{
-    Int_Des_t * p = ABC_CALLOC( Int_Des_t, 1 );
-    p->pName  = pName;
-    p->pNames = pNames;
-    Vec_PtrGrow( &p->vModels, nModels );
-    return p;
-}
-void Int_DesFree( Int_Des_t * p )
-{
-    Int_Ntk_t * pTemp; int i;
-    Vec_PtrForEachEntry( Int_Ntk_t *, &p->vModels, pTemp, i )
-        Int_NtkFree( pTemp );
-    ABC_FREE( p );
-}
-
-// replaces formal inputs by their indixes
-void Ptr_ManFindInputOutputNumbers( Int_Ntk_t * pModel, Vec_Int_t * vBox, Vec_Int_t * vMap ) 
-{
-    int i, iFormal, iName, nPis = Int_NtkPiNum(pModel);
-    Vec_IntForEachEntry( &pModel->vInputNames, iFormal, i )
-        Vec_IntWriteEntry( vMap, iFormal, i );
-    Vec_IntForEachEntry( &pModel->vOutputNames, iFormal, i )
-        Vec_IntWriteEntry( vMap, iFormal, nPis+i );
-    Vec_IntForEachEntryDouble( vBox, iFormal, iName, i )
-    {
-        if ( i == 0 ) continue;
-        assert( Vec_IntEntry(vMap, iFormal) >= 0 );
-        Vec_IntWriteEntry( vBox, i, Vec_IntEntry(vMap, iFormal) );
-    }
-    Vec_IntForEachEntry( &pModel->vInputNames, iFormal, i )
-        Vec_IntWriteEntry( vMap, iFormal, -1 );
-    Vec_IntForEachEntry( &pModel->vOutputNames, iFormal, i )
-        Vec_IntWriteEntry( vMap, iFormal, -1 );
-}
-void Ptr_ManConvertNtk( Int_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Wrd_t * vMap, Vec_Int_t * vMap2 )
-{
-    Vec_Int_t * vInputs  = (Vec_Int_t *)Vec_PtrEntry(vNtk, 1);
-    Vec_Int_t * vOutputs = (Vec_Int_t *)Vec_PtrEntry(vNtk, 2);
-    Vec_Ptr_t * vNodes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3);
-    Vec_Ptr_t * vBoxes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4);
-    Vec_Int_t * vNode, * vBox;
-    Int_Ntk_t * pModel;
-    Int_Obj_t * pObj;
-    int i, k, iFormal, iName, nPis, nOffset, nNonDriven = 0;
-
-    // map primary inputs
-    Vec_IntForEachEntry( vInputs, iName, i )
-    {
-        assert( ~Vec_WrdEntry(vMap, iName) == 0 ); // driven twice
-        Vec_WrdWriteEntry( vMap, iName, i );
-    }
-    // map internal nodes
-    nOffset = Vec_IntSize(vInputs);
-    Vec_PtrForEachEntry( Vec_Int_t *, vNodes, vNode, i )
-    {
-        iName = Vec_IntEntry(vNode, 0);
-        assert( ~Vec_WrdEntry(vMap, iName) == 0 ); // driven twice
-        Vec_WrdWriteEntry( vMap, iName, nOffset + i );
-    }
-    // map internal boxes
-    nOffset += Vec_PtrSize(vNodes);
-    Vec_PtrForEachEntry( Vec_Int_t *, vBoxes, vBox, i )
-    {
-        // get model name
-        iName = Vec_IntEntry( vBox, 0 );
-        assert( iName >= 1 && iName <= Int_DesNtkNum(pNtk->pMan) ); // bad model name
-        pModel = Int_DesNtk( pNtk->pMan, iName );
-        nPis = Int_NtkPiNum( pModel );
-        // replace inputs/outputs by their IDs
-        Ptr_ManFindInputOutputNumbers( pModel, vBox, vMap2 );
-        // go through outputs of this box
-        Vec_IntForEachEntryDouble( vBox, iFormal, iName, k )
-            if ( k > 0 && i >= nPis )  // output
-            {
-                assert( ~Vec_WrdEntry(vMap, iName) == 0 ); // driven twice
-                Vec_WrdWriteEntry( vMap, iName, (nOffset + i) | ((word)iFormal << 32) );
-            }
-    }
-
-    // save input names
-    Vec_IntForEachEntry( vInputs, iName, i )
-        Vec_IntPush( &pNtk->vInputNames, iName );
-    // create nodes with the given connectivity
-    Vec_PtrForEachEntry( Vec_Int_t *, vNodes, vNode, i )
-    {
-        pObj = Int_ObjAlloc( Vec_IntSize(vNode) - 2 );
-        pObj->iFunc = Vec_IntEntry(vNode, 1);
-        Vec_IntForEachEntryStart( vNode, iName, k, 2 )
-        {
-            Vec_WrdPush( &pObj->vFanins, Vec_WrdEntry(vMap, iName) );
-            nNonDriven += (~Vec_WrdEntry(vMap, iName) == 0);
-        }
-        Vec_PtrPush( &pNtk->vInstances, pObj );
-    }
-    // create boxes with the given connectivity
-    Vec_PtrForEachEntry( Vec_Int_t *, vBoxes, vBox, i )
-    {
-        pModel = Int_DesNtk( pNtk->pMan, Vec_IntEntry(vBox, 0) );
-        nPis = Int_NtkPiNum( pModel );
-        pObj = Int_ObjAlloc( nPis );
-        Vec_IntForEachEntryDouble( vBox, iFormal, iName, k )
-            if ( k > 0 && iFormal < nPis ) // input
-            {
-                Vec_WrdPush( &pObj->vFanins, Vec_WrdEntry(vMap, iName) );
-                nNonDriven += (~Vec_WrdEntry(vMap, iName) == 0);
-            }
-        Vec_PtrPush( &pNtk->vInstances, pObj );
-    }
-    // save output names
-    Vec_IntForEachEntry( vOutputs, iName, i )
-    {
-        Vec_IntPush( &pNtk->vOutputNames, iName );
-        Vec_WrdPush( &pNtk->vOutputs, Vec_WrdEntry(vMap, iName) );
-        nNonDriven += (~Vec_WrdEntry(vMap, iName) == 0);
-    }
-    if ( nNonDriven )
-        printf( "Model %s has %d non-driven nets.\n", Int_NtkName(pNtk), nNonDriven );
-}
-Int_Ntk_t * Ptr_ManConvertNtkInter( Int_Des_t * pDes, Vec_Ptr_t * vNtk, int Id )
-{
-    Vec_Int_t * vInputs  = (Vec_Int_t *)Vec_PtrEntry(vNtk, 1);
-    Vec_Int_t * vOutputs = (Vec_Int_t *)Vec_PtrEntry(vNtk, 2);
-    Vec_Ptr_t * vNodes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3);
-    Vec_Ptr_t * vBoxes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4);
-    return Int_NtkAlloc( pDes, Id, Vec_IntSize(vInputs), Vec_IntSize(vOutputs), Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) );
-}
-Int_Des_t * Ptr_ManConvert( Vec_Ptr_t * vDesPtr )
-{
-    Vec_Ptr_t * vNtk; int i;
-    char * pName = (char *)Vec_PtrEntry(vDesPtr, 0);
-    Vec_Ptr_t * vDes = Ptr_ManDumpToInt( vDesPtr );
-    Abc_Nam_t * pNames = (Abc_Nam_t *)Vec_PtrEntry(vDes, 0);
-    Vec_Wrd_t * vMap = Vec_WrdStartFull( Abc_NamObjNumMax(pNames) + 1 );
-    Vec_Int_t * vMap2 = Vec_IntStartFull( Abc_NamObjNumMax(pNames) + 1 );
-    Int_Des_t * pDes = Int_DesAlloc( pName, pNames, Vec_PtrSize(vDes)-1 );
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Vec_PtrPush( &pDes->vModels, Ptr_ManConvertNtkInter(pDes, vNtk, i) );
-    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Ptr_ManConvertNtk( Int_DesNtk(pDes, i), vNtk, vMap, vMap2 );
-    Ptr_ManFreeDes( vDes );
-    Vec_IntFree( vMap2 );
-    Vec_WrdFree( vMap );
-    return pDes;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates ccpy structures for each literal in the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Int_NtkCopyAlloc( Int_Ntk_t * p )
-{
-    Vec_Int_t * vCopies;
-    Int_Obj_t * pObj; int i, k, nOuts;
-    int nInputs = Vec_IntSize(&p->vInputNames);
-    int nEntries0 = nInputs + Vec_PtrSize(&p->vInstances);
-    int nEntries = nEntries0;
-    // count the number of entries
-    Vec_PtrForEachEntry( Int_Obj_t *, &p->vInstances, pObj, i )
-        nEntries += Int_ObjOutputNum(p, pObj) - 1;
-    if ( nEntries == nEntries0 )
-        return NULL;
-    // allocate the entries
-    vCopies = Vec_IntAlloc( nEntries );
-    Vec_IntFill( vCopies, nEntries0, -1 );
-    Vec_PtrForEachEntry( Int_Obj_t *, &p->vInstances, pObj, i )
-    {
-        nOuts = Int_ObjOutputNum( p, pObj );
-        Vec_IntWriteEntry( vCopies, nInputs + i, Vec_IntSize(vCopies) );
-        for ( k = 0; k < nOuts; k++ )
-            Vec_IntPush( vCopies, -1 );
-    }
-    assert( Vec_IntSize(vCopies) == nEntries );
-    return vCopies;
-}
-int Int_NtkCopyLookup( Int_Ntk_t * p, int iObj, int iOut )
-{
-    if ( iOut == 0 )
-        return Vec_IntEntry( p->vCopies, iObj );
-    return Vec_IntEntry( p->vCopies2, Vec_IntEntry(p->vCopies2, iObj) + iOut );
-}
-void Int_NtkCopyInsert( Int_Ntk_t * p, int iObj, int iOut, int Item )
-{
-    if ( iOut == 0 )
-        Vec_IntWriteEntry( p->vCopies, iObj, Item );
-    else
-        Vec_IntWriteEntry( p->vCopies2, Vec_IntEntry(p->vCopies2, iObj) + iOut, Item );
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cba/cba.c b/src/base/cba/cba.c
new file mode 100644
index 00000000..d4369533
--- /dev/null
+++ b/src/base/cba/cba.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [cba.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
new file mode 100644
index 00000000..810e2d23
--- /dev/null
+++ b/src/base/cba/cba.h
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+  FileName    [cba.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cba.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__cba__cba_h
+#define ABC__base__cba__cba_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/gia/gia.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilNam.h"
+#include "misc/mem/mem.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
+#include "misc/vec/vecWec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START 
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// network objects
+typedef enum { 
+    CBA_OBJ_NONE = 0,  // 0:  unused
+    CBA_OBJ_BARBUF,    // 1:  barrier buffer
+    CBA_OBJ_PI,        // 2:  input
+    CBA_OBJ_PO,        // 3:  output
+    CBA_OBJ_PIO,       // 4:  input
+    CBA_OBJ_NODE,      // 5:  node
+    CBA_OBJ_BOX,       // 6:  box
+    CBA_OBJ_PIN,       // 7:  box output
+    CBA_OBJ_LATCH,     // 8:  latch
+    CBA_OBJ_UNKNOWN    // 9:  unknown
+} Cba_ObjType_t; 
+
+// design
+typedef struct Cba_Man_t_ Cba_Man_t;
+struct Cba_Man_t_
+{
+    // design names
+    char *       pName;    // design name
+    char *       pSpec;    // spec file name
+    Abc_Nam_t *  pNames;   // name manager
+    Abc_Nam_t *  pModels;  // model name manager
+    Abc_Nam_t *  pFuncs;   // functionality manager
+    Cba_Man_t *  pLib;     // library
+    // internal data
+    Mem_Flex_t * pMem;     // memory
+    Vec_Ptr_t    vNtks;    // networks
+    int          iRoot;    // root network
+};
+
+// network
+typedef struct Cba_Ntk_t_ Cba_Ntk_t;
+struct Cba_Ntk_t_
+{
+    char *       pName;    // name
+    Cba_Man_t *  pDesign;  // design
+    // interface
+    Vec_Int_t    vInouts;  // inouts          (used by parser to store signals) 
+    Vec_Int_t    vInputs;  // inputs          (used by parser to store signals)
+    Vec_Int_t    vOutputs; // outputs         (used by parser to store signals) 
+    Vec_Int_t    vWires;   // wires           (used by parser to store signals)
+    // objects
+    Vec_Int_t    vTypes;   // types           (used by parser to store Cba_PrsType_t)
+    Vec_Int_t    vFuncs;   // functions       (used by parser to store function)
+    Vec_Int_t    vInstIds; // instance names  (used by parser to store instance name as NameId)
+    Vec_Wec_t    vFanins;  // fanins          (used by parser to store fanin/fanout/range as NameId)      
+    // attributes
+    Vec_Int_t    vNameIds; // original names as NameId  
+    Vec_Int_t    vRanges;  // ranges as NameId
+    Vec_Int_t    vCopies;  // copy pointers
+};
+
+
+static inline char *        Cba_ManName( Cba_Man_t * p )                    { return p->pName;                                                                            }
+static inline int           Cba_ManNtkNum( Cba_Man_t * p )                  { return Vec_PtrSize(&p->vNtks) - 1;                                                          }
+static inline Cba_Ntk_t *   Cba_ManNtk( Cba_Man_t * p, int i )              { assert( i > 0 ); return (Cba_Ntk_t *)Vec_PtrEntry(&p->vNtks, i);                            }
+static inline Cba_Ntk_t *   Cba_ManRoot( Cba_Man_t * p )                    { return Cba_ManNtk(p, p->iRoot);                                                             }
+
+static inline char *        Cba_NtkName( Cba_Ntk_t * p )                    { return p->pName;                                                                            }
+static inline int           Cba_NtkObjNum( Cba_Ntk_t * p )                  { return Vec_WecSize(&p->vFanins);                                                            }
+static inline char *        Cba_NtkStr( Cba_Ntk_t * p, int i )              { return Abc_NamStr(p->pDesign->pNames, i);                                                   }
+static inline char *        Cba_NtkModelStr( Cba_Ntk_t * p, int i )         { return Abc_NamStr(p->pDesign->pModels, i);                                                  }
+static inline char *        Cba_NtkFuncStr( Cba_Ntk_t * p, int i )          { return Abc_NamStr(p->pDesign->pFuncs, i);                                                   }
+
+static inline Cba_ObjType_t Cba_ObjType( Cba_Ntk_t * p, int i )             { return Vec_IntEntry(&p->vTypes, i);                                                         }
+static inline int           Cba_ObjFuncId( Cba_Ntk_t * p, int i )           { return Vec_IntEntry(&p->vFuncs, i);                                                         }
+static inline int           Cba_ObjInstId( Cba_Ntk_t * p, int i )           { return Vec_IntEntry(&p->vInstIds, i);                                                       }
+static inline Vec_Int_t *   Cba_ObjFanins( Cba_Ntk_t * p, int i )           { return Vec_WecEntry(&p->vFanins, i);                                                        }
+
+static inline int           Cba_ObjNameId( Cba_Ntk_t * p, int i )           { return Vec_IntEntry(&p->vNameIds, i);                                                       }
+static inline int           Cba_ObjRangeId( Cba_Ntk_t * p, int i )          { return Vec_IntEntry(&p->vRanges, i);                                                        }
+static inline int           Cba_ObjCopyId( Cba_Ntk_t * p, int i )           { return Vec_IntEntry(&p->vCopies, i);                                                        }
+
+static inline char *        Cba_ObjFuncStr( Cba_Ntk_t * p, int i )          { return Cba_NtkStr(p, Cba_ObjFuncId(p, i));                                                  }
+static inline char *        Cba_ObjInstStr( Cba_Ntk_t * p, int i )          { return Cba_NtkStr(p, Cba_ObjInstId(p, i));                                                  }
+static inline char *        Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { return Cba_NtkStr(p, Cba_ObjNameId(p, i));                                                  }
+static inline char *        Cba_ObjRangeStr( Cba_Ntk_t * p, int i )         { return Cba_NtkStr(p, Cba_ObjRangeId(p, i));                                                 }
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+
+#define Cba_ManForEachNtk( p, pNtk, i )                     \
+    for ( i = 1; (i <= Cba_ManNtkNum(p)) && (((pNtk) = Cba_ManNtk(p, i)), 1); i++ ) 
+
+#define Cba_NtkForEachObjType( p, Type, i )      \
+    for ( i = 0; (i < Cba_NtkObjNum(p))  && (((Type) = Cba_ObjType(p, i)), 1); i++ ) 
+#define Cba_NtkForEachObjTypeFuncFanins( p, Type, Func, vFanins, i )      \
+    for ( i = 0; (i < Cba_NtkObjNum(p))  && (((Type) = Cba_ObjType(p, i)), 1)  && (((Func) = Cba_ObjFuncId(p, i)), 1)  && (((vFanins) = Cba_ObjFanins(p, i)), 1); i++ ) 
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Cba_Ntk_t * Cba_NtkAlloc( Cba_Man_t * p, char * pName )
+{
+    Cba_Ntk_t * pNtk = ABC_CALLOC( Cba_Ntk_t, 1 );
+    pNtk->pDesign = p;
+    pNtk->pName = pName;
+    Vec_PtrPush( &p->vNtks, pNtk );
+    return pNtk;
+}
+static inline void Cba_NtkFree( Cba_Ntk_t * p )
+{
+//    Vec_IntErase( &p->vInouts );
+//    Vec_IntErase( &p->vInputs );
+//    Vec_IntErase( &p->vOutputs );
+//    Vec_IntErase( &p->vWires );
+
+//    Vec_IntErase( &p->vTypes );
+//    Vec_IntErase( &p->vFuncs );
+//    Vec_IntErase( &p->vInstIds );
+    ABC_FREE( p->vFanins.pArray );
+
+    Vec_IntErase( &p->vNameIds );
+    Vec_IntErase( &p->vRanges );
+    Vec_IntErase( &p->vCopies );
+    ABC_FREE( p );
+}
+
+
+static inline Cba_Man_t * Cba_ManAlloc( char * pFileName )
+{
+    Cba_Man_t * p;
+    p = ABC_CALLOC( Cba_Man_t, 1 );
+    // design names
+    p->pName      = Extra_FileDesignName( pFileName );
+    p->pSpec      = Abc_UtilStrsav( pFileName );
+    p->pNames     = Abc_NamStart( 1000, 20 );
+    p->pModels    = Abc_NamStart( 1000, 20 );
+    p->pFuncs     = Abc_NamStart( 1000, 20 );
+    // internal data
+    p->pMem       = Mem_FlexStart();
+    Vec_PtrPush( &p->vNtks, NULL );
+    return p;
+}
+static inline void Cba_ManFree( Cba_Man_t * p )
+{
+    Cba_Ntk_t * pNtk; int i;
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_NtkFree( pNtk );
+    Mem_FlexStop( p->pMem, 0 );
+    // design names
+    Abc_NamStop( p->pNames );
+    Abc_NamStop( p->pModels );
+    Abc_NamStop( p->pFuncs );
+    ABC_FREE( p->pName );
+    ABC_FREE( p->pSpec );
+    ABC_FREE( p );
+}
+
+
+/*=== cbaReadBlif.c =========================================================*/
+extern Cba_Man_t * Cba_PrsReadBlif( char * pFileName );
+/*=== cbaWriteBlif.c ========================================================*/
+extern void        Cba_PrsWriteBlif( char * pFileName, Cba_Man_t * pDes );
+/*=== cbaReadVer.c ==========================================================*/
+extern Cba_Man_t * Cba_PrsReadVerilog( char * pFileName );
+/*=== cbaWriteVer.c =========================================================*/
+extern void        Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * pDes );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
new file mode 100644
index 00000000..f4cea24a
--- /dev/null
+++ b/src/base/cba/cbaBlast.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [cbaBlast.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaBlast.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaBuild.c b/src/base/cba/cbaBuild.c
new file mode 100644
index 00000000..ca805d50
--- /dev/null
+++ b/src/base/cba/cbaBuild.c
@@ -0,0 +1,351 @@
+/**CFile****************************************************************
+
+  FileName    [cbaBuild.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaBuild.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Int_Des_t_ Int_Des_t;
+struct Int_Des_t_
+{
+    char *           pName;   // design name
+    Abc_Nam_t *      pNames;  // name manager
+    Vec_Ptr_t        vModels; // models
+};
+typedef struct Int_Obj_t_ Int_Obj_t;
+struct Int_Obj_t_
+{
+    int              iModel;
+    int              iFunc;
+    Vec_Wrd_t        vFanins;
+};
+typedef struct Int_Ntk_t_ Int_Ntk_t;
+struct Int_Ntk_t_
+{
+    int              iName;
+    int              nObjs;
+    Int_Des_t *      pMan;
+    Vec_Ptr_t        vInstances;
+    Vec_Wrd_t        vOutputs;
+    Vec_Int_t        vInputNames;
+    Vec_Int_t        vOutputNames;
+    Vec_Int_t *      vCopies;
+    Vec_Int_t *      vCopies2;
+};
+
+static inline char *      Int_DesName( Int_Des_t * p )       { return p->pName;                                     }
+static inline int         Int_DesNtkNum( Int_Des_t * p )     { return Vec_PtrSize( &p->vModels ) - 1;               }
+static inline Int_Ntk_t * Int_DesNtk( Int_Des_t * p, int i ) { return (Int_Ntk_t *)Vec_PtrEntry( &p->vModels, i );  }
+
+static inline char *      Int_NtkName( Int_Ntk_t * p )       { return Abc_NamStr( p->pMan->pNames, p->iName );      }
+static inline int         Int_NtkPiNum( Int_Ntk_t * p )      { return Vec_IntSize( &p->vInputNames );               }
+static inline int         Int_NtkPoNum( Int_Ntk_t * p )      { return Vec_IntSize( &p->vOutputNames );              }
+
+static inline int         Int_ObjInputNum( Int_Ntk_t * p, Int_Obj_t * pObj )  { return pObj->iModel ? Int_NtkPiNum(Int_DesNtk(p->pMan, pObj->iModel)) : Vec_WrdSize(&pObj->vFanins); }
+static inline int         Int_ObjOutputNum( Int_Ntk_t * p, Int_Obj_t * pObj ) { return pObj->iModel ? Int_NtkPoNum(Int_DesNtk(p->pMan, pObj->iModel)) : 1;                           }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transform Ptr into Int.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ptr_ManCheckArray( Vec_Ptr_t * vArray )
+{
+    if ( Vec_PtrSize(vArray) == 0 )
+        return 1;
+    if ( Abc_MaxInt(8, Vec_PtrSize(vArray)) == Vec_PtrCap(vArray) )
+        return 1;
+    assert( 0 );
+    return 0;
+}
+Vec_Int_t * Ptr_ManDumpArrayToInt( Abc_Nam_t * pNames, Vec_Ptr_t * vVec, int fNode )
+{
+    char * pName; int i;
+    Vec_Int_t * vNew = Vec_IntAlloc( Vec_PtrSize(vVec) );
+    Vec_PtrForEachEntry( char *, vVec, pName, i )
+        Vec_IntPush( vNew, (fNode && i == 1) ? Abc_Ptr2Int(pName) : Abc_NamStrFind(pNames, pName) );
+    return vNew;
+}
+Vec_Ptr_t * Ptr_ManDumpArrarArrayToInt( Abc_Nam_t * pNames, Vec_Ptr_t * vNodes, int fNode )
+{
+    Vec_Ptr_t * vNode; int i;
+    Vec_Ptr_t * vNew = Vec_PtrAlloc( Vec_PtrSize(vNodes) );
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
+        Vec_PtrPush( vNew, Ptr_ManDumpArrayToInt(pNames, vNode, fNode) );
+    assert( Ptr_ManCheckArray(vNew) );
+    return vNew;
+}
+Vec_Ptr_t * Ptr_ManDumpNtkToInt( Abc_Nam_t * pNames, Vec_Ptr_t * vNtk, int i )
+{
+    Vec_Ptr_t * vNew   = Vec_PtrAlloc( 5 );
+    assert( Abc_NamStrFind(pNames, (char *)Vec_PtrEntry(vNtk, 0)) == i );
+    Vec_PtrPush( vNew, Abc_Int2Ptr(i) );
+    Vec_PtrPush( vNew, Ptr_ManDumpArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0) );
+    Vec_PtrPush( vNew, Ptr_ManDumpArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 0) );
+    Vec_PtrPush( vNew, Ptr_ManDumpArrarArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3), 1) );
+    Vec_PtrPush( vNew, Ptr_ManDumpArrarArrayToInt(pNames, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4), 0) );
+    assert( Ptr_ManCheckArray(vNew) );
+    return vNew;
+}
+Vec_Ptr_t * Ptr_ManDumpToInt( Vec_Ptr_t * vDes )
+{
+    Vec_Ptr_t * vNew = Vec_PtrAlloc( Vec_PtrSize(vDes) );
+    Vec_Ptr_t * vNtk; int i;
+    // create module names
+    Abc_Nam_t * pNames = Abc_NamStart( 1000, 20 );
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Abc_NamStrFind( pNames, (char *)Vec_PtrEntry(vNtk, 0) );
+    assert( i == Abc_NamObjNumMax(pNames) );
+    // create resulting array
+    Vec_PtrPush( vNew, pNames );
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Vec_PtrPush( vNew, Ptr_ManDumpNtkToInt(pNames, vNtk, i) );
+    assert( Ptr_ManCheckArray(vNew) );
+    return vNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transform Ptr into Int.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Int_Obj_t * Int_ObjAlloc( int nFanins )
+{
+    Int_Obj_t * p = (Int_Obj_t *)ABC_CALLOC( char, sizeof(Int_Obj_t) + sizeof(word) * nFanins );
+    p->vFanins.pArray = (word *)((char *)p + sizeof(Int_Obj_t));
+    p->vFanins.nCap = nFanins;
+    return p;
+}
+void Int_ObjFree( Int_Obj_t * p )
+{
+    ABC_FREE( p );
+}
+Int_Ntk_t * Int_NtkAlloc( Int_Des_t * pMan, int Id, int nPis, int nPos, int nInsts )
+{
+    Int_Ntk_t * p = ABC_CALLOC( Int_Ntk_t, 1 );
+    p->iName = Id;
+    p->nObjs = nPis + nInsts;
+    p->pMan  = pMan;
+    Vec_PtrGrow( &p->vInstances,   nInsts );
+    Vec_WrdGrow( &p->vOutputs,     nPos );
+    Vec_IntGrow( &p->vInputNames,  nPis );
+    Vec_IntGrow( &p->vOutputNames, nPos );
+    return p;
+}
+void Int_NtkFree( Int_Ntk_t * p )
+{
+    Int_Obj_t * pObj; int i;
+    Vec_PtrForEachEntry( Int_Obj_t *, &p->vInstances, pObj, i )
+        Int_ObjFree( pObj );
+    ABC_FREE( p->vInstances.pArray );
+    ABC_FREE( p->vOutputs.pArray );
+    ABC_FREE( p->vInputNames.pArray );
+    ABC_FREE( p->vOutputNames.pArray );
+    Vec_IntFreeP( &p->vCopies );
+    Vec_IntFreeP( &p->vCopies2 );
+    ABC_FREE( p );
+}
+Int_Des_t * Int_DesAlloc( char * pName, Abc_Nam_t * pNames, int nModels )
+{
+    Int_Des_t * p = ABC_CALLOC( Int_Des_t, 1 );
+    p->pName  = pName;
+    p->pNames = pNames;
+    Vec_PtrGrow( &p->vModels, nModels );
+    return p;
+}
+void Int_DesFree( Int_Des_t * p )
+{
+    Int_Ntk_t * pTemp; int i;
+    Vec_PtrForEachEntry( Int_Ntk_t *, &p->vModels, pTemp, i )
+        Int_NtkFree( pTemp );
+    ABC_FREE( p );
+}
+
+// replaces formal inputs by their indixes
+void Ptr_ManFindInputOutputNumbers( Int_Ntk_t * pModel, Vec_Int_t * vBox, Vec_Int_t * vMap ) 
+{
+    int i, iFormal, iName, nPis = Int_NtkPiNum(pModel);
+    Vec_IntForEachEntry( &pModel->vInputNames, iFormal, i )
+        Vec_IntWriteEntry( vMap, iFormal, i );
+    Vec_IntForEachEntry( &pModel->vOutputNames, iFormal, i )
+        Vec_IntWriteEntry( vMap, iFormal, nPis+i );
+    Vec_IntForEachEntryDouble( vBox, iFormal, iName, i )
+    {
+        if ( i == 0 ) continue;
+        assert( Vec_IntEntry(vMap, iFormal) >= 0 );
+        Vec_IntWriteEntry( vBox, i, Vec_IntEntry(vMap, iFormal) );
+    }
+    Vec_IntForEachEntry( &pModel->vInputNames, iFormal, i )
+        Vec_IntWriteEntry( vMap, iFormal, -1 );
+    Vec_IntForEachEntry( &pModel->vOutputNames, iFormal, i )
+        Vec_IntWriteEntry( vMap, iFormal, -1 );
+}
+void Ptr_ManConvertNtk( Int_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Wrd_t * vMap, Vec_Int_t * vMap2 )
+{
+    Vec_Int_t * vInputs  = (Vec_Int_t *)Vec_PtrEntry(vNtk, 1);
+    Vec_Int_t * vOutputs = (Vec_Int_t *)Vec_PtrEntry(vNtk, 2);
+    Vec_Ptr_t * vNodes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3);
+    Vec_Ptr_t * vBoxes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4);
+    Vec_Int_t * vNode, * vBox;
+    Int_Ntk_t * pModel;
+    Int_Obj_t * pObj;
+    int i, k, iFormal, iName, nPis, nOffset, nNonDriven = 0;
+
+    // map primary inputs
+    Vec_IntForEachEntry( vInputs, iName, i )
+    {
+        assert( ~Vec_WrdEntry(vMap, iName) == 0 ); // driven twice
+        Vec_WrdWriteEntry( vMap, iName, i );
+    }
+    // map internal nodes
+    nOffset = Vec_IntSize(vInputs);
+    Vec_PtrForEachEntry( Vec_Int_t *, vNodes, vNode, i )
+    {
+        iName = Vec_IntEntry(vNode, 0);
+        assert( ~Vec_WrdEntry(vMap, iName) == 0 ); // driven twice
+        Vec_WrdWriteEntry( vMap, iName, nOffset + i );
+    }
+    // map internal boxes
+    nOffset += Vec_PtrSize(vNodes);
+    Vec_PtrForEachEntry( Vec_Int_t *, vBoxes, vBox, i )
+    {
+        // get model name
+        iName = Vec_IntEntry( vBox, 0 );
+        assert( iName >= 1 && iName <= Int_DesNtkNum(pNtk->pMan) ); // bad model name
+        pModel = Int_DesNtk( pNtk->pMan, iName );
+        nPis = Int_NtkPiNum( pModel );
+        // replace inputs/outputs by their IDs
+        Ptr_ManFindInputOutputNumbers( pModel, vBox, vMap2 );
+        // go through outputs of this box
+        Vec_IntForEachEntryDouble( vBox, iFormal, iName, k )
+            if ( k > 0 && i >= nPis )  // output
+            {
+                assert( ~Vec_WrdEntry(vMap, iName) == 0 ); // driven twice
+                Vec_WrdWriteEntry( vMap, iName, (nOffset + i) | ((word)iFormal << 32) );
+            }
+    }
+
+    // save input names
+    Vec_IntForEachEntry( vInputs, iName, i )
+        Vec_IntPush( &pNtk->vInputNames, iName );
+    // create nodes with the given connectivity
+    Vec_PtrForEachEntry( Vec_Int_t *, vNodes, vNode, i )
+    {
+        pObj = Int_ObjAlloc( Vec_IntSize(vNode) - 2 );
+        pObj->iFunc = Vec_IntEntry(vNode, 1);
+        Vec_IntForEachEntryStart( vNode, iName, k, 2 )
+        {
+            Vec_WrdPush( &pObj->vFanins, Vec_WrdEntry(vMap, iName) );
+            nNonDriven += (~Vec_WrdEntry(vMap, iName) == 0);
+        }
+        Vec_PtrPush( &pNtk->vInstances, pObj );
+    }
+    // create boxes with the given connectivity
+    Vec_PtrForEachEntry( Vec_Int_t *, vBoxes, vBox, i )
+    {
+        pModel = Int_DesNtk( pNtk->pMan, Vec_IntEntry(vBox, 0) );
+        nPis = Int_NtkPiNum( pModel );
+        pObj = Int_ObjAlloc( nPis );
+        Vec_IntForEachEntryDouble( vBox, iFormal, iName, k )
+            if ( k > 0 && iFormal < nPis ) // input
+            {
+                Vec_WrdPush( &pObj->vFanins, Vec_WrdEntry(vMap, iName) );
+                nNonDriven += (~Vec_WrdEntry(vMap, iName) == 0);
+            }
+        Vec_PtrPush( &pNtk->vInstances, pObj );
+    }
+    // save output names
+    Vec_IntForEachEntry( vOutputs, iName, i )
+    {
+        Vec_IntPush( &pNtk->vOutputNames, iName );
+        Vec_WrdPush( &pNtk->vOutputs, Vec_WrdEntry(vMap, iName) );
+        nNonDriven += (~Vec_WrdEntry(vMap, iName) == 0);
+    }
+    if ( nNonDriven )
+        printf( "Model %s has %d non-driven nets.\n", Int_NtkName(pNtk), nNonDriven );
+}
+Int_Ntk_t * Ptr_ManConvertNtkInter( Int_Des_t * pDes, Vec_Ptr_t * vNtk, int Id )
+{
+    Vec_Int_t * vInputs  = (Vec_Int_t *)Vec_PtrEntry(vNtk, 1);
+    Vec_Int_t * vOutputs = (Vec_Int_t *)Vec_PtrEntry(vNtk, 2);
+    Vec_Ptr_t * vNodes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3);
+    Vec_Ptr_t * vBoxes   = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4);
+    return Int_NtkAlloc( pDes, Id, Vec_IntSize(vInputs), Vec_IntSize(vOutputs), Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) );
+}
+Int_Des_t * Ptr_ManConvert( Vec_Ptr_t * vDesPtr )
+{
+    Vec_Ptr_t * vNtk; int i;
+    char * pName = (char *)Vec_PtrEntry(vDesPtr, 0);
+    Vec_Ptr_t * vDes = Ptr_ManDumpToInt( vDesPtr );
+    Abc_Nam_t * pNames = (Abc_Nam_t *)Vec_PtrEntry(vDes, 0);
+    Vec_Wrd_t * vMap = Vec_WrdStartFull( Abc_NamObjNumMax(pNames) + 1 );
+    Vec_Int_t * vMap2 = Vec_IntStartFull( Abc_NamObjNumMax(pNames) + 1 );
+    Int_Des_t * pDes = Int_DesAlloc( pName, pNames, Vec_PtrSize(vDes)-1 );
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Vec_PtrPush( &pDes->vModels, Ptr_ManConvertNtkInter(pDes, vNtk, i) );
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Ptr_ManConvertNtk( Int_DesNtk(pDes, i), vNtk, vMap, vMap2 );
+//    Ptr_ManFreeDes( vDes );
+    Vec_IntFree( vMap2 );
+    Vec_WrdFree( vMap );
+    return pDes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
new file mode 100644
index 00000000..93c1b397
--- /dev/null
+++ b/src/base/cba/cbaCom.c
@@ -0,0 +1,356 @@
+/**CFile****************************************************************
+
+  FileName    [cbaCom.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaCom.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+#include "base/main/mainInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int  Cba_CommandRead     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandWrite    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static inline Cba_Ntk_t * Cba_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Cba_Ntk_t *)pAbc->pAbcCba;                      }
+static inline void        Cba_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Cba_NtkFree(Cba_AbcGetNtk(pAbc));  }
+static inline void        Cba_AbcUpdateNtk( Abc_Frame_t * pAbc, Cba_Ntk_t * pNtk )  { Cba_AbcFreeNtk(pAbc); pAbc->pAbcCba = pNtk;             }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cba_Init( Abc_Frame_t * pAbc )
+{
+    Cmd_CommandAdd( pAbc, "New word level", "@read",       Cba_CommandRead,      0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@write",      Cba_CommandWrite,     0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@ps",         Cba_CommandPs,        0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@blast",      Cba_CommandBlast,     0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@test",       Cba_CommandTest,      0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cba_End( Abc_Frame_t * pAbc )
+{
+    Cba_AbcFreeNtk( pAbc );
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pFile;
+    Cba_Ntk_t * pNtk = NULL;
+    char * pFileName = NULL;
+    int c, fVerbose  =    0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf( "Cba_CommandRead(): Input file name should be given on the command line.\n" );
+        return 0;
+    }
+    // get the file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
+        Abc_Print( 1, "\n" );
+        return 0;
+    }
+    fclose( pFile );
+
+    // perform reading
+    //pNtk = Cba_ReadVer( pFileName );
+    Cba_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @read [-vh] <file_name>\n" );
+    Abc_Print( -2, "\t         reads word-level design from Verilog file\n" );
+    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_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
+    char * pFileName = NULL;
+    int c, fVerbose  =    0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandWrite(): There is no current design.\n" );
+        return 0;
+    }
+    if ( argc == globalUtilOptind )
+        pFileName = Extra_FileNameGenericAppend( pNtk->pName, "_out.v" );
+    else if ( argc == globalUtilOptind + 1 )
+        pFileName = argv[globalUtilOptind];
+    else
+    {
+        printf( "Output file name should be given on the command line.\n" );
+        return 0;
+    }
+    //Cba_WriteVer( pNtk, pFileName );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @write [-vh]\n" );
+    Abc_Print( -2, "\t         writes the design into a file\n" );
+    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_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandPs(): There is no current design.\n" );
+        return 0;
+    }
+//    Cba_NtkPrintStats( pNtk, fDistrib, fVerbose );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @ps [-vh]\n" );
+    Abc_Print( -2, "\t         prints statistics\n" );
+    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_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
+    Vec_Int_t * vBoxIds = NULL;
+    Gia_Man_t * pNew = NULL;
+    int c, fMulti = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'm':
+            fMulti ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandBlast(): There is no current design.\n" );
+        return 0;
+    }
+    if ( fMulti )
+    {
+//        vBoxIds = Cba_NtkCollectMultipliers( pNtk );
+//        if ( vBoxIds == NULL )
+//            Abc_Print( 1, "Warning:  There is no multipliers in the design.\n" );
+    }
+    // transform
+//    pNew = Cba_NtkBitBlast( pNtk, vBoxIds );
+//    Vec_IntFreeP( &vBoxIds );
+    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 [-mvh]\n" );
+    Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
+    Abc_Print( -2, "\t-m     : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "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_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandTest(): There is no current design.\n" );
+        return 0;
+    }
+    // transform
+//    pNtk = Cba_NtkUifNodePairs( pNtk, NULL );
+    Cba_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @test [-vh]\n" );
+    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaLib.c b/src/base/cba/cbaLib.c
new file mode 100644
index 00000000..339aa248
--- /dev/null
+++ b/src/base/cba/cbaLib.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [cbaLib.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaLib.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
new file mode 100644
index 00000000..253c0cda
--- /dev/null
+++ b/src/base/cba/cbaNtk.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [cbaNtk.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaNtk.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
new file mode 100644
index 00000000..dad10a7a
--- /dev/null
+++ b/src/base/cba/cbaPrs.h
@@ -0,0 +1,234 @@
+/**CFile****************************************************************
+
+  FileName    [cbaPrs.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaPrs.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__prs__prs_h
+#define ABC__base__prs__prs_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START 
+
+// parser objects (object types after parsing)
+typedef enum { 
+    CBA_PRS_NONE = 0,    // 0:  unused
+    CBA_PRS_NODE,        // 1:  .names/assign/box2 (box without formal/actual binding)
+    CBA_PRS_BOX,         // 2:  .subckt/.gate/box (box with formal/actual binding)
+    CBA_PRS_LATCH,       // 3:  .latch
+    CBA_PRS_CONCAT,      // 4:  concatenation
+    CBA_PRS_UNKNOWN      // 5:  unknown
+} Cba_PrsType_t; 
+
+// node types during parsing
+typedef enum { 
+    CBA_NODE_NONE = 0,   // 0:  unused
+    CBA_NODE_CONST,      // 1:  constant
+    CBA_NODE_BUF,        // 2:  buffer
+    CBA_NODE_INV,        // 3:  inverter
+    CBA_NODE_AND,        // 4:  AND
+    CBA_NODE_OR,         // 5:  OR
+    CBA_NODE_XOR,        // 6:  XOR
+    CBA_NODE_NAND,       // 7:  NAND
+    CBA_NODE_NOR,        // 8:  NOR
+    CBA_NODE_XNOR,       // 9  .XNOR
+    CBA_NODE_MUX,        // 10: MUX
+    CBA_NODE_MAJ,        // 11: MAJ
+    CBA_NODE_UNKNOWN     // 12: unknown
+} Cba_NodeType_t; 
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// parser
+typedef struct Cba_Prs_t_ Cba_Prs_t;
+struct Cba_Prs_t_
+{
+    // input data
+    char *       pName;       // file name
+    char *       pBuffer;     // file contents
+    char *       pLimit;      // end of file
+    char *       pCur;        // current position
+    // construction
+    Cba_Man_t *  pLibrary;
+    Cba_Man_t *  pDesign; 
+    // interface collected by the parser
+    int          iModuleName; // name Id
+    Vec_Int_t *  vInoutsCur;  // inouts
+    Vec_Int_t *  vInputsCur;  // inputs 
+    Vec_Int_t *  vOutputsCur; // outputs
+    Vec_Int_t *  vWiresCur;   // wires
+    // objects collected by the parser
+    Vec_Int_t *  vTypesCur;   // Cba_PrsType_t
+    Vec_Int_t *  vFuncsCur;   // functions (node->func; box->module; gate->cell; latch->init; concat->unused)
+    Vec_Int_t *  vInstIdsCur; // instance names
+    Vec_Wec_t *  vFaninsCur;  // instances
+    // temporary data
+    Vec_Str_t *  vCover;      // one SOP cover
+    Vec_Int_t *  vTemp;       // array of tokens
+    Vec_Int_t *  vTemp2;      // array of tokens
+    // error handling
+    char ErrorStr[1000];      // error
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// create error message
+static inline int Cba_PrsErrorSet( Cba_Prs_t * p, char * pError, int Value )
+{
+    assert( !p->ErrorStr[0] );
+    sprintf( p->ErrorStr, pError );
+    return Value;
+}
+// print error message
+static inline int Cba_PrsErrorPrint( Cba_Prs_t * p )
+{
+    char * pThis; int iLine = 0;
+    if ( !p->ErrorStr[0] ) return 1;
+    for ( pThis = p->pBuffer; pThis < p->pCur; pThis++ )
+        iLine += (int)(*pThis == '\n');
+    printf( "Line %d: %s\n", iLine, p->ErrorStr );
+    return 0;
+}
+
+
+// copy contents to the vector
+static inline void Cba_PrsSetupVecInt( Cba_Prs_t * p, Vec_Int_t * vTo, Vec_Int_t * vFrom )
+{
+    if ( Vec_IntSize(vFrom) == 0 )
+        return;
+    vTo->nSize = vTo->nCap = Vec_IntSize(vFrom);
+    vTo->pArray = (int *)Mem_FlexEntryFetch( p->pDesign->pMem, sizeof(int) * Vec_IntSize(vFrom) );
+    memcpy( Vec_IntArray(vTo), Vec_IntArray(vFrom), sizeof(int) * Vec_IntSize(vFrom) );
+    Vec_IntClear( vFrom );
+}
+static inline Cba_Ntk_t * Cba_PrsAddCurrentModel( Cba_Prs_t * p, int iNameId )
+{
+    Cba_Ntk_t * pNtk = Cba_NtkAlloc( p->pDesign, Abc_NamStr(p->pDesign->pNames, iNameId) );
+    assert( Vec_IntSize(p->vInputsCur) != 0 && Vec_IntSize(p->vOutputsCur) != 0 );
+    Cba_PrsSetupVecInt( p, &pNtk->vInouts,  p->vInoutsCur  );
+    Cba_PrsSetupVecInt( p, &pNtk->vInputs,  p->vInputsCur  );
+    Cba_PrsSetupVecInt( p, &pNtk->vOutputs, p->vOutputsCur );
+    Cba_PrsSetupVecInt( p, &pNtk->vWires,   p->vWiresCur   );
+    Cba_PrsSetupVecInt( p, &pNtk->vTypes,   p->vTypesCur   );
+    Cba_PrsSetupVecInt( p, &pNtk->vFuncs,   p->vFuncsCur   );
+    Cba_PrsSetupVecInt( p, &pNtk->vInstIds, p->vInstIdsCur );
+    pNtk->vFanins = *p->vFaninsCur;
+    Vec_WecZero( &pNtk->vFanins );
+    return pNtk;
+}
+
+
+
+static inline char * Cba_PrsLoadFile( char * pFileName, char ** ppLimit )
+{
+    char * pBuffer;
+    int nFileSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open input file.\n" );
+        return NULL;
+    }
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
+    pBuffer[0] = '\n';
+    RetValue = fread( pBuffer+1, nFileSize, 1, pFile );
+    // terminate the string with '\0'
+    pBuffer[nFileSize + 0] = '\n';
+    pBuffer[nFileSize + 1] = '\0';
+    *ppLimit = pBuffer + nFileSize + 2;
+    return pBuffer;
+}
+static inline Cba_Prs_t * Cba_PrsAlloc( char * pFileName )
+{
+    Cba_Prs_t * p;
+    char * pBuffer, * pLimit;
+    pBuffer = Cba_PrsLoadFile( pFileName, &pLimit );
+    if ( pBuffer == NULL )
+        return NULL;
+    p = ABC_CALLOC( Cba_Prs_t, 1 );
+    p->pName   = pFileName;
+    p->pBuffer = pBuffer;
+    p->pLimit  = pLimit;
+    p->pCur    = pBuffer;
+    p->pDesign = Cba_ManAlloc( pFileName );
+    // temporaries
+    p->vCover = Vec_StrAlloc( 1000 );
+    p->vTemp  = Vec_IntAlloc( 1000 );
+    p->vTemp2 = Vec_IntAlloc( 1000 );
+    return p;
+}
+static inline void Cba_PrsFree( Cba_Prs_t * p )
+{
+    if ( p->pDesign )
+        Cba_ManFree( p->pDesign );
+    Vec_IntFreeP( &p->vInoutsCur );
+    Vec_IntFreeP( &p->vInputsCur );
+    Vec_IntFreeP( &p->vOutputsCur );
+    Vec_IntFreeP( &p->vWiresCur );
+
+    Vec_IntFreeP( &p->vTypesCur );
+    Vec_IntFreeP( &p->vFuncsCur );
+    Vec_IntFreeP( &p->vInstIdsCur );
+    Vec_WecFreeP( &p->vFaninsCur );
+    // temporary
+    Vec_StrFreeP( &p->vCover );
+    Vec_IntFreeP( &p->vTemp );
+    Vec_IntFreeP( &p->vTemp2 );
+    ABC_FREE( p->pBuffer );
+    ABC_FREE( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cba.c ========================================================*/
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c
new file mode 100644
index 00000000..c324b37f
--- /dev/null
+++ b/src/base/cba/cbaReadBlif.c
@@ -0,0 +1,330 @@
+/**CFile****************************************************************
+
+  FileName    [cbaReadBlif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaReadBlif.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+#include "cbaPrs.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// BLIF keywords
+typedef enum { 
+    CBA_BLIF_NONE = 0, // 0:  unused
+    CBA_BLIF_MODEL,    // 1:  .model
+    CBA_BLIF_INPUTS,   // 2:  .inputs
+    CBA_BLIF_OUTPUTS,  // 3:  .outputs
+    CBA_BLIF_NAMES,    // 4:  .names
+    CBA_BLIF_SUBCKT,   // 5:  .subckt
+    CBA_BLIF_GATE,     // 6:  .gate
+    CBA_BLIF_LATCH,    // 7:  .latch
+    CBA_BLIF_END,      // 8:  .end
+    CBA_BLIF_UNKNOWN   // 9:  unknown
+} Cba_BlifType_t;
+
+const char * s_BlifTypes[CBA_BLIF_UNKNOWN+1] = {
+    NULL,              // 0:  unused
+    ".model",          // 1:  .model   
+    ".inputs",         // 2:  .inputs
+    ".outputs",        // 3:  .outputs
+    ".names",          // 4:  .names
+    ".subckt",         // 5:  .subckt
+    ".gate",           // 6:  .gate
+    ".latch",          // 7:  .latch
+    ".end",            // 8:  .end
+    NULL               // 9:  unknown
+};
+
+static inline void Cba_PrsAddBlifDirectives( Cba_Prs_t * p )
+{
+    int i;
+    for ( i = 1; s_BlifTypes[i]; i++ )
+        Abc_NamStrFindOrAdd( p->pDesign->pNames, (char *)s_BlifTypes[i],   NULL );
+    assert( Abc_NamObjNumMax(p->pDesign->pNames) == i );
+}
+
+static inline int  Cba_PrsIsSpace( char c )                    { return c == ' ' || c == '\t' || c == '\r';                     }
+static inline int  Cba_PrsIsOk( Cba_Prs_t * p )                { return (int)(p->pCur < p->pLimit);                             }
+static inline int  Cba_PrsIsChar( Cba_Prs_t * p, char c )      { return *p->pCur == 'c';                                        }
+static inline int  Cba_PrsIsLit( Cba_Prs_t * p )               { return *p->pCur == '0' || *p->pCur == '1' || *p->pCur == '-';  }
+static inline void Cba_PrsSkipToChar( Cba_Prs_t * p, char c )  { while ( *p->pCur != c ) p->pCur++;                             }
+static inline char Cba_PrsSkip( Cba_Prs_t * p )                { return *p->pCur++;                                             }
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reading names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cba_PrsSkipSpaces( Cba_Prs_t * p )
+{
+    while ( Cba_PrsIsSpace(*p->pCur) )
+        Cba_PrsSkip(p);
+    if ( Cba_PrsIsChar(p, '#') )  
+        Cba_PrsSkipToChar( p, '\n' );
+    else if ( Cba_PrsIsChar(p, '\\') )
+    {
+        Cba_PrsSkipToChar( p, '\n' );
+        Cba_PrsSkip(p);
+        Cba_PrsSkipSpaces( p );
+    }   
+}
+static inline int Cba_PrsReadName( Cba_Prs_t * p )
+{
+    char * pStart = p->pCur;
+    while ( !Cba_PrsIsSpace(*p->pCur) && !Cba_PrsIsChar(p, '\\') )
+        Cba_PrsSkip(p);
+    if ( pStart == p->pCur )
+        return 0;
+    return Abc_NamStrFindOrAddLim( p->pDesign->pNames, pStart, p->pCur, NULL );
+}
+static inline int Cba_PrsReadName2( Cba_Prs_t * p )
+{
+    char * pStart = p->pCur;
+    while ( !Cba_PrsIsSpace(*p->pCur) && !Cba_PrsIsChar(p, '\\') && !Cba_PrsIsChar(p, '=') )
+        Cba_PrsSkip(p);
+    if ( pStart == p->pCur )
+        return 0;
+    return Abc_NamStrFindOrAddLim( p->pDesign->pNames, pStart, p->pCur, NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cba_PrsReadCube( Cba_Prs_t * p )
+{
+    while ( Cba_PrsIsLit(p) )
+        Vec_StrPush( p->vCover, Cba_PrsSkip(p) );
+    Cba_PrsSkipSpaces( p );
+    Vec_StrPush( p->vCover, ' ' );
+    if ( !Cba_PrsIsLit(p) )                           return Cba_PrsErrorSet(p, "Cannot detect output literal.", 1);
+    Vec_StrPush( p->vCover, Cba_PrsSkip(p) );
+    return 1;
+}
+static inline void Cba_PrsSaveCover( Cba_Prs_t * p )
+{
+    int iToken;
+    assert( Vec_StrSize(p->vCover) > 0 );
+    Vec_StrPush( p->vCover, '\0' );
+    iToken = Abc_NamStrFindOrAdd( p->pDesign->pFuncs, Vec_StrArray(p->vCover), NULL );
+    Vec_StrClear( p->vCover );
+    assert( Vec_IntEntryLast(p->vFuncsCur) == 1 );
+    Vec_IntWriteEntry( p->vFuncsCur, Vec_IntSize(p->vFuncsCur)-1, iToken );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cba_PrsReadSignals( Cba_Prs_t * p, int fSkipFirst )
+{
+    Cba_PrsSkipSpaces( p );
+    Vec_IntFill( p->vTemp, fSkipFirst, -1 );
+    while ( !Cba_PrsIsChar(p, '\n') )
+    {
+        Vec_IntPush( p->vTemp, Cba_PrsReadName(p) );
+        Cba_PrsSkipSpaces( p );
+    }
+    if ( Vec_IntSize(p->vTemp) == 0 )  return Cba_PrsErrorSet(p, "List of signals is empty.", 1);
+    if ( Vec_IntCountZero(p->vTemp) )  return Cba_PrsErrorSet(p, "Cannot read names in the list.", 1); 
+    return 0;
+}
+static inline int Cba_PrsReadInputs( Cba_Prs_t * p )
+{
+    if ( Cba_PrsReadSignals(p, 0) )    return 1;
+    Vec_IntAppend( p->vInputsCur, p->vTemp );
+    return 0;
+}
+static inline int Cba_PrsReadOutputs( Cba_Prs_t * p )
+{
+    if ( Cba_PrsReadSignals(p, 0) )    return 1;
+    Vec_IntAppend( p->vOutputsCur, p->vTemp );
+    return 0;
+}
+static inline int Cba_PrsReadNode( Cba_Prs_t * p )
+{
+    if ( Cba_PrsReadSignals(p, 1) )    return 1;
+    Vec_IntWriteEntry( p->vTemp, 0, Vec_IntPop(p->vTemp) );
+    // save results
+    Vec_IntPush( p->vFuncsCur, 1 );
+    Vec_IntPush( p->vTypesCur, CBA_PRS_NODE );
+    Cba_PrsSetupVecInt( p, Vec_WecPushLevel(p->vFaninsCur), p->vTemp );
+    return 0;
+}
+static inline int Cba_PrsReadBox( Cba_Prs_t * p, int fGate )
+{
+    Cba_PrsSkipSpaces( p );
+    if ( Cba_PrsIsChar(p, '\n') )      return Cba_PrsErrorSet(p, "Cannot read model name.", 1);
+    Vec_IntPush( p->vFuncsCur, Cba_PrsReadName(p) );
+    Cba_PrsSkipSpaces( p );
+    if ( Cba_PrsIsChar(p, '\n') )      return Cba_PrsErrorSet(p, "Cannot read formal/actual inputs.", 1);
+    while ( !Cba_PrsIsChar(p, '\n') )
+    {
+        Vec_IntPush( p->vTemp, Cba_PrsReadName(p) );
+        Cba_PrsSkipSpaces( p );
+        if ( !Cba_PrsIsChar(p, '=') )  return Cba_PrsErrorSet(p, "Cannot find symbol \'=\'.", 1);
+        p->pCur++;
+        Cba_PrsSkipSpaces( p );
+        Vec_IntPush( p->vTemp, Cba_PrsReadName(p) );
+        Cba_PrsSkipSpaces( p );
+    }
+    // save results
+    Vec_IntPush( p->vTypesCur, CBA_PRS_BOX );
+    Cba_PrsSetupVecInt( p, Vec_WecPushLevel(p->vFaninsCur), p->vTemp );
+    return 0;
+}
+static inline int Cba_PrsReadLatch( Cba_Prs_t * p )
+{
+    Vec_IntFill( p->vTemp, 2, -1 );
+    Cba_PrsSkipSpaces( p );
+    if ( Cba_PrsIsChar(p, '\n') )      return Cba_PrsErrorSet(p, "Cannot read latch input.", 1);
+    Vec_IntWriteEntry( p->vTemp, 1, Cba_PrsReadName(p) );
+    Cba_PrsSkipSpaces( p );
+    if ( Cba_PrsIsChar(p, '\n') )      return Cba_PrsErrorSet(p, "Cannot read latch output.", 1);
+    Vec_IntWriteEntry( p->vTemp, 0, Cba_PrsReadName(p) );
+    if ( Cba_PrsIsChar(p, '0') )
+        Vec_IntPush( p->vFuncsCur, 0 );
+    else if ( Cba_PrsIsChar(p, '1') )
+        Vec_IntPush( p->vFuncsCur, 1 );
+    else if ( Cba_PrsIsChar(p, '2') || Cba_PrsIsChar(p, '\n') )
+        Vec_IntPush( p->vFuncsCur, 2 );
+    else                               return Cba_PrsErrorSet(p, "Cannot read latch init value.", 1);
+    // save results
+    Vec_IntPush( p->vTypesCur, CBA_PRS_LATCH );
+    Cba_PrsSetupVecInt( p, Vec_WecPushLevel(p->vFaninsCur), p->vTemp );
+    return 0;
+}
+static inline int Cba_PrsReadModel( Cba_Prs_t * p )
+{
+    Cba_PrsSkipSpaces( p );
+    if ( Vec_IntSize(p->vInputsCur) > 0 )           return Cba_PrsErrorSet(p, "Parsing previous model is unfinished.", 1);
+    p->iModuleName = Cba_PrsReadName( p );
+    if ( p->iModuleName == 0 )                      return Cba_PrsErrorSet(p, "Cannot read model name.", 1);
+    Cba_PrsSkipSpaces( p );
+    if ( !Cba_PrsIsChar(p, '\n') )                  return Cba_PrsErrorSet(p, "Trailing symbols on .model line.", 1);
+    return 0;
+}
+static inline int Cba_PrsReadEnd( Cba_Prs_t * p )
+{
+    if ( Vec_IntSize(p->vInputsCur) == 0 )          return Cba_PrsErrorSet(p, "Directive .end without .model.", 1);
+    Cba_PrsAddCurrentModel( p, p->iModuleName );
+    return 0;
+}
+
+static inline int Cba_PrsReadDirective( Cba_Prs_t * p )
+{
+    int iToken;
+    if ( !Cba_PrsIsChar(p, '.') )
+        return Cba_PrsReadCube( p );
+    if ( Vec_StrSize(p->vCover) > 0 ) // SOP was specified for the previous node
+        Cba_PrsSaveCover( p );
+    iToken = Cba_PrsReadName( p );  
+    if ( iToken == CBA_BLIF_MODEL )
+        return Cba_PrsReadModel( p );
+    if ( iToken == CBA_BLIF_INPUTS )
+        return Cba_PrsReadInputs( p );
+    if ( iToken == CBA_BLIF_OUTPUTS )
+        return Cba_PrsReadOutputs( p );
+    if ( iToken == CBA_BLIF_NAMES )
+        return Cba_PrsReadNode( p );
+    if ( iToken == CBA_BLIF_SUBCKT )
+        return Cba_PrsReadBox( p, 0 );
+    if ( iToken == CBA_BLIF_GATE )
+        return Cba_PrsReadBox( p, 1 );
+    if ( iToken == CBA_BLIF_LATCH )
+        return Cba_PrsReadLatch( p );
+    if ( iToken == CBA_BLIF_END )
+        return Cba_PrsReadEnd( p );
+    assert( 0 );
+    return 1;
+}
+static inline int Cba_PrsReadLines( Cba_Prs_t * p )
+{
+    while ( Cba_PrsIsChar(p, '\n') )
+    {
+        p->pCur++; Cba_PrsSkipSpaces( p );
+        if ( Cba_PrsIsChar(p, '\n') )    
+            continue;
+        if ( Cba_PrsReadDirective( p ) )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cba_Man_t * Cba_PrsReadBlif( char * pFileName )
+{
+    Cba_Man_t * pDesign = NULL;
+    Cba_Prs_t * p = Cba_PrsAlloc( pFileName );
+    if ( p == NULL )
+        return NULL;
+    Cba_PrsAddBlifDirectives( p );
+    Cba_PrsReadLines( p );
+    if ( Cba_PrsErrorPrint(p) )
+        ABC_SWAP( Cba_Man_t *, pDesign, p->pDesign );
+    Cba_PrsFree( p );
+    return pDesign;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
new file mode 100644
index 00000000..2000289c
--- /dev/null
+++ b/src/base/cba/cbaReadVer.c
@@ -0,0 +1,528 @@
+/**CFile****************************************************************
+
+  FileName    [cbaReadVer.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaReadVer.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+#include "cbaPrs.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// Verilog keywords
+typedef enum { 
+    CBA_VER_NONE = 0,  // 0:  unused
+    CBA_VER_MODULE,    // 1:  module
+    CBA_VER_INOUT,     // 2:  inout
+    CBA_VER_INPUT,     // 3:  input
+    CBA_VER_OUTPUT,    // 4:  output
+    CBA_VER_WIRE,      // 5:  wire
+    CBA_VER_ASSIGN,    // 6:  assign
+    CBA_VER_REG,       // 7:  reg
+    CBA_VER_ALWAYS,    // 8:  always
+    CBA_VER_DEFPARAM,  // 9:  always
+    CBA_VER_BEGIN,     // 10: begin
+    CBA_VER_END,       // 11: end
+    CBA_VER_ENDMODULE, // 12: endmodule
+    CBA_VER_UNKNOWN    // 13: unknown
+} Cba_VerType_t;
+
+const char * s_VerTypes[CBA_VER_UNKNOWN+1] = {
+    NULL,              // 0:  unused
+    "module",          // 1:  module
+    "inout",           // 2:  inout
+    "input",           // 3:  input
+    "output",          // 4:  output
+    "wire",            // 5:  wire
+    "assign",          // 6:  assign
+    "reg",             // 7:  reg
+    "always",          // 8:  always
+    "defparam",        // 9:  defparam
+    "begin",           // 10: begin
+    "end",             // 11: end
+    "endmodule",       // 12: endmodule
+    NULL               // 13: unknown 
+};
+
+static inline void Cba_PrsAddVerilogDirectives( Cba_Prs_t * p )
+{
+    int i;
+    for ( i = 1; s_VerTypes[i]; i++ )
+        Abc_NamStrFindOrAdd( p->pDesign->pNames, (char *)s_VerTypes[i],   NULL );
+    assert( Abc_NamObjNumMax(p->pDesign->pNames) == i );
+}
+
+
+// character recognition 
+static inline int Cba_IsSpace( char c )   { return (c == ' ' || c == '\n' || c == '\t' || c == '\r');                           }
+static inline int Cba_IsDigit( char c )   { return (c >= '0' && c <= '9');                                                      }
+static inline int Cba_IsDigitB( char c )  { return (c >= '0' && c <= '1');                                                      }
+static inline int Cba_IsDigitH( char c )  { return (c >= '0' && c <= '9') || (c >= 'A' && c <= 'F') || (c >= 'a' && c <= 'f');  }
+static inline int Cba_IsChar( char c )    { return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z');                            }
+static inline int Cba_IsSymb1( char c )   { return Cba_IsChar(c) || c == '_';                                                   }
+static inline int Cba_IsSymb2( char c )   { return Cba_IsSymb1(c) || Cba_IsDigit(c) || c == '$';                                }
+static inline int Cba_IsSymb( char c )    { return c >= 33 && c <= 126;                                                         }
+static inline int Cba_IsSymbC( char c )   { return Cba_IsDigit(c) || c == '\'' || c == 'b' || c == 'h' || c == 'd';             }
+
+
+static inline int Cba_PrsOk( Cba_Prs_t * p )                { return p->pCur < p->pLimit && !p->ErrorStr[0]; }
+static inline int Cba_PrsIsChar( Cba_Prs_t * p, char c )    { return *p->pCur == c;                          }
+static inline int Cba_PrsIsDigit( Cba_Prs_t * p )           { return Cba_IsDigit(*p->pCur);                  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+// collect predefined models names
+const char * s_KnownModels[100] = {
+    NULL,
+    "VERIFIC_",
+    "reduce_",
+    "add_",
+    "mult_",
+    "Select_",
+    "LessThan_",
+    "Decoder_",
+    "Mux_",
+    "ReadPort_",
+    "WritePort_",
+    "ClockedWritePort_",
+    NULL
+};
+
+// check if it is a known module
+static inline int Cba_PrsIsKnownModule( Cba_Prs_t * p, char * pName )
+{
+    int i;
+    for ( i = 1; s_KnownModels[i]; i++ )
+        if ( !strncmp(pName, s_KnownModels[i], strlen(s_KnownModels[i])) )
+            return 1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+// skip any number of spaces and comments
+static inline int Cba_PrsUtilSkipSpaces( Cba_Prs_t * p )
+{
+    while ( *p->pCur )
+    {
+        while ( Cba_IsSpace(*p->pCur) ) 
+            p->pCur++;
+        if ( p->pCur[0] == '/' && p->pCur[1] == '/' )
+        {
+            for ( p->pCur += 2; *p->pCur; p->pCur++ )
+                if ( p->pCur[0] == '\n' )
+                    { p->pCur++; break; }
+        }
+        else if ( p->pCur[0] == '/' && p->pCur[1] == '*' )
+        {
+            for ( p->pCur += 2; *p->pCur; p->pCur++ )
+                if ( p->pCur[0] == '*'  && p->pCur[1] == '/' )
+                    { p->pCur++; p->pCur++; break; }
+        }
+        else return 1;
+    }
+    return 0;
+}
+// skip everything including comments until the given char
+static inline int Cba_PrsUtilSkipUntilChar( Cba_Prs_t * p, char c )
+{
+    while ( *p->pCur )
+    {
+        if ( *p->pCur == c )
+            return 1;
+        if ( p->pCur[0] == '/' && p->pCur[1] == '/' ) // comment
+        {
+            for ( p->pCur += 2; *p->pCur; p->pCur++ )
+                if ( p->pCur[0] == '\n' )
+                    break;
+        }
+        else if ( p->pCur[0] == '/' && p->pCur[1] == '*' ) // comment
+        {
+            for ( p->pCur += 2; *p->pCur; p->pCur++ )
+                if ( p->pCur[0] == '*'  && p->pCur[1] == '/' )
+                    { p->pCur++; break; }
+        }
+        else if ( p->pCur[0] == '\\' ) // name
+        {
+            for ( p->pCur++; *p->pCur; p->pCur++ )
+                if ( p->pCur[0] == ' ' )
+                    break;
+        }
+        if ( *p->pCur == 0 )
+            return 0;
+        p->pCur++;
+    }
+    return 0;
+}
+// skip everything including comments until the given word
+static inline int Cba_PrsUtilSkipUntilWord( Cba_Prs_t * p, char * pWord )
+{
+    char * pPlace = strstr( p->pCur, pWord );
+    if ( pPlace == NULL )
+        return 0;
+    p->pCur = pPlace;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+static inline int Cba_PrsReadName( Cba_Prs_t * p )
+{
+    char * pStart = p->pCur;
+    if ( *p->pCur == '\\' ) // escaped name
+    {
+        pStart = ++p->pCur;
+        while ( !Cba_IsSpace(*p->pCur) ) 
+            p->pCur++;
+    }
+    else if ( Cba_IsDigit(*p->pCur) ) // constant
+    {
+        while ( Cba_IsDigit(*p->pCur) ) 
+            p->pCur++;
+        if ( *p->pCur != '\'' )
+            return Cba_PrsErrorSet(p, "Cannot read constant.", 0);
+        p->pCur++;
+        if ( *p->pCur == 'b' )
+            while ( Cba_IsDigitB(*p->pCur) ) 
+                p->pCur++;
+        else if ( *p->pCur == 'd' )
+            while ( Cba_IsDigit(*p->pCur) ) 
+                p->pCur++;
+        else if ( *p->pCur == 'h' )
+            while ( Cba_IsDigitH(*p->pCur) ) 
+                p->pCur++;
+        else
+            return Cba_PrsErrorSet(p, "Cannot read radix of constant.", 0);
+    }
+    else // simple name
+    {
+        if ( !Cba_IsSymb1(*p->pCur) )
+            return Cba_PrsErrorSet(p, "Cannot read first character of a name.", 0);
+        while ( Cba_IsSymb2(*p->pCur) ) 
+            p->pCur++;
+    }
+    if ( pStart == p->pCur )
+        return Cba_PrsErrorSet(p, "Cannot read name.", 0);
+    return Abc_NamStrFindOrAddLim( p->pDesign->pNames, pStart, p->pCur, NULL );
+}
+
+static inline int Cba_PrsReadRange( Cba_Prs_t * p )
+{
+    if ( !Cba_PrsIsChar(p, '[') )
+        return 0;
+    Vec_StrClear( p->vCover );
+    Vec_StrPush( p->vCover, *p->pCur++ );
+    Cba_PrsUtilSkipSpaces( p );
+    if ( !Cba_PrsIsDigit(p) )     return Cba_PrsErrorSet(p, "Cannot read digit in range specification.", 2);
+    while ( Cba_PrsIsDigit(p) )
+        Vec_StrPush( p->vCover, *p->pCur++ );
+    Cba_PrsUtilSkipSpaces( p );
+    if ( Cba_PrsIsChar(p, ':') )
+    {
+        Vec_StrPush( p->vCover, *p->pCur++ );
+        if ( !Cba_PrsIsDigit(p) ) return Cba_PrsErrorSet(p, "Cannot read digit in range specification.", 2);
+        while ( Cba_PrsIsDigit(p) )
+            Vec_StrPush( p->vCover, *p->pCur++ );
+        Cba_PrsUtilSkipSpaces( p );
+    }
+    if ( !Cba_PrsIsChar(p, ']') ) return Cba_PrsErrorSet(p, "Cannot read closing brace in range specification.", 2);
+    Vec_StrPush( p->vCover, *p->pCur++ );
+    return Abc_NamStrFindOrAddLim( p->pDesign->pNames, Vec_StrArray(p->vCover), Vec_StrArray(p->vCover)+Vec_StrSize(p->vCover), NULL );
+}
+static inline void Cba_PrsReadSignalList( Cba_Prs_t * p, Vec_Int_t * vTemp )
+{
+    int NameId, RangeId;
+    Vec_IntClear( vTemp );
+    while ( 1 )
+    {
+        Cba_PrsUtilSkipSpaces( p );
+        NameId  = Cba_PrsReadName( p );
+        Cba_PrsUtilSkipSpaces( p );
+        RangeId = Cba_PrsReadRange( p );
+        Vec_IntPushTwo( vTemp, NameId, RangeId );
+        Cba_PrsUtilSkipSpaces( p );
+        if ( !Cba_PrsIsChar(p, ',') )
+            break;
+        p->pCur++;
+    }
+}
+static inline int Cba_PrsReadDeclaration( Cba_Prs_t * p, int Type )
+{
+    int NameId, RangeId, RangeIdTemp;
+    Vec_Int_t * vSigs[4] = { p->vInoutsCur, p->vInputsCur, p->vOutputsCur, p->vWiresCur };
+    assert( Type >= CBA_VER_INOUT && Type <= CBA_VER_WIRE );
+    Cba_PrsUtilSkipSpaces( p );
+    RangeId = Cba_PrsReadRange( p );
+    Cba_PrsReadSignalList( p, p->vTemp );
+    Vec_IntForEachEntryDouble( p->vTemp, NameId, RangeId, RangeIdTemp )
+    {
+        if ( !RangeIdTemp )      return Cba_PrsErrorSet(p, "Range is specified twice in the declaration.", 0);
+        Vec_IntPushTwo( vSigs[Type - CBA_VER_INOUT], NameId, RangeId );
+    }
+    return 1;
+}
+static inline int Cba_PrsReadConcat( Cba_Prs_t * p )
+{
+    int iToken = Vec_WecSize( p->vFaninsCur );
+    assert( Cba_PrsIsChar(p, '{') );
+    p->pCur++;
+    Cba_PrsReadSignalList( p, p->vTemp2 );
+    if ( !Cba_PrsIsChar(p, '}') )  return Cba_PrsErrorSet(p, "Cannot read concatenation.", 0);
+    p->pCur++;
+    // assign
+    Vec_IntPush( p->vTypesCur, CBA_PRS_CONCAT );
+    Vec_IntPush( p->vFuncsCur, 0 );
+    Vec_IntPush( p->vInstIdsCur, 0 );
+    Cba_PrsSetupVecInt( p, Vec_WecPushLevel(p->vFaninsCur), p->vTemp2 );
+    return iToken;
+}
+
+static inline int Cba_PrsReadInstance( Cba_Prs_t * p, int Func )
+{
+    // have to assign Type, Func, InstId, vFanins
+    int FormId, NameId, RangeId, Type, InstId;
+    Vec_IntClear( p->vTemp );
+    Cba_PrsUtilSkipSpaces( p );
+    if ( Cba_PrsIsChar(p, '(') ) // node
+    {
+        Type = CBA_PRS_NODE;
+        InstId = 0;
+        p->pCur++;
+        while ( 1 )
+        {
+            Cba_PrsUtilSkipSpaces( p );
+            if ( Cba_PrsIsChar(p, '{') )
+            {
+                NameId = 0;
+                RangeId = Cba_PrsReadConcat( p );
+            }
+            else
+            {
+                NameId  = Cba_PrsReadName( p );
+                RangeId = Cba_PrsReadRange( p );
+            }
+            Vec_IntPushTwo( p->vTemp, NameId, RangeId );
+            Cba_PrsUtilSkipSpaces( p );
+            if ( Cba_PrsIsChar(p, ')') )
+                break;
+            if ( !Cba_PrsIsChar(p, ',') ) return Cba_PrsErrorSet(p, "Expecting comma in the instance definition.", 2);
+            p->pCur++;
+        }
+    }
+    else // box
+    {
+        Type = CBA_PRS_BOX;
+        InstId = Cba_PrsReadName( p );
+        Cba_PrsUtilSkipSpaces( p );
+        if ( !Cba_PrsIsChar(p, '(') ) return Cba_PrsErrorSet(p, "Expecting opening paranthesis in the instance definition.", 2);
+        p->pCur++;
+        while ( 1 )
+        {
+            Cba_PrsUtilSkipSpaces( p );
+            if ( !Cba_PrsIsChar(p, '.') ) return Cba_PrsErrorSet(p, "Expecting dot before the formal name.", 2);
+            p->pCur++;
+            FormId = Cba_PrsReadName( p );
+            Cba_PrsUtilSkipSpaces( p );
+            if ( !Cba_PrsIsChar(p, '(') ) return Cba_PrsErrorSet(p, "Expecting opening paranthesis after the formal name.", 2);
+            p->pCur++;
+            Cba_PrsUtilSkipSpaces( p );
+            if ( Cba_PrsIsChar(p, '{') )
+            {
+                NameId = 0;
+                RangeId = Cba_PrsReadConcat( p );
+            }
+            else
+            {
+                NameId  = Cba_PrsReadName( p );
+                RangeId = Cba_PrsReadRange( p );
+            }
+            Vec_IntPushTwo( p->vTemp, NameId, RangeId );
+            Cba_PrsUtilSkipSpaces( p );
+            if ( !Cba_PrsIsChar(p, ')') ) return Cba_PrsErrorSet(p, "Expecting opening paranthesis after the acctual name.", 2);
+            p->pCur++;
+            Cba_PrsUtilSkipSpaces( p );
+            if ( Cba_PrsIsChar(p, ')') )
+                break;
+            if ( !Cba_PrsIsChar(p, ',') ) return Cba_PrsErrorSet(p, "Expecting comma in the instance definition.", 2);
+            p->pCur++;
+        }
+    }
+    // assign
+    Vec_IntPush( p->vTypesCur, Type );
+    Vec_IntPush( p->vFuncsCur, Func );
+    Vec_IntPush( p->vInstIdsCur, InstId );
+    Cba_PrsSetupVecInt( p, Vec_WecPushLevel(p->vFaninsCur), p->vTemp );
+    return 0;
+}
+
+// this procedure can return:
+// 0 = reached end-of-file; 1 = successfully parsed; 2 = failed and skipped; 3 = error (failed and could not skip)
+static inline int Cba_PrsReadModule( Cba_Prs_t * p )
+{
+    int fKnown, iToken, iNameId;
+    assert( Vec_IntSize(p->vInputsCur) == 0 && Vec_IntSize(p->vOutputsCur) == 0 );
+    Cba_PrsUtilSkipSpaces( p );
+    if ( !Cba_PrsOk(p) )          return 0;
+    // read keyword
+    iToken = Cba_PrsReadName( p );
+    if (iToken != CBA_VER_MODULE) return Cba_PrsErrorSet(p, "Cannot read \"module\" keyword.", 3);
+    Cba_PrsUtilSkipSpaces( p );
+    if ( !Cba_PrsOk(p) )          return Cba_PrsErrorSet(p, "Module declaration ends abruptly.", 3);
+    // read module name
+    iToken = iNameId = Cba_PrsReadName( p );
+    Cba_PrsUtilSkipSpaces( p );
+    if ( !Cba_PrsOk(p) )          return Cba_PrsErrorSet(p, "Module declaration ends abruptly.", 3);
+    // check if module is known
+    fKnown = Cba_PrsIsKnownModule( p, Abc_NamStr(p->pDesign->pNames, iNameId) );
+    // skip arguments
+    Cba_PrsUtilSkipSpaces( p );
+    if ( !Cba_PrsOk(p) )          return Cba_PrsErrorSet(p, "Module declaration ends abruptly.", 3);
+    if ( !Cba_PrsIsChar(p, '(') ) return Cba_PrsErrorSet(p, "Cannot find \"(\" in the argument declaration.", 3);
+    Cba_PrsUtilSkipUntilChar( p, ')' );
+    if ( !Cba_PrsOk(p) )          return Cba_PrsErrorSet(p, "Module declaration ends abruptly.", 3);
+    assert( *p->pCur == ')' );
+    // find semicolumn
+    p->pCur++;
+    Cba_PrsUtilSkipSpaces( p );
+    if ( !Cba_PrsOk(p) )          return Cba_PrsErrorSet(p, "Module declaration ends abruptly.", 3);
+    // read declarations and instances
+    while ( Cba_PrsIsChar(p, ';') )
+    {
+        p->pCur++;
+        iToken = Cba_PrsReadName( p );
+        if ( iToken == CBA_VER_ENDMODULE )
+        {
+            Cba_PrsAddCurrentModel( p, iNameId );
+            return 0;
+        }
+        if ( iToken == CBA_VER_ALWAYS )
+        {
+            Cba_PrsUtilSkipUntilWord( p, "endmodule" );
+            if ( !Cba_PrsOk(p) )  return Cba_PrsErrorSet(p, "Module definition ends abruptly.", 3);
+            Cba_PrsAddCurrentModel( p, iNameId );
+            return 2;
+        }
+        if ( iToken >= CBA_VER_INOUT && iToken <= CBA_VER_WIRE ) // declaration
+            Cba_PrsReadDeclaration( p, iToken );
+        else if ( iToken == CBA_VER_REG || iToken == CBA_VER_DEFPARAM ) // unsupported keywords
+            Cba_PrsUtilSkipUntilChar( p, ';' );
+        else if ( !fKnown ) // read instance
+            Cba_PrsReadInstance( p, iToken );
+        else // skip known instance
+            Cba_PrsUtilSkipUntilChar( p, ';' );
+    }
+    return Cba_PrsErrorSet(p, "Cannot find \";\" in the module definition.", 3);
+
+}
+static inline int Cba_PrsReadDesign( Cba_Prs_t * p )
+{
+    while ( 1 )
+    {
+        int RetValue = Cba_PrsReadModule( p );
+        if ( RetValue == 0 ) // success
+            return 1;
+        if ( RetValue == 1 ) // end of file
+            continue;
+        if ( RetValue == 2 ) // failed and skipped
+            continue;
+        if ( RetValue == 3 ) // error
+            return 0;
+        assert( 0 );
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cba_Man_t * Cba_PrsReadVerilog( char * pFileName )
+{
+    Cba_Man_t * pDesign = NULL;
+    Cba_Prs_t * p = Cba_PrsAlloc( pFileName );
+    if ( p == NULL )
+        return NULL;
+    Cba_PrsAddVerilogDirectives( p );
+    Cba_PrsReadDesign( p );
+    if ( Cba_PrsErrorPrint(p) )
+        ABC_SWAP( Cba_Man_t *, pDesign, p->pDesign );
+    Cba_PrsFree( p );
+    return pDesign;
+}
+void Cba_PrsTest( char * pFileName )
+{
+    Cba_Man_t * pDes = Cba_PrsReadVerilog( pFileName );
+    Cba_PrsWriteVerilog( "__Test__.v", pDes );
+    Cba_ManFree( pDes );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaSimple.c b/src/base/cba/cbaSimple.c
new file mode 100644
index 00000000..573a1720
--- /dev/null
+++ b/src/base/cba/cbaSimple.c
@@ -0,0 +1,520 @@
+/**CFile****************************************************************
+
+  FileName    [cbaSimple.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaSimple.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+#include "base/abc/abc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+design = array containing design name (as the first entry in the array) followed by pointers to modules
+module = array containing module name (as the first entry in the array) followed by pointers to four arrays: 
+         {array of input names; array of output names; array of nodes; array of boxes}
+node   = array containing output name, followed by node type, followed by input names
+box    = array containing model name, instance name, followed by pairs of formal/actual names for each port
+*/
+
+typedef enum { 
+    PTR_OBJ_NONE,    // 0: non-existent object
+    PTR_OBJ_CONST0,  // 1: constant node
+    PTR_OBJ_PI,      // 2: primary input
+    PTR_OBJ_PO,      // 3: primary output
+    PTR_OBJ_FAN,     // 4: box output
+    PTR_OBJ_FLOP,    // 5: flip-flop
+    PTR_OBJ_BOX,     // 6: box
+    PTR_OBJ_NODE,    // 7: logic node
+
+    PTR_OBJ_C0,      // 8: logic node
+    PTR_OBJ_C1,      // 9: logic node
+    PTR_OBJ_BUF,     // 0: logic node
+    PTR_OBJ_INV,     // 1: logic node
+    PTR_OBJ_AND,     // 2: logic node
+    PTR_OBJ_OR,      // 3: logic node
+    PTR_OBJ_XOR,     // 4: logic node
+    PTR_OBJ_NAND,    // 5: logic node
+    PTR_OBJ_NOR,     // 6: logic node
+    PTR_OBJ_XNOR,    // 7: logic node
+    PTR_OBJ_MUX,     // 8: logic node
+    PTR_OBJ_MAJ,     // 9: logic node
+
+    PTR_VOID         // 0: placeholder
+} Ptr_ObjType_t;
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Node type conversions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ptr_TypeToName( Ptr_ObjType_t Type )
+{
+    if ( Type == PTR_OBJ_BUF )   return "buf";
+    if ( Type == PTR_OBJ_INV )   return "not";
+    if ( Type == PTR_OBJ_AND )   return "and";
+    if ( Type == PTR_OBJ_OR )    return "or";
+    if ( Type == PTR_OBJ_XOR )   return "xor";
+    if ( Type == PTR_OBJ_XNOR )  return "xnor";
+    assert( 0 );
+    return "???";
+}
+char * Ptr_TypeToSop( Ptr_ObjType_t Type )
+{
+    if ( Type == PTR_OBJ_BUF )   return "1 1\n";
+    if ( Type == PTR_OBJ_INV )   return "0 1\n";
+    if ( Type == PTR_OBJ_AND )   return "11 1\n";
+    if ( Type == PTR_OBJ_OR )    return "00 0\n";
+    if ( Type == PTR_OBJ_XOR )   return "01 1\n10 1\n";
+    if ( Type == PTR_OBJ_XNOR )  return "00 1\n11 1\n";
+    assert( 0 );
+    return "???";
+}
+Ptr_ObjType_t Ptr_SopToType( char * pSop )
+{
+    if ( !strcmp(pSop, "1 1\n") )        return PTR_OBJ_BUF;
+    if ( !strcmp(pSop, "0 1\n") )        return PTR_OBJ_INV;
+    if ( !strcmp(pSop, "11 1\n") )       return PTR_OBJ_AND;
+    if ( !strcmp(pSop, "00 0\n") )       return PTR_OBJ_OR;
+    if ( !strcmp(pSop, "-1 1\n1- 1\n") ) return PTR_OBJ_OR;
+    if ( !strcmp(pSop, "1- 1\n-1 1\n") ) return PTR_OBJ_OR;
+    if ( !strcmp(pSop, "01 1\n10 1\n") ) return PTR_OBJ_XOR;
+    if ( !strcmp(pSop, "10 1\n01 1\n") ) return PTR_OBJ_XOR;
+    if ( !strcmp(pSop, "11 1\n00 1\n") ) return PTR_OBJ_XNOR;
+    if ( !strcmp(pSop, "00 1\n11 1\n") ) return PTR_OBJ_XNOR;
+    assert( 0 );
+    return PTR_OBJ_NONE;
+}
+Ptr_ObjType_t Ptr_HopToType( Abc_Obj_t * pObj )
+{
+    static word uTruth, uTruths6[3] = {
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0xCCCCCCCCCCCCCCCC),
+        ABC_CONST(0xF0F0F0F0F0F0F0F0),
+    };
+    assert( Abc_ObjIsNode(pObj) );
+    uTruth = Hop_ManComputeTruth6( (Hop_Man_t *)Abc_ObjNtk(pObj)->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj) );
+    if ( uTruth ==  uTruths6[0] )                 return PTR_OBJ_BUF;
+    if ( uTruth == ~uTruths6[0] )                 return PTR_OBJ_INV;
+    if ( uTruth == (uTruths6[0] & uTruths6[1]) )  return PTR_OBJ_AND;
+    if ( uTruth == (uTruths6[0] | uTruths6[1]) )  return PTR_OBJ_OR;
+    if ( uTruth == (uTruths6[0] ^ uTruths6[1]) )  return PTR_OBJ_XOR;
+    if ( uTruth == (uTruths6[0] ^~uTruths6[1]) )  return PTR_OBJ_XNOR;
+    assert( 0 );
+    return PTR_OBJ_NONE;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dumping hierarchical Abc_Ntk_t in Ptr form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Ptr_ObjName( Abc_Obj_t * pObj )
+{
+    if ( Abc_ObjIsNet(pObj) || Abc_ObjIsBox(pObj) )
+        return Abc_ObjName(pObj);
+    if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) )
+        return Ptr_ObjName(Abc_ObjFanout0(pObj));
+    if ( Abc_ObjIsCo(pObj) )
+        return Ptr_ObjName(Abc_ObjFanin0(pObj));
+    assert( 0 );
+    return NULL;
+}
+static int Ptr_ManCheckArray( Vec_Ptr_t * vArray )
+{
+    if ( Vec_PtrSize(vArray) == 0 )
+        return 1;
+    if ( Abc_MaxInt(8, Vec_PtrSize(vArray)) == Vec_PtrCap(vArray) )
+        return 1;
+    assert( 0 );
+    return 0;
+}
+Vec_Ptr_t * Ptr_ManDumpNode( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin; int i;
+    Vec_Ptr_t * vNode = Vec_PtrAlloc( 2 + Abc_ObjFaninNum(pObj) );
+    assert( Abc_ObjIsNode(pObj) );
+    Vec_PtrPush( vNode, Ptr_ObjName(pObj) );
+    Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_HopToType(pObj)) );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Vec_PtrPush( vNode, Ptr_ObjName(pFanin) );
+    assert( Ptr_ManCheckArray(vNode) );
+    return vNode;
+}
+Vec_Ptr_t * Ptr_ManDumpNodes( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Vec_PtrPush( vNodes, Ptr_ManDumpNode(pObj) );
+    assert( Ptr_ManCheckArray(vNodes) );
+    return vNodes;
+}
+
+Vec_Ptr_t * Ptr_ManDumpBox( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pNext; int i;
+    Abc_Ntk_t * pModel = Abc_ObjModel(pObj);
+    Vec_Ptr_t * vBox = Vec_PtrAlloc( 2 + 2 * Abc_ObjFaninNum(pObj) + 2 * Abc_ObjFanoutNum(pObj) );
+    assert( Abc_ObjIsBox(pObj) );
+    Vec_PtrPush( vBox, Abc_NtkName(pModel) );
+    Vec_PtrPush( vBox, Ptr_ObjName(pObj) );
+    Abc_ObjForEachFanin( pObj, pNext, i )
+    {
+        Vec_PtrPush( vBox, Ptr_ObjName(Abc_NtkPi(pModel, i)) );
+        Vec_PtrPush( vBox, Ptr_ObjName(pNext) );
+    }
+    Abc_ObjForEachFanout( pObj, pNext, i )
+    {
+        Vec_PtrPush( vBox, Ptr_ObjName(Abc_NtkPo(pModel, i)) );
+        Vec_PtrPush( vBox, Ptr_ObjName(pNext) );
+    }
+    assert( Ptr_ManCheckArray(vBox) );
+    return vBox;
+}
+Vec_Ptr_t * Ptr_ManDumpBoxes( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    Vec_Ptr_t * vBoxes = Vec_PtrAlloc( Abc_NtkBoxNum(pNtk) );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Vec_PtrPush( vBoxes, Ptr_ManDumpBox(pObj) );
+    assert( Ptr_ManCheckArray(vBoxes) );
+    return vBoxes;
+}
+
+Vec_Ptr_t * Ptr_ManDumpInputs( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    Vec_Ptr_t * vSigs = Vec_PtrAlloc( Abc_NtkPiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Vec_PtrPush( vSigs, Ptr_ObjName(pObj) );
+    assert( Ptr_ManCheckArray(vSigs) );
+    return vSigs;
+}
+Vec_Ptr_t * Ptr_ManDumpOutputs( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    Vec_Ptr_t * vSigs = Vec_PtrAlloc( Abc_NtkPoNum(pNtk) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Vec_PtrPush( vSigs, Ptr_ObjName(pObj) );
+    assert( Ptr_ManCheckArray(vSigs) );
+    return vSigs;
+}
+Vec_Ptr_t * Ptr_ManDumpNtk( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNtk = Vec_PtrAlloc( 5 );
+    Vec_PtrPush( vNtk, Abc_NtkName(pNtk) );
+    Vec_PtrPush( vNtk, Ptr_ManDumpInputs(pNtk) );
+    Vec_PtrPush( vNtk, Ptr_ManDumpOutputs(pNtk) );
+    Vec_PtrPush( vNtk, Ptr_ManDumpNodes(pNtk) );
+    Vec_PtrPush( vNtk, Ptr_ManDumpBoxes(pNtk) );
+    assert( Ptr_ManCheckArray(vNtk) );
+    return vNtk;
+}
+Vec_Ptr_t * Ptr_ManDumpDes( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vDes;
+    Abc_Ntk_t * pTemp; int i;
+    vDes = Vec_PtrAlloc( 1 + Vec_PtrSize(pNtk->pDesign->vModules) );
+    Vec_PtrPush( vDes, pNtk->pDesign->pName );
+    Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
+        Vec_PtrPush( vDes, Ptr_ManDumpNtk(pTemp) );
+    assert( Ptr_ManCheckArray(vDes) );
+    return vDes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dumping Ptr into a Verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ptr_ManDumpNodeToBlif( FILE * pFile, Vec_Ptr_t * vNode )
+{
+    char * pName;  int i;
+    fprintf( pFile, ".names" );
+    Vec_PtrForEachEntryStart( char *, vNode, pName, i, 2 )
+        fprintf( pFile, " %s", pName );
+    fprintf( pFile, " %s\n", (char *)Vec_PtrEntry(vNode, 0) );
+    fprintf( pFile, "%s", Ptr_TypeToSop( (Ptr_ObjType_t)Abc_Ptr2Int(Vec_PtrEntry(vNode, 1)) ) );
+}
+void Ptr_ManDumpNodesToBlif( FILE * pFile, Vec_Ptr_t * vNodes )
+{
+    Vec_Ptr_t * vNode; int i;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
+        Ptr_ManDumpNodeToBlif( pFile, vNode );
+}
+
+void Ptr_ManDumpBoxToBlif( FILE * pFile, Vec_Ptr_t * vBox )
+{
+    char * pName; int i;
+    fprintf( pFile, "%s", (char *)Vec_PtrEntry(vBox, 0) );
+    Vec_PtrForEachEntryStart( char *, vBox, pName, i, 2 )
+        fprintf( pFile, " %s=%s", pName, (char *)Vec_PtrEntry(vBox, i+1) ), i++;
+    fprintf( pFile, "\n" );
+}
+void Ptr_ManDumpBoxesToBlif( FILE * pFile, Vec_Ptr_t * vBoxes )
+{
+    Vec_Ptr_t * vBox; int i;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vBoxes, vBox, i )
+        Ptr_ManDumpBoxToBlif( pFile, vBox );
+}
+
+void Ptr_ManDumpSignalsToBlif( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
+{
+    char * pSig; int i;
+    Vec_PtrForEachEntry( char *, vSigs, pSig, i )
+        fprintf( pFile, " %s", pSig );
+}
+void Ptr_ManDumpModuleToBlif( FILE * pFile, Vec_Ptr_t * vNtk )
+{
+    fprintf( pFile, ".model %s\n", (char *)Vec_PtrEntry(vNtk, 0) );
+    fprintf( pFile, ".inputs" );
+    Ptr_ManDumpSignalsToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs" );
+    Ptr_ManDumpSignalsToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
+    fprintf( pFile, "\n\n" );
+    Ptr_ManDumpNodesToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
+    fprintf( pFile, "\n" );
+    Ptr_ManDumpBoxesToBlif( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".end\n\n" );
+}
+void Ptr_ManDumpToBlif( char * pFileName, Vec_Ptr_t * vDes )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNtk; int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", (char *)Vec_PtrEntry(vDes, 0), Extra_TimeStamp() );
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Ptr_ManDumpModuleToBlif( pFile, vNtk );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dumping Ptr into a Verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ptr_ManDumpNodeToFile( FILE * pFile, Vec_Ptr_t * vNode )
+{
+    char * pName;  int i;
+    fprintf( pFile, "%s", Ptr_TypeToName( (Ptr_ObjType_t)Abc_Ptr2Int(Vec_PtrEntry(vNode, 1)) ) );
+    fprintf( pFile, "( %s", (char *)Vec_PtrEntry(vNode, 0) );
+    Vec_PtrForEachEntryStart( char *, vNode, pName, i, 2 )
+        fprintf( pFile, ", %s", pName );
+    fprintf( pFile, " );\n" );
+}
+void Ptr_ManDumpNodesToFile( FILE * pFile, Vec_Ptr_t * vNodes )
+{
+    Vec_Ptr_t * vNode; int i;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vNodes, vNode, i )
+        Ptr_ManDumpNodeToFile( pFile, vNode );
+}
+
+void Ptr_ManDumpBoxToFile( FILE * pFile, Vec_Ptr_t * vBox )
+{
+    char * pName; int i;
+    fprintf( pFile, "%s %s (", (char *)Vec_PtrEntry(vBox, 0), (char *)Vec_PtrEntry(vBox, 1) );
+    Vec_PtrForEachEntryStart( char *, vBox, pName, i, 2 )
+        fprintf( pFile, " .%s(%s)%s", pName, (char *)Vec_PtrEntry(vBox, i+1), i >= Vec_PtrSize(vBox)-2 ? "" : "," ), i++;
+    fprintf( pFile, " );\n" );
+}
+void Ptr_ManDumpBoxesToFile( FILE * pFile, Vec_Ptr_t * vBoxes )
+{
+    Vec_Ptr_t * vBox; int i;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vBoxes, vBox, i )
+        Ptr_ManDumpBoxToFile( pFile, vBox );
+}
+
+void Ptr_ManDumpSignalsToFile( FILE * pFile, Vec_Ptr_t * vSigs, int fSkipLastComma )
+{
+    char * pSig; int i;
+    Vec_PtrForEachEntry( char *, vSigs, pSig, i )
+        fprintf( pFile, " %s%s", pSig, (fSkipLastComma && i == Vec_PtrSize(vSigs)-1) ? "" : "," );
+}
+void Ptr_ManDumpModuleToFile( FILE * pFile, Vec_Ptr_t * vNtk )
+{
+    fprintf( pFile, "module %s\n", (char *)Vec_PtrEntry(vNtk, 0) );
+    fprintf( pFile, "(\n" );
+    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 0 );
+    fprintf( pFile, "\n" );
+    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
+    fprintf( pFile, "\n);\ninput" );
+    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), 1 );
+    fprintf( pFile, ";\noutput" );
+    Ptr_ManDumpSignalsToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), 1 );
+    fprintf( pFile, ";\n\n" );
+    Ptr_ManDumpNodesToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
+    fprintf( pFile, "\n" );
+    Ptr_ManDumpBoxesToFile( pFile, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
+    fprintf( pFile, "endmodule\n\n" );
+}
+void Ptr_ManDumpToFile( char * pFileName, Vec_Ptr_t * vDes )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNtk; int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", (char *)Vec_PtrEntry(vDes, 0), Extra_TimeStamp() );
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Ptr_ManDumpModuleToFile( pFile, vNtk );
+    fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count memory used by Ptr.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ptr_ManMemArray( Vec_Ptr_t * vArray )
+{
+    return (int)Vec_PtrMemory(vArray);
+}
+int Ptr_ManMemArrayArray( Vec_Ptr_t * vArrayArray )
+{
+    Vec_Ptr_t * vArray; int i, nBytes = 0;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vArrayArray, vArray, i )
+        nBytes += Ptr_ManMemArray(vArray);
+    return nBytes;
+}
+int Ptr_ManMemNtk( Vec_Ptr_t * vNtk )
+{
+    int nBytes = (int)Vec_PtrMemory(vNtk);
+    nBytes += Ptr_ManMemArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1) );
+    nBytes += Ptr_ManMemArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2) );
+    nBytes += Ptr_ManMemArrayArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3) );
+    nBytes += Ptr_ManMemArrayArray( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4) );
+    return nBytes;
+}
+int Ptr_ManMemDes( Vec_Ptr_t * vDes )
+{
+    Vec_Ptr_t * vNtk; int i, nBytes = (int)Vec_PtrMemory(vDes);
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        nBytes += Ptr_ManMemNtk(vNtk);
+    return nBytes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Free Ptr.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ptr_ManFreeNtk( Vec_Ptr_t * vNtk )
+{
+    Vec_PtrFree( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1) );
+    Vec_PtrFree( (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2) );
+    Vec_VecFree( (Vec_Vec_t *)Vec_PtrEntry(vNtk, 3) );
+    Vec_VecFree( (Vec_Vec_t *)Vec_PtrEntry(vNtk, 4) );
+    Vec_PtrFree( vNtk );
+}
+void Ptr_ManFreeDes( Vec_Ptr_t * vDes )
+{
+    Vec_Ptr_t * vNtk; int i;
+    Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
+        Ptr_ManFreeNtk( vNtk );
+    Vec_PtrFree( vDes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count memory use used by Ptr.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ptr_ManExperiment( Abc_Ntk_t * pNtk )
+{
+    abctime clk = Abc_Clock();
+    Vec_Ptr_t * vDes = Ptr_ManDumpDes( pNtk );
+    printf( "Converting to Ptr:  Memory = %6.3f MB  ", 1.0*Ptr_ManMemDes(vDes)/(1<<20) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Ptr_ManDumpToFile( Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.v"), vDes );
+    printf( "Finished writing output file \"%s\".\n", Extra_FileNameGenericAppend(pNtk->pDesign->pName, "_out.v") );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Ptr_ManFreeDes( vDes );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaWriteBlif.c b/src/base/cba/cbaWriteBlif.c
new file mode 100644
index 00000000..a5d96279
--- /dev/null
+++ b/src/base/cba/cbaWriteBlif.c
@@ -0,0 +1,138 @@
+/**CFile****************************************************************
+
+  FileName    [cbaWriteBlif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaWriteVer.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+#include "cbaPrs.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writing parser state into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_PrsWriteBlifArray( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vFanins, int fFirst )
+{
+    int NameId, i;
+    Vec_IntForEachEntryStart( vFanins, NameId, i, fFirst )
+        fprintf( pFile, " %s", Cba_NtkStr(p, NameId) );
+    if ( fFirst )
+        fprintf( pFile, " %s", Cba_NtkStr(p, Vec_IntEntry(vFanins,0)) );
+    fprintf( pFile, "\n" );
+}
+void Cba_PrsWriteBlifArray2( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vFanins )
+{
+    int FormId, NameId, i;
+    assert( Vec_IntSize(vFanins) % 2 == 0 );
+    Vec_IntForEachEntryDouble( vFanins, FormId, NameId, i )
+        fprintf( pFile, " %s=%s", Cba_NtkStr(p, FormId), Cba_NtkStr(p, NameId) );
+}
+void Cba_PrsWriteBlifLines( FILE * pFile, Cba_Ntk_t * p )
+{
+    Vec_Int_t * vFanins;
+    int Type, Func, i;
+    Cba_NtkForEachObjTypeFuncFanins( p, Type, Func, vFanins, i )
+        if ( Type == CBA_PRS_NODE ) // .names/assign/box2 (no formal/actual binding)
+        {
+            fprintf( pFile, ".names" );
+            Cba_PrsWriteBlifArray( pFile, p, vFanins, 1 );
+            fprintf( pFile, " %s", Cba_NtkStr(p,  Func) );
+        }
+        else if ( Type == CBA_PRS_BOX ) // .names/assign/box2 (no formal/actual binding)
+        {
+            fprintf( pFile, ".subckt" );
+            fprintf( pFile, " %s", Cba_NtkFuncStr(p,  Func) );
+            Cba_PrsWriteBlifArray2( pFile, p, vFanins );
+        }
+        else if ( Type == CBA_PRS_LATCH ) // .names/assign/box2 (no formal/actual binding)
+        {
+            fprintf( pFile, ".latch" );
+            fprintf( pFile, " %s", Cba_NtkFuncStr(p,  Vec_IntEntry(vFanins, 1)) );
+            fprintf( pFile, " %s", Cba_NtkFuncStr(p,  Vec_IntEntry(vFanins, 0)) );
+            fprintf( pFile, " %c\n", '0' + Func );
+        }
+}
+void Cba_PrsWriteBlifNtk( FILE * pFile, Cba_Ntk_t * p )
+{
+    assert( Vec_IntSize(&p->vTypes)   == Cba_NtkObjNum(p) );
+    assert( Vec_IntSize(&p->vFuncs)   == Cba_NtkObjNum(p) );
+    // write header
+    fprintf( pFile, ".model %s\n", Cba_NtkName(p) );
+    fprintf( pFile, ".inouts" );
+    Cba_PrsWriteBlifArray( pFile, p, &p->vInouts, 0 );
+    fprintf( pFile, ".inputs" );
+    Cba_PrsWriteBlifArray( pFile, p, &p->vInputs, 0 );
+    fprintf( pFile, ".outputs" );
+    Cba_PrsWriteBlifArray( pFile, p, &p->vOutputs, 0 );
+    // write objects
+    Cba_PrsWriteBlifLines( pFile, p );
+    fprintf( pFile, ".end\n" );
+}
+void Cba_PrsWriteBlif( char * pFileName, Cba_Man_t * pDes )
+{
+    FILE * pFile;
+    Cba_Ntk_t * pNtk; 
+    int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(pDes), Extra_TimeStamp() );
+    Cba_ManForEachNtk( pDes, pNtk, i )
+        Cba_PrsWriteBlifNtk( pFile, pNtk );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
new file mode 100644
index 00000000..d11c1d0e
--- /dev/null
+++ b/src/base/cba/cbaWriteVer.c
@@ -0,0 +1,210 @@
+/**CFile****************************************************************
+
+  FileName    [cba.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+#include "cbaPrs.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+/*
+
+// node types during parsing
+typedef enum { 
+    CBA_NODE_NONE = 0,   // 0:  unused
+    CBA_NODE_CONST,      // 1:  constant
+    CBA_NODE_BUF,        // 2:  buffer
+    CBA_NODE_INV,        // 3:  inverter
+    CBA_NODE_AND,        // 4:  AND
+    CBA_NODE_OR,         // 5:  OR
+    CBA_NODE_XOR,        // 6:  XOR
+    CBA_NODE_NAND,       // 7:  NAND
+    CBA_NODE_NOR,        // 8:  NOR
+    CBA_NODE_XNOR,       // 9  .XNOR
+    CBA_NODE_MUX,        // 10: MUX
+    CBA_NODE_MAJ,        // 11: MAJ
+    CBA_NODE_UNKNOWN     // 12: unknown
+} Cba_NodeType_t; 
+
+*/
+
+const char * s_NodeTypes[CBA_NODE_UNKNOWN+1] = {
+    NULL,             // 0:  unused
+    "const",          // 1:  constant
+    "buf",            // 2:  buffer
+    "not",            // 3:  inverter
+    "and",            // 4:  AND
+    "or",             // 5:  OR
+    "xor",            // 6:  XOR
+    "nand",           // 7:  NAND
+    "nor",            // 8:  NOR
+    "xnor",           // 9  .XNOR
+    "mux",            // 10: MUX
+    "maj",            // 11: MAJ
+    "???"             // 12: unknown
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writing parser state into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_PrsWriteVerilogMux( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vFanins )
+{
+    int NameId, RangeId, i;
+    char * pStrs[4] = { " = ", " ? ", " : ", ";\n" };
+    assert( Vec_IntSize(vFanins) == 8 );
+    fprintf( pFile, "assign " );
+    Vec_IntForEachEntryDouble( vFanins, NameId, RangeId, i )
+        fprintf( pFile, "%s%s%s", Cba_NtkStr(p, NameId), RangeId ? Cba_NtkStr(p, RangeId) : "", pStrs[i/2] );
+}
+void Cba_PrsWriteVerilogArray2( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vFanins )
+{
+    int NameId, RangeId, i;
+    assert( Vec_IntSize(vFanins) % 2 == 0 );
+    Vec_IntForEachEntryDouble( vFanins, NameId, RangeId, i )
+        fprintf( pFile, "%s%s%s", Cba_NtkStr(p, NameId), RangeId ? Cba_NtkStr(p, RangeId) : "", (i == Vec_IntSize(vFanins) - 2) ? "" : " ," );
+}
+void Cba_PrsWriteVerilogArray3( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vFanins )
+{
+    int FormId, NameId, RangeId, i;
+    assert( Vec_IntSize(vFanins) % 3 == 0 );
+    Vec_IntForEachEntryTriple( vFanins, FormId, NameId, RangeId, i )
+        fprintf( pFile, ".%s(%s%s)%s", Cba_NtkStr(p, FormId), Cba_NtkStr(p, NameId), RangeId ? Cba_NtkStr(p, RangeId) : "", (i == Vec_IntSize(vFanins) - 3) ? "" : " ," );
+}
+void Cba_PrsWriteVerilogConcat( FILE * pFile, Cba_Ntk_t * p, int Id )
+{
+    fprintf( pFile, "{" );
+    Cba_PrsWriteVerilogArray2( pFile, p, Cba_ObjFanins(p, Id) );
+    fprintf( pFile, "}" );
+}
+void Cba_PrsWriteVerilogNodes( FILE * pFile, Cba_Ntk_t * p )
+{
+    int Type, Func, i;
+    Cba_NtkForEachObjType( p, Type, i )
+        if ( Type == CBA_PRS_NODE ) // .names/assign/box2 (no formal/actual binding)
+        {
+            Func = Cba_ObjFuncId(p, i);
+            if ( Func >= CBA_NODE_BUF && Func <= CBA_NODE_XNOR )
+            {
+                fprintf( pFile, "%s (", s_NodeTypes[Func] );
+                Cba_PrsWriteVerilogArray2( pFile, p, Cba_ObjFanins(p, i) );
+                fprintf( pFile, ");\n" );
+            }
+            else if ( Func == CBA_NODE_MUX )
+                Cba_PrsWriteVerilogMux( pFile, p, Cba_ObjFanins(p, i) );
+            else assert( 0 );
+        }
+}
+void Cba_PrsWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p )
+{
+    int Type, i;
+    Cba_NtkForEachObjType( p, Type, i )
+        if ( Type == CBA_PRS_BOX ) // .subckt/.gate/box (formal/actual binding) 
+        {
+            fprintf( pFile, "%s %s (", Cba_ObjFuncStr(p, i), Cba_ObjInstStr(p, i) );
+            Cba_PrsWriteVerilogArray3( pFile, p, Cba_ObjFanins(p, i) );
+            fprintf( pFile, ");\n" );
+        }
+}
+void Cba_PrsWriteVerilogSignals( FILE * pFile, Cba_Ntk_t * p, int SigType )
+{
+    int NameId, RangeId, i;
+    char * pSigNames[4]  = { "inout", "input", "output", "wire" }; 
+    Vec_Int_t * vSigs[4] = { &p->vInouts, &p->vInputs, &p->vOutputs, &p->vWires };
+    Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i )
+        fprintf( pFile, "%s %s%s;\n", pSigNames[SigType], RangeId ? Cba_NtkStr(p, RangeId) : "", Cba_NtkStr(p, NameId) );
+}
+void Cba_PrsWriteVerilogSignalList( FILE * pFile, Cba_Ntk_t * p, int SigType, int fSkipComma )
+{
+    int NameId, RangeId, i;
+    Vec_Int_t * vSigs[4] = { &p->vInouts, &p->vInputs, &p->vOutputs, &p->vWires };
+    Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i )
+        fprintf( pFile, " %s%s", Cba_NtkStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 2) ? "" : "," );
+}
+void Cba_PrsWriteVerilogNtk( FILE * pFile, Cba_Ntk_t * p )
+{
+    int s;
+    assert( Vec_IntSize(&p->vTypes)   == Cba_NtkObjNum(p) );
+    assert( Vec_IntSize(&p->vFuncs)   == Cba_NtkObjNum(p) );
+    assert( Vec_IntSize(&p->vInstIds) == Cba_NtkObjNum(p) );
+    // write header
+    fprintf( pFile, "module %s (\n", Cba_NtkName(p) );
+    for ( s = 0; s < 3; s++ )
+        Cba_PrsWriteVerilogSignalList( pFile, p, s, s==2 );
+    fprintf( pFile, ");\n" );
+    // write declarations
+    for ( s = 0; s < 4; s++ )
+        Cba_PrsWriteVerilogSignals( pFile, p, s );
+    // write objects
+    Cba_PrsWriteVerilogNodes( pFile, p );
+    Cba_PrsWriteVerilogBoxes( pFile, p );
+    fprintf( pFile, "endmodule\n" );
+}
+void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * pDes )
+{
+    FILE * pFile;
+    Cba_Ntk_t * pNtk; 
+    int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(pDes), Extra_TimeStamp() );
+    Cba_ManForEachNtk( pDes, pNtk, i )
+        Cba_PrsWriteVerilogNtk( pFile, pNtk );
+    fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/module.make b/src/base/cba/module.make
new file mode 100644
index 00000000..0b1a9e17
--- /dev/null
+++ b/src/base/cba/module.make
@@ -0,0 +1,10 @@
+SRC +=    src/base/cba/cbaBlast.c \
+    src/base/cba/cbaBuild.c \
+    src/base/cba/cbaCom.c \
+    src/base/cba/cbaLib.c \
+    src/base/cba/cbaNtk.c \
+    src/base/cba/cbaReadBlif.c \
+    src/base/cba/cbaReadVer.c \
+    src/base/cba/cbaSimple.c \
+    src/base/cba/cbaWriteBlif.c \
+    src/base/cba/cbaWriteVer.c 
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index f0d17a2d..eda304aa 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -49,6 +49,8 @@ extern void Scl_Init( Abc_Frame_t * pAbc );
 extern void Scl_End( Abc_Frame_t * pAbc );
 extern void Wlc_Init( Abc_Frame_t * pAbc );
 extern void Wlc_End( Abc_Frame_t * pAbc );
+extern void Cba_Init( Abc_Frame_t * pAbc );
+extern void Cba_End( Abc_Frame_t * pAbc );
 extern void Test_Init( Abc_Frame_t * pAbc );
 extern void Test_End( Abc_Frame_t * pAbc );
 extern void Abc2_Init( Abc_Frame_t * pAbc );
@@ -104,6 +106,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Load_Init( pAbc );
     Scl_Init( pAbc );
     Wlc_Init( pAbc );
+    Cba_Init( pAbc );
     Test_Init( pAbc );
     for( p = s_InitializerStart ; p ; p = p->next )
         if(p->init)
@@ -139,6 +142,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Load_End( pAbc );
     Scl_End( pAbc );
     Wlc_End( pAbc );
+    Cba_End( pAbc );
     Test_End( pAbc );
 }
 
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 3d7a7eac..89b961d4 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -127,6 +127,7 @@ struct Abc_Frame_t_
     void *          pAbc85Best;
     void *          pAbc85Delay;
     void *          pAbcWlc;
+    void *          pAbcCba;
 };
 
 typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 5d9c405f..3dee5f4e 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -106,6 +106,7 @@ extern char *       Extra_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern void         Extra_FileNameCorrectPath( char * FileName );
 extern char *       Extra_FileNameWithoutPath( char * FileName );
 extern char *       Extra_FilePathWithoutName( char * FileName );
+extern char *       Extra_FileDesignName( char * pFileName );
 extern int          Extra_FileCheck( char * pFileName );
 extern int          Extra_FileSize( char * pFileName );
 extern char *       Extra_FileRead( FILE * pFile );
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index ee9168f6..6b4453a5 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -247,6 +247,25 @@ char * Extra_FilePathWithoutName( char * FileName )
     ABC_FREE( FileName );
     return NULL;
 }
+char * Extra_FileDesignName( char * pFileName )
+{
+    char * pBeg, * pEnd, * pStore, * pCur;
+    // find the first dot
+    for ( pEnd = pFileName; *pEnd; pEnd++ )
+        if ( *pEnd == '.' )
+            break;
+    // find the first char
+    for ( pBeg = pEnd - 1; pBeg >= pFileName; pBeg-- )
+        if ( !((*pBeg >= 'a' && *pBeg <= 'z') || (*pBeg >= 'A' && *pBeg <= 'Z') || (*pBeg >= '0' && *pBeg <= '9') || *pBeg == '_') )
+            break;
+    pBeg++;
+    // fill up storage
+    pStore = ABC_ALLOC( char, pEnd - pBeg + 1 );
+    for ( pCur = pStore; pBeg < pEnd; pBeg++, pCur++ )
+        *pCur = *pBeg;
+    *pCur = 0;
+    return pStore;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/util/utilNam.c b/src/misc/util/utilNam.c
index 5fb38c51..76c86aff 100644
--- a/src/misc/util/utilNam.c
+++ b/src/misc/util/utilNam.c
@@ -237,7 +237,7 @@ int Abc_NamMemAlloc( Abc_Nam_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NamStrHash( const char * pStr, int nTableSize )
+int Abc_NamStrHash( const char * pStr, const char * pLim, int nTableSize )
 {
     static int s_FPrimes[128] = { 
         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
@@ -255,11 +255,22 @@ int Abc_NamStrHash( const char * pStr, int nTableSize )
         8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
     };
     unsigned i, uHash;
-    for ( uHash = 0, i = 0; pStr[i]; i++ )
-        if ( i & 1 ) 
-            uHash *= pStr[i] * s_FPrimes[i & 0x7F];
-        else
-            uHash ^= pStr[i] * s_FPrimes[i & 0x7F];
+    if ( pLim )
+    {
+        for ( uHash = 0, i = 0; pStr < pLim; i++ )
+            if ( i & 1 ) 
+                uHash *= pStr[i] * s_FPrimes[i & 0x7F];
+            else
+                uHash ^= pStr[i] * s_FPrimes[i & 0x7F];
+    }
+    else
+    {
+        for ( uHash = 0, i = 0; pStr[i]; i++ )
+            if ( i & 1 ) 
+                uHash *= pStr[i] * s_FPrimes[i & 0x7F];
+            else
+                uHash ^= pStr[i] * s_FPrimes[i & 0x7F];
+    }
     return uHash % nTableSize;
 }
 
@@ -274,10 +285,10 @@ int Abc_NamStrHash( const char * pStr, int nTableSize )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int * Abc_NamStrHashFind( Abc_Nam_t * p, const char * pStr )
+static inline int * Abc_NamStrHashFind( Abc_Nam_t * p, const char * pStr, const char * pLim )
 {
     char * pThis;
-    int * pPlace = (int *)(p->pBins + Abc_NamStrHash( pStr, p->nBins ));
+    int * pPlace = (int *)(p->pBins + Abc_NamStrHash( pStr, pLim, p->nBins ));
     assert( *pStr );
     for ( pThis = (*pPlace)? Abc_NamIntToStr(p, *pPlace) : NULL; 
           pThis;    pPlace = Abc_NamIntToNextP(p, *pPlace), 
@@ -318,7 +329,7 @@ void Abc_NamStrHashResize( Abc_Nam_t * p )
     Vec_IntForEachEntryStart( vInt2HandleOld, iHandleOld, i, 1 )
     {
         pThis   = Abc_NamHandleToStr( p, iHandleOld );
-        piPlace = Abc_NamStrHashFind( p, pThis );
+        piPlace = Abc_NamStrHashFind( p, pThis, NULL );
         assert( *piPlace == 0 );
         *piPlace = Vec_IntSize( p->vInt2Handle );
         assert( Vec_IntSize( p->vInt2Handle ) == i );
@@ -343,7 +354,11 @@ void Abc_NamStrHashResize( Abc_Nam_t * p )
 ***********************************************************************/
 int Abc_NamStrFind( Abc_Nam_t * p, char * pStr )
 {
-    return *Abc_NamStrHashFind( p, pStr );
+    return *Abc_NamStrHashFind( p, pStr, NULL );
+}
+int Abc_NamStrFindLim( Abc_Nam_t * p, char * pStr, char * pLim )
+{
+    return *Abc_NamStrHashFind( p, pStr, pLim );
 }
 
 /**Function*************************************************************
@@ -368,7 +383,7 @@ int Abc_NamStrFindOrAdd( Abc_Nam_t * p, char * pStr, int * pfFound )
                 break;
         assert( i < (int)strlen(pStr) );
     }
-    piPlace = Abc_NamStrHashFind( p, pStr );
+    piPlace = Abc_NamStrHashFind( p, pStr, NULL );
     if ( *piPlace )
     {
         if ( pfFound )
@@ -396,6 +411,41 @@ int Abc_NamStrFindOrAdd( Abc_Nam_t * p, char * pStr, int * pfFound )
         Abc_NamStrHashResize( p );
     return Vec_IntSize(p->vInt2Handle) - 1;
 }
+int Abc_NamStrFindOrAddLim( Abc_Nam_t * p, char * pStr, char * pLim, int * pfFound )
+{
+    int iHandleNew;
+    int *piPlace;
+    char * pStore;
+    piPlace = Abc_NamStrHashFind( p, pStr, pLim );
+    if ( *piPlace )
+    {
+        if ( pfFound )
+            *pfFound = 1;
+        return *piPlace;
+    }
+    if ( pfFound )
+        *pfFound = 0;
+    iHandleNew = p->iHandle + (pLim - pStr) + 1;
+    while ( p->nStore < iHandleNew )
+    {
+        p->nStore *= 3;
+        p->nStore /= 2;
+        p->pStore  = ABC_REALLOC( char, p->pStore, p->nStore );
+    }
+    assert( p->nStore >= iHandleNew );
+    // create new handle
+    *piPlace = Vec_IntSize( p->vInt2Handle );
+    pStore = Abc_NamHandleToStr( p, p->iHandle );
+    strncpy( pStore, pStr, pLim - pStr );
+    pStore[pLim - pStr] = 0;
+    Vec_IntPush( p->vInt2Handle, p->iHandle );
+    Vec_IntPush( p->vInt2Next, 0 );
+    p->iHandle = iHandleNew;
+    // extend the hash table
+    if ( Vec_IntSize(p->vInt2Handle) > 2 * p->nBins )
+        Abc_NamStrHashResize( p );
+    return Vec_IntSize(p->vInt2Handle) - 1;
+}
 
 /**Function*************************************************************
 
@@ -435,7 +485,7 @@ Vec_Int_t * Abc_NamComputeIdMap( Abc_Nam_t * p1, Abc_Nam_t * p2 )
     Vec_IntForEachEntryStart( p1->vInt2Handle, iHandle1, i, 1 )
     {
         pThis = Abc_NamHandleToStr( p1, iHandle1 );
-        piPlace = Abc_NamStrHashFind( p2, pThis );
+        piPlace = Abc_NamStrHashFind( p2, pThis, NULL );
         Vec_IntWriteEntry( vMap, i, *piPlace );
 //        Abc_Print( 1, "%d->%d  ", i, *piPlace );
     }
diff --git a/src/misc/util/utilNam.h b/src/misc/util/utilNam.h
index 9f3048f3..86802802 100644
--- a/src/misc/util/utilNam.h
+++ b/src/misc/util/utilNam.h
@@ -59,7 +59,9 @@ extern int             Abc_NamObjNumMax( Abc_Nam_t * p );
 extern int             Abc_NamMemUsed( Abc_Nam_t * p );
 extern int             Abc_NamMemAlloc( Abc_Nam_t * p );
 extern int             Abc_NamStrFind( Abc_Nam_t * p, char * pStr );
+extern int             Abc_NamStrFindLim( Abc_Nam_t * p, char * pStr, char * pLim );
 extern int             Abc_NamStrFindOrAdd( Abc_Nam_t * p, char * pStr, int * pfFound );
+extern int             Abc_NamStrFindOrAddLim( Abc_Nam_t * p, char * pStr, char * pLim, int * pfFound );
 extern char *          Abc_NamStr( Abc_Nam_t * p, int id );
 extern Vec_Int_t *     Abc_NamComputeIdMap( Abc_Nam_t * p1, Abc_Nam_t * p2 );
 extern int             Abc_NamReportCommon( Vec_Int_t * vNameIds1, Abc_Nam_t * p1, Abc_Nam_t * p2 );
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 26c67073..3e195bd3 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -65,6 +65,8 @@ struct Vec_Int_t_
     for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
 #define Vec_IntForEachEntryDouble( vVec, Entry1, Entry2, i )                                \
     for ( i = 0; (i+1 < Vec_IntSize(vVec)) && (((Entry1) = Vec_IntEntry(vVec, i)), 1) && (((Entry2) = Vec_IntEntry(vVec, i+1)), 1); i += 2 )
+#define Vec_IntForEachEntryTriple( vVec, Entry1, Entry2, Entry3, i )                                \
+    for ( i = 0; (i+2 < Vec_IntSize(vVec)) && (((Entry1) = Vec_IntEntry(vVec, i)), 1) && (((Entry2) = Vec_IntEntry(vVec, i+1)), 1) && (((Entry3) = Vec_IntEntry(vVec, i+2)), 1); i += 3 )
 #define Vec_IntForEachEntryThisNext( vVec, This, Next, i )                                  \
     for ( i = 0, (This) = (Next) = (Vec_IntSize(vVec) ? Vec_IntEntry(vVec, 0) : -1); (i+1 < Vec_IntSize(vVec)) && (((Next) = Vec_IntEntry(vVec, i+1)), 1); i += 2, (This) = (Next) )
 
@@ -696,6 +698,11 @@ static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
     }
     p->pArray[p->nSize++] = Entry;
 }
+static inline void Vec_IntPushTwo( Vec_Int_t * p, int Entry1, int Entry2 )
+{
+    Vec_IntPush( p, Entry1 );
+    Vec_IntPush( p, Entry2 );
+}
 static inline void Vec_IntPushArray( Vec_Int_t * p, int * pEntries, int nEntries )
 {
     int i;
@@ -1045,6 +1052,34 @@ static inline void Vec_IntReverseOrder( Vec_Int_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Removes odd entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntRemoveOdd( Vec_Int_t * p )
+{
+    int i;
+    assert( (p->nSize & 1) == 0 );
+    p->nSize >>= 1;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = p->pArray[2*i];
+}
+static inline void Vec_IntRemoveEven( Vec_Int_t * p )
+{
+    int i;
+    assert( (p->nSize & 1) == 0 );
+    p->nSize >>= 1;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = p->pArray[2*i+1];
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -1144,6 +1179,13 @@ static inline int Vec_IntCountPositive( Vec_Int_t * p )
         Counter += (p->pArray[i] > 0);
     return Counter;
 }
+static inline int Vec_IntCountZero( Vec_Int_t * p ) 
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nSize; i++ )
+        Counter += (p->pArray[i] == 0);
+    return Counter;
+}
 
 /**Function*************************************************************