Version abc70302

6 files changed, 391 insertions, 27 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 3603519f..68b2dbd2 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -29,6 +29,7 @@ static int IoCommandRead        ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadAiger   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBaf     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlif    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadBlifMv  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -43,6 +44,7 @@ static int IoCommandWriteHie    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteAiger  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBaf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBench  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCnf    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -78,6 +80,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_aiger",    IoCommandReadAiger,    1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_baf",      IoCommandReadBaf,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv",  IoCommandReadBlif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_bench",    IoCommandReadBench,    1 );
 //    Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
@@ -92,6 +95,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_aiger",   IoCommandWriteAiger,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_baf",     IoCommandWriteBaf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
@@ -371,6 +375,60 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadBlifMv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int fCheck;
+    int c;
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    // read the file using the corresponding file reader
+    pNtk = Io_Read( pFileName, IO_FILE_BLIFMV, fCheck );
+    if ( pNtk == NULL )
+        return 1;
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_blif_mv [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in BLIF-MV format\n" );
+    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" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
@@ -988,13 +1046,18 @@ usage:
 int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
+    int fWriteSymbols;
     int c;
 
+    fWriteSymbols = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 's':
+                fWriteSymbols ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1006,12 +1069,23 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER );
+    if ( fWriteSymbols )
+        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER );
+    else
+    {
+        if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
+        {
+            fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
+            return 1;
+        }
+        Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 );
+    }
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_aiger [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\n" );
     fprintf( pAbc->Err, "\t         write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
+    fprintf( pAbc->Err, "\t-s     : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .aig)\n" );
     return 1;
@@ -1096,7 +1170,7 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_blif [-lh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_blif [-h] <file>\n" );
     fprintf( pAbc->Err, "\t         write the network into a BLIF file\n" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .blif)\n" );
@@ -1114,16 +1188,64 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    char * pFileName;
+    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 output file name
+    pFileName = argv[globalUtilOptind];
+    // call the corresponding file writer
+    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIFMV );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_blif_mv [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the network into a BLIF-MV file\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .blif)\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
+    int fUseLuts;
     int c;
 
+    fUseLuts = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'l':
+                fUseLuts ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1135,12 +1257,22 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
+    if ( !fUseLuts )
+        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
+    else
+    {
+        Abc_Ntk_t * pNtkTemp;
+        pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
+        Abc_NtkToAig( pNtkTemp );
+        Io_WriteBenchLut( pNtkTemp, pFileName );
+        Abc_NtkDelete( pNtkTemp );
+    }
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_bench [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_bench [-lh] <file>\n" );
     fprintf( pAbc->Err, "\t         write the network in BENCH format\n" );
+    fprintf( pAbc->Err, "\t-l     : toggle using LUTs in the output [default = %s]\n", fUseLuts? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .bench)\n" );
     return 1;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 7e23b6e4..45762b77 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -87,7 +87,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fCheck );
 /*=== abcReadVerilog.c ========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcWriteAiger.c =========================================================*/
-extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName );
+extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols );
 /*=== abcWriteBaf.c ===========================================================*/
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBlif.c ==========================================================*/
@@ -98,6 +98,7 @@ extern void               Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteBench.c =========================================================*/
 extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
+extern int                Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ===========================================================*/
 extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes );
 /*=== abcWriteDot.c ===========================================================*/
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 7e54e5e3..bd01f914 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -84,7 +84,8 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     Vec_Str_t * vString;
-    char * pType, ** ppNames;
+    unsigned uTruth[8];
+    char * pType, ** ppNames, * pString;
     int iLine, nNames;
     
     // allocate the empty network
