Organizing commands for barbuf-aware flow.

11 files changed, 606 insertions, 163 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 70f479ab..5c13efdc 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -66,16 +66,16 @@ typedef enum {
     CBA_NODE_BUF,      // 3:  buffer
     CBA_NODE_INV,      // 4:  inverter
     CBA_NODE_AND,      // 5:  AND
-    CBA_NODE_NAND,     // 6:  NAND
-    CBA_NODE_OR,       // 7:  OR
-    CBA_NODE_NOR,      // 8:  NOR
-    CBA_NODE_XOR,      // 9:  XOR
-    CBA_NODE_XNOR,     // 10  XNOR
-    CBA_NODE_MUX,      // 11: MUX
-    CBA_NODE_MAJ,      // 12: MAJ
-    CBA_NODE_AND00,    // 13: AND00
-    CBA_NODE_AND01,    // 14: AND01
-    CBA_NODE_AND10,    // 15: AND10
+    CBA_NODE_AND00,    // 6:  AND00
+    CBA_NODE_AND01,    // 7:  AND01
+    CBA_NODE_AND10,    // 8:  AND10
+    CBA_NODE_NAND,     // 9:  NAND
+    CBA_NODE_OR,       // 10: OR
+    CBA_NODE_NOR,      // 11: NOR
+    CBA_NODE_XOR,      // 12: XOR
+    CBA_NODE_XNOR,     // 13  XNOR
+    CBA_NODE_MUX,      // 14: MUX
+    CBA_NODE_MAJ,      // 15: MAJ
     CBA_NODE_UNKNOWN   // 16: unknown
 } Cba_NodeType_t; 
 
@@ -130,6 +130,7 @@ struct Cba_Ntk_t_
 
 
 static inline char *         Cba_ManName( Cba_Man_t * p )                    { return p->pName;                                                                            }
+static inline char *         Cba_ManSpec( Cba_Man_t * p )                    { return p->pSpec;                                                                            }
 static inline int            Cba_ManNtkNum( Cba_Man_t * p )                  { return Vec_PtrSize(&p->vNtks) - 1;                                                          }
 static inline int            Cba_ManNtkId( Cba_Man_t * p, char * pName )     { return Abc_NamStrFind(p->pModels, pName);                                                   }
 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);                            }
@@ -145,6 +146,9 @@ static inline int            Cba_NtkObjNum( Cba_Ntk_t * p )                  { r
 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_NtkBoxNum( Cba_Ntk_t * p )                  { return Vec_IntSize(&p->vBoxes);                                                             }
+static inline int            Cba_NtkBoxNumCount( Cba_Ntk_t * p )             { return Vec_IntCountEntry(&p->vTypes, CBA_OBJ_BOX);                                          }
+static inline int            Cba_NtkNodeNum( Cba_Ntk_t * p )                 { return Vec_IntCountEntry(&p->vTypes, CBA_OBJ_NODE);                                         }
+
 static inline int            Cba_NtkPi( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vInputs, i);                                                        }
 static inline int            Cba_NtkPo( Cba_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vOutputs, i);                                                       }
 static inline char *         Cba_NtkStr( Cba_Ntk_t * p, int i )              { return Abc_NamStr(p->pDesign->pNames, i);                                                   }
@@ -263,23 +267,31 @@ static inline int Cba_ManHandleBuffer( Cba_Man_t * p, int iFanin )
     pArray[1] = iFanin;
     return h;
 }
-static inline void Cba_ManSetupArray( Cba_Man_t * p, Vec_Int_t * vTo, Vec_Int_t * vFrom )
+static inline void Cba_ManAllocArray( Cba_Man_t * p, Vec_Int_t * vTo, int nSize )
 {
-    if ( Vec_IntSize(vFrom) == 0 )
+    if ( nSize == 0 )
         return;
-    vTo->nSize = vTo->nCap = Vec_IntSize(vFrom);
-    vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * Vec_IntSize(vFrom) );
-    memcpy( Vec_IntArray(vTo), Vec_IntArray(vFrom), sizeof(int) * Vec_IntSize(vFrom) );
-    Vec_IntClear( vFrom );
+    vTo->nSize  = 0;
+    vTo->nCap   = nSize;
+    vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * nSize );
 }
 static inline void Cba_ManFetchArray( Cba_Man_t * p, Vec_Int_t * vTo, int nSize )
 {
     if ( nSize == 0 )
         return;
-    vTo->nSize = vTo->nCap = nSize;
+    vTo->nSize  = vTo->nCap = nSize;
     vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * nSize );
     memset( Vec_IntArray(vTo), 0xff, sizeof(int) * nSize );
 }
+static inline void Cba_ManSetupArray( Cba_Man_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 *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * Vec_IntSize(vFrom) );
+    memcpy( Vec_IntArray(vTo), Vec_IntArray(vFrom), sizeof(int) * Vec_IntSize(vFrom) );
+    Vec_IntClear( vFrom );
+}
 
 // constructors desctructors
 static inline Cba_Ntk_t * Cba_NtkAlloc( Cba_Man_t * p, char * pName )
@@ -303,37 +315,29 @@ static inline void Cba_NtkResize( Cba_Ntk_t * p, int nObjs )
     Cba_ManFetchArray( p->pDesign, &p->vFanins,  nObjs );
     Cba_ManFetchArray( p->pDesign, &p->vNameIds, nObjs );
 }
