1 files changed, 264 insertions, 189 deletions

diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index c375301d..0480d75d 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -182,7 +182,7 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
 
 /**Function*************************************************************
 
-  Synopsis    [Collect all nodes names used that are not inputs/outputs.]
+  Synopsis    [Writing word-level Verilog.]
 
   Description []
                
@@ -191,234 +191,309 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Cba_NtkCollectWires( Cba_Ntk_t * p, Vec_Int_t * vMap, Vec_Int_t * vWires )
+void Cba_ManWriteRange( Cba_Ntk_t * p, int Beg, int End )
 {
-    int i, k, iTerm, iObj, NameId;
-    Vec_IntClear( vWires );
-    Cba_NtkForEachPi( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 1 );
-    Cba_NtkForEachPo( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 1 );
-    Cba_NtkForEachBox( p, iObj )
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    Vec_StrPrintStr( vStr, "[" );
+    Vec_StrPrintNum( vStr, End );
+    Vec_StrPrintStr( vStr, ":" );
+    Vec_StrPrintNum( vStr, Beg );
+    Vec_StrPrintStr( vStr, "]" );
+}
+void Cba_ManWriteLit( Cba_Ntk_t * p, int NameId, int iBit )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    Vec_StrPrintStr( vStr, Cba_NtkStr(p, NameId) );
+    if ( iBit == -1 )
+        return;
+    Vec_StrPrintStr( vStr, "[" );
+    Vec_StrPrintNum( vStr, iBit );
+    Vec_StrPrintStr( vStr, "]" );
+}
+void Cba_ManWriteSig( Cba_Ntk_t * p, int iObj )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    int iNameId = Cba_ObjName(p, iObj);
+    if ( Cba_NameType(iNameId) == CBA_NAME_BIN )
+        Cba_ManWriteLit( p, Abc_Lit2Var2(iNameId), -1 );
+    else if ( Cba_NameType(iNameId) == CBA_NAME_WORD )
+        Cba_ManWriteLit( p, Abc_Lit2Var2(iNameId), 0 );
+    else if ( Cba_NameType(iNameId) == CBA_NAME_INDEX )
     {
-        Cba_BoxForEachBi( p, iObj, iTerm, k )
-        {
-            NameId = Cba_ObjName( p, iTerm );
-            if ( Vec_IntEntry(vMap, NameId) == 0 )
-            {
-                Vec_IntWriteEntry( vMap, NameId, 1 );
-                Vec_IntPush( vWires, iTerm );
-            }
-        }
-        Cba_BoxForEachBo( p, iObj, iTerm, k )
+        int iBit = Abc_Lit2Var2(iNameId);
+        iNameId = Cba_ObjName(p, iObj - iBit);
+        if ( Cba_NameType(iNameId) == CBA_NAME_WORD )
+            Cba_ManWriteLit( p, Abc_Lit2Var2(iNameId), iBit );
+        else if ( Cba_NameType(iNameId) == CBA_NAME_INFO )
+            Cba_ManWriteLit( p, Cba_NtkInfoName(p, Abc_Lit2Var2(iNameId)), Cba_NtkInfoIndex(p, Abc_Lit2Var2(iNameId), iBit) );
+        else assert( 0 );
+    }
+    else if ( Cba_NameType(iNameId) == CBA_NAME_INFO )
+        Cba_ManWriteLit( p, Cba_NtkInfoName(p, Abc_Lit2Var2(iNameId)), Cba_NtkInfoIndex(p, Abc_Lit2Var2(iNameId), 0) );
+    else assert( 0 );
+}
+void Cba_ManWriteConcat( Cba_Ntk_t * p, int iStart, int nObjs )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut; int i;
+    assert( nObjs >= 1 );
+    if ( nObjs == 1 )
+        Cba_ManWriteSig( p, iStart );
+    else
+    {
+        Vec_StrPrintStr( vStr, "{" );
+        for ( i = nObjs - 1; i >= 0; i-- )
         {
-            NameId = Cba_ObjName( p, iTerm );
-            if ( Vec_IntEntry(vMap, NameId) == 0 )
-            {
-                Vec_IntWriteEntry( vMap, NameId, 1 );
-                Vec_IntPush( vWires, iTerm );
-            }
+            Vec_StrPrintStr( vStr, i < nObjs - 1 ? ", " : "" );
+            if ( Cba_ObjIsBo(p, iStart) )
+                Cba_ManWriteSig( p, iStart + i );
+            else if ( Cba_ObjIsBi(p, iStart) )
+                Cba_ManWriteSig( p, Cba_ObjFanin(p, iStart - i) );
+            else assert( 0 );
         }
+        Vec_StrPrintStr( vStr, "}" );
     }
-    Cba_NtkForEachPi( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
-    Cba_NtkForEachPo( p, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
-    Vec_IntForEachEntry( vWires, iObj, i )
-        Vec_IntWriteEntry( vMap, Cba_ObjName(p, iObj), 0 );
-    //Vec_IntSort( vWires, 0 );
-    return vWires;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cba_ManWriteVerilogArray2( FILE * pFile, Cba_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
+void Cba_ManWriteGate( Cba_Ntk_t * p, int iObj )
 {
-    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) ? "" : ", " );
+    Vec_Str_t * vStr = p->pDesign->vOut; int iTerm, k;
+    char * pGateName = Abc_NamStr(p->pDesign->pMods, Cba_BoxNtkId(p, iObj));
+    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen( Abc_FrameGetGlobalFrame() );
+    Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pGateName, NULL );
+    Vec_StrPrintStr( vStr, "  " );
+    Vec_StrPrintStr( vStr, pGateName );
+    Vec_StrPrintStr( vStr, " (" );
+    Cba_BoxForEachBi( p, iObj, iTerm, k )
+    {
+        Vec_StrPrintStr( vStr, k ? ", ." : "." );
+        Vec_StrPrintStr( vStr, Mio_GateReadPinName(pGate, k) );
+        Vec_StrPrintStr( vStr, "(" );
+        Cba_ManWriteSig( p, iTerm );
+        Vec_StrPrintStr( vStr, ")" );
+    }
+    Cba_BoxForEachBo( p, iObj, iTerm, k )
+    {
+        Vec_StrPrintStr( vStr, Cba_BoxBiNum(p, iObj) ? ", ." : "." );
+        Vec_StrPrintStr( vStr, Mio_GateReadOutName(pGate) );
+        Vec_StrPrintStr( vStr, "(" );
+        Cba_ManWriteSig( p, iTerm );
+        Vec_StrPrintStr( vStr, ")" );
+    }
+    Vec_StrPrintStr( vStr, " );\n" );
 }
-void Cba_ManWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p )
+void Cba_ManWriteAssign( Cba_Ntk_t * p, int iObj )
 {
-    int i, k, iTerm;
-    Cba_NtkForEachBox( p, i ) // .subckt/.gate/box (formal/actual binding) 
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    Cba_ObjType_t Type = Cba_ObjType(p, iObj);
+    int nInputs = Cba_BoxBiNum(p, iObj);
+    int nOutputs = Cba_BoxBoNum(p, iObj);
+    assert( nOutputs == 1 );
+    Vec_StrPrintStr( vStr, "  assign " );
+    Cba_ManWriteSig( p, iObj + 1 );
+    Vec_StrPrintStr( vStr, " = " );
+    if ( nInputs == 0 )
+    {
+        if ( Type == CBA_BOX_CF )
+            Vec_StrPrintStr( vStr, "1\'b0" );
+        else if ( Type == CBA_BOX_CT )
+            Vec_StrPrintStr( vStr, "1\'b1" );
+        else if ( Type == CBA_BOX_CX )
+            Vec_StrPrintStr( vStr, "1\'bx" );
+        else if ( Type == CBA_BOX_CZ )
+            Vec_StrPrintStr( vStr, "1\'bz" );
+        else assert( 0 );       
+    }
+    else if ( nInputs == 1 )
     {
-        if ( Cba_ObjIsBoxUser(p, i) )
+        if ( Type == CBA_BOX_INV )
+            Vec_StrPrintStr( vStr, "~" );
+        else assert( Type == CBA_BOX_BUF );
+        Cba_ManWriteSig( p, iObj - 1 );
+    }
+    else if ( nInputs == 2 )
+    {
+        if ( Type == CBA_BOX_XNOR )
         {
-            Cba_Ntk_t * pModel = Cba_BoxNtk( p, i );
-            fprintf( pFile, "  %s %s (", Cba_NtkName(pModel), Cba_ObjNameStr(p, i) ? Cba_ObjNameStr(p, i) : "" );
-            Cba_NtkForEachPi( pModel, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", k ? ", " : "", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_BoxBi(p, i, k)) );
-            Cba_NtkForEachPo( pModel, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", Cba_NtkPiNum(pModel) ? ", " : "", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_BoxBo(p, i, k)) );
-            fprintf( pFile, ");\n" );
+            Vec_StrPrintStr( vStr, "~" );
+            Type = CBA_BOX_XOR;
         }
-        else if ( Cba_ObjIsGate(p, i) )
+        Cba_ManWriteSig( p, iObj - 1 );
+        if ( Type == CBA_BOX_AND )
+            Vec_StrPrintStr( vStr, " & " );
+        else if ( Type == CBA_BOX_OR )
+            Vec_StrPrintStr( vStr, " | " );
+        else if ( Type == CBA_BOX_XOR )
+            Vec_StrPrintStr( vStr, " ^ " );
+        else assert( 0 );
+        Cba_ManWriteSig( p, iObj - 2 );
+    }
+    Vec_StrPrintStr( vStr, ";\n" );
+}
+void Cba_ManWriteVerilogBoxes( Cba_Ntk_t * p )
+{
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    int iObj, k, i, o;
+    Cba_NtkForEachBox( p, iObj ) // .subckt/.gate/box (formal/actual binding) 
+    {
+        Cba_Ntk_t * pModel = NULL;
+        char * pName = NULL;
+        // write mapped
+        if ( Cba_ObjIsGate(p, iObj) )
         {
-            char * pGateName = Abc_NamStr(p->pDesign->pMods, Cba_BoxNtkId(p, i));
-            Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen( Abc_FrameGetGlobalFrame() );
-            Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pGateName, NULL );
-            fprintf( pFile, "  %s (", pGateName );
-            Cba_BoxForEachBi( p, i, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", k ? ", " : "", Mio_GateReadPinName(pGate, k), Cba_ObjNameStr(p, iTerm) );
-            Cba_BoxForEachBo( p, i, iTerm, k )
-                fprintf( pFile, "%s.%s(%s)", Cba_BoxBiNum(p, i) ? ", " : "", Mio_GateReadOutName(pGate), Cba_ObjNameStr(p, iTerm) );
-            fprintf( pFile, ");\n" );
+            Cba_ManWriteGate( p, iObj );
+            continue;
         }
-/*
-        else if ( Cba_BoxNtkId(p, i) )
+        // write primitives as assign-statements
+        if ( Cba_BoxNtkName(p, iObj) == NULL )
         {
-            int pRanges[8]; char pSymbs[8];
-            char * pName = Cba_BoxNtkName(p, i);
-            int nSigs = Cba_NtkNameRanges( pName, pRanges, pSymbs );
-            int s, k, iTerm, nInputs = 0;
-            fprintf( pFile, "  %s ( ", pName );
-            for ( s = 0; s < nSigs-1; s++ )
-            {
-                fprintf( pFile, "%s.%c(", nInputs ? ", " : "", pSymbs[s] );
-                if ( pRanges[s] == 1 )
-                {
-                    iTerm = Cba_BoxBi(p, i, nInputs++);
-                    fprintf( pFile, "%s", Cba_ObjNameStr(p, iTerm) );
-                }
-                else
-                {
-                    assert( pRanges[s] > 1 );
-                    fprintf( pFile, "{" );
-                    for ( k = 0; k < pRanges[s]; k++ )
-                    {
-                        iTerm = Cba_BoxBi(p, i, nInputs++);
-                        fprintf( pFile, "%s%s", k ? ", " : "", Cba_ObjNameStr(p, iTerm) );
-                    }
-                    fprintf( pFile, "}" );
-                }
-                fprintf( pFile, ")" );
-            }
-            assert( nInputs == Cba_BoxBiNum(p, i) );
-            fprintf( pFile, "%s.%c(", nInputs ? ", " : "", pSymbs[nSigs-1] );
-            if ( pRanges[nSigs-1] == 1 )
-            {
-                iTerm = Cba_BoxBo(p, i, 0);
-                fprintf( pFile, "%s", Cba_ObjNameStr(p, iTerm) );
-            }
-            else
+            Cba_ManWriteAssign( p, iObj );
+            continue;
+        }
+
+        // write header
+        if ( Cba_ObjIsBoxUser(p, iObj) )
+            pModel = Cba_BoxNtk( p, iObj );
+        else if ( Cba_BoxNtkId(p, iObj) )
+            pName = Cba_BoxNtkName(p, iObj);
+        else assert( 0 );
+        Vec_StrPrintStr( vStr, "  " );
+        Vec_StrPrintStr( vStr, pModel ? Cba_NtkName(pModel) : pName );
+        Vec_StrPrintStr( vStr, " " );
+        Vec_StrPrintStr( vStr, Cba_ObjName(p, iObj) ? Cba_ObjNameStr(p, iObj) : ""  );
+
+        // write arguments
+        i = o = 0;
+        Vec_StrPrintStr( vStr, " (" );
+        if ( pModel )
+        {
+            int Value, Beg, End, Range;
+            assert( Cba_NtkInfoNum(pModel) );
+            Vec_IntForEachEntryTriple( &pModel->vInfo, Value, Beg, End, k )
             {
-                assert( pRanges[nSigs-1] > 1 );
-                fprintf( pFile, "{" );
-                for ( k = 0; k < pRanges[nSigs-1]; k++ )
-                {
-                    iTerm = Cba_BoxBo(p, i, k);
-                    fprintf( pFile, "%s%s", k ? ", " : "", Cba_ObjNameStr(p, iTerm) );
-                }
-                fprintf( pFile, "}" );
+                int NameId = Abc_Lit2Var2( Value );
+                int Type = Abc_Lit2Att2( Value );
+                Vec_StrPrintStr( vStr, k ? ", ." : "." );
+                Vec_StrPrintStr( vStr, Cba_NtkStr(p, NameId) );
+                Vec_StrPrintStr( vStr, "(" );
+                Range = Cba_InfoRange( Beg, End );
+                assert( Range > 0 );
+                if ( Type == 1 )
+                    Cba_ManWriteConcat( p, Cba_BoxBi(p, iObj, i), Range ), i += Range;
+                else if ( Type == 2 )
+                    Cba_ManWriteConcat( p, Cba_BoxBo(p, iObj, o), Range ), o += Range;
+                else assert( 0 );
+                Vec_StrPrintStr( vStr, ")" );
             }
-            fprintf( pFile, ") );\n" );
         }
-*/
         else
         {
-            Cba_ObjType_t Type = Cba_ObjType( p, i );
-            int nInputs = Cba_BoxBiNum(p, i);
-            fprintf( pFile, "  %s (", Ptr_TypeToName(Type) );
-            Cba_BoxForEachBo( p, i, iTerm, k )
-                fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iTerm), nInputs ? ", " : "" );
-            Cba_BoxForEachBi( p, i, iTerm, k )
-                fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iTerm), k < nInputs - 1 ? ", " : "" );
-            fprintf( pFile, ");\n" );
+            int pRanges[8]; char pSymbs[8];
+            int nSigs = Cba_NtkNameRanges( pName, pRanges, pSymbs );
+            for ( k = 0; k < nSigs; k++ )
+            {
+                Vec_StrPrintStr( vStr, k ? ", ." : "." );
+                Vec_StrPush( vStr, pSymbs[k] );
+                Vec_StrPrintStr( vStr, "(" );
+                if ( k < nSigs - 1 )
+                    Cba_ManWriteConcat( p, Cba_BoxBi(p, iObj, i), pRanges[k] ), i += pRanges[k];
+                else 
+                    Cba_ManWriteConcat( p, Cba_BoxBo(p, iObj, o), pRanges[k] ), o += pRanges[k];
+                Vec_StrPrintStr( vStr, ")" );
+            }
         }
