Merge remote-tracking branch 'upstream/master' into yosys-experimental

9 files changed, 447 insertions, 22 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index a5cffbf4..5cf74ef9 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -24,6 +24,13 @@
 #include "proof/abs/abs.h"
 #include "sat/bmc/bmc.h"
 
+#ifdef WIN32
+#include <process.h> 
+#define unlink _unlink
+#else
+#include <unistd.h>
+#endif
+
 ABC_NAMESPACE_IMPL_START
 
 ////////////////////////////////////////////////////////////////////////
@@ -49,6 +56,7 @@ static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadStatus  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadGig     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadJson    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadSF      ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWrite       ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteHie    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -118,6 +126,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_status",   IoCommandReadStatus,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "&read_gig",     IoCommandReadGig,      0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_json",     IoCommandReadJson,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_sf",       IoCommandReadSF,       0 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_hie",     IoCommandWriteHie,     0 );
@@ -1415,6 +1424,73 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadSF( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Io_TransformSF2PLA( char * pNameIn, char * pNameOut );
+
+    Abc_Ntk_t * pNtk;
+    FILE * pFile;
+    char * pFileName, * pFileTemp = "_temp_sf_.pla";
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
+        return 1;
+    }
+    fclose( pFile );
+    Io_TransformSF2PLA( pFileName, pFileTemp );
+    pNtk = Io_Read( pFileTemp, IO_FILE_PLA, 1, 0 );
+    unlink( pFileTemp );
+    if ( pNtk == NULL )
+        return 1;
+    ABC_FREE( pNtk->pName );
+    pNtk->pName = Extra_FileNameGeneric( pFileName );
+    ABC_FREE( pNtk->pSpec );
+    pNtk->pSpec = Abc_UtilStrsav( pFileName );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    Abc_FrameClearVerifStatus( pAbc );
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_sf [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         reads file in SF format\n" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -2906,17 +2982,36 @@ usage:
 ***********************************************************************/
 int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
 {
+    extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules );
     char * pFileName;
-    int c, fOnlyAnds = 0;
+    int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0;
+    int nLutSize = -1;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'K':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                nLutSize = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( nLutSize < 2 || nLutSize > 6 )
+                    goto usage;
+                break;
+            case 'f':
+                fFixed ^= 1;
+                break;
             case 'a':
                 fOnlyAnds ^= 1;
                 break;
+            case 'm':
+                fNoModules ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -2930,6 +3025,8 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
+    if ( fFixed )
+        nLutSize = 6;
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
@@ -2941,14 +3038,19 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
         Io_WriteVerilog( pNtkTemp, pFileName, 1 );
         Abc_NtkDelete( pNtkTemp );
     }
+    else if ( nLutSize >= 2 && nLutSize <= 6 )
+        Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules );
     else
-    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG );
+        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_verilog [-ah] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the current network in Verilog format\n" );
+    fprintf( pAbc->Err, "\t-K num : write the network using instances of K-LUTs (2 <= K <= 6) [default = not used]\n" );
+    fprintf( pAbc->Err, "\t-f     : toggle using fixed format [default = %s]\n", fFixed? "yes":"no" );
     fprintf( pAbc->Err, "\t-a     : toggle writing expressions with only ANDs (without XORs and MUXes) [default = %s]\n", fOnlyAnds? "yes":"no" );
