Version abc70219

8 files changed, 284 insertions, 131 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2267d4e7..3603519f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -55,7 +55,7 @@ static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 
-extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+extern int glo_fMapped;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -139,11 +139,15 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
 
     fCheck = 1;
+    glo_fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mch" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                glo_fMapped ^= 1;
+                break;
             case 'c':
                 fCheck ^= 1;
                 break;
@@ -166,10 +170,11 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
+    fprintf( pAbc->Err, "usage: read [-mch] <file>\n" );
     fprintf( pAbc->Err, "\t         replaces the current network by the network read from <file>\n" );
     fprintf( pAbc->Err, "\t         by calling the parser that matches the extension of <file>\n" );
     fprintf( pAbc->Err, "\t         (to read a hierarchical design, use \"read_hie\")\n" );
+    fprintf( pAbc->Err, "\t-m     : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
@@ -332,7 +337,13 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtk = Io_ReadBlifAsAig( pFileName, fCheck );
     else
 //        pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck );
+    {
+        Abc_Ntk_t * pTemp;
         pNtk = Io_ReadBlif( pFileName, fCheck );
+        pNtk = Abc_NtkToLogic( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+    }
+
     if ( pNtk == NULL )
         return 1;
     // replace the current network
@@ -657,11 +668,15 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
     fCheck = 1;
+    glo_fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mch" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                glo_fMapped ^= 1;
+                break;
             case 'c':
                 fCheck ^= 1;
                 break;
@@ -684,8 +699,9 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_verilog [-ch] <file>\n" );
-    fprintf( pAbc->Err, "\t         read the network in Verilog (IWLS 2005 subset)\n" );
+    fprintf( pAbc->Err, "usage: read_verilog [-mch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in Verilog (IWLS 2002/2005 subset)\n" );
+    fprintf( pAbc->Err, "\t-m     : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
@@ -712,6 +728,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCheck;
     int c;
     extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib );
+    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
 
     fCheck = 1;
     Extra_UtilGetoptReset();
@@ -921,11 +938,15 @@ int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pBaseName, * pFileName;
     int c;
 
+    glo_fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                glo_fMapped ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -946,6 +967,7 @@ usage:
     fprintf( pAbc->Err, "usage: write_hie [-h] <orig> <file>\n" );
     fprintf( pAbc->Err, "\t         writes the current network into <file> by calling\n" );
     fprintf( pAbc->Err, "\t         the hierarchical writer that matches the extension of <file>\n" );
+    fprintf( pAbc->Err, "\t-m     : toggle reading mapped Verilog for <orig> [default = %s]\n", glo_fMapped? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\torig   : the name of the original file with the hierarchical design\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index d8213994..7e54e5e3 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
                 else
                 {
-                    printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
+                    printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
                     Vec_StrFree( vString );
                     Abc_NtkDelete( pNtk );
                     return NULL;
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 46a202e1..3e09caf0 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -98,6 +98,7 @@ static int               Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
 static int               Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
+static int               Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens );
 
 static int               Io_MvCharIsSpace( char s )  { return s == ' ' || s == '\t' || s == '\r' || s == '\n';  }
 static int               Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!';  }
@@ -568,7 +569,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
         // parse directives
         if ( *(pCur-1) != '.' )
             continue;
-        if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) )
+        if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) || !strncmp(pCur, "gate", 4) )
             Vec_PtrPush( p->pLatest->vNames, pCur );
         else if ( p->fBlifMv && (!strncmp(pCur, "def ", 4) || !strncmp(pCur, "default ", 8)) )
             continue;
@@ -1464,6 +1465,10 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
     char * pName;
     assert( !p->pMan->fBlifMv );
     Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
+    // parse the mapped node
+    if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") )
+        return Io_MvParseLineGateBlif( p, vTokens );
+    // parse the regular name line
     assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
     pName = Vec_PtrEntryLast( vTokens );
     pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
@@ -1483,6 +1488,104 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
 }
 
 