+        Vec_StrPrintStr( vStr, " );\n" );
+        assert( i == Cba_BoxBiNum(p, iObj) );
+        assert( o == Cba_BoxBoNum(p, iObj) );
     }
 }
-void Cba_ManWriteVerilogSignals( FILE * pFile, Cba_Ntk_t * p, int SigType, int fNoRange, Vec_Int_t * vWires )
-{
-    int NameId, RangeId, i;
-    char * pSigNames[3]  = { "input", "output", "wire" }; 
-    Vec_Int_t * vSigs[3] = { &p->vInputs, &p->vOutputs, 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, Vec_Int_t * vWires )
-{
-    int NameId, RangeId, i;
-    Vec_Int_t * vSigs[3] = { &p->vInputs, &p->vOutputs, 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, Vec_Int_t * vWires )
+void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p )
 {
-    int s;
+    char * pKeyword[4] = { "wire ", "input ", "output ", "inout " };
+    Vec_Str_t * vStr = p->pDesign->vOut;
+    int k, iObj, iTerm, Value, Beg, End, Length;
+    assert( Cba_NtkInfoNum(p) );
     assert( Vec_IntSize(&p->vFanin) == Cba_NtkObjNum(p) );
-    // collect wires
-    Cba_NtkCollectWires( p, vMap, vWires );
+//    Cba_NtkPrint( p );
     // write header
-    fprintf( pFile, "module %s (\n", Cba_NtkName(p) );
-    for ( s = 0; s < 2; s++ )
+    Vec_StrPrintStr( vStr, "module " );
+    Vec_StrPrintStr( vStr, Cba_NtkName(p) );
+    Vec_StrPrintStr( vStr, " (\n    " );
+    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
+    if ( Abc_Lit2Att2(Value) != 0 )
     {
-        fprintf( pFile, "    " );
-        Cba_ManWriteVerilogSignalList( pFile, p, s, s==1, 1, vWires );
-        fprintf( pFile, "\n" );
+        Vec_StrPrintStr( vStr, k ? ", " : "" );
+        Vec_StrPrintStr( vStr, Cba_NtkStr(p, Abc_Lit2Var2(Value)) );
     }
-    fprintf( pFile, "  );\n" );
-    // write declarations
-    for ( s = 0; s < 3; s++ )
-        Cba_ManWriteVerilogSignals( pFile, p, s, 1, vWires );
-    fprintf( pFile, "\n" );
+    Vec_StrPrintStr( vStr, "\n  );\n" );
+    // write inputs/outputs
+    Vec_IntForEachEntryTriple( &p->vInfo, Value, Beg, End, k )
+    if ( Abc_Lit2Att2(Value) != 0 )
+    {
+        Vec_StrPrintStr( vStr, "  " );
+        Vec_StrPrintStr( vStr, pKeyword[Abc_Lit2Att2(Value)] );
+        if ( Beg >= 0 )
+            Cba_ManWriteRange( p, Beg, End );
+        Vec_StrPrintStr( vStr, Cba_NtkStr(p, Abc_Lit2Var2(Value)) );
+        Vec_StrPrintStr( vStr, ";\n" );
+    }
+    Vec_StrPrintStr( vStr, "\n" );
+    // write word-level wires
+    Cba_NtkForEachBox( p, iObj )
+    Cba_BoxForEachBo( p, iObj, iTerm, k )
+        if ( Cba_NameType(Cba_ObjName(p, iTerm)) == CBA_NAME_WORD )
+        {
+            int Beg, End;
+            Cba_ObjGetRange( p, iTerm, &Beg, &End );
+            Vec_StrPrintStr( vStr, "  wire " );
+            Cba_ManWriteRange( p, Beg, End );
+            Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iTerm) );
+            Vec_StrPrintStr( vStr, ";\n" );
+        }
+    // write bit-level wires
+    Length = 7;
+    Vec_StrPrintStr( vStr, "  wire " );
+    Cba_NtkForEachBox( p, iObj )
+    Cba_BoxForEachBo( p, iObj, iTerm, k )
+        if ( Cba_NameType(Cba_ObjName(p, iTerm)) == CBA_NAME_BIN )
+        {
+            if ( Length > 72 )
+                Vec_StrPrintStr( vStr, ";\n  wire " ), Length = 7;
+            if ( Length > 7 )
+                Vec_StrPrintStr( vStr, ", " );
+            Vec_StrPrintStr( vStr, Cba_ObjNameStr(p, iTerm) ); 
+            Length += strlen(Cba_ObjNameStr(p, iTerm));
+        }
+    Vec_StrPrintStr( vStr, ";\n\n" );
     // write objects