-static inline Cba_Man_t * Cba_ManAlloc( char * pFileName )
+static inline Cba_Man_t * Cba_ManAlloc( Cba_Man_t * pOld, char * pFileName )
 {
     Cba_Man_t * p = ABC_CALLOC( Cba_Man_t, 1 );
-    p->pName    = Extra_FileDesignName( pFileName );
-    p->pSpec    = Abc_UtilStrsav( pFileName );
-    p->pNames   = Abc_NamStart( 1000, 24 );
-    p->pModels  = Abc_NamStart( 1000, 24 );
-    p->pFuncs   = Abc_NamStart( 1000, 24 );
-    Vec_SetAlloc_( &p->Mem, 20 );
+    p->pName    = pOld ? Abc_UtilStrsav( Cba_ManName(pOld) ) : Extra_FileDesignName( pFileName );
+    p->pSpec    = pOld ? Abc_UtilStrsav( Cba_ManSpec(pOld) ) : Abc_UtilStrsav( pFileName );
+    p->pNames   = pOld ? Abc_NamRef( pOld->pNames )  : Abc_NamStart( 1000, 24 );
+    p->pModels  = pOld ? Abc_NamRef( pOld->pModels ) : Abc_NamStart( 1000, 24 );
+    p->pFuncs   = pOld ? Abc_NamRef( pOld->pFuncs )  : Abc_NamStart( 1000, 24 );
+    p->iRoot    = 1;
+    Vec_SetAlloc_( &p->Mem, 18 );
     Vec_PtrPush( &p->vNtks, NULL );
-    p->iRoot = 1;
     return p;
 }
 static inline Cba_Man_t * Cba_ManClone( Cba_Man_t * pOld )
 {
     Cba_Ntk_t * pNtk, * pNtkNew; int i;
-    Cba_Man_t * p = ABC_CALLOC( Cba_Man_t, 1 );
-    p->pName    = Extra_FileDesignName( pOld->pName );
-    p->pSpec    = Abc_UtilStrsav( pOld->pSpec );
-    p->pNames   = Abc_NamRef( pOld->pNames );
-    p->pModels  = Abc_NamRef( pOld->pModels );
-    p->pFuncs   = Abc_NamRef( pOld->pFuncs );
-    p->iRoot    = 1;
-    Vec_SetAlloc_( &p->Mem, 20 );
-    Vec_PtrPush( &p->vNtks, NULL );
+    Cba_Man_t * p = Cba_ManAlloc( pOld, NULL );
     Cba_ManForEachNtk( pOld, pNtk, i )
     {
         pNtkNew = Cba_NtkAlloc( p, Cba_NtkName(pNtk) );
         Cba_ManFetchArray( p, &pNtkNew->vInputs,  Cba_NtkPiNum(pNtk) );
         Cba_ManFetchArray( p, &pNtkNew->vOutputs, Cba_NtkPoNum(pNtk) );
-        Cba_ManFetchArray( p, &pNtkNew->vBoxes,   Cba_NtkBoxNum(pNtk) );
+        Cba_ManFetchArray( p, &pNtkNew->vBoxes,   Cba_NtkBoxNumCount(pNtk) );
         Vec_IntShrink( &pNtkNew->vBoxes, 0 );
     }
     assert( Cba_ManNtkNum(p) == Cba_ManNtkNum(pOld) );
@@ -367,6 +371,26 @@ static inline int Cba_ManMemory( Cba_Man_t * p )
     return nMem;
 }
 
+static inline Cba_NtkPrintStats( Cba_Ntk_t * p )
+{
+    printf( "%-32s ",      Cba_NtkName(p) );
+    printf( "pi =%5d  ",   Cba_NtkPiNum(p) );
+    printf( "pi =%5d  ",   Cba_NtkPoNum(p) );
+    printf( "box =%6d  ",  Cba_NtkBoxNum(p) );
+    printf( "node =%6d  ", Cba_NtkNodeNum(p) );
+    printf( "obj =%6d  ",  Cba_NtkObjNum(p) );
+    printf( "\n" );
+}
+static inline Cba_ManPrintStats( Cba_Man_t * p, int fVerbose )
+{
+    Cba_Ntk_t * pNtk; int i;
+    Cba_ManForEachNtk( p, pNtk, i )
+    {
+        printf( "Module %4d : ", i );
+        Cba_NtkPrintStats( pNtk );
+    }
+}
+   
 static inline Cba_NodeType_t Ptr_SopToType( char * pSop )
 {
     if ( !strcmp(pSop, " 1\n") )         return CBA_NODE_C0;
@@ -397,9 +421,13 @@ static inline char * Ptr_TypeToName( Cba_NodeType_t Type )
     if ( Type == CBA_NODE_AND00 ) return "and00";
     if ( Type == CBA_NODE_AND01 ) return "and01";
     if ( Type == CBA_NODE_AND10 ) return "and10";
+    if ( Type == CBA_NODE_NAND )  return "nand";
     if ( Type == CBA_NODE_OR )    return "or";
+    if ( Type == CBA_NODE_NOR )   return "nor";
     if ( Type == CBA_NODE_XOR )   return "xor";
     if ( Type == CBA_NODE_XNOR )  return "xnor";
+    if ( Type == CBA_NODE_MUX )   return "mux";
+    if ( Type == CBA_NODE_MAJ )   return "maj";
     assert( 0 );
     return "???";
 }
@@ -413,13 +441,22 @@ static inline char * Ptr_TypeToSop( Cba_NodeType_t Type )
     if ( Type == CBA_NODE_AND00 ) return "00 1\n";
     if ( Type == CBA_NODE_AND01 ) return "01 1\n";
     if ( Type == CBA_NODE_AND10 ) return "10 1\n";
+    if ( Type == CBA_NODE_NAND )  return "11 0\n";
     if ( Type == CBA_NODE_OR )    return "00 0\n";
+    if ( Type == CBA_NODE_NOR )   return "00 1\n";
     if ( Type == CBA_NODE_XOR )   return "01 1\n10 1\n";
     if ( Type == CBA_NODE_XNOR )  return "00 1\n11 1\n";
+    if ( Type == CBA_NODE_MUX )   return "11- 1\n0-1 1\n";
+    if ( Type == CBA_NODE_MAJ )   return "11- 1\n1-1 1\n-11 1\n";
     assert( 0 );
     return "???";
 }
 
+
+/*=== cbaBlast.c =========================================================*/
+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 );
 /*=== cbaBuild.c =========================================================*/
 extern Cba_Man_t * Cba_ManBuild( Cba_Man_t * p );
 /*=== cbaReadBlif.c =========================================================*/
@@ -431,13 +468,16 @@ extern void        Cba_PrsWriteBlif( char * pFileName, Cba_Man_t * p );
 extern void        Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p );
 /*=== cbaWriteVer.c =========================================================*/
 extern void        Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p );
+extern void        Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p );
 /*=== cbaNtk.c =========================================================*/
 extern void        Cba_ManAssignInternNames( Cba_Man_t * p );
 extern int         Cba_NtkNodeNum( Cba_Ntk_t * p );
 extern int         Cba_ManObjNum( Cba_Man_t * p );
 extern Cba_Man_t * Cba_ManDupStart( Cba_Man_t * p, Vec_Int_t * vNtkSizes );
 extern Cba_Man_t * Cba_ManDup( Cba_Man_t * p );
-
+/*=== cbaSimple.c =========================================================*/
+extern Cba_Man_t * Cba_PrsReadPtr( Vec_Ptr_t * vDes );
+extern void        Ptr_ManFreeDes( Vec_Ptr_t * vDes );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index 25476f43..808f3035 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -63,26 +63,28 @@ int Cba_ManAddBarbuf( Gia_Man_t * pNew, int iRes, Cba_Man_t * p, int iLNtk, int
     }
     return iBufLit;
 }