+#include "mio.h"
+#include "main.h"
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Io_ReadBlifCleanName( char * pName )
+{
+    int i, Length;
+    Length = strlen(pName);
+    for ( i = 0; i < Length; i++ )
+        if ( pName[i] == '=' )
+            return pName + i + 1;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
+{
+    Mio_Library_t * pGenlib; 
+    Mio_Gate_t * pGate;
+    Abc_Obj_t * pNode;
+    char ** ppNames, * pName;
+    int i, nNames;
+
+    pName = vTokens->pArray[0];
+
+    // check that the library is available
+    pGenlib = Abc_FrameReadLibGen();
+    if ( pGenlib == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
+        return 0;
+    }
+
+    // create a new node and add it to the network
+    if ( vTokens->nSize < 2 )
+    {
+        sprintf( p->pMan->sError, "Line %d: The .gate line has less than two tokens.", Io_MvGetLine(p->pMan, pName) );
+        return 0;
+    }
+
+    // get the gate
+    pGate = Mio_LibraryReadGateByName( pGenlib, vTokens->pArray[1] );
+    if ( pGate == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), vTokens->pArray[1] );
+        return 0;
+    }
+
+    // if this is the first line with gate, update the network type
+    if ( Abc_NtkNodeNum(p->pNtk) == 0 )
+    {
+        assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
+        p->pNtk->ntkFunc = ABC_FUNC_MAP;
+        Extra_MmFlexStop( p->pNtk->pManFunc );
+        p->pNtk->pManFunc = pGenlib;
+    }
+
+    // remove the formal parameter names
+    for ( i = 2; i < vTokens->nSize; i++ )
+    {
+        vTokens->pArray[i] = Io_ReadBlifCleanName( vTokens->pArray[i] );
+        if ( vTokens->pArray[i] == NULL )
+        {
+            sprintf( p->pMan->sError, "Line %d: Invalid gate input assignment.", Io_MvGetLine(p->pMan, pName) );
+            return 0;
+        }
+    }
+
+    // create the node
+    ppNames = (char **)vTokens->pArray + 2;
+    nNames  = vTokens->nSize - 3;
+    pNode   = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames );
+
+    // set the pointer to the functionality of the node
+    Abc_ObjSetData( pNode, pGate );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 5956a9bc..090cf254 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -45,13 +45,12 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
 {
     Abc_Ntk_t * pNtk;
     Abc_Lib_t * pDesign;
-    int i;
 
     // parse the verilog file
-    pDesign = Ver_ParseFile( pFileName, NULL, 1, fCheck );
+    pDesign = Ver_ParseFile( pFileName, NULL, fCheck, 1 );
     if ( pDesign == NULL )
         return NULL;
-
+/*
     // extract the master network
     pNtk = Vec_PtrEntryLast( pDesign->vModules );
     pNtk->pDesign = pDesign;
@@ -75,6 +74,28 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
         // check that there is no cyclic dependency
         Abc_NtkIsAcyclicHierarchy( pNtk );
     }
+*/
+    // extract the master network
+    pNtk = Vec_PtrEntry( pDesign->vModules, 0 );
+    pNtk->pDesign = pDesign;
+    pDesign->pManFunc = NULL;
+
+//Io_WriteVerilog( pNtk, "_temp.v" );
+
+    // verify the design for cyclic dependence
+    assert( Vec_PtrSize(pDesign->vModules) > 0 );
+    if ( Vec_PtrSize(pDesign->vModules) == 1 )
+    {
+//        printf( "Warning: The design is not hierarchical.\n" );
+        Abc_LibFree( pDesign, pNtk );
+        pNtk->pDesign = NULL;
+        pNtk->pSpec = Extra_UtilStrsav( pFileName );
+    }
+    else
+    {
+        // check that there is no cyclic dependency
+        Abc_NtkIsAcyclicHierarchy( pNtk );
+    }
     return pNtk;
 }
 
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 2de93ddf..0ac3181a 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -209,7 +209,7 @@ Abc_NtkPrintStats( stdout, pNtk, 0 );
     // convert blackboxes
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
-        printf( "Hierarchy reader converted %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
         pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
         Abc_NtkDelete( pTemp );
         if ( pNtk == NULL )
@@ -219,7 +219,7 @@ Abc_NtkPrintStats( stdout, pNtk, 0 );
         }
     }
     // convert the netlist into the logic network