-    Cba_ManWriteVerilogBoxes( pFile, p );
-    fprintf( pFile, "endmodule\n\n" );
+    Cba_ManWriteVerilogBoxes( p );
+    Vec_StrPrintStr( vStr, "endmodule\n\n" );
 }
 void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p )
 {
-    FILE * pFile;
-    Cba_Ntk_t * pNtk; 
-    Vec_Int_t * vMap, * vWires;
-    int i;
+    Cba_Ntk_t * pNtk; int i;
     // check the library
     if ( p->pMioLib && p->pMioLib != Abc_FrameReadLibGen() )
     {
         printf( "Genlib library used in the mapped design is not longer a current library.\n" );
         return;
     }
-    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() );
+    // derive the stream
+    p->vOut = Vec_StrAlloc( 10000 );
     Cba_ManAssignInternNames( p );
-    vMap = Vec_IntStart( Abc_NamObjNumMax(p->pStrs) + 1 );
-    vWires = Vec_IntAlloc( 1000 );
     Cba_ManForEachNtk( p, pNtk, i )
-        Cba_ManWriteVerilogNtk( pFile, pNtk, vMap, vWires );
-    Vec_IntFree( vWires );
-    Vec_IntFree( vMap );
-    fclose( pFile );
+        Cba_ManWriteVerilogNtk( pNtk );
+    // dump into file
+    if ( p->vOut && Vec_StrSize(p->vOut) > 0 )
+    {
+        FILE * pFile = fopen( pFileName, "wb" );
+        if ( pFile == NULL )
+            printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        else
+        {
+            fwrite( Vec_StrArray(p->vOut), 1, Vec_StrSize(p->vOut), pFile );
+            fclose( pFile );
+        }
+    }
+    Vec_StrFreeP( &p->vOut );
 }