-int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, Vec_Int_t * vMap )
+int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, int fBuffers, Vec_Int_t * vMap )
 {
     int iRes = Cba_NtkCopy( p, i );
     if ( iRes >= 0 )
         return iRes;
     if ( Cba_ObjIsCo(p, i) )
-        iRes = Cba_ManExtract_rec( pNew, p, Cba_ObjFanin0(p, i), vMap );
+        iRes = Cba_ManExtract_rec( pNew, p, Cba_ObjFanin0(p, i), fBuffers, vMap );
     else if ( Cba_ObjIsBo(p, i) )
     {
         Cba_Ntk_t * pBox = Cba_ObjBoModel( p, i );
         int iObj = Cba_NtkPo( pBox, Cba_ObjCioIndex(p, i) );
-        iRes = Cba_ManExtract_rec( pNew, pBox, iObj, vMap );
-        iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pBox), iObj, vMap );
+        iRes = Cba_ManExtract_rec( pNew, pBox, iObj, fBuffers, vMap );
+        if ( fBuffers )
+            iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pBox), iObj, vMap );
     }
     else if ( Cba_ObjIsPi(p, i) )
     {
         Cba_Ntk_t * pHost = Cba_NtkHostNtk( p );
         int iObj = Cba_ObjBoxBi( pHost, Cba_NtkHostObj(p), Cba_ObjCioIndex(p, i) );
-        iRes = Cba_ManExtract_rec( pNew, pHost, iObj, vMap );
-        iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pHost), iObj, vMap );
+        iRes = Cba_ManExtract_rec( pNew, pHost, iObj, fBuffers, vMap );
+        if ( fBuffers )
+            iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pHost), iObj, vMap );
     }
     else if ( Cba_ObjIsNode(p, i) )
     {
@@ -100,15 +102,15 @@ int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, Vec_Int_t * vMap
         else if ( pFanins[0] == 1 )
         {
             if ( Type == CBA_NODE_BUF )
-                iRes = Cba_ManExtract_rec( pNew, p, pFanins[1], vMap );
+                iRes = Cba_ManExtract_rec( pNew, p, pFanins[1], fBuffers, vMap );
             else if ( Type == CBA_NODE_INV )
-                iRes = Abc_LitNot( Cba_ManExtract_rec( pNew, p, pFanins[1], vMap ) );
+                iRes = Abc_LitNot( Cba_ManExtract_rec( pNew, p, pFanins[1], fBuffers, vMap ) );
             else assert( 0 );
         }
         else
         {
             for ( k = 0; k < pFanins[0]; k++ )
-                pLits[k] = Cba_ManExtract_rec( pNew, p, pFanins[k+1], vMap );
+                pLits[k] = Cba_ManExtract_rec( pNew, p, pFanins[k+1], fBuffers, vMap );
             if ( Type == CBA_NODE_AND )
                 iRes = Gia_ManHashAnd( pNew, pLits[0], pLits[1] );
             else if ( Type == CBA_NODE_OR )
@@ -124,7 +126,7 @@ int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, Vec_Int_t * vMap
     Cba_NtkSetCopy( p, i, iRes );
     return iRes;
 }
-Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fVerbose )
+Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fBuffers, int fVerbose )
 {
     Cba_Ntk_t * pRoot = Cba_ManRoot(p);
     Gia_Man_t * pNew, * pTemp; 
@@ -154,7 +156,7 @@ Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fVerbose )
     pNew->vBarBufs = Vec_IntAlloc( 10000 );
     vMap = Vec_IntStartFull( 10000 );
     Cba_NtkForEachPo( pRoot, iObj, i )
-        Cba_ManExtract_rec( pNew, pRoot, iObj, vMap );
+        Cba_ManExtract_rec( pNew, pRoot, iObj, fBuffers, vMap );
     Vec_IntFreeP( &vMap );
     Gia_ManHashStop( pNew );
 
@@ -166,7 +168,7 @@ Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fVerbose )
     // cleanup
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
-    Gia_ManPrintStats( pNew, NULL );
+    //Gia_ManPrintStats( pNew, NULL );
     return pNew;
 }
 