+    fprintf( pAbc->Err, "\t-m     : toggle writing additional modules [default = %s]\n", !fNoModules? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index f87d971f..9cf41413 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -480,6 +480,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     if ( pCur < pContents + nFileSize && *pCur != 'c' )
     {
         int Counter = 0;
+        int fNodeNames = 0;
         while ( pCur < pContents + nFileSize && *pCur != 'c' )
         {
             // get the terminal type
@@ -490,6 +491,12 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
                 vTerms = pNtkNew->vBoxes;
             else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
                 vTerms = pNtkNew->vPos;
+            else if ( *pCur == 'n' )
+            {
+                fNodeNames++;
+                while ( *pCur++ != '\n' );
+                continue;
+            }
             else
             {
 //                fprintf( stdout, "Wrong terminal type.\n" );
@@ -543,6 +550,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         }
 //        if ( Counter )
 //            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
+        if ( fNodeNames )
+            printf( "Io_ReadAiger(): The names of internal nodes are not supported. Ignoring %d node names.\n", fNodeNames );
     }
     else
     {
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 3ea3fb70..42eb908d 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -88,7 +88,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode, * pNet;
     Vec_Str_t * vString;
-    unsigned uTruth[8];
+    unsigned uTruth[2048];
     char * pType, ** ppNames, * pString;
     int iLine, nNames, nDigits, fLutsPresent = 0;
     
@@ -161,7 +161,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                 ppNames = (char **)vTokens->pArray + 3;
                 nNames  = vTokens->nSize - 3;
                 // check the number of inputs
-                if ( nNames > 8 )
+                if ( nNames > 15 )
                 {
                     printf( "%s: Currently cannot read truth tables with more than 8 inputs (%d).\n", Extra_FileReaderGetFileName(p), nNames );
                     Vec_StrFree( vString );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 405b44d6..e8979c9b 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -22,6 +22,9 @@
 #include "base/main/main.h"
 #include "map/mio/mio.h"
 
+
+
+
 ABC_NAMESPACE_IMPL_START
 
 
@@ -877,10 +880,13 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         return 1;
     }
     // set timing info
-    //Abc_NtkTimeSetArrival( p->pNtkCur, Abc_ObjFanin0(pNet)->Id, (float)TimeRise, (float)TimeFall );
-    Vec_IntPush( p->vInArrs, Abc_ObjFanin0(pNet)->Id );
-    Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeRise) );
-    Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeFall) );
+    //    printf("Debug: Forcing setting of arrival times\n");
+    if (Abc_ObjFaninNum(pNet) >0){
+      Abc_NtkTimeSetArrival( p->pNtkCur, Abc_ObjFanin0(pNet)->Id, (float)TimeRise, (float)TimeFall );
+      Vec_IntPush( p->vInArrs, Abc_ObjFanin0(pNet)->Id );
+      Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeRise) );
+      Vec_IntPush( p->vInArrs, Abc_Float2Int((float)TimeFall) );
+    }
     return 0;
 }
 
@@ -928,7 +934,10 @@ int Io_ReadBlifNetworkOutputRequired( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         return 1;
     }
     // set timing info
-//    Abc_NtkTimeSetRequired( p->pNtkCur, Abc_ObjFanout0(pNet)->Id, (float)TimeRise, (float)TimeFall );
+    //    printf("Setting required time for object %d to R %f F %f\n",
+    //	   Abc_ObjFanout0(pNet)->Id, (float)TimeRise, (float)TimeFall );
+    
+    Abc_NtkTimeSetRequired( p->pNtkCur, Abc_ObjFanout0(pNet)->Id, (float)TimeRise, (float)TimeFall );
     Vec_IntPush( p->vOutReqs, Abc_ObjFanout0(pNet)->Id );
     Vec_IntPush( p->vOutReqs, Abc_Float2Int((float)TimeRise) );
     Vec_IntPush( p->vOutReqs, Abc_Float2Int((float)TimeFall) );
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index c1808ef5..e5c6fe49 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -1351,7 +1351,8 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
     Abc_Ntk_t * pModel;
     Abc_Obj_t * pBox, * pNet, * pTerm;
     char * pToken, * pName, * pName2, ** ppNames;
-    int nEquals, Last, i, k;
+    int nEquals, i, k;
+    word Last;
 
     // split the line into tokens
     nEquals = Io_MvCountChars( pLine, '=' );
@@ -1404,9 +1405,9 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
         pName2 = NULL;
         pName = Abc_ObjName(Abc_ObjFanout0(pTerm));
         for ( k = 0; k < nEquals; k++ )
-            if ( !strcmp( ppNames[2*((k+Last)%nEquals)], pName ) )
+            if ( !strcmp( ppNames[2*(int)((k+Last)%nEquals)], pName ) )
             {
-                pName2 = ppNames[2*((k+Last)%nEquals)+1];
+                pName2 = ppNames[2*(int)((k+Last)%nEquals)+1];
                 Last = k+Last+1;
                 break;
             }