@@ -114,11 +115,71 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
         {
             // get the node name and the node type
             pType = vTokens->pArray[1];
-            if ( strcmp(pType, "DFF") == 0 )
+            if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE
             {
                 pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
                 Abc_LatchSetInit0( pNode );
             }
+            else if ( strcmp(pType, "LUT") == 0 )
+            {
+                ppNames = (char **)vTokens->pArray + 3;
+                nNames  = vTokens->nSize - 3;
+                // check the number of inputs
+                if ( nNames > 8 )
+                {
+                    printf( "%s: Currently cannot read truth tables with more than 8 inputs (%d).\n", Extra_FileReaderGetFileName(p), nNames );
+                    Vec_StrFree( vString );
+                    Abc_NtkDelete( pNtk );
+                    return NULL;
+                }
+                // get the hex string
+                pString = vTokens->pArray[2];
+                if ( strncmp( pString, "0x", 2 ) )
+                {
+                    printf( "%s: The LUT signature (%s) does not look like a hexadecimal beginning with \"0x\".\n", Extra_FileReaderGetFileName(p), pString );
+                    Vec_StrFree( vString );
+                    Abc_NtkDelete( pNtk );
+                    return NULL;
+                }
+                pString += 2;
+                if ( !Extra_ReadHexadecimal( uTruth, pString, nNames ) )
+                {
+                    printf( "%s: Reading hexadecimal number (%s) has failed.\n", Extra_FileReaderGetFileName(p), pString );
+                    Vec_StrFree( vString );
+                    Abc_NtkDelete( pNtk );
+                    return NULL;
+                }
+                // check if the node is a constant node
+                if ( Extra_TruthIsConst0(uTruth, nNames) )
+                {
+                    pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 );
+                    Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
+                }
+                else if ( Extra_TruthIsConst1(uTruth, nNames) )
+                {
+                    pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 );
+                    Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
+                }
+                else
+                {
+                    // create the node
+                    pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
+                    assert( nNames > 0 );
+                    if ( nNames > 1 )
+                        Abc_ObjSetData( pNode, Abc_SopCreateFromTruth(pNtk->pManFunc, nNames, uTruth) );
+                    else if ( pString[0] == '2' )
+                        Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
+                    else if ( pString[0] == '1' )
+                        Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
+                    else
+                    {
+                        printf( "%s: Reading truth table (%s) of single-input node has failed.\n", Extra_FileReaderGetFileName(p), pString );
+                        Vec_StrFree( vString );
+                        Abc_NtkDelete( pNtk );
+                        return NULL;
+                    }
+                }
+            }
             else
             {
                 // create a new node and add it to the network
@@ -144,10 +205,10 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
                 else if ( strncmp(pType, "MUX", 3) == 0 )
                     Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
-                else if ( strncmp(pType, "vdd", 3) == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
                 else if ( strncmp(pType, "gnd", 3) == 0 )
                     Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
+                else if ( strncmp(pType, "vdd", 3) == 0 )
+                    Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
                 else
                 {
                     printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 9845fbab..94ec4316 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( FileType == IO_FILE_AIGER )
-            Io_WriteAiger( pNtk, pFileName );
+            Io_WriteAiger( pNtk, pFileName, 1 );
         else // if ( FileType == IO_FILE_BAF )
             Io_WriteBaf( pNtk, pFileName );
         return;
@@ -310,7 +310,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
     {
         if ( !Abc_NtkIsStrash(pNtk) )
         {
-            fprintf( stdout, "Writing BENCH is available for AIGs.\n" );
+            fprintf( stdout, "Writing traditional BENCH is available for AIGs only (use \"write_bench\").\n" );
             return;
         }
         pNtkTemp = Abc_NtkToNetlistBench( pNtk );
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 00768356..a1ff4456 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -146,7 +146,7 @@ static int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
 {
     ProgressBar * pProgress;
     FILE * pFile;
@@ -225,18 +225,21 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
     // write the buffer
     fwrite( pBuffer, 1, Pos, pFile );
     free( pBuffer );
-/*
+
     // write the symbol table
-    // write PIs
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
-    // write latches
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
-    // write POs
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
-*/
+    if ( fWriteSymbols )
+    {
+        // write PIs
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
+        // write latches
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
+        // write POs
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
+    }
+
     // write the comment
     fprintf( pFile, "c\n" );
     fprintf( pFile, "%s\n", pNtk->pName );
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 4cf320b1..e63489f4 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -24,8 +24,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int    Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk );
-static int    Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode );
+static int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk );
+
+static int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode );
+
+static int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -47,6 +52,11 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
     Abc_Ntk_t * pExdc;
     FILE * pFile;
     assert( Abc_NtkIsSopNetlist(pNtk) );
+    if ( !Io_WriteBenchCheckNames(pNtk) )
+    {
+        fprintf( stdout, "Io_WriteBench(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
+        return 0;
+    }
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
@@ -148,6 +158,163 @@ int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the network in BENCH format with LUTs and DFFRSE.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    Abc_Ntk_t * pExdc;
+    FILE * pFile;
+    assert( Abc_NtkIsAigNetlist(pNtk) );
+    if ( !Io_WriteBenchCheckNames(pNtk) )
+    {
+        fprintf( stdout, "Io_WriteBenchLut(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the BENCH format. Use \"short_names\".\n" );
+        return 0;
+    }
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
+        return 0;
+    }
+    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    // write the network
+    Io_WriteBenchLutOne( pFile, pNtk );
+    // write EXDC network if it exists
+    pExdc = Abc_NtkExdc( pNtk );
+    if ( pExdc )
+        printf( "Io_WriteBench: EXDC is not written (warning).\n" );
+    // finalize the file
+    fclose( pFile );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the network in BENCH format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    Vec_Int_t * vMemory;
+    int i;
+
+    // write the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pNode, i )
+        fprintf( pFile, "INPUT(%s)\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        fprintf( pFile, "%-11s = DFFRSE( %s, gnd, gnd, gnd, gnd )\n", 
+            Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode))), Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
+
+    // write internal nodes
+    vMemory = Vec_IntAlloc( 10000 );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Io_WriteBenchLutOneNode( pFile, pNode, vMemory );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_IntFree( vMemory );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the network in BENCH format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth )
+{
+    Abc_Obj_t * pFanin;
+    unsigned * pTruth;
+    int i, nFanins;
+    assert( Abc_ObjIsNode(pNode) );
+    nFanins = Abc_ObjFaninNum(pNode);
+    assert( nFanins <= 8 );
+    // compute the truth table
+    pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth );
+    if ( Hop_IsComplement(pNode->pData) )
+        Extra_TruthNot( pTruth, pTruth, nFanins );
+    // consider simple cases
+    if ( Extra_TruthIsConst0(pTruth, nFanins) )
+    {
+        fprintf( pFile, "%-11s = gnd\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        return 1;
+    }
+    if ( Extra_TruthIsConst1(pTruth, nFanins) )
+    {
+        fprintf( pFile, "%-11s = vdd\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        return 1;
+    }
+    if ( nFanins == 1 )
+    {
+        fprintf( pFile, "%-11s = LUT 0x%d ( %s )\n",  
+            Abc_ObjName(Abc_ObjFanout0(pNode)), 
+            Abc_NodeIsBuf(pNode)? 2 : 1,
+            Abc_ObjName(Abc_ObjFanin0(pNode)) );
+        return 1;
+    }
+    // write it in the hexadecimal form
+    fprintf( pFile, "%-11s = LUT 0x",  Abc_ObjName(Abc_ObjFanout0(pNode)) );
+    Extra_PrintHexadecimal( pFile, pTruth, nFanins );
+    // write the fanins
+    fprintf( pFile, " (" );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        fprintf( pFile, " %s%s", Abc_ObjName(pFanin), ((i==nFanins-1)? "" : ",") );
+    fprintf( pFile, " )\n" );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the names cannot be written into the bench file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    char * pName;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        for ( pName = Nm_ManFindNameById(pNtk->pManName, i); pName && *pName; pName++ )
+            if ( *pName == '(' || *pName == ')' )
+                return 0;
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////