@@ -347,7 +349,7 @@ Cba_Man_t * Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia )
 ***********************************************************************/
 Cba_Man_t * Cba_ManBlastTest( Cba_Man_t * p )
 {
-    Gia_Man_t * pGia = Cba_ManExtract( p, 0 );
+    Gia_Man_t * pGia = Cba_ManExtract( p, 1, 0 );
     Cba_Man_t * pNew = Cba_ManInsertGia( p, pGia );
     Gia_ManStop( pGia );
     Cba_ManAssignInternNames( pNew );
@@ -355,6 +357,26 @@ Cba_Man_t * Cba_ManBlastTest( Cba_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc )
+{
+    Abc_Ntk_t * pNtk = pAbc;
+    Cba_Man_t * pNew = NULL;
+    return pNew;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cba/cbaBuild.c b/src/base/cba/cbaBuild.c
index b353e8f6..ddacc409 100644
--- a/src/base/cba/cbaBuild.c
+++ b/src/base/cba/cbaBuild.c
@@ -204,7 +204,6 @@ Cba_Ntk_t * Cba_NtkBuild( Cba_Man_t * pNew, Cba_Ntk_t * pNtk, Vec_Int_t * vMap,
         {
             ObjId = Vec_IntEntry( &pNtkNew->vBoxes, nBoxes++ );
             pNtkBox = Cba_ObjBoxModel( pNtk, iObj );
-            Cba_NtkSetHost( pNtkBox, Cba_NtkId(pNtk), ObjId );
             // collect fanins
             Vec_IntFill( vTemp, Cba_NtkPiNum(pNtkBox), -1 );
             Vec_IntForEachEntry( vFanins, Index, i )
@@ -227,6 +226,7 @@ Cba_Ntk_t * Cba_NtkBuild( Cba_Man_t * pNew, Cba_Ntk_t * pNtk, Vec_Int_t * vMap,
             // create box
             Vec_IntWriteEntry( &pNtkNew->vTypes,  ObjId, CBA_OBJ_BOX );
             Vec_IntWriteEntry( &pNtkNew->vFuncs,  ObjId, Cba_ManNtkId(pNew, Cba_NtkName(pNtkBox)) );
+            Cba_NtkSetHost( Cba_ObjBoxModel(pNtkNew, ObjId), Cba_NtkId(pNtkNew), ObjId );
             // create box inputs
             Cba_BoxForEachBi( pNtkNew, ObjId, FaninId, i )
             {
@@ -311,7 +311,8 @@ Cba_Man_t * Cba_ManBuild( Cba_Man_t * p )
     Vec_Int_t * vMap   = Vec_IntStartFull( Abc_NamObjNumMax(p->pNames) + 1 );
     Vec_Int_t * vNonDr = Vec_IntAlloc( 1000 );
     Vec_Int_t * vTemp  = Vec_IntAlloc( 1000 );
-    Cba_Ntk_t * pNtk; int i, nObjs;
+    Cba_Ntk_t * pNtk;  
+    int i, nObjs;
     assert( Abc_NamObjNumMax(p->pModels) == Cba_ManNtkNum(p) + 1 );
     Cba_ManForEachNtk( p, pNtk, i )
     {
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index 94eb4b88..05f4dfe6 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "cba.h"
+#include "proof/cec/cec.h"
 #include "base/main/mainInt.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -30,12 +31,14 @@ ABC_NAMESPACE_IMPL_START
 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_CommandPut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Cba_CommandCec      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Cba_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-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->pAbcCba ) Cba_ManFree(Cba_NtkMan(Cba_AbcGetNtk(pAbc)));  }
-static inline void        Cba_AbcUpdateNtk( Abc_Frame_t * pAbc, Cba_Ntk_t * pNtk )  { Cba_AbcFreeNtk(pAbc); pAbc->pAbcCba = pNtk;                         }
+static inline Cba_Man_t * Cba_AbcGetMan( Abc_Frame_t * pAbc )                       { return (Cba_Man_t *)pAbc->pAbcCba;                        }
+static inline void        Cba_AbcFreeMan( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcCba ) Cba_ManFree(Cba_AbcGetMan(pAbc));    }
+static inline void        Cba_AbcUpdateMan( Abc_Frame_t * pAbc, Cba_Man_t * p )     { Cba_AbcFreeMan(pAbc); pAbc->pAbcCba = p;                  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,7 +60,9 @@ 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", "@put",        Cba_CommandPut,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@get",        Cba_CommandGet,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@cec",        Cba_CommandCec,       0 );
     Cmd_CommandAdd( pAbc, "New word level", "@test",       Cba_CommandTest,      0 );
 }
 
@@ -74,7 +79,7 @@ void Cba_Init( Abc_Frame_t * pAbc )
 ******************************************************************************/
 void Cba_End( Abc_Frame_t * pAbc )
 {
-    Cba_AbcFreeNtk( pAbc );
+    Cba_AbcFreeMan( pAbc );
 }
 
 
@@ -92,14 +97,17 @@ void Cba_End( Abc_Frame_t * pAbc )
 int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pFile;
-    Cba_Ntk_t * pNtk = NULL;
+    Cba_Man_t * p = NULL, * pTemp;
     char * pFileName = NULL;
-    int c, fVerbose  =    0;
+    int c, fUseAbc = 0, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fUseAbc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -127,12 +135,30 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // perform reading
-    //pNtk = Cba_ReadVer( pFileName );
-    Cba_AbcUpdateNtk( pAbc, pNtk );
+    if ( fUseAbc )
+    {
+        extern Vec_Ptr_t * Ptr_AbcDeriveDes( Abc_Ntk_t * pNtk );
+        Abc_Ntk_t * pAbcNtk = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), 0 );
+        Vec_Ptr_t * vDes = Ptr_AbcDeriveDes( pAbcNtk );
+        p = Cba_PrsReadPtr( vDes );
+        ABC_FREE( p->pSpec );
+        p->pSpec = Abc_UtilStrsav( pAbcNtk->pSpec );
+        Abc_NtkDelete( pAbcNtk );
+        Ptr_ManFreeDes( vDes ); // points to names in pAbcNtk
+    }
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" )  )
+        p = Cba_PrsReadBlif( pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+        p = Cba_PrsReadVerilog( pFileName );
+    else assert( 0 );
+    p = Cba_ManBuild( pTemp = p );
+    Cba_ManFree( pTemp );
+    Cba_AbcUpdateMan( pAbc, p );
     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, "usage: @read [-avh] <file_name>\n" );
+    Abc_Print( -2, "\t         reads hierarchical design in BLIF or Verilog\n" );
+    Abc_Print( -2, "\t-a     : toggle using old ABC parser [default = %s]\n", fUseAbc? "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;
@@ -151,7 +177,7 @@ usage:
 ******************************************************************************/
 int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
+    Cba_Man_t * p = Cba_AbcGetMan(pAbc);
     char * pFileName = NULL;
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
@@ -168,26 +194,35 @@ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( p == NULL )
     {
         Abc_Print( 1, "Cba_CommandWrite(): There is no current design.\n" );
         return 0;
     }
-    if ( argc == globalUtilOptind )
-        pFileName = Extra_FileNameGenericAppend( Cba_NtkMan(pNtk)->pName, "_out.v" );
-    else if ( argc == globalUtilOptind + 1 )
+    if ( argc == globalUtilOptind + 1 )
         pFileName = argv[globalUtilOptind];
-    else
+    else if ( argc == globalUtilOptind && p )
+        pFileName = Extra_FileNameGenericAppend( Cba_ManName(p), "_out.v" );
+    else 
     {
         printf( "Output file name should be given on the command line.\n" );
         return 0;
     }
-    //Cba_WriteVer( pNtk, pFileName );
+    // perform writing
+    if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" )  )
+        Cba_ManWriteBlif( pFileName, p );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+        Cba_ManWriteVerilog( pFileName, p );
+    else 
+    {
+        printf( "Unrecognized output file extension.\n" );
+        return 0;
+    }
     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         writes the design into a file in BLIF or Verilog\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;
 }
@@ -206,7 +241,7 @@ usage:
 ******************************************************************************/
 int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
+    Cba_Man_t * p = Cba_AbcGetMan(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -222,12 +257,12 @@ int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( p == NULL )
     {
         Abc_Print( 1, "Cba_CommandPs(): There is no current design.\n" );
         return 0;
     }
-//    Cba_NtkPrintStats( pNtk, fDistrib, fVerbose );
+    Cba_ManPrintStats( p, fVerbose );
     return 0;
 usage:
     Abc_Print( -2, "usage: @ps [-vh]\n" );
@@ -248,19 +283,68 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
-int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cba_Man_t * p = Cba_AbcGetMan(pAbc);
+    Gia_Man_t * pGia = NULL;
+    int c, 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 ( p == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandPut(): There is no current design.\n" );
+        return 0;
+    }
+    pGia = Cba_ManExtract( p, 1, 0 );
+    if ( pGia == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandPut(): Conversion to AIG has failed.\n" );
+        return 0;
+    }
+    Abc_FrameUpdateGia( pAbc, pGia );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @put [-mvh]\n" );
+    Abc_Print( -2, "\t         extracts AIG with barrier buffers from the hierarchical design\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_CommandGet( 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;
+    Cba_Man_t * pNew, * p = Cba_AbcGetMan(pAbc);
+    int c, fMapped = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'm':
-            fMulti ^= 1;
+            fMapped ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -271,31 +355,148 @@ int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Cba_CommandGet(): There is no current design.\n" );
+        return 0;
+    }
+    if ( fMapped )
+    {
+        if ( pAbc->pNtkCur == NULL )
+        {
+            Abc_Print( 1, "Cba_CommandGet(): There is no current mapped design.\n" );
+            return 0;
+        }
+        pNew = Cba_ManInsertAbc( p, pAbc->pNtkCur );
+    }
+    else
+    {
+        if ( pAbc->pGia == NULL )
+        {
+            Abc_Print( 1, "Cba_CommandGet(): There is no current AIG.\n" );
+            return 0;
+        }
+        pNew = Cba_ManInsertGia( p, pAbc->pGia );
+    }
+    Cba_AbcUpdateMan( pAbc, pNew );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @get [-mvh]\n" );
+    Abc_Print( -2, "\t         extracts AIG or mapped network into the hierarchical design\n" );
+    Abc_Print( -2, "\t-m     : toggle using mapped network from main-space [default = %s]\n", fMapped? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cba_Man_t * pTemp, * p = Cba_AbcGetMan(pAbc);
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    Gia_Man_t * pFirst, * pSecond, * pMiter;
+    char * FileName, * pStr, ** pArgvNew;
+    int c, nArgcNew, fDumpMiter = 0, fVerbose  = 0;
+    FILE * pFile;
+    Cec_ManCecSetDefaultParams( pPars );
+    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 ( p == NULL )
     {
-        Abc_Print( 1, "Cba_CommandBlast(): There is no current design.\n" );
+        Abc_Print( 1, "Cba_CommandCec(): There is no current design.\n" );
         return 0;
     }
-    if ( fMulti )
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
     {
-//        vBoxIds = Cba_NtkCollectMultipliers( pNtk );
-//        if ( vBoxIds == NULL )
-//            Abc_Print( 1, "Warning:  There is no multipliers in the design.\n" );
+        if ( p->pSpec == NULL )
+        {
+            Abc_Print( -1, "File name is not given on the command line.\n" );
+            return 1;
+        }
+        FileName = p->pSpec;
+    }
+    else
+        FileName = pArgvNew[0];
+    // fix the wrong symbol
+    for ( pStr = FileName; *pStr; pStr++ )
+        if ( *pStr == '>' )
+            *pStr = '\\';
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".v", ".blif", NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+        Abc_Print( 1, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+    // extract AIG from the current design
+    pFirst = Cba_ManExtract( p, 0, 0 );
+    if ( pFirst == NULL )
+    {
+        Abc_Print( -1, "Extracting AIG from the current design has failed.\n" );
+        return 0;
     }
-    // transform
-//    pNew = Cba_NtkBitBlast( pNtk, vBoxIds );
-//    Vec_IntFreeP( &vBoxIds );
-    if ( pNew == NULL )
+    // extract AIG from the second design
+    if ( !strcmp( Extra_FileNameExtension(FileName), "blif" )  )
+        p = Cba_PrsReadBlif( FileName );
+    else if ( !strcmp( Extra_FileNameExtension(FileName), "v" )  )
+        p = Cba_PrsReadVerilog( FileName );
+    else assert( 0 );
+    p = Cba_ManBuild( pTemp = p );
+    Cba_ManFree( pTemp );
+    pSecond = Cba_ManExtract( p, 0, 0 );
+    Cba_ManFree( p );
+    if ( pSecond == NULL )
     {
-        Abc_Print( 1, "Cba_CommandBlast(): Bit-blasting has failed.\n" );
+        Gia_ManStop( pFirst );
+        Abc_Print( -1, "Extracting AIG from the original design has failed.\n" );
         return 0;
     }
-    Abc_FrameUpdateGia( pAbc, pNew );
+    // compute the miter
+    pMiter = Gia_ManMiter( pFirst, pSecond, 0, 1, 0, 0, pPars->fVerbose );
+    if ( pMiter )
+    {
+        int fDumpMiter = 0;
+        if ( fDumpMiter )
+        {
+            Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+        }
+        pAbc->Status = Cec_ManVerify( pMiter, pPars );
+        //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
+        Gia_ManStop( pMiter );
+    }
+    Gia_ManStop( pFirst );
+    Gia_ManStop( pSecond );
     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, "usage: @cec [-vh]\n" );
+    Abc_Print( -2, "\t         combinational equivalence checking for the hierarchical design\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;
@@ -314,12 +515,7 @@ usage:
 ******************************************************************************/
 int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Cba_ManReadDesExperiment( Abc_Ntk_t * pNtk );
-    Abc_Ntk_t * pAbcNtk;
-    //Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc);
-//    char * pFileName = "c/hie/dump/1/netlist_1.v";
-//    char * pFileName = "c/hie/dump/3/netlist_18.v";
-    char * pFileName = "c/hie/dump/1/netlist_0.v";
+    extern void Cba_PrsReadVerilogTest( char * pFileName );
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -342,10 +538,7 @@ int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 */
-    // transform
-    pAbcNtk = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), 0 );
-    Cba_ManReadDesExperiment( pAbcNtk );
-    Abc_NtkDelete( pAbcNtk );
+    Cba_PrsReadVerilogTest( NULL );
     return 0;
 usage:
     Abc_Print( -2, "usage: @test [-vh]\n" );
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 13949606..af48f227 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -74,13 +74,6 @@ void Cba_ManAssignInternNames( Cba_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cba_NtkNodeNum( Cba_Ntk_t * p )
-{ 
-    int iObj, Count = 0;
-    Cba_NtkForEachNode( p, iObj )
-        Count++;
-    return Count;
-}
 int Cba_ManObjNum( Cba_Man_t * p )
 {
     Cba_Ntk_t * pNtk; 
@@ -136,6 +129,9 @@ void Cba_NtkDupStart( Cba_Ntk_t * pNew, Cba_Ntk_t * p )
         Cba_ObjDupStart( pNew, p, iObj );
         Cba_BoxForEachBo( p, iObj, iTerm, k )
             Cba_ObjDupStart( pNew, p, iTerm );
+        // connect box outputs to boxes
+        Cba_BoxForEachBo( p, iObj, iTerm, k )
+            Vec_IntWriteEntry( &pNew->vFanins, Cba_NtkCopy(p, iTerm), Cba_NtkCopy(p, Cba_ObjFanin0(p, iTerm)) );
     }
     assert( Cba_NtkBoxNum(p) == Cba_NtkBoxNum(pNew) );
 }
@@ -174,10 +170,11 @@ void Cba_NtkDupNodes( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vTemp )
     // connect
     Cba_NtkForEachObjType( p, Type, i )
     {
-        if ( Type == CBA_OBJ_PI || Type == CBA_OBJ_BOX )
+        if ( Type == CBA_OBJ_PI || Type == CBA_OBJ_BOX || Type == CBA_OBJ_BO )
             continue;
-        if ( Type == CBA_OBJ_PO || Type == CBA_OBJ_BI || Type == CBA_OBJ_BO )
+        if ( Type == CBA_OBJ_PO || Type == CBA_OBJ_BI )
         {
+            assert( Vec_IntEntry(&pNew->vFanins, Cba_NtkCopy(p, i)) == -1 );
             Vec_IntWriteEntry( &pNew->vFanins, Cba_NtkCopy(p, i), Cba_NtkCopy(p, Cba_ObjFanin0(p, i)) );
             continue;
         }
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
index 3715935e..12a2c065 100644
--- a/src/base/cba/cbaPrs.h
+++ b/src/base/cba/cbaPrs.h
@@ -168,7 +168,7 @@ static inline Cba_Prs_t * Cba_PrsAlloc( char * pFileName )
     p->pBuffer = pBuffer;
     p->pLimit  = pLimit;
     p->pCur    = pBuffer;
-    p->pDesign = Cba_ManAlloc( pFileName );
+    p->pDesign = Cba_ManAlloc( NULL, pFileName );
     return p;
 }
 static inline void Cba_PrsFree( Cba_Prs_t * p )
@@ -195,6 +195,20 @@ static inline void Cba_PrsFree( Cba_Prs_t * p )
     ABC_FREE( p->pBuffer );
     ABC_FREE( p );
 }
+static inline void Cba_PrsRemapBoxModels( Cba_Man_t * p )
+{
+    Cba_Ntk_t * pNtk; 
+    int i, Type, iObj;
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_NtkForEachObjType( pNtk, Type, iObj )
+            if ( Type == CBA_OBJ_BOX )
+            {
+                char * pName = Abc_NamStr( p->pNames, Cba_ObjFuncId(pNtk, iObj) );
+                int iModelId = Abc_NamStrFind( p->pModels, pName );
+                assert( iModelId > 0 );
+                Vec_IntWriteEntry( &pNtk->vFuncs, iObj, iModelId );
+            }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///
diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c
index 08152075..83ec12f5 100644
--- a/src/base/cba/cbaReadBlif.c
+++ b/src/base/cba/cbaReadBlif.c
@@ -64,9 +64,9 @@ static inline void Cba_PrsAddBlifDirectives( Cba_Prs_t * p )
     for ( i = 1; s_BlifTypes[i]; i++ )
         Abc_NamStrFindOrAdd( p->pDesign->pNames, (char *)s_BlifTypes[i],   NULL );
     assert( Abc_NamObjNumMax(p->pDesign->pNames) == i );
-    Abc_NamStrFindOrAdd( p->pDesign->pFuncs, (char *)" 0\n",   NULL );  // default const 0 function
-    Abc_NamStrFindOrAdd( p->pDesign->pFuncs, (char *)"1 1\n",   NULL ); // default buffer function
-    assert( Abc_NamObjNumMax(p->pDesign->pFuncs) == 3 );
+    for ( i = 1; i < CBA_NODE_UNKNOWN; i++ )
+        Abc_NamStrFindOrAdd( p->pDesign->pFuncs, Ptr_TypeToSop(i),   NULL );
+    assert( Abc_NamObjNumMax(p->pDesign->pFuncs) == i-1 );
 }
 
 
@@ -408,6 +408,7 @@ Cba_Man_t * Cba_PrsReadBlif( char * pFileName )
     if ( Cba_PrsErrorPrint(p) )
         ABC_SWAP( Cba_Man_t *, pDesign, p->pDesign );
     Cba_PrsFree( p );
+    Cba_PrsRemapBoxModels( pDesign );
     return pDesign;
 }
 
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index c5718dc1..714830ab 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -80,7 +80,7 @@ static inline int Cba_IsChar( char c )    { return (c >= 'a' && c <= 'z') || (c
 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_PrsIsChar( Cba_Prs_t * p, char c )    { return *p->pCur == c;                          }
+static inline int Cba_PrsIsChar( Cba_Prs_t * p, char c )    { return p->pCur[0] == c;                        }
 static inline int Cba_PrsIsChar1( Cba_Prs_t * p, char c )   { return p->pCur[1] == c;                        }
 static inline int Cba_PrsIsDigit( Cba_Prs_t * p )           { return Cba_IsDigit(*p->pCur);                  }
 
@@ -720,6 +720,7 @@ Cba_Man_t * Cba_PrsReadVerilog( char * pFileName )
     if ( Cba_PrsErrorPrint(p) )
         ABC_SWAP( Cba_Man_t *, pDesign, p->pDesign );
     Cba_PrsFree( p );
+    Cba_PrsRemapBoxModels( pDesign );
     return pDesign;
 }
 
@@ -727,18 +728,18 @@ void Cba_PrsReadVerilogTest( char * pFileName )
 {
     abctime clk = Abc_Clock();
     extern void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p );
-//    Cba_Man_t * p = Cba_PrsReadVerilog( "c/hie/dump/1/netlist_1.v" );
+    Cba_Man_t * p = Cba_PrsReadVerilog( "c/hie/dump/1/netlist_1.v" );
 //    Cba_Man_t * p = Cba_PrsReadVerilog( "aga/me/me_wide.v" );
-    Cba_Man_t * p = Cba_PrsReadVerilog( "aga/ray/ray_wide.v" );
+//    Cba_Man_t * p = Cba_PrsReadVerilog( "aga/ray/ray_wide.v" );
     if ( !p ) return;
     printf( "Finished reading %d networks. ", Cba_ManNtkNum(p) );
     printf( "NameIDs = %d. ", Abc_NamObjNumMax(p->pNames) );
     printf( "Memory = %.2f MB. ", 1.0*Cba_ManMemory(p)/(1<<20) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 //    Abc_NamPrint( p->pDesign->pNames );
-//    Cba_PrsWriteVerilog( "c/hie/dump/1/netlist_1_out.v", p );
+    Cba_PrsWriteVerilog( "c/hie/dump/1/netlist_1_out.v", p );
 //    Cba_PrsWriteVerilog( "aga/me/me_wide_out.v", p );
-    Cba_PrsWriteVerilog( "aga/ray/ray_wide_out.v", p );
+//    Cba_PrsWriteVerilog( "aga/ray/ray_wide_out.v", p );
     Cba_ManFree( p );
 }
 
diff --git a/src/base/cba/cbaSimple.c b/src/base/cba/cbaSimple.c
index 7d363be9..7fe6cb0a 100644
--- a/src/base/cba/cbaSimple.c
+++ b/src/base/cba/cbaSimple.c
@@ -60,6 +60,8 @@ Cba_NodeType_t Ptr_HopToType( Abc_Obj_t * pObj )
     };
     assert( Abc_ObjIsNode(pObj) );
     uTruth = Hop_ManComputeTruth6( (Hop_Man_t *)Abc_ObjNtk(pObj)->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj) );