-    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    pNtk = Abc_NtkToLogic( pTemp = pNtk );
     Abc_NtkDelete( pTemp );
     if ( pNtk == NULL )
     {
@@ -244,7 +244,6 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
 {
     Abc_Ntk_t * pNtk, * pTemp;
     // detect the file type
-
     if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
         pNtk = Io_ReadBlifMv( pFileName, 0, fCheck );
 //    else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
@@ -274,7 +273,7 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
     // convert blackboxes
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
-        printf( "Hierarchy reader converted %d blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
+        printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) );
         pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk );
         Abc_NtkDelete( pTemp );
         if ( pNtk == NULL )
@@ -284,7 +283,7 @@ Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck )
         }
     }
     // convert the netlist into the logic network
-    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    pNtk = Abc_NtkToLogic( pTemp = pNtk );
     Abc_NtkDelete( pTemp );
     if ( pNtk == NULL )
     {
@@ -350,6 +349,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
         Io_WriteGml( pNtk, pFileName );
         return;
     }
+
     // convert logic network into netlist
     if ( FileType == IO_FILE_PLA )
     {
@@ -359,13 +359,13 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( Abc_NtkIsComb(pNtk) )
-            pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 1 );
+            pNtkTemp = Abc_NtkToNetlist( pNtk, 1 );
         else
         {
             fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
             pNtkCopy = Abc_NtkDup( pNtk );
             Abc_NtkMakeComb( pNtkCopy );
-            pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 1 );
+            pNtkTemp = Abc_NtkToNetlist( pNtk, 1 );
             Abc_NtkDelete( pNtkCopy );
         }
     }
@@ -376,31 +376,37 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             fprintf( stdout, "Writing BENCH is available for AIGs.\n" );
             return;
         }
-        pNtkTemp = Abc_NtkLogicToNetlistBench( pNtk );
+        pNtkTemp = Abc_NtkToNetlistBench( pNtk );
     }
     else
-        pNtkTemp = Abc_NtkLogicToNetlist( pNtk, 0 );
+        pNtkTemp = Abc_NtkToNetlist( pNtk, 0 );
+
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Converting to netlist has failed.\n" );
         return;
     }
+
     if ( FileType == IO_FILE_BLIF )
+    {
+        if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
+            Abc_NtkToSop( pNtkTemp, 0 );
         Io_WriteBlif( pNtkTemp, pFileName, 1 );
+    }
     else if ( FileType == IO_FILE_BENCH )
         Io_WriteBench( pNtkTemp, pFileName );
     else if ( FileType == IO_FILE_PLA )
         Io_WritePla( pNtkTemp, pFileName );
     else if ( FileType == IO_FILE_EQN )
     {
-        if ( Abc_NtkIsSopNetlist(pNtkTemp) )
-            Abc_NtkSopToAig( pNtkTemp );
+        if ( !Abc_NtkHasAig(pNtkTemp) )
+            Abc_NtkToAig( pNtkTemp );
         Io_WriteEqn( pNtkTemp, pFileName );
     }
     else if ( FileType == IO_FILE_VERILOG )
     {
-        if ( Abc_NtkIsSopNetlist(pNtkTemp) )
-            Abc_NtkSopToAig( pNtkTemp );
+        if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
+            Abc_NtkToAig( pNtkTemp );
         Io_WriteVerilog( pNtkTemp, pFileName );
     }
     else 
@@ -451,25 +457,17 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
     // reintroduce the boxes into the netlist
     if ( Abc_NtkBlackboxNum(pNtkBase) > 0 )
     {
-        // bring the current network to the same representation
-        if ( Abc_NtkIsLogic(pNtk) )
-        {
-            if ( Abc_NtkIsSopNetlist(pNtkBase) )
-                Abc_NtkLogicToSop( pNtk, 0 );
-            else if ( Abc_NtkIsAigNetlist(pNtkBase) )
-                Abc_NtkLogicToAig( pNtk );
-        }
         // derive the netlist
-        pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 );
+        pNtkResult = Abc_NtkToNetlist( pNtk, 0 );
         pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult );
         Abc_NtkDelete( pNtkTemp );
         if ( pNtkResult )
