summaryrefslogtreecommitdiffstats
path: root/src/base/io
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/io')
-rw-r--r--src/base/io/io.c766
-rw-r--r--src/base/io/io.h74
-rw-r--r--src/base/io/ioInt.h49
-rw-r--r--src/base/io/ioRead.c74
-rw-r--r--src/base/io/ioReadBench.c227
-rw-r--r--src/base/io/ioReadBlif.c642
-rw-r--r--src/base/io/ioReadVerilog.c888
-rw-r--r--src/base/io/ioWriteBench.c224
-rw-r--r--src/base/io/ioWriteBlif.c344
-rw-r--r--src/base/io/ioWriteBlifLogic.c402
-rw-r--r--src/base/io/ioWriteCnf.c76
-rw-r--r--src/base/io/ioWriteGate.c263
-rw-r--r--src/base/io/module.make10
13 files changed, 4039 insertions, 0 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c
new file mode 100644
index 00000000..4698de91
--- /dev/null
+++ b/src/base/io/io.c
@@ -0,0 +1,766 @@
+/**CFile****************************************************************
+
+ FileName [io.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Command file.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: io.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+#include "mainInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
+
+static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteGate ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_Init( Abc_Frame_t * pAbc )
+{
+ Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
+
+ Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_gate", IoCommandWriteGate, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_End()
+{
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ pNtk = Io_Read( FileName, fCheck );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from file has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network from file in Verilog/BLIF/BENCH 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 IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pTemp;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ pNtk = Io_ReadBlif( FileName, fCheck );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from BLIF file has failed.\n" );
+ return 1;
+ }
+
+ pNtk = Abc_NtkLogic( pTemp = pNtk );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+ return 1;
+ }
+
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_blif [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network in binary BLIF 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, * pTemp;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ pNtk = Io_ReadBench( FileName, fCheck );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from BENCH file has failed.\n" );
+ return 1;
+ }
+
+ pNtk = Abc_NtkLogic( pTemp = pNtk );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_bench [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network in BENCH 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 IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pTemp;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ pNtk = Io_ReadVerilog( FileName, fCheck );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from Verilog file has failed.\n" );
+ return 1;
+ }
+
+ pNtk = Abc_NtkLogic( pTemp = pNtk );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ 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, "\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 IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pTemp;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+// pNtk = Io_ReadPla( FileName, fCheck );
+ fprintf( pAbc->Err, "This command is currently not implemented.\n" );
+ pNtk = NULL;
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from PLA file has failed.\n" );
+ return 1;
+ }
+
+ pNtk = Abc_NtkLogic( pTemp = pNtk );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_pla [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network in PLA\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 IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * FileName;
+ int fMadeComb;
+ int fWriteLatches;
+ int c;
+
+ fWriteLatches = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'l':
+ fWriteLatches ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pNtkCur == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ if ( Abc_NtkIsLogicMap(pAbc->pNtkCur) )
+ {
+ fprintf( pAbc->Out, "Use \"write_gate\" or unmap the network (\"unmap\").\n" );
+ return 1;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ if ( Abc_NtkIsNetlist(pAbc->pNtkCur) )
+ {
+ if ( !fWriteLatches )
+ fMadeComb = Abc_NtkMakeComb( pAbc->pNtkCur );
+ Io_WriteBlif( pAbc->pNtkCur, FileName );
+ if ( !fWriteLatches && fMadeComb )
+ Abc_NtkMakeSeq( pAbc->pNtkCur );
+ }
+ else if ( Abc_NtkIsLogicSop(pAbc->pNtkCur) || Abc_NtkIsAig(pAbc->pNtkCur) )
+ {
+ Io_WriteBlifLogic( pAbc->pNtkCur, FileName, fWriteLatches );
+ }
+ else if ( Abc_NtkIsLogicBdd(pAbc->pNtkCur) )
+ {
+// printf( "Converting node functions from BDD to SOP.\n" );
+ Abc_NtkBddToSop(pAbc->pNtkCur);
+ Io_WriteBlifLogic( pAbc->pNtkCur, FileName, fWriteLatches );
+ }
+ else
+ {
+ assert( 0 );
+ }
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_blif [-lh] <file>\n" );
+ fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
+ fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "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;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteGate( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * FileName;
+ int fWriteLatches;
+ int c;
+
+ pNtk = pAbc->pNtkCur;
+ fWriteLatches = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'l':
+ fWriteLatches ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( !Abc_NtkIsLogicMap(pNtk) )
+ {
+ fprintf( pAbc->Out, "The network is not mapped.\n" );
+ return 0;
+ }
+/*
+ if ( Abc_NtkLatchNum(pNtk) > 0 )
+ {
+ fprintf( pAbc->Out, "The network has latches.\n" );
+ return 0;
+ }
+*/
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ Io_WriteGate( pNtk, FileName );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_gate [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the network into a mapped BLIF file (.gate ...)\n" );
+// fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "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;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * FileName;
+ int fWriteLatches;
+ int c;
+
+ pNtk = pAbc->pNtkCur;
+ fWriteLatches = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'l':
+ fWriteLatches ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( !Abc_NtkIsAig(pNtk) )
+ {
+ fprintf( pAbc->Out, "The network should be an AIG.\n" );
+ return 0;
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ Io_WriteBench( pNtk, FileName );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_bench [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the network in BENCH format\n" );
+// fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "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;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * FileName;
+ int c;
+
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pNtkCur == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ if ( !Io_WriteCnf( pAbc->pNtkCur, FileName ) )
+ {
+ printf( "Writing CNF has failed.\n" );
+ return 1;
+ }
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_cnf [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the miter cone into a CNF file\n" );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/io.h b/src/base/io/io.h
new file mode 100644
index 00000000..ba61faac
--- /dev/null
+++ b/src/base/io/io.h
@@ -0,0 +1,74 @@
+/**CFile****************************************************************
+
+ FileName [io.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: io.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __IO_H__
+#define __IO_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define IO_WRITE_LINE_LENGTH 78 // the output line length
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== abcRead.c ==========================================================*/
+extern Abc_Ntk_t * Io_Read( char * pFileName, int fCheck );
+/*=== abcReadBlif.c ==========================================================*/
+extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
+/*=== abcReadBench.c ==========================================================*/
+extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck );
+/*=== abcReadVerilog.c ==========================================================*/
+extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
+extern void Io_ReadSetNonDrivenNets( Abc_Ntk_t * pNet );
+/*=== abcWriteBlif.c ==========================================================*/
+extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName );
+extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
+/*=== abcWriteBlifLogic.c ==========================================================*/
+extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
+/*=== abcWriteBench.c ==========================================================*/
+extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteGate.c ==========================================================*/
+extern int Io_WriteGate( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteCnf.c ==========================================================*/
+extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/base/io/ioInt.h b/src/base/io/ioInt.h
new file mode 100644
index 00000000..69d125fc
--- /dev/null
+++ b/src/base/io/ioInt.h
@@ -0,0 +1,49 @@
+/**CFile****************************************************************
+
+ FileName [ioInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __IO_INT_H__
+#define __IO_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
new file mode 100644
index 00000000..18e4b153
--- /dev/null
+++ b/src/base/io/ioRead.c
@@ -0,0 +1,74 @@
+/**CFile****************************************************************
+
+ FileName [ioRead.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedure to read network from file.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioRead.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Read the network from a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
+{
+ Abc_Ntk_t * pNtk, * pTemp;
+ // set the new network
+ if ( Extra_FileNameCheckExtension( pFileName, "blif" ) )
+ pNtk = Io_ReadBlif( pFileName, fCheck );
+ else if ( Extra_FileNameCheckExtension( pFileName, "v" ) )
+ pNtk = Io_ReadVerilog( pFileName, fCheck );
+ else if ( Extra_FileNameCheckExtension( pFileName, "bench" ) )
+ pNtk = Io_ReadBench( pFileName, fCheck );
+ else
+ {
+ fprintf( stderr, "Unknown file format\n" );
+ return NULL;
+ }
+ if ( pNtk == NULL )
+ return NULL;
+ pNtk = Abc_NtkLogic( pTemp = pNtk );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ {
+ fprintf( stdout, "Converting to logic network after reading has failed.\n" );
+ return NULL;
+ }
+ return pNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
new file mode 100644
index 00000000..0660adc7
--- /dev/null
+++ b/src/base/io/ioReadBench.c
@@ -0,0 +1,227 @@
+/**CFile****************************************************************
+
+ FileName [ioReadBench.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to read BENCH files.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioReadBench.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Read the network from BENCH file.]
+
+ Description [Currently works only for the miter cone.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
+{
+ Extra_FileReader_t * p;
+ Abc_Ntk_t * pNtk;
+
+ // start the file
+ p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r,()=" );
+ if ( p == NULL )
+ return NULL;
+
+ // read the network
+ pNtk = Io_ReadBenchNetwork( p );
+ Extra_FileReaderFree( p );
+ if ( pNtk == NULL )
+ return NULL;
+
+ // make sure that everything is okay with the network structure
+ if ( fCheck && !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Io_ReadBench: The network check has failed.\n" );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ return pNtk;
+}
+/**Function*************************************************************
+
+ Synopsis [Read the network from BENCH file.]
+
+ Description [Currently works only for the miter cone.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
+{
+ ProgressBar * pProgress;
+ Vec_Ptr_t * vTokens;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pNet, * pLatch, * pNode;
+ Vec_Str_t * vString;
+ char * pType;
+ int SymbolIn, SymbolOut, i, iLine;
+
+ // allocate the empty network
+ pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
+
+ // set the specs
+ pNtk->pName = util_strsav( Extra_FileReaderGetFileName(p) );
+ pNtk->pSpec = util_strsav( Extra_FileReaderGetFileName(p) );
+
+ // go through the lines of the file
+ vString = Vec_StrAlloc( 100 );
+ pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
+ for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+ {
+ Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
+
+ if ( vTokens->nSize == 1 )
+ {
+ printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+
+ // get the type of the line
+ if ( strncmp( vTokens->pArray[0], "INPUT", 5 ) == 0 )
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
+ if ( Abc_ObjIsPi(pNet) )
+ printf( "Warning: PI net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
+ else
+ Abc_NtkMarkNetPi( pNet );
+ }
+ else if ( strncmp( vTokens->pArray[0], "OUTPUT", 5 ) == 0 )
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
+ if ( Abc_ObjIsPo(pNet) )
+ printf( "Warning: PO net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
+ else
+ Abc_NtkMarkNetPo( pNet );
+ }
+ else
+ {
+ // get the node name and the node type
+ pType = vTokens->pArray[1];
+ if ( strcmp(pType, "DFF") == 0 )
+ {
+ // create a new node and add it to the network
+ pLatch = Abc_NtkCreateLatch( pNtk );
+ // create the LO (PI)
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[0] );
+ Abc_ObjAddFanin( pNet, pLatch );
+ Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LO );
+ // save the LI (PO)
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[2] );
+ Abc_ObjAddFanin( pLatch, pNet );
+ Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LI );
+ }
+ else
+ {
+ // create a new node and add it to the network
+ pNode = Abc_NtkCreateNode( pNtk );
+ // get the input symbol to be inserted
+ if ( !strncmp(pType, "BUF", 3) || !strcmp(pType, "AND") || !strcmp(pType, "NAND") )
+ SymbolIn = '1';
+ else if ( !strncmp(pType, "NOT", 3) || !strcmp(pType, "OR") || !strcmp(pType, "NOR") )
+ SymbolIn = '0';
+ else if ( !strcmp(pType, "XOR") || !strcmp(pType, "NXOR") )
+ SymbolIn = '*';
+ else
+ {
+ printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ // get the output symbol
+ if ( !strcmp(pType, "NAND") || !strcmp(pType, "OR") || !strcmp(pType, "NXOR") )
+ SymbolOut = '0';
+ else
+ SymbolOut = '1';
+
+ // add the fanout net
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[0] );
+ Abc_ObjAddFanin( pNet, pNode );
+ // add the fanin nets
+ for ( i = 2; i < vTokens->nSize; i++ )
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
+ Abc_ObjAddFanin( pNode, pNet );
+ }
+ if ( SymbolIn != '*' )
+ {
+ // fill in the function
+ Vec_StrFill( vString, vTokens->nSize - 2, (char)SymbolIn );
+ Vec_StrPush( vString, ' ' );
+ Vec_StrPush( vString, (char)SymbolOut );
+ Vec_StrPush( vString, '\n' );
+ Vec_StrPush( vString, '\0' );
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, vString->pArray) );
+ }
+ else
+ { // write XOR/NXOR gates
+ assert( i == 4 );
+ if ( SymbolOut == '1' )
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "01 1\n10 1\n") );
+ else
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "00 1\n11 1\n") );
+ }
+ }
+ }
+ }
+ Extra_ProgressBarStop( pProgress );
+ // check if constant have been added
+ if ( pNet = Abc_NtkFindNet( pNtk, "vdd" ) )
+ {
+ // create the constant 1 node
+ pNode = Abc_NtkCreateNode( pNtk );
+ Abc_ObjAddFanin( pNet, pNode );
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 1\n") );
+ }
+ if ( pNet = Abc_NtkFindNet( pNtk, "gnd" ) )
+ {
+ // create the constant 1 node
+ pNode = Abc_NtkCreateNode( pNtk );
+ Abc_ObjAddFanin( pNet, pNode );
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+ }
+
+ Io_ReadSetNonDrivenNets( pNtk );
+ Vec_StrFree( vString );
+ return pNtk;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
new file mode 100644
index 00000000..6d9c2347
--- /dev/null
+++ b/src/base/io/ioReadBlif.c
@@ -0,0 +1,642 @@
+/**CFile****************************************************************
+
+ FileName [ioReadBlif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to read BLIF files.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioReadBlif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Io_ReadBlif_t_ Io_ReadBlif_t; // all reading info
+struct Io_ReadBlif_t_
+{
+ // general info about file
+ char * pFileName; // the name of the file
+ Extra_FileReader_t* pReader; // the input file reader
+ // current processing info
+ Abc_Ntk_t * pNtk; // the primary network
+ Abc_Ntk_t * pNtkExdc; // the exdc network
+ int fParsingExdc; // this flag is on, when we are parsing EXDC network
+ int LineCur; // the line currently parsed
+ // temporary storage for tokens
+ Vec_Ptr_t * vNewTokens; // the temporary storage for the tokens
+ Vec_Str_t * vCubes; // the temporary storage for the tokens
+ // the error message
+ FILE * Output; // the output stream
+ char sError[1000]; // the error string generated during parsing
+};
+
+static Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName );
+static void Io_ReadBlifFree( Io_ReadBlif_t * p );
+static void Io_ReadBlifPrintErrorMessage( Io_ReadBlif_t * p );
+static Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p );
+static Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p );
+
+static int Io_ReadBlifNetworkInputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
+static int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
+static int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
+static int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens );
+static int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
+static int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Read the network from BLIF file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck )
+{
+ Io_ReadBlif_t * p;
+ Abc_Ntk_t * pNtk, * pNtkExdc;
+
+ // start the file
+ p = Io_ReadBlifFile( pFileName );
+ if ( p == NULL )
+ return NULL;
+
+ // read the network
+ pNtk = Io_ReadBlifNetwork( p );
+ if ( pNtk == NULL )
+ {
+ Io_ReadBlifFree( p );
+ return NULL;
+ }
+ Abc_NtkTimeFinalize( pNtk );
+
+ // read the EXDC network
+ if ( p->fParsingExdc )
+ {
+ pNtkExdc = Io_ReadBlifNetwork( p );
+ if ( pNtkExdc == NULL )
+ {
+ Abc_NtkDelete( pNtk );
+ Io_ReadBlifFree( p );
+ return NULL;
+ }
+ pNtk->pExdc = pNtkExdc;
+ }
+ Io_ReadBlifFree( p );
+
+ // make sure that everything is okay with the network structure
+ if ( fCheck && !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Io_ReadBlif: The network check has failed.\n" );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the reading data structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName )
+{
+ Extra_FileReader_t * pReader;
+ Io_ReadBlif_t * p;
+
+ // start the reader
+ pReader = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r" );
+ if ( pReader == NULL )
+ return NULL;
+
+ // start the reading data structure
+ p = ALLOC( Io_ReadBlif_t, 1 );
+ memset( p, 0, sizeof(Io_ReadBlif_t) );
+ p->pFileName = pFileName;
+ p->pReader = pReader;
+ p->Output = stdout;
+ p->vNewTokens = Vec_PtrAlloc( 100 );
+ p->vCubes = Vec_StrAlloc( 100 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees the data structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadBlifFree( Io_ReadBlif_t * p )
+{
+ Extra_FileReaderFree( p->pReader );
+ Vec_PtrFree( p->vNewTokens );
+ Vec_StrFree( p->vCubes );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the error message including the file name and line number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadBlifPrintErrorMessage( Io_ReadBlif_t * p )
+{
+ if ( p->LineCur == 0 ) // the line number is not given
+ fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
+ else // print the error message with the line number
+ fprintf( p->Output, "%s (line %d): %s\n", p->pFileName, p->LineCur, p->sError );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gets the tokens taking into account the line breaks.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p )
+{
+ Vec_Ptr_t * vTokens;
+ char * pLastToken;
+ int i;
+
+ // get rid of the old tokens
+ if ( p->vNewTokens->nSize > 0 )
+ {
+ for ( i = 0; i < p->vNewTokens->nSize; i++ )
+ free( p->vNewTokens->pArray[i] );
+ p->vNewTokens->nSize = 0;
+ }
+
+ // get the new tokens
+ vTokens = Extra_FileReaderGetTokens(p->pReader);
+ if ( vTokens == NULL )
+ return vTokens;
+
+ // check if there is a transfer to another line
+ pLastToken = vTokens->pArray[vTokens->nSize - 1];
+ if ( pLastToken[ strlen(pLastToken)-1 ] != '\\' )
+ return vTokens;
+
+ // remove the slash
+ pLastToken[ strlen(pLastToken)-1 ] = 0;
+ if ( pLastToken[0] == 0 )
+ vTokens->nSize--;
+ // load them into the new array
+ for ( i = 0; i < vTokens->nSize; i++ )
+ Vec_PtrPush( p->vNewTokens, util_strsav(vTokens->pArray[i]) );
+
+ // load as long as there is the line break
+ while ( 1 )
+ {
+ // get the new tokens
+ vTokens = Extra_FileReaderGetTokens(p->pReader);
+ if ( vTokens->nSize == 0 )
+ return p->vNewTokens;
+ // check if there is a transfer to another line
+ pLastToken = vTokens->pArray[vTokens->nSize - 1];
+ if ( pLastToken[ strlen(pLastToken)-1 ] == '\\' )
+ {
+ // remove the slash
+ pLastToken[ strlen(pLastToken)-1 ] = 0;
+ if ( pLastToken[0] == 0 )
+ vTokens->nSize--;
+ // load them into the new array
+ for ( i = 0; i < vTokens->nSize; i++ )
+ Vec_PtrPush( p->vNewTokens, util_strsav(vTokens->pArray[i]) );
+ continue;
+ }
+ // otherwise, load them and break
+ for ( i = 0; i < vTokens->nSize; i++ )
+ Vec_PtrPush( p->vNewTokens, util_strsav(vTokens->pArray[i]) );
+ break;
+ }
+ return p->vNewTokens;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Reads the BLIF file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
+{
+ ProgressBar * pProgress;
+ Vec_Ptr_t * vTokens;
+ char * pModelName;
+ int iLine, fTokensReady, fStatus;
+
+ // read the model name
+ if ( !p->fParsingExdc )
+ {
+ // read the model name
+ vTokens = Io_ReadBlifGetTokens(p);
+ if ( vTokens == NULL || strcmp( vTokens->pArray[0], ".model" ) )
+ {
+ p->LineCur = 0;
+ sprintf( p->sError, "Wrong input file format." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return NULL;
+ }
+ pModelName = vTokens->pArray[1];
+ // allocate the empty network
+ p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
+ p->pNtk->pName = util_strsav( pModelName );
+ p->pNtk->pSpec = util_strsav( p->pFileName );
+ }
+ else
+ p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
+
+ // read the inputs/outputs
+ pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
+ fTokensReady = fStatus = 0;
+ for ( iLine = 0; fTokensReady || (vTokens = Io_ReadBlifGetTokens(p)); iLine++ )
+ {
+ if ( iLine % 1000 == 0 )
+ Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p->pReader), NULL );
+
+ // consider different line types
+ fTokensReady = 0;
+ if ( !strcmp( vTokens->pArray[0], ".names" ) )
+ { fStatus = Io_ReadBlifNetworkNames( p, &vTokens ); fTokensReady = 1; }
+ else if ( !strcmp( vTokens->pArray[0], ".latch" ) )
+ fStatus = Io_ReadBlifNetworkLatch( p, vTokens );
+ else if ( !strcmp( vTokens->pArray[0], ".inputs" ) )
+ fStatus = Io_ReadBlifNetworkInputs( p, vTokens );
+ else if ( !strcmp( vTokens->pArray[0], ".outputs" ) )
+ fStatus = Io_ReadBlifNetworkOutputs( p, vTokens );
+ else if ( !strcmp( vTokens->pArray[0], ".input_arrival" ) )
+ fStatus = Io_ReadBlifNetworkInputArrival( p, vTokens );
+ else if ( !strcmp( vTokens->pArray[0], ".default_input_arrival" ) )
+ fStatus = Io_ReadBlifNetworkDefaultInputArrival( p, vTokens );
+ else if ( !strcmp( vTokens->pArray[0], ".exdc" ) )
+ { p->fParsingExdc = 1; break; }
+ else if ( !strcmp( vTokens->pArray[0], ".end" ) )
+ break;
+ else
+ printf( "%s (line %d): Skipping directive \"%s\".\n", p->pFileName,
+ Extra_FileReaderGetLineNumber(p->pReader, 0), vTokens->pArray[0] );
+ if ( vTokens == NULL ) // some files do not have ".end" in the end
+ break;
+ if ( fStatus == 1 )
+ return NULL;
+ }
+ Extra_ProgressBarStop( pProgress );
+ Io_ReadSetNonDrivenNets( p->pNtk );
+ return p->pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadBlifNetworkInputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
+{
+ Abc_Ntk_t * pNtk = p->pNtk;
+ Abc_Obj_t * pNet;
+ int i;
+ for ( i = 1; i < vTokens->nSize; i++ )
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
+ if ( Abc_ObjIsPi(pNet) )
+ printf( "Warning: PI net \"%s\" appears twice in the list.\n", vTokens->pArray[i] );
+ else
+ Abc_NtkMarkNetPi( pNet );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
+{
+ Abc_Ntk_t * pNtk = p->pNtk;
+ Abc_Obj_t * pNet;
+ int i;
+ for ( i = 1; i < vTokens->nSize; i++ )
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
+ if ( Abc_ObjIsPo(pNet) )
+ printf( "Warning: PO net \"%s\" appears twice in the list.\n", vTokens->pArray[i] );
+ else
+ Abc_NtkMarkNetPo( pNet );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
+{
+ Abc_Ntk_t * pNtk = p->pNtk;
+ Abc_Obj_t * pNet, * pLatch;
+ int ResetValue;
+
+ if ( vTokens->nSize < 3 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "The .latch line does not have enough tokens." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ // create a new node and add it to the network
+ pLatch = Abc_NtkCreateLatch( pNtk );
+ // create the LO (PI)
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[2] );
+ Abc_ObjAddFanin( pNet, pLatch );
+ Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LO );
+ // save the LI (PO)
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
+ Abc_ObjAddFanin( pLatch, pNet );
+ Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LI );
+ // get the latch reset value
+ if ( vTokens->nSize == 3 )
+ ResetValue = 2;
+ else
+ {
+ ResetValue = atoi(vTokens->pArray[3]);
+ if ( ResetValue != 0 && ResetValue != 1 && ResetValue != 2 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "The .latch line has an unknown reset value (%s).", vTokens->pArray[3] );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ }
+ Abc_ObjSetData( pLatch, (void *)ResetValue );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
+{
+ Vec_Ptr_t * vTokens = *pvTokens;
+ Abc_Ntk_t * pNtk = p->pNtk;
+ Abc_Obj_t * pNet, * pNode;
+ char * pToken, Char;
+ int i, nFanins;
+
+ // create a new node and add it to the network
+ pNode = Abc_NtkCreateNode( pNtk );
+ if ( vTokens->nSize < 2 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "The .names line has less than two tokens." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ // go through the nets
+ for ( i = 1; i < vTokens->nSize - 1; i++ )
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
+ Abc_ObjAddFanin( pNode, pNet );
+ }
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[vTokens->nSize - 1] );
+ Abc_ObjAddFanin( pNet, pNode );
+
+ // derive the functionality of the node
+ p->vCubes->nSize = 0;
+ nFanins = vTokens->nSize - 2;
+ if ( nFanins == 0 )
+ while ( vTokens = Io_ReadBlifGetTokens(p) )
+ {
+ pToken = vTokens->pArray[0];
+ if ( pToken[0] == '.' )
+ break;
+ // read the cube
+ if ( vTokens->nSize != 1 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "The number of tokens in the constant cube is wrong." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ // create the cube
+ Char = ((char *)vTokens->pArray[0])[0];
+ Vec_StrPush( p->vCubes, ' ' );
+ Vec_StrPush( p->vCubes, Char );
+ Vec_StrPush( p->vCubes, '\n' );
+ }
+ else
+ while ( vTokens = Io_ReadBlifGetTokens(p) )
+ {
+ pToken = vTokens->pArray[0];
+ if ( pToken[0] == '.' )
+ break;
+ // read the cube
+ if ( vTokens->nSize != 2 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "The number of tokens in the cube is wrong." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ // create the cube
+ for ( i = 0; i < nFanins; i++ )
+ Vec_StrPush( p->vCubes, ((char *)vTokens->pArray[0])[i] );
+ // check the char
+ Char = ((char *)vTokens->pArray[1])[0];
+ if ( Char != '0' && Char != '1' )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "The output character in the constant cube is wrong." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ Vec_StrPush( p->vCubes, ' ' );
+ Vec_StrPush( p->vCubes, Char );
+ Vec_StrPush( p->vCubes, '\n' );
+ }
+ // if there is nothing there
+ if ( p->vCubes->nSize == 0 )
+ {
+ // create an empty cube
+ Vec_StrPush( p->vCubes, ' ' );
+ Vec_StrPush( p->vCubes, '0' );
+ Vec_StrPush( p->vCubes, '\n' );
+ }
+ Vec_StrPush( p->vCubes, 0 );
+ // set the pointer to the functionality of the node
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, p->vCubes->pArray) );
+ // return the last array of tokens
+ *pvTokens = vTokens;
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
+{
+ Abc_Obj_t * pNet;
+ char * pFoo1, * pFoo2;
+ double TimeRise, TimeFall;
+
+ // make sure this is indeed the .inputs line
+ assert( strncmp( vTokens->pArray[0], ".input_arrival", 14 ) == 0 );
+ if ( vTokens->nSize != 4 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "Wrong number of arguments on .input_arrival line." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ pNet = Abc_NtkFindNet( p->pNtk, vTokens->pArray[1] );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "Cannot find object corresponding to %s on .input_arrival line.", vTokens->pArray[1] );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ TimeRise = strtod( vTokens->pArray[2], &pFoo1 );
+ TimeFall = strtod( vTokens->pArray[3], &pFoo2 );
+ if ( *pFoo1 != '\0' || *pFoo2 != '\0' )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "Bad value (%s %s) for rise or fall time on .input_arrival line.", vTokens->pArray[2], vTokens->pArray[3] );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ // set the arrival time
+ Abc_NtkTimeSetArrival( p->pNtk, pNet->Id, (float)TimeRise, (float)TimeFall );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
+{
+ char * pFoo1, * pFoo2;
+ double TimeRise, TimeFall;
+
+ // make sure this is indeed the .inputs line
+ assert( strncmp( vTokens->pArray[0], ".default_input_arrival", 23 ) == 0 );
+ if ( vTokens->nSize != 3 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "Wrong number of arguments on .default_input_arrival line." );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ TimeRise = strtod( vTokens->pArray[1], &pFoo1 );
+ TimeFall = strtod( vTokens->pArray[2], &pFoo2 );
+ if ( *pFoo1 != '\0' || *pFoo2 != '\0' )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+ sprintf( p->sError, "Bad value (%s %s) for rise or fall time on .default_input_arrival line.", vTokens->pArray[1], vTokens->pArray[2] );
+ Io_ReadBlifPrintErrorMessage( p );
+ return 1;
+ }
+ // set the arrival time
+ Abc_NtkTimeSetDefaultArrival( p->pNtk, (float)TimeRise, (float)TimeFall );
+ return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
new file mode 100644
index 00000000..a3b5a0bf
--- /dev/null
+++ b/src/base/io/ioReadVerilog.c
@@ -0,0 +1,888 @@
+/**CFile****************************************************************
+
+ FileName [ioReadVerilog.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to read a subset of structural Verilog from IWLS 2005 benchmark.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioReadVerilog.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Io_ReadVer_t_ Io_ReadVer_t; // all reading info
+struct Io_ReadVer_t_
+{
+ // general info about file
+ char * pFileName; // the name of the file
+ Extra_FileReader_t* pReader; // the input file reader
+ // current processing info
+ st_table * tKeywords; // mapping of keywords into codes
+ Abc_Ntk_t * pNtk; // the primary network
+ // the error message
+ FILE * Output; // the output stream
+ char sError[1000]; // the error string generated during parsing
+ int LineCur; // the line currently being parsed
+ Vec_Ptr_t * vSkipped; // temporary storage for skipped objects
+};
+
+// verilog keyword types
+typedef enum {
+ VER_NONE = 0,
+ VER_MODULE = -1,
+ VER_ENDMODULE = -2,
+ VER_INPUT = -3,
+ VER_OUTPUT = -4,
+ VER_INOUT = -5,
+ VER_WIRE = -6,
+ VER_ASSIGN = -7
+} Ver_KeywordType_t;
+
+// the list of verilog keywords
+static char * s_Keywords[10] =
+{
+ NULL, // unused
+ "module", // -1
+ "endmodule", // -2
+ "input", // -3
+ "output", // -4
+ "inout", // -5
+ "wire", // -6
+ "assign" // -7
+};
+
+// the list of gates in the Cadence library
+static char * s_CadenceGates[40][5] =
+{
+ { "INVX1", "1", "1", "0 1\n", NULL }, // 0
+ { "INVX2", "1", "1", "0 1\n", NULL }, // 1
+ { "INVX4", "1", "1", "0 1\n", NULL }, // 2
+ { "INVX8", "1", "1", "0 1\n", NULL }, // 3
+ { "BUFX1", "1", "1", "1 1\n", NULL }, // 4
+ { "BUFX3", "1", "1", "1 1\n", NULL }, // 5
+ { "NOR2X1", "2", "1", "00 1\n", NULL }, // 6
+ { "NOR3X1", "3", "1", "000 1\n", NULL }, // 7
+ { "NOR4X1", "4", "1", "0000 1\n", NULL }, // 8
+ { "NAND2X1", "2", "1", "11 0\n", NULL }, // 9
+ { "NAND2X2", "2", "1", "11 0\n", NULL }, // 10
+ { "NAND3X1", "3", "1", "111 0\n", NULL }, // 11
+ { "NAND4X1", "4", "1", "1111 0\n", NULL }, // 12
+ { "OR2X1", "2", "1", "00 0\n", NULL }, // 13
+ { "OR4X1", "4", "1", "0000 0\n", NULL }, // 14
+ { "AND2X1", "2", "1", "11 1\n", NULL }, // 15
+ { "XOR2X1", "2", "1", "01 1\n10 1\n", NULL }, // 16
+ { "MX2X1", "3", "1", "01- 1\n1-1 1\n", NULL }, // 17
+ { "OAI21X1", "3", "1", "00- 1\n--0 1\n", NULL }, // 18
+ { "OAI22X1", "4", "1", "00-- 1\n--00 1\n", NULL }, // 19
+ { "OAI33X1", "6", "1", "000--- 1\n---000 1\n", NULL }, // 20
+ { "AOI21X1", "3", "1", "11- 0\n--1 0\n", NULL }, // 21
+ { "AOI22X1", "4", "1", "11-- 0\n--11 0\n", NULL }, // 22
+ { "CLKBUFX1", "1", "1", "1 1\n", NULL }, // 23
+ { "CLKBUFX2", "1", "1", "1 1\n", NULL }, // 24
+ { "CLKBUFX3", "1", "1", "1 1\n", NULL }, // 25
+ { "ADDHX1", "2", "2", "11 1\n", "01 1\n10 1\n" }, // 26
+ { "ADDFX1", "3", "2", "11- 1\n-11 1\n1-1 1\n", "001 1\n010 1\n100 1\n111 1\n" }, // 27
+ { "DFFSRX1", "1", "1", NULL, NULL }, // 28
+ { "DFFX1", "1", "1", NULL, NULL }, // 29
+ { "SDFFSRX1", "1", "1", NULL, NULL }, // 30
+ { "TLATSRX1", "1", "1", NULL, NULL }, // 31
+ { "TLATX1", "1", "1", NULL, NULL }, // 32
+ { "TBUFX1", "1", "1", NULL, NULL }, // 33
+ { "TBUFX2", "1", "1", NULL, NULL }, // 34
+ { "TBUFX4", "1", "1", NULL, NULL }, // 35
+ { "TBUFX8", "1", "1", NULL, NULL }, // 36
+ { "TINVX1", "1", "1", NULL, NULL } // 37
+};
+
+static Io_ReadVer_t * Io_ReadVerFile( char * pFileName );
+static Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p );
+static bool Io_ReadVerNetworkAssign( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens );
+static bool Io_ReadVerNetworkSignal( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens, int LineType );
+static bool Io_ReadVerNetworkGateSimple( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens, int LineType );
+static bool Io_ReadVerNetworkGateComplex( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens, int LineType );
+static bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens );
+static void Io_ReadVerPrintErrorMessage( Io_ReadVer_t * p );
+static void Io_ReadVerFree( Io_ReadVer_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Read the network from BENCH file.]
+
+ Description [Currently works only for the miter cone.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
+{
+ Io_ReadVer_t * p;
+ Abc_Ntk_t * pNtk;
+
+ // start the file
+ p = Io_ReadVerFile( pFileName );
+ if ( p == NULL )
+ return NULL;
+
+ // read the network
+ pNtk = Io_ReadVerNetwork( p );
+ Io_ReadVerFree( p );
+ if ( pNtk == NULL )
+ return NULL;
+
+ // make sure that everything is okay with the network structure
+ if ( fCheck && !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Io_ReadVerilog: The network check has failed.\n" );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the reading data structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Io_ReadVer_t * Io_ReadVerFile( char * pFileName )
+{
+ Extra_FileReader_t * pReader;
+ Io_ReadVer_t * p;
+ int i;
+
+ // start the reader
+ pReader = Extra_FileReaderAlloc( pFileName, "/", ";", " \t\r\n,()" );
+ if ( pReader == NULL )
+ return NULL;
+
+ // start the reading data structure
+ p = ALLOC( Io_ReadVer_t, 1 );
+ memset( p, 0, sizeof(Io_ReadVer_t) );
+ p->pFileName = pFileName;
+ p->pReader = pReader;
+ p->Output = stdout;
+ p->vSkipped = Vec_PtrAlloc( 100 );
+
+ // insert the keywords and gate names into the hash table
+ p->tKeywords = st_init_table(strcmp, st_strhash);
+ for ( i = 0; i < 10; i++ )
+ if ( s_Keywords[i] )
+ st_insert( p->tKeywords, (char *)s_Keywords[i], (char *)-i );
+ for ( i = 0; i < 40; i++ )
+ if ( s_CadenceGates[i][0] )
+ st_insert( p->tKeywords, (char *)s_CadenceGates[i][0], (char *)i );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees the data structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadVerFree( Io_ReadVer_t * p )
+{
+ Extra_FileReaderFree( p->pReader );
+ Vec_PtrFree( p->vSkipped );
+ st_free_table( p->tKeywords );
+ FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the error message including the file name and line number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadVerPrintErrorMessage( Io_ReadVer_t * p )
+{
+ if ( p->LineCur == 0 ) // the line number is not given
+ fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
+ else // print the error message with the line number
+ fprintf( p->Output, "%s (line %d): %s\n", p->pFileName, p->LineCur, p->sError );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the verilog file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p )
+{
+ char Buffer[1000];
+ ProgressBar * pProgress;
+ Ver_KeywordType_t LineType;
+ Vec_Ptr_t * vTokens;
+ Abc_Ntk_t * pNtk;
+ char * pModelName;
+ int i;
+
+ // read the model name
+ vTokens = Extra_FileReaderGetTokens( p->pReader );
+ if ( vTokens == NULL || strcmp( vTokens->pArray[0], "module" ) )
+ {
+ p->LineCur = 0;
+ sprintf( p->sError, "Wrong input file format." );
+ Io_ReadVerPrintErrorMessage( p );
+ return NULL;
+ }
+ pModelName = vTokens->pArray[1];
+
+ // allocate the empty network
+ pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
+ pNtk->pName = util_strsav( pModelName );
+ pNtk->pSpec = util_strsav( p->pFileName );
+
+ // read the inputs/outputs
+ pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
+ for ( i = 0; vTokens = Extra_FileReaderGetTokens(p->pReader); i++ )
+ {
+ Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p->pReader), NULL );
+
+ // get the line type
+ if ( !st_lookup( p->tKeywords, vTokens->pArray[0], (char **)&LineType ) )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "The first token \"%s\" cannot be recognized.", vTokens->pArray[0] );
+ Io_ReadVerPrintErrorMessage( p );
+ return NULL;
+ }
+ // consider Verilog directives
+ if ( LineType < 0 )
+ {
+ if ( LineType == VER_ENDMODULE )
+ break;
+ if ( LineType == VER_ASSIGN )
+ {
+ if ( !Io_ReadVerNetworkAssign( p, pNtk, vTokens ) )
+ return NULL;
+ continue;
+ }
+ if ( !Io_ReadVerNetworkSignal( p, pNtk, vTokens, LineType ) )
+ return NULL;
+ continue;
+ }
+ // proces single output gates
+ if ( LineType < 26 )
+ {
+ if ( !Io_ReadVerNetworkGateSimple( p, pNtk, vTokens, LineType ) )
+ return NULL;
+ continue;
+ }
+ // process complex gates
+ if ( LineType < 28 )
+ {
+ if ( !Io_ReadVerNetworkGateComplex( p, pNtk, vTokens, LineType ) )
+ return NULL;
+ continue;
+
+ }
+ // process the latches
+ if ( LineType < 33 )
+ {
+ if ( !Io_ReadVerNetworkLatch( p, pNtk, vTokens ) )
+ return NULL;
+ continue;
+ }
+ // add the tri-state element to the skipped ones
+ sprintf( Buffer, "%s %s", vTokens->pArray[0], vTokens->pArray[1] );
+ Vec_PtrPush( p->vSkipped, util_strsav(Buffer) );
+ }
+ Extra_ProgressBarStop( pProgress );
+
+ if ( p->vSkipped->nSize > 0 )
+ {
+ printf( "IoReadVerilog() skipped %d tri-state elements:\n", p->vSkipped->nSize );
+ for ( i = 0; i < p->vSkipped->nSize; i++ )
+ {
+ if ( i < 2 )
+ printf( "%s,\n", p->vSkipped->pArray[i] );
+ else
+ {
+ printf( "%s, etc.\n", p->vSkipped->pArray[i] );
+ break;
+ }
+ }
+ for ( i = 0; i < p->vSkipped->nSize; i++ )
+ free( p->vSkipped->pArray[i] );
+ }
+ Io_ReadSetNonDrivenNets( pNtk );
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads one assign directive in the verilog file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Io_ReadVerNetworkAssign( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens )
+{
+ Abc_Obj_t * pNet, * pNode;
+
+ assert( strcmp( vTokens->pArray[0], "assign" ) == 0 );
+
+ if ( strcmp( vTokens->pArray[3], "1'b0" ) != 0 && strcmp( vTokens->pArray[3], "1'b1" ) != 0 )
+ {
+ // handle assignment to a variable
+ if ( vTokens->nSize == 4 && (pNet = Abc_NtkFindNet(pNtk, vTokens->pArray[3])) )
+ {
+ // allocate the buffer node
+ pNode = Abc_NtkCreateNode( pNtk );
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1 1\n") );
+ // add the fanin net
+ Abc_ObjAddFanin( pNode, pNet );
+ // add the fanout net
+ pNet = Abc_NtkFindNet(pNtk, vTokens->pArray[1]);
+ Abc_ObjAddFanin( pNet, pNode );
+ return 1;
+ }
+ // produce error in case of more complex assignment
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "The assign operator is handled only for assignment to a variable and a constant." );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ // allocate constant node
+ pNode = Abc_NtkCreateNode( pNtk );
+ // set the constant function
+ if ( ((char *)vTokens->pArray[3])[3] == '0' )
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+ else
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 1\n") );
+ // set the fanout net
+ pNet = Abc_NtkFindNet( pNtk, vTokens->pArray[1] );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
+ sprintf( p->sError, "Cannot find net \"%s\".", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNet, pNode );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads one signal the verilog file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Io_ReadVerNetworkSignal( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens, int LineType )
+{
+ char Buffer[1000];
+ Abc_Obj_t * pNet;
+ char * pToken;
+ int nSignals, k, Start, s;
+
+ nSignals = 0;
+ pToken = vTokens->pArray[1];
+ if ( pToken[0] == '[' )
+ {
+ nSignals = atoi(pToken + 1) + 1;
+ if ( nSignals < 1 || nSignals > 1024 )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Incorrect number of signals in the expression \"%s\".", pToken );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ if ( nSignals == 1 )
+ nSignals = 0;
+ Start = 2;
+ }
+ else
+ Start = 1;
+ for ( k = Start; k < vTokens->nSize; k++ )
+ {
+ pToken = vTokens->pArray[k];
+ // print the signal name
+ if ( nSignals )
+ {
+ for ( s = 0; s < nSignals; s++ )
+ {
+ sprintf( Buffer, "%s[%d]", pToken, s );
+ pNet = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+ if ( LineType == VER_INPUT || LineType == VER_INOUT )
+ Abc_NtkMarkNetPi( pNet );
+ if ( LineType == VER_OUTPUT || LineType == VER_INOUT )
+ Abc_NtkMarkNetPo( pNet );
+ }
+ }
+ else
+ {
+ pNet = Abc_NtkFindOrCreateNet( pNtk, pToken );
+ if ( LineType == VER_INPUT || LineType == VER_INOUT )
+ Abc_NtkMarkNetPi( pNet );
+ if ( LineType == VER_OUTPUT || LineType == VER_INOUT )
+ Abc_NtkMarkNetPo( pNet );
+ }
+ }
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Reads a simple gate from the verilog file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Io_ReadVerNetworkGateSimple( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens, int LineType )
+{
+ Abc_Obj_t * pNode, * pNet, * pNodeConst, * pNetConst;
+ char * pToken;
+ int nFanins, k;
+
+ // create the node
+ pNode = Abc_NtkCreateNode( pNtk );
+ // set the function
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, s_CadenceGates[LineType][3]) );
+ // skip the gate type and gate name
+ // add the fanin nets
+ nFanins = s_CadenceGates[LineType][1][0] - '0';
+ for ( k = 2; k < vTokens->nSize - 1; k++ )
+ {
+ pToken = vTokens->pArray[k];
+ if ( pToken[0] == '.' )
+ continue;
+ pNet = Abc_NtkFindNet( pNtk, pToken );
+ if ( pNet )
+ {
+ Abc_ObjAddFanin( pNode, pNet );
+ continue;
+ }
+ // handle the case of a constant
+ if ( strcmp( pToken, "1'b0" ) == 0 || strcmp( pToken, "1'b1" ) == 0 )
+ {
+ // create the net and link it to the node
+ pNetConst = Abc_NtkFindOrCreateNet( pNtk, pToken );
+ Abc_ObjAddFanin( pNode, pNetConst );
+ // allocate constant node
+ pNodeConst = Abc_NtkCreateNode( pNtk );
+ // set the constant function
+ if ( pToken[3] == '0' )
+ Abc_ObjSetData( pNodeConst, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+ else
+ Abc_ObjSetData( pNodeConst, Abc_SopRegister(pNtk->pManFunc, " 1\n") );
+ // add this node as the fanin of the constant net
+ Abc_ObjAddFanin( pNetConst, pNodeConst );
+ continue;
+ }
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find net \"%s\".", pToken );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ if ( Abc_ObjFaninNum(pNode) != nFanins )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Gate \"%s\" has a wrong number of inputs.", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+
+ // add the fanout net
+ pToken = vTokens->pArray[vTokens->nSize - 1];
+ if ( pToken[0] == '.' )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Gate \"%s\" does not have a fanout.", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ pNet = Abc_NtkFindNet( pNtk, pToken );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find net \"%s\".", pToken );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNet, pNode );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads a complex gate from the verilog file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Io_ReadVerNetworkGateComplex( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens, int LineType )
+{
+ Abc_Obj_t * pNode1, * pNode2, * pNet;
+ char * pToken, * pToken1, * pToken2;
+ int nFanins, k;
+
+ // create the nodes
+ pNode1 = Abc_NtkCreateNode( pNtk );
+ Abc_ObjSetData( pNode1, Abc_SopRegister(pNtk->pManFunc, s_CadenceGates[LineType][3]) );
+ pNode2 = Abc_NtkCreateNode( pNtk );
+ Abc_ObjSetData( pNode2, Abc_SopRegister(pNtk->pManFunc, s_CadenceGates[LineType][4]) );
+ // skip the gate type and gate name
+ // add the fanin nets
+ nFanins = s_CadenceGates[LineType][1][0] - '0';
+ for ( k = 2; k < vTokens->nSize; k++ )
+ {
+ pToken = vTokens->pArray[k];
+ if ( pToken[0] == '.' )
+ continue;
+ pNet = Abc_NtkFindNet( pNtk, pToken );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find net \"%s\".", pToken );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNode1, pNet );
+ Abc_ObjAddFanin( pNode2, pNet );
+ if ( Abc_ObjFaninNum(pNode1) == nFanins )
+ {
+ k++;
+ break;
+ }
+ }
+ // find the tokens corresponding to the output
+ pToken1 = pToken2 = NULL;
+ for ( ; k < vTokens->nSize; k++ )
+ {
+ pToken = vTokens->pArray[k];
+ if ( pToken[0] == '.' )
+ continue;
+ if ( pToken1 == NULL )
+ pToken1 = pToken;
+ else
+ pToken2 = pToken;
+ }
+ // quit if one of the tokens is not given
+ if ( pToken1 == NULL || pToken2 == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "An output of a two-output gate \"%s\" is not specified.", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+
+ // add the fanout net
+ pNet = Abc_NtkFindNet( pNtk, pToken1 );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find net \"%s\".", pToken1 );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNet, pNode1 );
+
+ // add the fanout net
+ pNet = Abc_NtkFindNet( pNtk, pToken2 );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find net \"%s\".", pToken2 );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNet, pNode2 );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads a latch from the verilog file.]
+
+ Description [This procedure treats T-latch as if it were D-latch.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens )
+{
+ Abc_Obj_t * pLatch, * pNet, * pNode;
+ char * pToken, * pToken2, * pTokenRN, * pTokenSN, * pTokenSI, * pTokenSE, * pTokenD, * pTokenQ, * pTokenQN;
+ int k, fRN1, fSN1;
+
+ // collect the FF signals
+ pTokenRN = pTokenSN = pTokenSI = pTokenSE = pTokenD = pTokenQ = pTokenQN = NULL;
+ for ( k = 2; k < vTokens->nSize-1; k++ )
+ {
+ pToken = vTokens->pArray[k];
+ pToken2 = vTokens->pArray[k+1];
+ if ( pToken[1] == 'R' && pToken[2] == 'N' && pToken[3] == 0 )
+ pTokenRN = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'S' && pToken[2] == 'N' && pToken[3] == 0 )
+ pTokenSN = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'S' && pToken[2] == 'I' && pToken[3] == 0 )
+ pTokenSI = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'S' && pToken[2] == 'E' && pToken[3] == 0 )
+ pTokenSE = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'D' && pToken[2] == 0 )
+ pTokenD = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'Q' && pToken[2] == 0 )
+ pTokenQ = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'Q' && pToken[2] == 'N' && pToken[3] == 0 )
+ pTokenQN = (pToken2[0] == '.')? NULL : pToken2;
+ else if ( pToken[1] == 'C' && pToken[2] == 'K' && pToken[3] == 0 ) {}
+ else
+ assert( 0 );
+ if ( pToken2[0] != '.' )
+ k++;
+ }
+
+ if ( pTokenD == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
+ sprintf( p->sError, "Cannot read pin D of the latch \"%s\".", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ if ( pTokenQ == NULL && pTokenQN == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
+ sprintf( p->sError, "Cannot read pins Q/QN of the latch \"%s\".", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ if ( (pTokenRN == NULL) ^ (pTokenSN == NULL) )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
+ sprintf( p->sError, "Cannot read pins RN/SN of the latch \"%s\".", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+
+ // create the latch
+ pLatch = Abc_NtkCreateLatch( pNtk );
+ // create the LO (PI)
+ pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
+ Abc_ObjAddFanin( pNet, pLatch );
+ Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LO );
+ // save the LI (PO)
+ pNet = Abc_NtkFindNet( pNtk, pTokenD );
+ if ( pNet == NULL )
+ {
+ // check the case if it is not a constant input
+ if ( strcmp( pTokenD, "1'b0" ) && strcmp( pTokenD, "1'b1" ) )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find latch input net \"%s\".", pTokenD );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+
+ // create the constant net
+ if ( strcmp( pTokenD, "1'b0" ) == 0 )
+ pNet = Abc_NtkFindOrCreateNet( pNtk, "Constant0" );
+ else
+ pNet = Abc_NtkFindOrCreateNet( pNtk, "Constant1" );
+
+ // drive it with the constant node
+ if ( Abc_ObjFaninNum( pNet ) == 0 )
+ {
+ // allocate constant node
+ pNode = Abc_NtkCreateNode( pNtk );
+ // set the constant function
+ if ( strcmp( pTokenD, "1'b0" ) == 0 )
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+ else
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 1\n") );
+ // add the fanout net
+ Abc_ObjAddFanin( pNet, pNode );
+ }
+ }
+ Abc_ObjAddFanin( pLatch, pNet );
+ Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LI );
+
+ // create the buffer if Q signal is available
+ if ( pTokenQ )
+ {
+ // create the node
+ pNode = Abc_NtkCreateNode( pNtk);
+ // set the function
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1 1\n") );
+ // create fanin and fanout nets
+ pNet = Abc_NtkFindNet( pNtk, vTokens->pArray[1] );
+ Abc_ObjAddFanin( pNode, pNet );
+ pNet = Abc_NtkFindNet( pNtk, pTokenQ );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find latch output net \"%s\".", pTokenQ );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNet, pNode );
+ }
+ if ( pTokenQN )
+ {
+ // create the node
+ pNode = Abc_NtkCreateNode( pNtk );
+ // set the function
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "0 1\n") );
+ // create fanin and fanout nets
+ pNet = Abc_NtkFindNet( pNtk, vTokens->pArray[1] );
+ Abc_ObjAddFanin( pNode, pNet );
+ pNet = Abc_NtkFindNet( pNtk, pTokenQN );
+ if ( pNet == NULL )
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot find latch output net \"%s\".", pTokenQN );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNet, pNode );
+ }
+
+ // set the initial value
+ if ( pTokenRN == NULL && pTokenSN == NULL )
+ Abc_ObjSetData( pLatch, (char *)2 );
+ else
+ {
+ fRN1 = (strcmp( pTokenRN, "1'b1" ) == 0);
+ fSN1 = (strcmp( pTokenSN, "1'b1" ) == 0);
+ if ( fRN1 && fSN1 )
+ Abc_ObjSetData( pLatch, (char *)2 );
+ else if ( fRN1 )
+ Abc_ObjSetData( pLatch, (char *)1 );
+ else if ( fSN1 )
+ Abc_ObjSetData( pLatch, (char *)0 );
+ else
+ {
+ p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
+ sprintf( p->sError, "Cannot read the initial value of latch \"%s\".", vTokens->pArray[1] );
+ Io_ReadVerPrintErrorMessage( p );
+ return 0;
+ }
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the verilog file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadSetNonDrivenNets( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNets;
+ Abc_Obj_t * pNet, * pNode;
+ int i;
+
+ // check for non-driven nets
+ vNets = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachNet( pNtk, pNet, i )
+ {
+ if ( !Abc_ObjIsPi(pNet) && Abc_ObjFaninNum(pNet) == 0 )
+ {
+ // add the constant 0 driver
+ pNode = Abc_NtkCreateNode( pNtk );
+ // set the constant function
+ Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+ // add the fanout net
+ Abc_ObjAddFanin( pNet, pNode );
+ // add the net to those for which the warning will be printed
+ Vec_PtrPush( vNets, pNet->pData );
+ }
+ }
+
+ // print the warning
+ if ( vNets->nSize > 0 )
+ {
+ printf( "The reader added constant-zero driver to %d non-driven nets:\n", vNets->nSize );
+ for ( i = 0; i < vNets->nSize; i++ )
+ {
+ if ( i == 0 )
+ printf( "%s", vNets->pArray[i] );
+ else if ( i == 1 )
+ printf( ", %s", vNets->pArray[i] );
+ else if ( i == 2 )
+ {
+ printf( ", %s, etc.", vNets->pArray[i] );
+ break;
+ }
+ }
+ printf( "\n" );
+ }
+ Vec_PtrFree( vNets );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
new file mode 100644
index 00000000..954c2238
--- /dev/null
+++ b/src/base/io/ioWriteBench.c
@@ -0,0 +1,224 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteBench.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write the network in BENCH format.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteBench.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode );
+static char * Io_BenchNodeName( Abc_Obj_t * pObj, int fPhase );
+static char * Io_BenchNodeNameInv( Abc_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the network in BENCH format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ Abc_Ntk_t * pExdc;
+ FILE * pFile;
+ assert( Abc_NtkIsAig(pNtk) );
+ 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->pSpec, Extra_TimeStamp() );
+ // write the network
+ Io_WriteBenchOne( pFile, pNtk );
+ // write EXDC network if it exists
+ pExdc = Abc_NtkExdc( pNtk );
+ if ( pExdc )
+ {
+ printf( "Io_WriteBench: EXDC is not written (warning).\n" );
+// fprintf( pFile, "\n" );
+// fprintf( pFile, ".exdc\n" );
+// Io_LogicWriteOne( pFile, pExdc );
+ }
+ // finalize the file
+ fclose( pFile );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the network in BENCH format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ ProgressBar * pProgress;
+ Abc_Obj_t * pNode;
+ int i;
+
+ assert( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsAig(pNtk) );
+
+ // write the PIs/POs/latches
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ fprintf( pFile, "INPUT(%s)\n", Abc_NtkNamePi(pNtk,i) );
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ fprintf( pFile, "OUTPUT(%s)\n", Abc_NtkNamePo(pNtk,i) );
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ fprintf( pFile, "%-11s = DFF(%s)\n",
+ Abc_NtkNameLatch(pNtk,i), Abc_NtkNameLatchInput(pNtk,i) );
+
+ // set the node names
+ Abc_NtkCleanCopy( pNtk );
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ pNode->pCopy = (Abc_Obj_t *)Abc_NtkNameCi(pNtk,i);
+
+ // write intervers for COs appearing in negative polarity
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ {
+ if ( Abc_AigNodeIsUsedCompl(pNode) )
+ fprintf( pFile, "%-11s = NOT(%s)\n",
+ Io_BenchNodeNameInv(pNode),
+ Abc_NtkNameCi(pNtk,i) );
+ }
+
+ // write internal nodes
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ if ( Abc_NodeIsConst(pNode) )
+ continue;
+ Io_WriteBenchOneNode( pFile, pNode );
+ }
+ Extra_ProgressBarStop( pProgress );
+
+ // write buffers for CO
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ {
+ fprintf( pFile, "%-11s = BUFF(%s)\n",
+ (i < Abc_NtkPoNum(pNtk))? Abc_NtkNamePo(pNtk,i) :
+ Abc_NtkNameLatchInput( pNtk, i-Abc_NtkPoNum(pNtk) ),
+ Io_BenchNodeName( Abc_ObjFanin0(pNode), !Abc_ObjFaninC0(pNode) ) );
+ }
+ Abc_NtkCleanCopy( pNtk );
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the network in BENCH format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+ assert( Abc_ObjIsNode(pNode) );
+ // write the AND gate
+ fprintf( pFile, "%-11s", Io_BenchNodeName( pNode, 1 ) );
+ fprintf( pFile, " = AND(%s, ", Io_BenchNodeName( Abc_ObjFanin0(pNode), !Abc_ObjFaninC0(pNode) ) );
+ fprintf( pFile, "%s)\n", Io_BenchNodeName( Abc_ObjFanin1(pNode), !Abc_ObjFaninC1(pNode) ) );
+
+ // write the inverter if necessary
+ if ( Abc_AigNodeIsUsedCompl(pNode) )
+ {
+ fprintf( pFile, "%-11s = NOT(", Io_BenchNodeName( pNode, 0 ) );
+ fprintf( pFile, "%s)\n", Io_BenchNodeName( pNode, 1 ) );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the name of an internal AIG node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Io_BenchNodeName( Abc_Obj_t * pObj, int fPhase )
+{
+ static char Buffer[500];
+ if ( pObj->pCopy ) // PIs and latches
+ {
+ sprintf( Buffer, "%s%s", (char *)pObj->pCopy, (fPhase? "":"_c") );
+ return Buffer;
+ }
+ assert( Abc_ObjIsNode(pObj) );
+ if ( Abc_NodeIsConst(pObj) ) // constant node
+ {
+ if ( fPhase )
+ sprintf( Buffer, "%s", "vdd" );
+ else
+ sprintf( Buffer, "%s", "gnd" );
+ return Buffer;
+ }
+ // internal nodes
+ sprintf( Buffer, "%s%s", Abc_ObjName(pObj), (fPhase? "":"_c") );
+ return Buffer;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the name of an internal AIG node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Io_BenchNodeNameInv( Abc_Obj_t * pObj )
+{
+ static char Buffer[500];
+ sprintf( Buffer, "%s%s", Abc_ObjName(pObj), "_c" );
+ return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
new file mode 100644
index 00000000..d9c69273
--- /dev/null
+++ b/src/base/io/ioWriteBlif.c
@@ -0,0 +1,344 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteBlif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write BLIF files.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteBlif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Write the network into a BLIF file with the given name.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName )
+{
+ Abc_Ntk_t * pExdc;
+ FILE * pFile;
+ assert( Abc_NtkIsNetlist(pNtk) );
+ pFile = fopen( FileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteBlif(): Cannot open the output file.\n" );
+ return;
+ }
+ // write the model name
+ fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
+ // write the network
+ Io_NtkWriteOne( pFile, pNtk );
+ // write EXDC network if it exists
+ pExdc = Abc_NtkExdc( pNtk );
+ if ( pExdc )
+ {
+ fprintf( pFile, "\n" );
+ fprintf( pFile, ".exdc\n" );
+ Io_NtkWriteOne( pFile, pExdc );
+ }
+ // finalize the file
+ fprintf( pFile, ".end\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write one network.]
+
+ Description [Writes a network composed of PIs, POs, internal nodes,
+ and latches. The following rules are used to print the names of
+ internal nodes:
+ ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ ProgressBar * pProgress;
+ Abc_Obj_t * pNode, * pLatch;
+ int i;
+
+ // write the PIs
+ fprintf( pFile, ".inputs" );
+ Io_NtkWritePis( pFile, pNtk );
+ fprintf( pFile, "\n" );
+
+ // write the POs
+ fprintf( pFile, ".outputs" );
+ Io_NtkWritePos( pFile, pNtk );
+ fprintf( pFile, "\n" );
+
+ // write the timing info
+ Io_WriteTimingInfo( pFile, pNtk );
+
+ // write the latches
+ if ( !Abc_NtkIsComb(pNtk) )
+ {
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ Io_NtkWriteLatch( pFile, pLatch );
+ fprintf( pFile, "\n" );
+ }
+
+ // write each internal node
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Io_NtkWriteNode( pFile, pNode );
+ }
+ Extra_ProgressBarStop( pProgress );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNet;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int i;
+
+ LineLength = 7;
+ NameCounter = 0;
+ Abc_NtkForEachPi( pNtk, pNet, i )
+ {
+ // get the line length after this name is written
+ AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", Abc_ObjName(pNet) );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNet;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int i;
+
+ LineLength = 8;
+ NameCounter = 0;
+ Abc_NtkForEachPo( pNtk, pNet, i )
+ {
+ // get the line length after this name is written
+ AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", Abc_ObjName(pNet) );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Write the latch into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
+{
+ Abc_Obj_t * pNetLi, * pNetLo;
+ int Reset;
+ pNetLi = Abc_ObjFanin0( pLatch );
+ pNetLo = Abc_ObjFanout0( pLatch );
+ Reset = (int)Abc_ObjData( pLatch );
+ // write the latch line
+ fprintf( pFile, ".latch" );
+ fprintf( pFile, " %10s", Abc_ObjName(pNetLi) );
+ fprintf( pFile, " %10s", Abc_ObjName(pNetLo) );
+ fprintf( pFile, " %d\n", Reset );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Write the node into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+ // write the .names line
+ fprintf( pFile, ".names" );
+ Io_NtkWriteNodeFanins( pFile, pNode );
+ fprintf( pFile, "\n" );
+ // write the cubes
+ fprintf( pFile, "%s", Abc_ObjData(pNode) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pNet;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ char * pName;
+ int i;
+
+ LineLength = 6;
+ NameCounter = 0;
+ Abc_ObjForEachFanin( pNode, pNet, i )
+ {
+ // get the fanin name
+ pName = Abc_ObjName(pNet);
+ // get the line length after the fanin name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+
+ // get the output name
+ pName = Abc_ObjName(Abc_ObjFanout0(pNode));
+ // get the line length after the output name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength > 75 )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the timing info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ Abc_Time_t * pTime, * pTimeDef;
+ int i;
+
+ if ( pNtk->pManTime == NULL )
+ return;
+
+ pTimeDef = Abc_NtkReadDefaultArrival( pNtk );
+ fprintf( pFile, ".default_input_arrival %g %g\n", pTimeDef->Rise, pTimeDef->Fall );
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ {
+ pTime = Abc_NodeReadArrival(pNode);
+ if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
+ continue;
+ fprintf( pFile, ".input_arrival %s %g %g\n", Abc_NtkNamePi(pNtk,i), pTime->Rise, pTime->Fall );
+ }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteBlifLogic.c b/src/base/io/ioWriteBlifLogic.c
new file mode 100644
index 00000000..aa1d65b9
--- /dev/null
+++ b/src/base/io/ioWriteBlifLogic.c
@@ -0,0 +1,402 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteBlifLogic.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write BLIF files for a logic network.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteBlifLogic.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_LogicWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
+static void Io_LogicWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
+static void Io_LogicWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
+static void Io_LogicWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode, int fMark );
+static void Io_LogicWriteNode( FILE * pFile, Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Write the network into a BLIF file with the given name.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
+{
+ Abc_Ntk_t * pExdc;
+ FILE * pFile;
+ assert( !Abc_NtkIsNetlist(pNtk) );
+ pFile = fopen( FileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteBlifLogic(): Cannot open the output file.\n" );
+ return;
+ }
+ // write the model name
+ fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
+ // write the network
+ Io_LogicWriteOne( pFile, pNtk, fWriteLatches );
+ // write EXDC network if it exists
+ pExdc = Abc_NtkExdc( pNtk );
+ if ( pExdc )
+ {
+ fprintf( pFile, "\n" );
+ fprintf( pFile, ".exdc\n" );
+ Io_LogicWriteOne( pFile, pExdc, 0 );
+ }
+ // finalize the file
+ fprintf( pFile, ".end\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write one network.]
+
+ Description [Writes a network composed of PIs, POs, internal nodes,
+ and latches. The following rules are used to print the names of
+ internal nodes: ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_LogicWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
+{
+ ProgressBar * pProgress;
+ Abc_Obj_t * pNode, * pLatch, * pDriver;
+ Vec_Ptr_t * vNodes;
+ int i;
+
+ assert( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsAig(pNtk) );
+
+ // print a warning about choice nodes
+ if ( i = Abc_NtkCountChoiceNodes( pNtk ) )
+ printf( "Warning: The AIG is written into the file, including %d choice nodes.\n", i );
+
+ // write the PIs
+ fprintf( pFile, ".inputs" );
+ Io_LogicWritePis( pFile, pNtk, fWriteLatches );
+ fprintf( pFile, "\n" );
+
+ // write the POs
+ fprintf( pFile, ".outputs" );
+ Io_LogicWritePos( pFile, pNtk, fWriteLatches );
+ fprintf( pFile, "\n" );
+
+ if ( fWriteLatches )
+ {
+ // write the timing info
+ Io_WriteTimingInfo( pFile, pNtk );
+ // write the latches
+ if ( Abc_NtkLatchNum(pNtk) )
+ {
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ fprintf( pFile, ".latch %10s %10s %d\n",
+ Abc_NtkNameLatchInput(pNtk,i), Abc_NtkNameLatch(pNtk,i), (int)pLatch->pData );
+ fprintf( pFile, "\n" );
+ }
+ }
+
+ // set the node names
+ Abc_NtkLogicTransferNames( pNtk );
+
+ // collect internal nodes
+ if ( Abc_NtkIsAig(pNtk) )
+ vNodes = Abc_AigDfs( pNtk );
+ else
+ vNodes = Abc_NtkDfs( pNtk );
+ // write internal nodes
+ pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+ for ( i = 0; i < vNodes->nSize; i++ )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Io_LogicWriteNode( pFile, Vec_PtrEntry(vNodes, i) );
+ }
+ Extra_ProgressBarStop( pProgress );
+ Vec_PtrFree( vNodes );
+
+ // write inverters/buffers for each CO
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ {
+ pDriver = Abc_ObjFanin0(pLatch);
+ // consider the case when the latch is driving itself
+ if ( pDriver == pLatch )
+ {
+ fprintf( pFile, ".names %s %s\n%d 1\n",
+ Abc_NtkNameLatch(pNtk,i), Abc_NtkNameLatchInput(pNtk,i), !Abc_ObjFaninC0(pLatch) );
+ continue;
+ }
+ // skip if they have the same name
+ if ( pDriver->pCopy && strcmp( (char *)pDriver->pCopy, Abc_NtkNameLatchInput(pNtk,i) ) == 0 )
+ {
+ /*
+ Abc_Obj_t * pFanout;
+ int k;
+ printf( "latch name = %s.\n", (char *)pLatch->pCopy );
+ printf( "driver name = %s.\n", (char *)pDriver->pCopy );
+ Abc_ObjForEachFanout( pDriver, pFanout, k )
+ printf( "driver's fanout name = %s. Fanins = %d. Compl0 = %d. \n",
+ Abc_ObjName(pFanout), Abc_ObjFaninNum(pFanout), Abc_ObjFaninC0(pFanout) );
+ */
+ assert( !Abc_ObjFaninC0(pLatch) );
+ continue;
+ }
+ // write inverter/buffer depending on whether the edge is complemented
+ fprintf( pFile, ".names %s %s\n%d 1\n",
+ Abc_ObjName(pDriver), Abc_NtkNameLatchInput(pNtk,i), !Abc_ObjFaninC0(pLatch) );
+ }
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ {
+ pDriver = Abc_ObjFanin0(pNode);
+ // skip if they have the same name
+ if ( pDriver->pCopy && strcmp( (char *)pDriver->pCopy, Abc_NtkNamePo(pNtk,i) ) == 0 )
+ {
+ assert( !Abc_ObjFaninC0(pNode) );
+ continue;
+ }
+ // write inverter/buffer depending on whether the PO is complemented
+ fprintf( pFile, ".names %s %s\n%d 1\n",
+ Abc_ObjName(pDriver), Abc_NtkNamePo(pNtk,i), !Abc_ObjFaninC0(pNode) );
+ }
+ Abc_NtkCleanCopy( pNtk );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_LogicWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
+{
+ char * pName;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int nLimit;
+ int i;
+
+ LineLength = 7;
+ NameCounter = 0;
+ nLimit = fWriteLatches? Abc_NtkPiNum(pNtk) : Abc_NtkCiNum(pNtk);
+ for ( i = 0; i < nLimit; i++ )
+ {
+ pName = pNtk->vNamesPi->pArray[i];
+ // get the line length after this name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_LogicWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
+{
+ char * pName;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int nLimit;
+ int i;
+
+ LineLength = 8;
+ NameCounter = 0;
+ nLimit = fWriteLatches? Abc_NtkPoNum(pNtk) : Abc_NtkCoNum(pNtk);
+ for ( i = 0; i < nLimit; i++ )
+ {
+ pName = pNtk->vNamesPo->pArray[i];
+ // get the line length after this name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Write the node into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_LogicWriteNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pTemp;
+ int i, k, nFanins, fMark;
+
+ assert( !Abc_ObjIsComplement( pNode ) );
+ assert( Abc_ObjIsNode(pNode) );
+
+ // set the mark that is true if the node is a choice node
+ fMark = Abc_NtkIsAig(pNode->pNtk) && Abc_NodeIsChoice(pNode);
+
+ // write the .names line
+ fprintf( pFile, ".names" );
+ Io_LogicWriteNodeFanins( pFile, pNode, fMark );
+ fprintf( pFile, "\n" );
+ // write the cubes
+ if ( Abc_NtkIsLogicSop(pNode->pNtk) )
+ fprintf( pFile, "%s", Abc_ObjData(pNode) );
+ else if ( Abc_NtkIsAig(pNode->pNtk) )
+ {
+ if ( pNode == Abc_AigConst1(pNode->pNtk->pManFunc) )
+ {
+ fprintf( pFile, " 1\n" );
+ return;
+ }
+
+ assert( Abc_ObjFaninNum(pNode) == 2 );
+ // write the AND gate
+ for ( i = 0; i < 2; i++ )
+ fprintf( pFile, "%d", !Abc_ObjFaninC(pNode,i) );
+ fprintf( pFile, " 1\n" );
+ // write the choice node if present
+ if ( fMark )
+ {
+ // count the number of fanins of the choice node and write the names line
+ nFanins = 1;
+ fprintf( pFile, ".names %sc", Abc_ObjName(pNode) );
+ for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData, nFanins++ )
+ fprintf( pFile, " %s", Abc_ObjName(pTemp) );
+ fprintf( pFile, " %s\n", Abc_ObjName(pNode) );
+ // write the cubes for each of the fanins
+ for ( i = 0, pTemp = pNode; pTemp; pTemp = pTemp->pData, i++ )
+ {
+ for ( k = 0; k < nFanins; k++ )
+ if ( k == i )
+ fprintf( pFile, "%d", (int)(pNode->fPhase == pTemp->fPhase) );
+ else
+ fprintf( pFile, "-" );
+ fprintf( pFile, " 1\n" );
+ }
+ }
+ }
+ else
+ {
+ assert( 0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_LogicWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode, int fMark )
+{
+ Abc_Obj_t * pFanin;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ char * pName;
+ int i;
+
+ LineLength = 6;
+ NameCounter = 0;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ // get the fanin name
+ pName = Abc_ObjName(pFanin);
+ // get the line length after the fanin name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+
+ // get the output name
+ pName = Abc_ObjName(pNode);
+ // get the line length after the output name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength > 75 )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s%s", pName, fMark? "c" : "" );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
new file mode 100644
index 00000000..144ff167
--- /dev/null
+++ b/src/base/io/ioWriteCnf.c
@@ -0,0 +1,76 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteCnf.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to CNF of the miter cone.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Write the miter cone into a CNF file for the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ solver * pSat;
+ if ( !Abc_NtkIsLogicBdd(pNtk) )
+ {
+ fprintf( stdout, "Io_WriteCnf(): Currently can process logic networks with BDDs.\n" );
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ {
+ fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter (the network with one PO).\n" );
+ return 0;
+ }
+ if ( Abc_NtkLatchNum(pNtk) != 0 )
+ {
+ fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter for combinational circuits.\n" );
+ return 0;
+ }
+ // create solver with clauses
+ pSat = Abc_NtkMiterSatCreate( pNtk );
+ // write the clauses
+ Asat_SolverWriteDimacs( pSat, pFileName );
+ // free the solver
+ solver_delete( pSat );
+ return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteGate.c b/src/base/io/ioWriteGate.c
new file mode 100644
index 00000000..3a3c45eb
--- /dev/null
+++ b/src/base/io/ioWriteGate.c
@@ -0,0 +1,263 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteGate.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write the mapped network.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteGate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+#include "main.h"
+#include "mio.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteGateOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteGatePis( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteGatePos( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteGateNode( FILE * pFile, Abc_Obj_t * pNode, Mio_Gate_t * pGate );
+static char * Io_ReadNodeName( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes mapped network into a BLIF file compatible with SIS.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteGate( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ Abc_Ntk_t * pExdc;
+ FILE * pFile;
+
+ assert( Abc_NtkIsLogicMap(pNtk) );
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteGate(): Cannot open the output file.\n" );
+ return 0;
+ }
+ // write the model name
+ fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
+ // write the network
+ Io_WriteGateOne( pFile, pNtk );
+ // write EXDC network if it exists
+ pExdc = Abc_NtkExdc( pNtk );
+ if ( pExdc )
+ printf( "Io_WriteGate: EXDC is not written (warning).\n" );
+ // finalize the file
+ fprintf( pFile, ".end\n" );
+ fclose( pFile );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write one network.]
+
+ Description [Writes a network composed of PIs, POs, internal nodes,
+ and latches. The following rules are used to print the names of
+ internal nodes: ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteGateOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ ProgressBar * pProgress;
+ Abc_Obj_t * pNode, * pLatch;
+ int i;
+
+ assert( Abc_NtkIsLogicMap(pNtk) );
+ assert( Abc_NtkLogicHasSimplePos(pNtk) );
+
+ // write the PIs
+ fprintf( pFile, ".inputs" );
+ Io_WriteGatePis( pFile, pNtk );
+ fprintf( pFile, "\n" );
+
+ // write the POs
+ fprintf( pFile, ".outputs" );
+ Io_WriteGatePos( pFile, pNtk );
+ fprintf( pFile, "\n" );
+
+ // write the timing info
+ Io_WriteTimingInfo( pFile, pNtk );
+
+ // write the latches
+ if ( Abc_NtkLatchNum(pNtk) )
+ {
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ fprintf( pFile, ".latch %s %s %d\n",
+ Abc_NtkNameLatchInput(pNtk,i), Abc_NtkNameLatch(pNtk,i), (int)pLatch->pData );
+ fprintf( pFile, "\n" );
+ }
+ // set the node names
+ Abc_NtkLogicTransferNames( pNtk );
+ // write internal nodes
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Io_WriteGateNode( pFile, pNode, pNode->pData );
+ }
+ Extra_ProgressBarStop( pProgress );
+ Abc_NtkCleanCopy( pNtk );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteGatePis( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ char * pName;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int i;
+
+ LineLength = 7;
+ NameCounter = 0;
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ {
+ pName = pNtk->vNamesPi->pArray[i];
+ // get the line length after this name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteGatePos( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ char * pName;
+ int i;
+
+ LineLength = 8;
+ NameCounter = 0;
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ {
+ pName = pNtk->vNamesPo->pArray[i];
+ // get the line length after this name is written
+ AddedLength = strlen(pName) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \\\n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", pName );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write the node into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteGateNode( FILE * pFile, Abc_Obj_t * pNode, Mio_Gate_t * pGate )
+{
+ Mio_Pin_t * pGatePin;
+ int i;
+ // do not write the buffer whose input and output have the same name
+ if ( Abc_ObjFaninNum(pNode) == 1 && Abc_ObjFanin0(pNode)->pCopy && pNode->pCopy )
+ if ( strcmp( (char*)Abc_ObjFanin0(pNode)->pCopy, (char*)pNode->pCopy ) == 0 )
+ return;
+ // write the node
+ fprintf( pFile, ".gate %s ", Mio_GateReadName(pGate) );
+ for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+ fprintf( pFile, "%s=%s ", Mio_PinReadName(pGatePin), Io_ReadNodeName( Abc_ObjFanin(pNode,i) ) );
+ assert ( i == Abc_ObjFaninNum(pNode) );
+ fprintf( pFile, "%s=%s\n", Mio_GateReadOutName(pGate), Io_ReadNodeName(pNode) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the name of the node to write.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Io_ReadNodeName( Abc_Obj_t * pNode )
+{
+ if ( pNode->pCopy )
+ return (char *)pNode->pCopy;
+ return Abc_ObjName(pNode);
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
new file mode 100644
index 00000000..d9f46c2c
--- /dev/null
+++ b/src/base/io/module.make
@@ -0,0 +1,10 @@
+SRC += src/base/io/io.c \
+ src/base/io/ioRead.c \
+ src/base/io/ioReadBench.c \
+ src/base/io/ioReadBlif.c \
+ src/base/io/ioReadVerilog.c \
+ src/base/io/ioWriteBench.c \
+ src/base/io/ioWriteBlif.c \
+ src/base/io/ioWriteBlifLogic.c \
+ src/base/io/ioWriteCnf.c \
+ src/base/io/ioWriteGate.c