+    if ( uTruth ==  0 )                           return CBA_NODE_C0;
+    if ( uTruth == ~(word)0 )                     return CBA_NODE_C1;
     if ( uTruth ==  uTruths6[0] )                 return CBA_NODE_BUF;
     if ( uTruth == ~uTruths6[0] )                 return CBA_NODE_INV;
     if ( uTruth == (uTruths6[0] & uTruths6[1]) )  return CBA_NODE_AND;
@@ -107,7 +109,11 @@ Vec_Ptr_t * Ptr_AbcDeriveNode( Abc_Obj_t * pObj )
     Vec_Ptr_t * vNode = Vec_PtrAlloc( 2 + Abc_ObjFaninNum(pObj) );
     assert( Abc_ObjIsNode(pObj) );
     Vec_PtrPush( vNode, Ptr_AbcObjName(pObj) );
-    Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_HopToType(pObj)) );
+    if ( Abc_NtkHasAig(pObj->pNtk) )
+        Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_HopToType(pObj)) );
+    else if ( Abc_NtkHasSop(pObj->pNtk) )
+        Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_SopToType((char *)pObj->pData)) );
+    else assert( 0 );
     Abc_ObjForEachFanin( pObj, pFanin, i )
         Vec_PtrPush( vNode, Ptr_AbcObjName(pFanin) );
     assert( Ptr_CheckArray(vNode) );