@@ -1656,7 +1657,7 @@ static int Io_MvWriteValues( Abc_Obj_t * pNode, Vec_Str_t * vFunc )
 ***********************************************************************/
 static int Io_MvParseLiteralMv( Io_MvMod_t * p, Abc_Obj_t * pNode, char * pToken, Vec_Str_t * vFunc, int iLit )
 {
-    char Buffer[10];
+    char Buffer[16];
     Io_MvVar_t * pVar;
     Abc_Obj_t * pFanin, * pNet;
     char * pCur, * pNext;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index c6b47b11..ddfcc91a 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -862,6 +862,62 @@ FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mo
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Tranform SF into PLA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_TransformSF2PLA( char * pNameIn, char * pNameOut )
+{
+    int fStart = 0, Size = 1000000;
+    char * pBuffer, * pToken;
+    FILE * pFileIn  = fopen( pNameIn,  "rb" );
+    FILE * pFileOut = fopen( pNameOut, "wb" );
+    if ( pFileIn == NULL )
+    {
+        if ( pFileOut ) fclose( pFileOut );
+        printf( "Cannot open file \"%s\" for reading.\n", pNameIn );
+        return;
+    }
+    if ( pFileOut == NULL )
+    {
+        if ( pFileIn )  fclose( pFileIn );
+        printf( "Cannot open file \"%s\" for reading.\n", pNameOut );
+        return;
+    }
+    pBuffer = ABC_ALLOC( char, Size );
+    fprintf( pFileOut, ".type fd\n" );
+    while ( fgets(pBuffer, Size, pFileIn) )
+    {
+        if ( strstr(pBuffer, "END_SDF") )
+            break;
+        if ( strstr(pBuffer, "SDF") )
+        {
+            char * pRes = fgets(pBuffer, Size, pFileIn);
+            assert( pRes != NULL );
+            if ( (pToken = strtok( pBuffer, " \t\r\n" )) )
+                fprintf( pFileOut, ".i %d\n", atoi(pToken) );
+            if ( (pToken = strtok( NULL, " \t\r\n" )) )
+                fprintf( pFileOut, ".o %d\n", atoi(pToken) );
+            if ( (pToken = strtok( NULL, " \t\r\n" )) )
+                fprintf( pFileOut, ".p %d\n", atoi(pToken) );
+            fStart = 1;
+        }
+        else if ( fStart )
+            fprintf( pFileOut, "%s", pBuffer );
+    }
+    fprintf( pFileOut, ".e\n" );
+    fclose( pFileIn );
+    fclose( pFileOut );
+    ABC_FREE( pBuffer );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 81d64582..23de719e 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -259,7 +259,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
     int i, nFanins;
     assert( Abc_ObjIsNode(pNode) );
     nFanins = Abc_ObjFaninNum(pNode);
-    assert( nFanins <= 8 );
+    assert( nFanins <= 15 );
     // compute the truth table
     pTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNode->pNtk->pManFunc, Hop_Regular((Hop_Obj_t *)pNode->pData), nFanins, vTruth, 0 );
     if ( Hop_IsComplement((Hop_Obj_t *)pNode->pData) )
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index d9687c6e..0ab3c4d2 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -100,7 +100,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
             return;
@@ -463,7 +463,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
             return;
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index 2e481324..e05aed2e 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -567,6 +567,14 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
                 Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin)));
             // write the formula
             Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0, fOnlyAnds );
+            if ( pObj->fPersist )
+            {
+                Abc_Obj_t * pFan0 = Abc_ObjFanin0(Abc_ObjFanin(pObj, 0));
+                Abc_Obj_t * pFan1 = Abc_ObjFanin0(Abc_ObjFanin(pObj, 1));
+                int Cond = Abc_ObjIsNode(pFan0) && Abc_ObjIsNode(pFan1) && !pFan0->fPersist && !pFan1->fPersist;
+                fprintf( pFile, "; // MUXF7 %s\n", Cond ? "":"to be legalized" );
+            }
+            else
             fprintf( pFile, ";\n" );
             // clear the input names
             Abc_ObjForEachFanin( pObj, pFanin, k )
