Adding binary dump to CBA.

9 files changed, 413 insertions, 11 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 27dd6434..bb8f33a1 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -783,6 +783,10 @@ SOURCE=.\src\base\cba\cbaBlast.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\cba\cbaCba.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\cba\cbaCom.c
 # End Source File
 # Begin Source File
@@ -819,6 +823,10 @@ SOURCE=.\src\base\cba\cbaReadBlif.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\cba\cbaReadSmt.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\cba\cbaReadVer.c
 # End Source File
 # Begin Source File
@@ -827,6 +835,10 @@ SOURCE=.\src\base\cba\cbaWriteBlif.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\cba\cbaWriteSmt.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\cba\cbaWriteVer.c
 # End Source File
 # End Group
diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 2ac3ed35..ae575073 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -71,11 +71,13 @@ typedef enum {
     CBA_BOX_RXOR,
     CBA_BOX_RXNOR,
 
+    CBA_BOX_N1MUX,  
     CBA_BOX_SEL,
     CBA_BOX_PSEL,
     CBA_BOX_ENC,
     CBA_BOX_PENC,
     CBA_BOX_DEC,
+    CBA_BOX_EDEC,
 
     CBA_BOX_ADD,
     CBA_BOX_SUB,
@@ -84,6 +86,7 @@ typedef enum {
     CBA_BOX_MOD,
     CBA_BOX_REM,
     CBA_BOX_POW,
+    CBA_BOX_MIN,
     CBA_BOX_ABS,
 
     CBA_BOX_LTHAN,
@@ -113,7 +116,7 @@ typedef enum {
     CBA_BOX_DFF,
     CBA_BOX_DFFRS,
 
-    CBA_BOX_UNKNOWN   // 50
+    CBA_BOX_UNKNOWN   // 67
 } Cba_ObjType_t; 
 
 
@@ -156,6 +159,7 @@ struct Cba_Man_t_
     int          iRoot;    // root network
     int          nNtks;    // number of current networks
     Cba_Ntk_t *  pNtks;    // networks
+    Vec_Int_t    vInfo;    // box info
     // user data
     Vec_Int_t    vBuf2RootNtk;
     Vec_Int_t    vBuf2RootObj;
@@ -176,6 +180,7 @@ static inline Cba_Ntk_t *    Cba_ManNtkFind( Cba_Man_t * p, char * pName )   { r
 static inline Cba_Ntk_t *    Cba_ManRoot( Cba_Man_t * p )                    { return Cba_ManNtk(p, p->iRoot);                                                             }
 static inline char *         Cba_ManStr( Cba_Man_t * p, int i )              { return Abc_NamStr(p->pStrs, i);                                                             }
 static inline int            Cba_ManStrId( Cba_Man_t * p, char * pStr )      { return Abc_NamStrFind(p->pStrs, pStr);                                                      }
+static inline int            Cba_ManInfoNum( Cba_Man_t * p )                 { return Vec_IntSize(&p->vInfo) >> 2;                                                         }
 
 static inline int            Cba_NtkId( Cba_Ntk_t * p )                      { int i = p - p->pDesign->pNtks; assert(Cba_ManNtkIsOk(p->pDesign, i)); return i;             }
 static inline Cba_Man_t *    Cba_NtkMan( Cba_Ntk_t * p )                     { return p->pDesign;                                                                          }
@@ -186,7 +191,7 @@ static inline Cba_Ntk_t *    Cba_NtkCopyNtk(Cba_Man_t * pNew, Cba_Ntk_t * p) { r
 static inline void           Cba_NtkSetCopy( Cba_Ntk_t * p, int i )          { assert(p->iCopy == -1); p->iCopy = i;                                                       }
 
 static inline int            Cba_NtkObjNum( Cba_Ntk_t * p )                  { return Vec_StrSize(&p->vType);                                                              }
-static inline int            Cba_NtkAllocNum( Cba_Ntk_t * p )                { return Vec_StrCap(&p->vType);                                                               }
+static inline int            Cba_NtkObjNumAlloc( Cba_Ntk_t * p )             { return Vec_StrCap(&p->vType);                                                               }
 static inline int            Cba_NtkPiNum( Cba_Ntk_t * p )                   { return Vec_IntSize(&p->vInputs);                                                            }
 static inline int            Cba_NtkPoNum( Cba_Ntk_t * p )                   { return Vec_IntSize(&p->vOutputs);                                                           }
 static inline int            Cba_NtkPioNum( Cba_Ntk_t * p )                  { return Cba_NtkPiNum(p) + Cba_NtkPoNum(p);                                                   }
@@ -207,9 +212,9 @@ static inline Cba_Ntk_t *    Cba_NtkHostNtk( Cba_Ntk_t * p )                 { r
 static inline int            Cba_NtkHostObj( Cba_Ntk_t * p )                 { return p->iBoxObj;                                                                          }
 static inline void           Cba_NtkSetHost( Cba_Ntk_t * p, int n, int i )   { assert(p->iBoxNtk == -1); p->iBoxNtk = n; p->iBoxObj = i;                                   }
 
-static inline void           Cba_NtkStartNames( Cba_Ntk_t * p )              { assert(Cba_NtkAllocNum(p)); Vec_IntFill(&p->vName,  Cba_NtkAllocNum(p),  0);                }
-static inline void           Cba_NtkStartRanges( Cba_Ntk_t * p )             { assert(Cba_NtkAllocNum(p)); Vec_IntFill(&p->vRange, Cba_NtkAllocNum(p),  0);                }
-static inline void           Cba_NtkStartCopies( Cba_Ntk_t * p )             { assert(Cba_NtkAllocNum(p)); Vec_IntFill(&p->vCopy,  Cba_NtkAllocNum(p), -1);                }
+static inline void           Cba_NtkStartNames( Cba_Ntk_t * p )              { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vName,  Cba_NtkObjNumAlloc(p),  0);          }
+static inline void           Cba_NtkStartRanges( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vRange, Cba_NtkObjNumAlloc(p),  0);          }
+static inline void           Cba_NtkStartCopies( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vCopy,  Cba_NtkObjNumAlloc(p), -1);          }
 static inline void           Cba_NtkFreeNames( Cba_Ntk_t * p )               { Vec_IntErase(&p->vName);                                                                    }
 static inline void           Cba_NtkFreeRanges( Cba_Ntk_t * p )              { Vec_IntErase(&p->vRange);                                                                   }
 static inline void           Cba_NtkFreeCopies( Cba_Ntk_t * p )              { Vec_IntErase(&p->vCopy);                                                                    }
@@ -247,8 +252,8 @@ static inline void           Cba_ObjSetName( Cba_Ntk_t * p, int i, int x )   { a
 static inline void           Cba_ObjSetRange( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjRange(p, i) == 0);  Vec_IntWriteEntry( &p->vRange, i, x );                    }
 static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1);  Vec_IntWriteEntry( &p->vCopy,  i, x );                    }
 