@@ -601,47 +607,36 @@ void Cba_PrsReadBoxes( Cba_Man_t * p, Vec_Ptr_t * vBoxes, Vec_Int_t * vTypesCur,
         Vec_IntPush( vFaninsCur,  Cba_ManHandleArray(p, Cba_PrsReadList(p, vBox, vList, 0, 1)) ); 
     }
 }
-void Cba_PrsReadModule( Cba_Man_t * p, Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk )   
-{
-    Vec_Int_t * vInputsCur  = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vOutputsCur = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vTypesCur   = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vFuncsCur   = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vInstIdsCur = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vFaninsCur  = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vList       = Vec_IntAlloc( 1000 );
-    Vec_Int_t * vBoxes      = Vec_IntStart( Vec_PtrSize((Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4)) );
-
-    Cba_PrsReadList( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), vInputsCur,  -1, -1 );
-    Cba_PrsReadList( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), vOutputsCur, -1, -1 );
-    Cba_PrsReadNodes( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3), vTypesCur, vFuncsCur, vInstIdsCur, vFaninsCur, vList );
-    Cba_PrsReadBoxes( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4), vTypesCur, vFuncsCur, vInstIdsCur, vFaninsCur, vList );
-
-    Cba_ManSetupArray( p, &pNtk->vInputs,  vInputsCur  );
-    Cba_ManSetupArray( p, &pNtk->vOutputs, vOutputsCur );
-    Cba_ManSetupArray( p, &pNtk->vTypes,   vTypesCur   );
-    Cba_ManSetupArray( p, &pNtk->vFuncs,   vFuncsCur   );
-    Cba_ManSetupArray( p, &pNtk->vInstIds, vInstIdsCur );
-    Cba_ManSetupArray( p, &pNtk->vFanins,  vFaninsCur  );
-    Cba_ManSetupArray( p, &pNtk->vBoxes,   vBoxes      );
-
-    Vec_IntFree( vInputsCur );
-    Vec_IntFree( vOutputsCur );
-    Vec_IntFree( vTypesCur );
-    Vec_IntFree( vFuncsCur );
-    Vec_IntFree( vInstIdsCur );
-    Vec_IntFree( vFaninsCur );
-    Vec_IntFree( vList );
-    Vec_IntFree( vBoxes );
+void Cba_PrsReadModule( Cba_Man_t * p, Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Int_t * vList )   
+{
+    Vec_Ptr_t * vInputs  = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1);
+    Vec_Ptr_t * vOutputs = (Vec_Ptr_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);
+
+    Cba_ManAllocArray( p, &pNtk->vInputs,  Vec_PtrSize(vInputs) );
+    Cba_ManAllocArray( p, &pNtk->vOutputs, Vec_PtrSize(vOutputs) ); 
+    Cba_ManAllocArray( p, &pNtk->vTypes,   Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); 
+    Cba_ManAllocArray( p, &pNtk->vFuncs,   Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); 
+    Cba_ManAllocArray( p, &pNtk->vInstIds, Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); 
+    Cba_ManAllocArray( p, &pNtk->vFanins,  Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); 
+    Cba_ManAllocArray( p, &pNtk->vBoxes,   Vec_PtrSize(vBoxes) ); 
+
+    Cba_PrsReadList( p, vInputs,  &pNtk->vInputs,  -1, -1 );
+    Cba_PrsReadList( p, vOutputs, &pNtk->vOutputs, -1, -1 );
+    Cba_PrsReadNodes( p, vNodes,  &pNtk->vTypes, &pNtk->vFuncs, &pNtk->vInstIds, &pNtk->vFanins, vList );
+    Cba_PrsReadBoxes( p, vBoxes,  &pNtk->vTypes, &pNtk->vFuncs, &pNtk->vInstIds, &pNtk->vFanins, vList );
 }
 Cba_Man_t * Cba_PrsReadPtr( Vec_Ptr_t * vDes )
 {
     Vec_Ptr_t * vNtk; int i;
-    Cba_Man_t * p = Cba_ManAlloc( (char *)Vec_PtrEntry(vDes, 0) );
+    Vec_Int_t * vList = Vec_IntAlloc( 100 );
+    Cba_Man_t * p = Cba_ManAlloc( NULL, (char *)Vec_PtrEntry(vDes, 0) );
     Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
         Cba_NtkAlloc( p, (char *)Vec_PtrEntry(vNtk, 0) );
     Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 )
