Version abc60419

4 files changed, 548 insertions, 44 deletions

diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 9d74a782..f6d92af7 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -212,6 +212,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
         pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
+    else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) 
+    {
+        printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, 
+            Extra_FileReaderGetLineNumber(p->pReader, 0), p->vTokens->pArray[0] );
+        return NULL;
+    }
 
     // read the inputs/outputs
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
new file mode 100644
index 00000000..75467d4d
--- /dev/null
+++ b/src/base/io/ioWriteVer.c
@@ -0,0 +1,497 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteVerilog.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to output a special subset of Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteVerilog.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+#include "main.h"
+#include "mio.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
+static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
+static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
+static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+
+    if ( !(Abc_NtkIsNetlist(pNtk) && (Abc_NtkHasMapping(pNtk) || Io_WriteVerilogCheckNtk(pNtk))) )
+    {
+        printf( "Io_WriteVerilog(): Can produce Verilog for a subset of logic networks.\n" );
+        printf( "The network should be either an AIG or a network after technology mapping.\n" );
+        printf( "The current network is not in the subset; the output files is not written.\n" );
+        return;
+    }
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // write the equations for the network
+    Io_WriteVerilogInt( pFile, pNtk );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    // write inputs and outputs
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
+    Io_WriteVerilogPis( pFile, pNtk, 3 );
+    fprintf( pFile, ",\n   " );
+    Io_WriteVerilogPos( pFile, pNtk, 3 );
+    fprintf( pFile, "  );\n" );
+    // write inputs, outputs, registers, and wires
+    fprintf( pFile, "  input gclk," );
+    Io_WriteVerilogPis( pFile, pNtk, 10 );
+    fprintf( pFile, ";\n" );
+    fprintf( pFile, "  output" );
+    Io_WriteVerilogPos( pFile, pNtk, 5 );
+    fprintf( pFile, ";\n" );
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+    fprintf( pFile, "  reg" );
+    Io_WriteVerilogRegs( pFile, pNtk, 4 );
+    fprintf( pFile, ";\n" );
+    }
+    fprintf( pFile, "  wire" );
+    Io_WriteVerilogWires( pFile, pNtk, 4 );
+    fprintf( pFile, ";\n" );
+    // write registers
+    Io_WriteVerilogLatches( pFile, pNtk );
+    // write the nodes
+    if ( Abc_NtkHasMapping(pNtk) )
+        Io_WriteVerilogGates( pFile, pNtk );
+    else
+        Io_WriteVerilogNodes( pFile, pNtk );
+    // finalize the file
+    fprintf( pFile, "endmodule\n\n" );
+    fclose( pFile );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanout0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of wires
+    nNodes = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        nNodes++;
+    }
+
+    // write the wires
+    Counter = 0;
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the regs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pLatch, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of latches
+    nNodes = Abc_NtkLatchNum(pNtk);
+
+    // write the wires
+    Counter = 0;
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pNet = Abc_ObjFanout0(pLatch);
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
+            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
+            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Mio_Gate_t * pGate;
+    Mio_Pin_t * pGatePin;
+    Abc_Obj_t * pObj;
+    int i, k, Counter, nDigits, nFanins;
+
+    Counter = 1;
+    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        pGate = pObj->pData;
+        nFanins = Abc_ObjFaninNum(pObj);
+        fprintf( pFile, "  %s g%0*d", Mio_GateReadName(pGate), nDigits, Counter++ );
+        fprintf( pFile, "(.%s (%s),", Mio_GateReadOutName(pGate), Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        for ( pGatePin = Mio_GateReadPins(pGate), k = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), k++ )
+            fprintf( pFile, " .%s (%s)%s", Mio_PinReadName(pGatePin), Io_WriteVerilogGetName(Abc_ObjFanin(pObj,k)), k==nFanins-1? "":"," );
+        fprintf( pFile, ");\n" );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nFanins;
+    char * pName;
+
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        assert( Abc_SopGetCubeNum(pObj->pData) == 1 );
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            pName = Abc_SopIsInv(pObj->pData)? "not" : "and";
+            fprintf( pFile, "  %s(%s, ", pName, Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+            fprintf( pFile, "%s);\n", Io_WriteVerilogGetName(Abc_ObjFanin0(pObj)) );
+            continue;
+        }
+        pName = Abc_SopIsComplement(pObj->pData)? "or" : "and";
+        fprintf( pFile, "  %s(%s, ", pName, Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : ", ") );
+        fprintf( pFile, ");\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 2;
+    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
+    }
+    for ( ; i < nInMax; i++ )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" );
+    }
+    fprintf( pFile, ");\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_SopGetCubeNum(pObj->pData) > 1 )
+        {
+            printf( "Node %s contains a cover with more than one cube.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the name for writing the Verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+{
+    static char Buffer[20];
+    char * pName;
+    pName = Abc_ObjName(pObj);
+    if ( pName[0] != '[' )
+        return pName;
+    // replace the brackets; as a result, the length of the name does not change
+    strcpy( Buffer, pName );
+    Buffer[0] = 'x';
+    Buffer[strlen(Buffer)-1] = 'x';
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerAux.c
index f56da052..f0814c84 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerAux.c
@@ -24,14 +24,14 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
-static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
-static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+static void Io_WriteVerilogAuxInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogAuxPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogAuxPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogAuxWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogAuxNodes( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogAuxArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
+static int Io_WriteVerilogAuxCheckNtk( Abc_Ntk_t * pNtk );
+static char * Io_WriteVerilogAuxGetName( Abc_Obj_t * pObj );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,30 +48,30 @@ static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteVerilogAux( Abc_Ntk_t * pNtk, char * pFileName )
 {
     FILE * pFile;
 
-    if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogCheckNtk(pNtk) )
+    if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogAuxCheckNtk(pNtk) )
     {
-        printf( "Io_WriteVerilog(): Can write Verilog for a very special subset of logic networks.\n" );
+        printf( "Io_WriteVerilogAux(): Can write Verilog for a very special subset of logic networks.\n" );
         printf( "The current network is not in the subset; writing Verilog is not performed.\n" );
         return;
     }
 
     if ( Abc_NtkLatchNum(pNtk) > 0 )
-        printf( "Io_WriteVerilog(): Warning: only combinational portion is being written.\n" );
+        printf( "Io_WriteVerilogAux(): Warning: only combinational portion is being written.\n" );
 
     // start the output stream
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
-        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
+        fprintf( stdout, "Io_WriteVerilogAux(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
 
     // write the equations for the network
-    Io_WriteVerilogInt( pFile, pNtk );
+    Io_WriteVerilogAuxInt( pFile, pNtk );
     fprintf( pFile, "\n" );
     fclose( pFile );
 }
@@ -87,27 +87,27 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogAuxInt( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     // write inputs and outputs
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     fprintf( pFile, "module %s (\n   ", Abc_NtkName(pNtk) );
-    Io_WriteVerilogPis( pFile, pNtk, 3 );
+    Io_WriteVerilogAuxPis( pFile, pNtk, 3 );
     fprintf( pFile, ",\n   " );
-    Io_WriteVerilogPos( pFile, pNtk, 3 );
+    Io_WriteVerilogAuxPos( pFile, pNtk, 3 );
     fprintf( pFile, "  );\n" );
     // write inputs, outputs and wires
     fprintf( pFile, "  input" );
-    Io_WriteVerilogPis( pFile, pNtk, 5 );
+    Io_WriteVerilogAuxPis( pFile, pNtk, 5 );
     fprintf( pFile, ";\n" );
     fprintf( pFile, "  output" );
-    Io_WriteVerilogPos( pFile, pNtk, 5 );
+    Io_WriteVerilogAuxPos( pFile, pNtk, 5 );
     fprintf( pFile, ";\n" );
     fprintf( pFile, "  wire" );
-    Io_WriteVerilogWires( pFile, pNtk, 4 );
+    Io_WriteVerilogAuxWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
     // write the nodes
-    Io_WriteVerilogNodes( pFile, pNtk );
+    Io_WriteVerilogAuxNodes( pFile, pNtk );
     // finalize the file
     fprintf( pFile, "endmodule\n\n" );
     fclose( pFile );
@@ -124,7 +124,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogAuxPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
     Abc_Obj_t * pTerm, * pNet;
     int LineLength;
@@ -163,7 +163,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogAuxPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
     Abc_Obj_t * pTerm, * pNet;
     int LineLength;
@@ -202,7 +202,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogAuxWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
     Abc_Obj_t * pTerm, * pNet;
     int LineLength;
@@ -243,7 +243,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogAuxGetName(pNet), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -260,7 +260,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogAuxNodes( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     int i, nCubes, nFanins, Counter, nDigits, fPadZeros;
@@ -284,62 +284,62 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
         if ( nCubes == 0 )
         {
             fprintf( pFile, "  ts_gnd g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 0, fPadZeros );
         }
         else if ( nCubes == 1 && nFanins == 0 )
         {
             fprintf( pFile, "  ts_vdd g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 0, fPadZeros );
         }
         else if ( nFanins == 1 && Abc_SopIsInv(pObj->pData) )
         {
             fprintf( pFile, "  ts_inv g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 1, fPadZeros );
         }
         else if ( nFanins == 1 )
         {
             fprintf( pFile, "  ts_buf g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 1, fPadZeros );
         }
         else if ( nFanins <= 4 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 4, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 4, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 4, fPadZeros );
         }
         else if ( nFanins <= 6 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 6, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 6, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 6, fPadZeros );
         }
         else if ( nFanins == 7 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 7, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 7, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 7, fPadZeros );
         }
         else if ( nFanins == 8 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 8, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 8, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 8, fPadZeros );
         }
         else if ( nFanins <= 16 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 16, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 16, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 16, fPadZeros );
         }
         else if ( nFanins <= 32 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 32, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 32, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 32, fPadZeros );
         }
         else if ( nFanins <= 64 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 64, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 64, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 64, fPadZeros );
         }
         else if ( nFanins <= 128 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 128, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 128, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 128, fPadZeros );
         }
     }
 }