-static inline int            Cba_BoxBiNum( Cba_Ntk_t * p, int i )            { int s = i-1; assert(Cba_ObjIsBox(p, i)); while (i < Cba_NtkObjNum(p) && Cba_ObjIsBi(p, --i)); return s - i;         }
-static inline int            Cba_BoxBoNum( Cba_Ntk_t * p, int i )            { int s = i+1; assert(Cba_ObjIsBox(p, i)); while (i < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, ++i)); return i - s;         }
+static inline int            Cba_BoxBiNum( Cba_Ntk_t * p, int i )            { int s = i-1; assert(Cba_ObjIsBox(p, i)); while (--i >= 0               && Cba_ObjIsBi(p, i)); return s - i;  }
+static inline int            Cba_BoxBoNum( Cba_Ntk_t * p, int i )            { int s = i+1; assert(Cba_ObjIsBox(p, i)); while (++i < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, i)); return i - s;  }
 static inline int            Cba_BoxSize( Cba_Ntk_t * p, int i )             { return 1 + Cba_BoxBiNum(p, i) + Cba_BoxBoNum(p, i);                                         }
 static inline int            Cba_BoxBi( Cba_Ntk_t * p, int b, int i )        { assert(Cba_ObjIsBox(p, b)); return b - 1 - i;                                               }
 static inline int            Cba_BoxBo( Cba_Ntk_t * p, int b, int i )        { assert(Cba_ObjIsBox(p, b)); return b + 1 + i;                                               }