-        Cba_PrsReadModule( p, Cba_ManNtk(p, i), vNtk );
+        Cba_PrsReadModule( p, Cba_ManNtk(p, i), vNtk, vList );
+    Vec_IntFree( vList );
     return p;
 }
 
diff --git a/src/base/cba/cbaWriteBlif.c b/src/base/cba/cbaWriteBlif.c
index 01749754..656ae8c0 100644
--- a/src/base/cba/cbaWriteBlif.c
+++ b/src/base/cba/cbaWriteBlif.c
@@ -114,7 +114,7 @@ void Cba_PrsWriteBlif( char * pFileName, Cba_Man_t * p )
         printf( "Cannot open output file \"%s\".\n", pFileName );
         return;
     }
-    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() );
+    fprintf( pFile, "# Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() );
     Cba_ManForEachNtk( p, pNtk, i )
         Cba_PrsWriteBlifNtk( pFile, pNtk );
     fclose( pFile );
@@ -207,7 +207,8 @@ void Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p )
         printf( "Cannot open output file \"%s\".\n", pFileName );
         return;
     }
-    fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() );
+    fprintf( pFile, "# Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() );
+    Cba_ManAssignInternNames( p );
     Cba_ManForEachNtk( p, pNtk, i )
         Cba_ManWriteBlifNtk( pFile, pNtk );
     fclose( pFile );
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index 8e72ee9a..d928da4b 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -120,7 +120,7 @@ void Cba_PrsWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p )
     Cba_NtkForEachObjType( p, Type, i )
         if ( Type == CBA_OBJ_BOX ) // .subckt/.gate/box (formal/actual binding) 
         {
-            fprintf( pFile, "  %s %s (", Cba_ObjFuncStr(p, i), Cba_ObjInstStr(p, i) );
+            fprintf( pFile, "  %s %s (", Cba_NtkName(Cba_ObjBoxModel(p, i)), Cba_ObjInstStr(p, i) );
             Cba_PrsWriteVerilogArray3( pFile, p, Cba_ObjFaninVec(p, i) );
             fprintf( pFile, ");\n" );
         }