-            printf( "Hierarchy writer reintroduced %d blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) );
+            printf( "Hierarchy writer reintroduced %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtkBase) );
     }
     else
     {
         printf( "Warning: The output network does not contain blackboxes.\n" );
-        pNtkResult = Abc_NtkLogicToNetlist( pNtk, 0 );
+        pNtkResult = Abc_NtkToNetlist( pNtk, 0 );
     }
     Abc_NtkDelete( pNtkBase );
     if ( pNtkResult == NULL )
@@ -477,11 +475,15 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
 
     // write the resulting network
     if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF )
+    {
+        if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
+            Abc_NtkToSop( pNtkResult, 0 );
         Io_WriteBlif( pNtkResult, pFileName, 1 );
+    }
     else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG )
     {
-        if ( Abc_NtkIsSopNetlist(pNtkResult) )
-            Abc_NtkSopToAig( pNtkResult );
+        if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
+            Abc_NtkToAig( pNtkResult );
         Io_WriteVerilog( pNtkResult, pFileName );
     }
     else 
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index e48d0be8..417fe2a3 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -32,9 +32,9 @@ static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWriteSubckt( FILE * pFile, Abc_Obj_t * pNode );
 static void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length );
 static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode );
-static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length );
 static void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch );
 
 ////////////////////////////////////////////////////////////////////////
@@ -56,7 +56,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
     Abc_Ntk_t * pNtkTemp;
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
+    pNtkTemp = Abc_NtkToNetlist(pNtk,0);
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Writing BLIF has failed.\n" );
@@ -97,13 +97,22 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
     if ( Abc_NtkBlackboxNum(pNtk) > 0 )
     {
         Abc_Ntk_t * pNtkTemp;
-        Abc_Obj_t * pObj;
         int i;
+/*
+        Abc_Obj_t * pObj;
         Abc_NtkForEachBlackbox( pNtk, pObj, i )
         {
             pNtkTemp = pObj->pData;
             assert( pNtkTemp != NULL && Abc_NtkHasBlackbox(pNtkTemp) );
-            fprintf( pFile, "\n\n", Abc_NtkName(pNtk) );
+            fprintf( pFile, "\n\n" );
+            Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
+        }
+*/
+        Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
+        {
+            if ( pNtkTemp == pNtk )
+                continue;
+            fprintf( pFile, "\n\n" );
             Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
         }
     }
@@ -156,7 +165,7 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
 {
     ProgressBar * pProgress;
     Abc_Obj_t * pNode, * pLatch;
-    int i;
+    int i, Length;
 
     // write the PIs
     fprintf( pFile, ".inputs" );
@@ -206,11 +215,12 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     }
 
     // write each internal node
+    Length = Abc_NtkHasMapping(pNtk)? Mio_LibraryReadGateNameMax(pNtk->pManFunc) : 0;
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        Io_NtkWriteNode( pFile, pNode );
+        Io_NtkWriteNode( pFile, pNode, Length );
     }
     Extra_ProgressBarStop( pProgress );
 }
@@ -454,13 +464,13 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
+void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length )
 {
     if ( Abc_NtkHasMapping(pNode->pNtk) )
     {
         // write the .gate line
         fprintf( pFile, ".gate" );
-        Io_NtkWriteNodeGate( pFile, pNode );
+        Io_NtkWriteNodeGate( pFile, pNode, Length );
         fprintf( pFile, "\n" );
     }
     else
@@ -485,17 +495,17 @@ void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode )
+void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length )
 {
     Mio_Gate_t * pGate = pNode->pData;
     Mio_Pin_t * pGatePin;
     int i;
     // write the node
-    fprintf( pFile, " %s ", Mio_GateReadName(pGate) );
+    fprintf( pFile, " %-*s ", Length, Mio_GateReadName(pGate) );
     for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
         fprintf( pFile, "%s=%s ", Mio_PinReadName(pGatePin), Abc_ObjName( Abc_ObjFanin(pNode,i) ) );
     assert ( i == Abc_ObjFaninNum(pNode) );
-    fprintf( pFile, "%s=%s", Mio_GateReadOutName(pGate), Abc_ObjName(pNode) );
+    fprintf( pFile, "%s=%s", Mio_GateReadOutName(pGate), Abc_ObjName( Abc_ObjFanout0(pNode) ) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 88695668..e1b2d956 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -66,7 +66,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
     }
     // convert to logic BDD network
     if ( Abc_NtkIsLogic(pNtk) )
-        Abc_NtkLogicToBdd( pNtk );
+        Abc_NtkToBdd( pNtk );
     // create solver with clauses
     pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
     if ( pSat == NULL )
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index 9524bdef..bf5182fb 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -34,7 +34,7 @@ static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk );
 static int  Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