@@ -441,7 +446,7 @@ static inline void Cba_NtkDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
     Cba_NtkForEachCo( p, iObj )
         Cba_ObjSetFanin( pNew, Cba_ObjCopy(p, iObj), Cba_ObjCopy(p, Cba_ObjFanin(p, iObj)) );
     //Cba_NtkFreeCopies( p ); // needed for host ntk
-    assert( Cba_NtkObjNum(pNew) == Cba_NtkAllocNum(pNew) );
+    assert( Cba_NtkObjNum(pNew) == Cba_NtkObjNumAlloc(pNew) );
 }
 static inline void Cba_NtkDupUserBoxes( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
 {
@@ -578,6 +583,7 @@ static inline void Cba_ManFree( Cba_Man_t * p )
     Vec_IntErase( &p->vBuf2LeafObj );
     Vec_IntErase( &p->vBuf2RootNtk );
     Vec_IntErase( &p->vBuf2RootObj );
+    Vec_IntErase( &p->vInfo );
     Abc_NamDeref( p->pStrs );
     Abc_NamDeref( p->pMods );
     ABC_FREE( p->pName );
@@ -747,6 +753,9 @@ extern Vec_Ptr_t * Abc_FrameExportPtr();
 extern Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fBuffers, int fVerbose );
 extern Cba_Man_t * Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia );
 extern void *      Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc );
+/*=== cbaCba.c ===============================================================*/
+extern Cba_Man_t * Cba_ManReadCba( char * pFileName );
+extern void        Cba_ManWriteCba( char * pFileName, Cba_Man_t * p );
 /*=== cbaNtk.c ===============================================================*/
 extern void        Cba_ManAssignInternNames( Cba_Man_t * p );
 extern Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p );
@@ -763,6 +772,8 @@ extern void        Prs_ManVecFree( Vec_Ptr_t * vPrs );
 extern Cba_Man_t * Prs_ManBuildCba( char * pFileName, Vec_Ptr_t * vDes );
 /*=== cbaReadBlif.c ==========================================================*/
 extern Vec_Ptr_t * Prs_ManReadBlif( char * pFileName );
+/*=== cbaReadSmt.c ===========================================================*/
+extern Vec_Ptr_t * Prs_ManReadSmt( char * pFileName );
 /*=== cbaReadVer.c ===========================================================*/
 extern Vec_Ptr_t * Prs_ManReadVerilog( char * pFileName );
 /*=== cbaWriteBlif.c =========================================================*/
@@ -772,7 +783,6 @@ extern void        Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p );
 extern void        Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
 extern void        Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p );
 