@@ -186,6 +186,61 @@ void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Collect all nodes names used that are not inputs/outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cba_NtkCollectWires( Cba_Ntk_t * p, Vec_Int_t * vMap )
+{
+    Vec_Int_t * vWires = &p->vWires; 
+    int i, iObj, iFanin, Type, NameId;
+    Vec_IntClear( vWires );
+    Cba_NtkForEachPi( p, iObj, i )
+        Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 1 );
+    Cba_NtkForEachPo( p, iObj, i )
+        Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 1 );
+    Cba_NtkForEachObjType( p, Type, iObj )
+    {
+        if ( Type == CBA_OBJ_NODE )
+        {
+            Vec_Int_t * vFanins = Cba_ObjFaninVec( p, iObj );
+            Vec_IntForEachEntry( vFanins, iFanin, i )
+            {
+                NameId = Cba_ObjNameId( p, iFanin );
+                if ( Vec_IntEntry(vMap, NameId) == 0 )
+                {
+                    Vec_IntWriteEntry( vMap, NameId, 1 );
+                    Vec_IntPush( vWires, NameId );
+                }
+            }
+        }
+        else if ( Cba_ObjIsPo(p, iObj) || Cba_ObjIsBi(p, iObj) )
+        {
+            iFanin = Cba_ObjFanin0( p, iObj );
+            NameId = Cba_ObjNameId( p, iFanin );
+            if ( Vec_IntEntry(vMap, NameId) == 0 )
+            {
+                Vec_IntWriteEntry( vMap, NameId, 1 );
+                Vec_IntPush( vWires, NameId );
+            }
+        }
+    }
+    Cba_NtkForEachPi( p, iObj, i )
+        Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 );
+    Cba_NtkForEachPo( p, iObj, i )
+        Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 );
+    Vec_IntForEachEntry( vWires, NameId, i )
+        Vec_IntWriteEntry( vMap, NameId, 0 );
+    return vWires;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -195,6 +250,129 @@ void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Cba_ManWriteVerilogArray2( FILE * pFile, Cba_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
+{
+    int i, iFanin;
+    fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iObj), (Vec_IntSize(vFanins) == 0) ? "" : ", " );
+    Vec_IntForEachEntry( vFanins, iFanin, i )
+        fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iFanin), (i == Vec_IntSize(vFanins) - 1) ? "" : ", " );
+}
+void Cba_ManWriteVerilogNodes( FILE * pFile, Cba_Ntk_t * p )
+{
+    int Type, Func, i;
+    Cba_NtkForEachObjType( p, Type, i )
+        if ( Type == CBA_OBJ_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 (", Ptr_TypeToName(Func) );
+                Cba_ManWriteVerilogArray2( pFile, p, i, Cba_ObjFaninVec(p, i) );
+                fprintf( pFile, ");\n" );
+            }
+//            else if ( Func == CBA_NODE_MUX )
+//                Cba_PrsWriteVerilogMux( pFile, p, Cba_ObjFaninVec(p, i) );
+            else
+            {
+                //char * pName = Cba_NtkStr(p, Func);
+                assert( 0 );
+            }
+        }
+}
+void Cba_ManWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p )
+{
+    int i, k, iTerm, Type;
+    Cba_NtkForEachObjType( p, Type, i )
+        if ( Type == CBA_OBJ_BOX ) // .subckt/.gate/box (formal/actual binding) 
+        {
+            Cba_Ntk_t * pModel = Cba_ObjBoxModel( p, i );
+            fprintf( pFile, "  %s %s (", Cba_NtkName(pModel), Vec_IntSize(&p->vInstIds) ? Cba_ObjInstStr(p, i) : "" );
+            Cba_NtkForEachPi( pModel, iTerm, k )
+                fprintf( pFile, " %s=%s", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_ObjBoxBi(p, i, k)) );
+            Cba_NtkForEachPo( pModel, iTerm, k )
+                fprintf( pFile, " %s=%s", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_ObjBoxBo(p, i, k)) );
+            fprintf( pFile, "\n" );
+        }
+}
+void Cba_ManWriteVerilogSignals( FILE * pFile, Cba_Ntk_t * p, int SigType, int fNoRange )
+{
+    int NameId, RangeId, i;
+    char * pSigNames[4]  = { "inout", "input", "output", "wire" }; 
+    Vec_Int_t * vSigs[4] = { &p->vInouts, &p->vInputs, &p->vOutputs, &p->vWires };
+    if ( fNoRange )
+    {
+        Vec_IntForEachEntry( vSigs[SigType], NameId, i )
+            fprintf( pFile, "  %s %s;\n", pSigNames[SigType], SigType==3 ? Cba_NtkStr(p, NameId) : Cba_ObjNameStr(p, NameId) );
+    }
+    else
+    {
+        Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i )
+            fprintf( pFile, "  %s %s%s;\n", pSigNames[SigType], RangeId ? Cba_NtkStr(p, RangeId) : "", SigType==3 ? Cba_NtkStr(p, NameId) : Cba_ObjNameStr(p, NameId) );
+    }
+}
+void Cba_ManWriteVerilogSignalList( FILE * pFile, Cba_Ntk_t * p, int SigType, int fSkipComma, int fNoRange )
+{
+    int NameId, RangeId, i;
+    Vec_Int_t * vSigs[4] = { &p->vInouts, &p->vInputs, &p->vOutputs, &p->vWires };
+    if ( fNoRange )
+    {
+        Vec_IntForEachEntry( vSigs[SigType], NameId, i )
+            fprintf( pFile, "%s%s", Cba_ObjNameStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 1) ? "" : ", " );
+    }
+    else
+    {
+        Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i )
+            fprintf( pFile, "%s%s", Cba_ObjNameStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 2) ? "" : ", " );
+    }
+}
+void Cba_ManWriteVerilogNtk( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vMap )
+{
+    int s;
+    assert( Vec_IntSize(&p->vTypes)   == Cba_NtkObjNum(p) );
+    assert( Vec_IntSize(&p->vFuncs)   == Cba_NtkObjNum(p) );
+    // collect wires
+    Cba_NtkCollectWires( p, vMap );
+    // write header
+    fprintf( pFile, "module %s (\n", Cba_NtkName(p) );
+    for ( s = 0; s < 3; s++ )
+    {
+        if ( s == 0 && Vec_IntSize(&p->vInouts) == 0 ) 
+            continue;
+        fprintf( pFile, "    " );
+        Cba_ManWriteVerilogSignalList( pFile, p, s, s==2, 1 );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "  );\n" );
+    // write declarations
+    for ( s = 0; s < 4; s++ )
+        Cba_ManWriteVerilogSignals( pFile, p, s, 1 );
+    fprintf( pFile, "\n" );
+    // write objects
+    Cba_ManWriteVerilogNodes( pFile, p );
+    Cba_ManWriteVerilogBoxes( pFile, p );
+    fprintf( pFile, "endmodule\n\n" );
+    Vec_IntErase( &p->vWires );
+}
+void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p )
+{
+    FILE * pFile;
+    Cba_Ntk_t * pNtk; 
+    Vec_Int_t * vMap;
+    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(p), Extra_TimeStamp() );
+    Cba_ManAssignInternNames( p );
+    vMap = Vec_IntStart( Abc_NamObjNumMax(p->pNames) + 1 );
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_ManWriteVerilogNtk( pFile, pNtk, vMap );
+    Vec_IntFree( vMap );
+    fclose( pFile );
+}
 
 
 ////////////////////////////////////////////////////////////////////////