-static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+static char * Io_WriteVerilogGetName( char * pName );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,9 +57,9 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     FILE * pFile;
     int i;
     // can only write nodes represented using local AIGs
-    if ( !Abc_NtkIsAigNetlist(pNtk) )
+    if ( !Abc_NtkIsAigNetlist(pNtk) && !Abc_NtkIsMappedNetlist(pNtk) )
     {
-        printf( "Io_WriteVerilog(): Can produce Verilog for AIG netlists only.\n" );
+        printf( "Io_WriteVerilog(): Can produce Verilog for mapped or AIG netlists only.\n" );
         return;
     }
     // start the output stream
@@ -77,16 +77,17 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     // write modules
     if ( pNtk->pDesign )
     {
+        // write the network first
+        Io_WriteVerilogInt( pFile, pNtk );
+        // write other things
         Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNetlist, i )
         {
             assert( Abc_NtkIsNetlist(pNetlist) );
             if ( pNetlist == pNtk )
                 continue;
-            Io_WriteVerilogInt( pFile, pNetlist );
             fprintf( pFile, "\n" );
+            Io_WriteVerilogInt( pFile, pNetlist );
         }
-        // write the network last
-        Io_WriteVerilogInt( pFile, pNtk );
     }
     else
     {
@@ -185,7 +186,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
     {
         pNet = Abc_ObjFanout0(pTerm);
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -193,7 +194,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -224,7 +225,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
     {
         pNet = Abc_ObjFanin0(pTerm);
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -232,7 +233,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -273,7 +274,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             continue;
         Counter++;
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -281,7 +282,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_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -290,7 +291,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj));
         Counter++;
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -298,7 +299,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_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -311,7 +312,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             pNet = Abc_ObjFanin0(pTerm);
             Counter++;
             // get the line length after this name is written
-            AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+            AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
             if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
             { // write the line extender
                 fprintf( pFile, "\n   " );
@@ -319,7 +320,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_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
             LineLength += AddedLength;
             NameCounter++;
         }
@@ -330,7 +331,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
                 continue;
             Counter++;
             // get the line length after this name is written
-            AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+            AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
             if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
             { // write the line extender
                 fprintf( pFile, "\n   " );
@@ -338,7 +339,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_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
             LineLength += AddedLength;
             NameCounter++;
         }
@@ -377,7 +378,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         pNet = Abc_ObjFanout0(Abc_ObjFanout0(pLatch));
         Counter++;
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(pNet)) + 2;
+        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -385,7 +386,7 @@ void Io_WriteVerilogRegs( 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_WriteVerilogGetName(Abc_ObjName(pNet)), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -402,35 +403,6 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogLatches2( FILE * pFile, Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pLatch;
-    int i;
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-//        fprintf( pFile, "  always @(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
-        fprintf( pFile, "  always begin %s",     Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-        fprintf( pFile, " = %s; end\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) );
-        if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
-//            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) );
-            fprintf( pFile, "  initial begin %s = 0; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-        else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
-//            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pLatch)) );
-            fprintf( pFile, "  initial begin %s = 1; end\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the latches.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pLatch;
@@ -442,8 +414,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "  always begin\n" );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        fprintf( pFile, "    %s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
-        fprintf( pFile, " <= %s;\n", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) );
+        fprintf( pFile, "    %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
+        fprintf( pFile, " <= %s;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch)))) );
     }
     fprintf( pFile, "  end\n" );
     // check if there are initial values
@@ -453,13 +425,13 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     if ( i == Abc_NtkLatchNum(pNtk) )
         return;
     // write the initial values
-    fprintf( pFile, "  initial begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) );
+    fprintf( pFile, "  initial begin\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0)))) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
-            fprintf( pFile, "    %s <= 1\'b0;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
+            fprintf( pFile, "    %s <= 1\'b0;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
         else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
-            fprintf( pFile, "    %s <= 1\'b1;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) );
+            fprintf( pFile, "    %s <= 1\'b1;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
     }
     fprintf( pFile, "  end\n" );
 }
@@ -481,48 +453,73 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkBox;
     Abc_Obj_t * pObj, * pTerm, * pFanin;
     Hop_Obj_t * pFunc;
-    int i, k, Counter, nDigits;
-
-    Counter = 1;
-    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+    int i, k, Counter, nDigits, Length;
 
     // write boxes
+    nDigits = Extra_Base10Log( Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
+    Counter = 0;
     Abc_NtkForEachBox( pNtk, pObj, i )
     {
         if ( Abc_ObjIsLatch(pObj) )
             continue;
         pNtkBox = pObj->pData;
-        fprintf( pFile, "  %s g%0*d", pNtkBox->pName, nDigits, Counter++ );
+        fprintf( pFile, "  %s box%0*d", pNtkBox->pName, nDigits, Counter++ );
         fprintf( pFile, "(" );
         Abc_NtkForEachPi( pNtkBox, pTerm, k )
         {
-            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanout0(pTerm)) );
-            fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjFanin0(Abc_ObjFanin(pObj,k))) );
+            fprintf( pFile, ".%s",   Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pTerm))) );
+            fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin(pObj,k)))) );
         }
         Abc_NtkForEachPo( pNtkBox, pTerm, k )
         {
-            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanin0(pTerm)) );
-            fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_ObjFanout(pObj,k))), k==Abc_NtkPoNum(pNtkBox)-1? "":", " );
+            fprintf( pFile, ".%s",   Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin0(pTerm))) );
+            fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout(pObj,k)))), k==Abc_NtkPoNum(pNtkBox)-1? "":", " );
         }
         fprintf( pFile, ");\n" );
     }
     // write nodes