@@ -631,10 +639,8 @@ int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
 char * Io_WriteVerilogGetName( char * pName )
 {
     static char Buffer[500];
-    int Length, i;
-    Length = strlen(pName);
-    // consider the case of a signal having name "0" or "1"
-    if ( !(Length == 1 && (pName[0] == '0' || pName[0] == '1')) )
+    int i, Length = strlen(pName);
+    if ( pName[0] < '0' || pName[0] > '9' )
     {
         for ( i = 0; i < Length; i++ )
             if ( !((pName[i] >= 'a' && pName[i] <= 'z') || 
@@ -653,6 +659,248 @@ char * Io_WriteVerilogGetName( char * pName )
     return Buffer;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Write the network of K-input LUTs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteLutModule( FILE * pFile, int nLutSize )
+{    
+    fprintf( pFile, "module lut%d #( parameter TT = %d\'h0 ) ( input [%d:0] in, output out );\n", nLutSize, 1<<nLutSize, nLutSize-1 );
+    fprintf( pFile, "    assign out = TT[in];\n" );
+    fprintf( pFile, "endmodule\n\n" );
+}
+void Io_WriteFixedModules( FILE * pFile )
+{    
+    fprintf( pFile, "module LUT6 #( parameter INIT = 64\'h0000000000000000 ) (\n" );
+    fprintf( pFile, "    output O,\n" );
+    fprintf( pFile, "    input I0,\n" );
+    fprintf( pFile, "    input I1,\n" );
+    fprintf( pFile, "    input I2,\n" );
+    fprintf( pFile, "    input I3,\n" );
+    fprintf( pFile, "    input I4,\n" );
+    fprintf( pFile, "    input I5\n" );
+    fprintf( pFile, ");\n" );
+    fprintf( pFile, "    assign O = INIT[ {I5, I4, I3, I2, I1, I0} ];\n" );
+    fprintf( pFile, "endmodule\n\n" );
+
+    fprintf( pFile, "module MUXF7 (\n" );
+    fprintf( pFile, "    output O,\n" );
+    fprintf( pFile, "    input I0,\n" );
+    fprintf( pFile, "    input I1,\n" );
+    fprintf( pFile, "    input S\n" );
+    fprintf( pFile, ");\n" );
+    fprintf( pFile, "    assign O = S ? I1 : I0;\n" );
+    fprintf( pFile, "endmodule\n\n" );
+
+    fprintf( pFile, "module MUXF8 (\n" );
+    fprintf( pFile, "    output O,\n" );
+    fprintf( pFile, "    input I0,\n" );
+    fprintf( pFile, "    input I1,\n" );
+    fprintf( pFile, "    input S\n" );
+    fprintf( pFile, ");\n" );
+    fprintf( pFile, "    assign O = S ? I1 : I0;\n" );
+    fprintf( pFile, "endmodule\n\n" );
+}
+void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed )
+{
+    Abc_Ntk_t * pNtkBox;
+    Abc_Obj_t * pObj, * pTerm;
+    int i, k, Counter, nDigits, Length = 0;
+
+    // write boxes
+    nDigits = Abc_Base10Log( Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
+    Counter = 0;
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        pNtkBox = (Abc_Ntk_t *)pObj->pData;
+        fprintf( pFile, "  %s box%0*d", pNtkBox->pName, nDigits, Counter++ );
+        fprintf( pFile, "(" );
+        Abc_NtkForEachPi( pNtkBox, pTerm, 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_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" );
+    }
+
+    // find the longest signal name
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        Length = Abc_MaxInt( Length, strlen(Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj)))) );
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Length = Abc_MaxInt( Length, strlen(Io_WriteVerilogGetName(Abc_ObjName(pTerm))) );
+    }
+
+    // write LUT instances
+    nDigits = Abc_Base10Log( Abc_NtkNodeNum(pNtk) );
+    Counter = 0;
+    if ( fFixed )
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( pObj->fPersist )
+        {
+            int One = Abc_ObjFanin0(Abc_ObjFanin(pObj, 1))->fPersist && Abc_ObjFanin0(Abc_ObjFanin(pObj, 2))->fPersist;
+            fprintf( pFile, "  MUXF%d                       ", 7+One );
+            fprintf( pFile, " mux_%0*d (", nDigits, Counter++ );
+            fprintf( pFile, " %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+            for ( k = Abc_ObjFaninNum(pObj) - 1; k >= 0; k-- )
+                fprintf( pFile, ", %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin(pObj, k))) );
+            fprintf( pFile, " );\n" );
+        }
+        else
+        {
+            word Truth = Abc_SopToTruth( (char *)pObj->pData, Abc_ObjFaninNum(pObj) );
+            fprintf( pFile, "  LUT6 #(64\'h" );
+            fprintf( pFile, "%08x%08x", (unsigned)(Truth >> 32), (unsigned)Truth );
+            fprintf( pFile, ") lut_%0*d (", nDigits, Counter++ );
+            fprintf( pFile, " %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+            for ( k = 0; k < Abc_ObjFaninNum(pObj); k++ )
+                fprintf( pFile, ", %*s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin(pObj, k))) );
+            for (      ; k < 6; k++ )
+                fprintf( pFile, ", %*s", Length, "1\'b0" );
+            fprintf( pFile, " );\n" );
+        }
+    }
+    else
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        word Truth = Abc_SopToTruth( (char *)pObj->pData, Abc_ObjFaninNum(pObj) );
+        fprintf( pFile, "  lut%d #(%d\'h", nLutSize, 1<<nLutSize );
+        if ( nLutSize == 6 )
+            fprintf( pFile, "%08x%08x", (unsigned)(Truth >> 32), (unsigned)Truth );
+        else
+            fprintf( pFile, "%0*x", 1<<(nLutSize-2), Abc_InfoMask(1 << nLutSize) & (unsigned)Truth );
+        fprintf( pFile, ") lut_%0*d ( {", nDigits, Counter++ );
+        for ( k = nLutSize - 1; k >= Abc_ObjFaninNum(pObj); k-- )
+            fprintf( pFile, "%*s, ", Length, "1\'b0" );
+        for ( k = Abc_ObjFaninNum(pObj) - 1; k >= 0; k-- )
+            fprintf( pFile, "%*s%s", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanin(pObj, k))), k==0 ? "":", " );
+        fprintf( pFile, "}, %*s );\n", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
+    }
+}
+void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed )
+{
+    // write inputs and outputs
+//    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
+    fprintf( pFile, "module %s ( ", Io_WriteVerilogGetName(Abc_NtkName(pNtk)) );
+    // add the clock signal if it does not exist
+    if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
+        fprintf( pFile, "clock, " );
+    // write other primary inputs
+    fprintf( pFile, "\n   " );
+    if ( Abc_NtkPiNum(pNtk) > 0  )
+    {
+        Io_WriteVerilogPis( pFile, pNtk, 3 );
+        fprintf( pFile, ",\n   " );
+    }
+    if ( Abc_NtkPoNum(pNtk) > 0  )
+        Io_WriteVerilogPos( pFile, pNtk, 3 );
+    fprintf( pFile, "  );\n\n" );
+    // add the clock signal if it does not exist
+    if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
+        fprintf( pFile, "  input  clock;\n" );
+    // write inputs, outputs, registers, and wires
+    if ( Abc_NtkPiNum(pNtk) > 0  )
+    {
+//        fprintf( pFile, "  input gclk," );
+        fprintf( pFile, "  input " );
+        Io_WriteVerilogPis( pFile, pNtk, 10 );
+        fprintf( pFile, ";\n" );
+    }
+    if ( Abc_NtkPoNum(pNtk) > 0  )
+    {
+        fprintf( pFile, "  output" );
+        Io_WriteVerilogPos( pFile, pNtk, 5 );
+        fprintf( pFile, ";\n\n" );
+    }
+    // if this is not a blackbox, write internal signals
+    if ( !Abc_NtkHasBlackbox(pNtk) )
+    {
+        if ( Abc_NtkLatchNum(pNtk) > 0 )
+        {
+            fprintf( pFile, "  reg" );
+            Io_WriteVerilogRegs( pFile, pNtk, 4 );
+            fprintf( pFile, ";\n\n" );
+        }
+        if ( Io_WriteVerilogWiresCount(pNtk) > 0 )
+        {
+            fprintf( pFile, "  wire" );
+            Io_WriteVerilogWires( pFile, pNtk, 4 );
+            fprintf( pFile, ";\n\n" );
+        }
+        // write nodes
+        Io_WriteVerilogObjectsLut( pFile, pNtk, nLutSize, fFixed );        
+        // write registers
+        if ( Abc_NtkLatchNum(pNtk) > 0 )
+        {
+            fprintf( pFile, "\n" );
+            Io_WriteVerilogLatches( pFile, pNtk );
+        }
+    }
+    // finalize the file
+    fprintf( pFile, "\nendmodule\n\n" );
+} 
+void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules )
+{
+    FILE * pFile;
+    Abc_Ntk_t * pNtkTemp;
+    Abc_Obj_t * pObj; 
+    int i, Counter = 0;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        if ( Abc_ObjFaninNum(pObj) > nLutSize )
+        {
+            if ( Counter < 3 )
+                printf( "Node \"%s\" has the fanin count (%d) larger than the LUT size (%d).\n", Abc_ObjName(pObj), Abc_ObjFaninNum(pObj), nLutSize );
+            Counter++;
+        }
+    if ( Counter )
+    {
+        printf( "In total, %d internal logic nodes exceed the fanin count limit. Verilog is not written.\n", Counter );
+        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
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    fprintf( pFile, "\n" );
+    if ( !fNoModules )
+    {
+        if ( fFixed )
+            Io_WriteFixedModules( pFile );
+        else
+            Io_WriteLutModule( pFile, nLutSize );
+    }
+    pNtkTemp = Abc_NtkToNetlist( pNtk );
+    Abc_NtkToSop( pNtkTemp, -1, ABC_INFINITY );
+    Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize, fFixed );
+    Abc_NtkDelete( pNtkTemp );
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////