-
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/base/cba/cbaCba.c b/src/base/cba/cbaCba.c
new file mode 100644
index 00000000..ffa21dff
--- /dev/null
+++ b/src/base/cba/cbaCba.c
@@ -0,0 +1,239 @@
+/**CFile****************************************************************
+
+  FileName    [cbaCba.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Verilog parser.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaCba.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Read CBA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CbaManReadCbaLine( Vec_Str_t * vOut, int * pPos, char * pBuffer, char * pLimit )
+{
+    char c; 
+    while ( (c = Vec_StrEntry(vOut, (*pPos)++)) != '\n' && pBuffer < pLimit )
+        *pBuffer++ = c;
+    *pBuffer = 0;
+    return pBuffer < pLimit;
+}
+int CbaManReadCbaNameAndNums( char * pBuffer, int * Num1, int * Num2, int * Num3 )
+{
+    *Num1 = *Num2 = *Num3 = -1;
+    // read name
+    while ( *pBuffer && *pBuffer != ' ' )
+        pBuffer++;
+    if ( !*pBuffer )
+        return 0;
+    assert( *pBuffer == ' ' );
+    *pBuffer = 0;
+    // read Num1
+    *Num1 = atoi(++pBuffer);
+    while ( *pBuffer && *pBuffer != ' ' )
+        pBuffer++;
+    if ( !*pBuffer )
+        return 0;
+    // read Num2
+    assert( *pBuffer == ' ' );
+    *Num2 = atoi(++pBuffer);
+    while ( *pBuffer && *pBuffer != ' ' )
+        pBuffer++;
+    if ( !*pBuffer )
+        return 1;
+    // read Num3
+    assert( *pBuffer == ' ' );
+    *Num3 = atoi(++pBuffer);
+    return 1;
+}
+void Cba_ManReadCbaVecStr( Vec_Str_t * vOut, int * pPos, Vec_Str_t * p, int nSize )
+{
+    memcpy( Vec_StrArray(p), Vec_StrArray(vOut) + *pPos, nSize );
+    *pPos += nSize;
+    p->nSize = nSize;
+    assert( Vec_StrSize(p) == Vec_StrCap(p) );
+}
+void Cba_ManReadCbaVecInt( Vec_Str_t * vOut, int * pPos, Vec_Int_t * p, int nSize )
+{
+    memcpy( Vec_IntArray(p), Vec_StrArray(vOut) + *pPos, nSize );
+    *pPos += nSize;
+    p->nSize = nSize / 4;
+    assert( Vec_IntSize(p) == Vec_IntCap(p) );
+}
+void Cba_ManReadCbaNtk( Vec_Str_t * vOut, int * pPos, Cba_Ntk_t * pNtk )
+{
+    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vInputs,  4 * Cba_NtkPiNumAlloc(pNtk) );
+    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vOutputs, 4 * Cba_NtkPoNumAlloc(pNtk) );
+    Cba_ManReadCbaVecStr( vOut, pPos, &pNtk->vType,        Cba_NtkObjNumAlloc(pNtk) );
+    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vIndex,   4 * Cba_NtkObjNumAlloc(pNtk) );
+    Cba_ManReadCbaVecInt( vOut, pPos, &pNtk->vFanin,   4 * Cba_NtkObjNumAlloc(pNtk) );
+}
+Cba_Man_t * Cba_ManReadCbaInt( Vec_Str_t * vOut )
+{
+    Cba_Man_t * p;
+    Cba_Ntk_t * pNtk;
+    char Buffer[1000] = "#"; 
+    int i, NameId, Pos = 0, Num1, Num2, Num3;
+    while ( Buffer[0] == '#' )
+        if ( !CbaManReadCbaLine(vOut, &Pos, Buffer, Buffer+1000) )
+            return NULL;
+    if ( !CbaManReadCbaNameAndNums(Buffer, &Num1, &Num2, &Num3) )
+        return NULL;
+    // start manager
+    assert( Num1 > 0 && Num2 >= 0 );
+    p = Cba_ManAlloc( Buffer, Num1 );
+    Vec_IntGrow( &p->vInfo, 4 * Num2 );
+    // start networks
+    Cba_ManForEachNtk( p, pNtk, i )
+    {
+        if ( !CbaManReadCbaLine(vOut, &Pos, Buffer, Buffer+1000) )
+        {
+            Cba_ManFree( p );
+            return NULL;
+        }
+        if ( !CbaManReadCbaNameAndNums(Buffer, &Num1, &Num2, &Num3) )
+        {
+            Cba_ManFree( p );
+            return NULL;
+        }
+        assert( Num1 > 0 && Num2 > 0 && Num3 > 0 );
+        NameId = Abc_NamStrFindOrAdd( p->pStrs, Buffer, NULL );
+        Cba_NtkAlloc( pNtk, NameId, Num1, Num2, Num3 );
+    }
+    // read networks
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_ManReadCbaNtk( vOut, &Pos, pNtk );
+    Cba_ManReadCbaVecInt( vOut, &Pos, &p->vInfo,  4 * Vec_IntSize(&p->vInfo) );
+    assert( Pos == Vec_StrSize(vOut) );
+    return p;
+}
+Cba_Man_t * Cba_ManReadCba( char * pFileName )
+{
+    Cba_Man_t * p;
+    FILE * pFile;
+    Vec_Str_t * vOut;
+    int nFileSize;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    rewind( pFile ); 
+    // load the contents
+    vOut = Vec_StrAlloc( nFileSize );
+    vOut->nSize = vOut->nCap;
+    assert( nFileSize == Vec_StrSize(vOut) );
+    nFileSize = fread( Vec_StrArray(vOut), 1, Vec_StrSize(vOut), pFile );
+    assert( nFileSize == Vec_StrSize(vOut) );
+    fclose( pFile );
+    // read the library
+    p = Cba_ManReadCbaInt( vOut );
+    if ( p != NULL )
+    {
+        ABC_FREE( p->pSpec );
+        p->pSpec = Abc_UtilStrsav( pFileName );
+    }
+    Vec_StrFree( vOut );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write CBA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_ManWriteCbaNtk( Vec_Str_t * vOut, Cba_Ntk_t * pNtk )
+{
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vInputs),  4 * Cba_NtkPiNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vOutputs), 4 * Cba_NtkPoNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_StrArray(&pNtk->vType),        Cba_NtkObjNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vIndex),   4 * Cba_NtkObjNum(pNtk) );
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&pNtk->vFanin),   4 * Cba_NtkObjNum(pNtk) );
+}
+void Cba_ManWriteCbaInt( Vec_Str_t * vOut, Cba_Man_t * p )
+{
+    char Buffer[1000];
+    Cba_Ntk_t * pNtk; int i;
+    sprintf( Buffer, "# Design \"%s\" written by ABC on %s\n", Cba_ManName(p), Extra_TimeStamp() );
+    Vec_StrPrintStr( vOut, Buffer );
+    // write short info
+    sprintf( Buffer, "%s %d %d \n", Cba_ManName(p), Cba_ManNtkNum(p), Cba_ManInfoNum(p) );
+    Vec_StrPrintStr( vOut, Buffer );
+    Cba_ManForEachNtk( p, pNtk, i )
+    {
+        sprintf( Buffer, "%s %d %d %d \n", Cba_NtkName(pNtk), Cba_NtkPiNum(pNtk), Cba_NtkPoNum(pNtk), Cba_NtkObjNum(pNtk) );
+        Vec_StrPrintStr( vOut, Buffer );
+    }
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_ManWriteCbaNtk( vOut, pNtk );
+    Vec_StrPushBuffer( vOut, (char *)Vec_IntArray(&p->vInfo), 16 * Cba_ManInfoNum(p) );
+}
+void Cba_ManWriteCba( char * pFileName, Cba_Man_t * p )
+{
+    Vec_Str_t * vOut;
+    assert( p->pMioLib == NULL );
+    vOut = Vec_StrAlloc( 10000 );
+    Cba_ManWriteCbaInt( vOut, p );
+    if ( Vec_StrSize(vOut) > 0 )
+    {
+        FILE * pFile = fopen( pFileName, "wb" );
+        if ( pFile == NULL )
+            printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        else
+        {
+            fwrite( Vec_StrArray(vOut), 1, Vec_StrSize(vOut), pFile );
+            fclose( pFile );
+        }
+    }
+    Vec_StrFree( vOut );    
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index 73c479d5..9229d876 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -172,7 +172,7 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     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 )) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", ".smt", ".cba", NULL )) )
             Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
         Abc_Print( 1, "\n" );
         return 0;
@@ -207,6 +207,17 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
             p = Prs_ManBuildCba( pFileName, vDes );
         Prs_ManVecFree( vDes );
     }
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" )  )
+    {
+        vDes = Prs_ManReadSmt( pFileName );
+        if ( vDes && Vec_PtrSize(vDes) )
+            p = Prs_ManBuildCba( pFileName, vDes );
+        Prs_ManVecFree( vDes );
+    }
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "cba" )  )
+    {
+        p = Cba_ManReadCba( pFileName );
+    }
     else assert( 0 );
     Cba_AbcUpdateMan( pAbc, p );
     return 0;
@@ -268,6 +279,8 @@ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         Cba_ManWriteBlif( pFileName, p );
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
         Cba_ManWriteVerilog( pFileName, p );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "cba" )  )
+        Cba_ManWriteCba( pFileName, p );
     else 
     {
         printf( "Unrecognized output file extension.\n" );
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index e009f4b1..5189eed5 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -264,7 +264,7 @@ Cba_Man_t * Cba_ManCollapseInt( Cba_Man_t * p )
     assert( Vec_IntSize(vSigs) == Cba_NtkPoNum(pRoot) );
     Cba_NtkForEachPo( pRoot, iObj, i )
         Cba_ObjAlloc( pRootNew, CBA_OBJ_PO, i, Vec_IntEntry(vSigs, i) );
-    assert( Cba_NtkObjNum(pRootNew) == Cba_NtkAllocNum(pRootNew) );
+    assert( Cba_NtkObjNum(pRootNew) == Cba_NtkObjNumAlloc(pRootNew) );
     Vec_IntFree( vSigs );
     // transfer PI/PO names
     Cba_NtkStartNames( pRootNew );
diff --git a/src/base/cba/cbaReadSmt.c b/src/base/cba/cbaReadSmt.c
new file mode 100644
index 00000000..5099e80d
--- /dev/null
+++ b/src/base/cba/cbaReadSmt.c
@@ -0,0 +1,66 @@
+/**CFile****************************************************************
+
+  FileName    [cbaReadSmt.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [BLIF parser.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaReadSmt.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    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Prs_ManReadSmt( char * pFileName )
+{
+    Vec_Ptr_t * vPrs = NULL;
+    Prs_Man_t * p = Prs_ManAlloc( pFileName );
+    if ( p == NULL )
+        return NULL;
+//    Prs_ManReadLines( p );
+    if ( Prs_ManErrorPrint(p) )
+        ABC_SWAP( Vec_Ptr_t *, vPrs, p->vNtks );
+    Prs_ManFree( p );
+    return vPrs;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaWriteSmt.c b/src/base/cba/cbaWriteSmt.c
new file mode 100644
index 00000000..5d1a0a51
--- /dev/null
+++ b/src/base/cba/cbaWriteSmt.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [cbaWriteSmt.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Verilog parser.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaWriteSmt.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/module.make b/src/base/cba/module.make
index 0003e56b..3239be1d 100644
--- a/src/base/cba/module.make
+++ b/src/base/cba/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/base/cba/cbaBlast.c \
+    src/base/cba/cbaCba.c \
     src/base/cba/cbaCom.c \
     src/base/cba/cbaLib.c \
     src/base/cba/cbaNtk.c \
@@ -7,6 +8,8 @@ SRC +=    src/base/cba/cbaBlast.c \
     src/base/cba/cbaPtr.c \
     src/base/cba/cbaPtrAbc.c \
     src/base/cba/cbaReadBlif.c \
+    src/base/cba/cbaReadSmt.c \
     src/base/cba/cbaReadVer.c \
     src/base/cba/cbaWriteBlif.c \
+    src/base/cba/cbaWriteSmt.c \
     src/base/cba/cbaWriteVer.c 
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index b8a8433d..3dd6cfac 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -553,6 +553,13 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
     }
     p->pArray[p->nSize++] = Entry;
 }
+static inline void Vec_StrPushBuffer( Vec_Str_t * p, char * pBuffer, int nSize )
+{
+    if ( p->nSize + nSize > p->nCap )
+        Vec_StrGrow( p, 2 * (p->nSize + nSize) );
+    memcpy( p->pArray + p->nSize, pBuffer, nSize );
+    p->nSize += nSize;
+}
 
 /**Function*************************************************************