@@ -355,16 +355,16 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+void Io_WriteVerilogAuxArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
 {
     Abc_Obj_t * pFanin;
     int i, Counter = 2;
-    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+    fprintf( pFile, "(.z (%s)", Io_WriteVerilogAuxGetName(Abc_ObjFanout0(pObj)) );
     Abc_ObjForEachFanin( pObj, pFanin, i )
     {
         if ( Counter++ % 4 == 0 )
             fprintf( pFile, "\n   " );
-        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
+        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogAuxGetName(Abc_ObjFanin(pObj,i)) );
     }
     for ( ; i < nInMax; i++ )
     {
@@ -386,7 +386,7 @@ void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZe
   SeeAlso     []
 
 ***********************************************************************/
-int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
+int Io_WriteVerilogAuxCheckNtk( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     char * pSop;
@@ -423,7 +423,7 @@ int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+char * Io_WriteVerilogAuxGetName( Abc_Obj_t * pObj )
 {
     static char Buffer[20];
     char * pName;
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 8693c8eb..2d5e4b9e 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -17,4 +17,5 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioWriteGml.c \
     src/base/io/ioWriteList.c \
     src/base/io/ioWritePla.c \
-    src/base/io/ioWriteVerilog.c
+    src/base/io/ioWriteVer.c \
+    src/base/io/ioWriteVerAux.c