-    vLevels = Vec_VecAlloc( 10 );
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    if ( Abc_NtkHasMapping(pNtk) )
     {
-        pFunc = pObj->pData;
-        fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
-        // set the input names
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(pFanin));
-        // write the formula
-        Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
-        fprintf( pFile, ";\n" );
-        // clear the input names
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            free( Hop_IthVar(pNtk->pManFunc, k)->pData );
+        Length  = Mio_LibraryReadGateNameMax(pNtk->pManFunc);
+        nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+        Counter = 0;
+        Abc_NtkForEachNode( pNtk, pObj, k )
+        {
+            Mio_Gate_t * pGate = pObj->pData;
+            Mio_Pin_t * pGatePin;
+            // write the node
+            fprintf( pFile, "  %-*s g%0*d", Length, Mio_GateReadName(pGate), nDigits, Counter++ );
+            fprintf( pFile, "(" );
+            for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+            {
+                fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_PinReadName(pGatePin)) );
+                fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanin(pObj,i) )) );
+            }
+            assert ( i == Abc_ObjFaninNum(pObj) );
+            fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_GateReadOutName(pGate)) );
+            fprintf( pFile, "(%s)", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanout0(pObj) )) );
+            fprintf( pFile, ");\n" );
+        }
+    }
+    else
+    {
+        vLevels = Vec_VecAlloc( 10 );
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            pFunc = pObj->pData;
+            fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+            // set the input names
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin)));
+            // write the formula
+            Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
+            fprintf( pFile, ";\n" );
+            // clear the input names
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                free( Hop_IthVar(pNtk->pManFunc, k)->pData );
+        }
+        Vec_VecFree( vLevels );
     }
-    Vec_VecFree( vLevels );
 }
 
 /**Function*************************************************************
@@ -577,12 +574,10 @@ int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+char * Io_WriteVerilogGetName( char * pName )
 {
     static char Buffer[500];
-    char * pName;
     int Length, i;
-    pName = Abc_ObjName(pObj);
     Length = strlen(pName);
     // consider the case of a signal having name "0" or "1"
     if ( !(Length == 1 && (pName[0] == '0' || pName[0] == '1')) )