summaryrefslogtreecommitdiffstats
path: root/src/base/io
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2010-11-01 01:35:04 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2010-11-01 01:35:04 -0700
commit6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch)
tree0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/base/io
parentf0e77f6797c0504b0da25a56152b707d3357f386 (diff)
downloadabc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz
abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2
abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip
initial commit of public abc
Diffstat (limited to 'src/base/io')
-rw-r--r--src/base/io/io.c279
-rw-r--r--src/base/io/ioAbc.h26
-rw-r--r--src/base/io/ioInt.h8
-rw-r--r--src/base/io/ioReadAiger.c27
-rw-r--r--src/base/io/ioReadBaf.c15
-rw-r--r--src/base/io/ioReadBblif.c15
-rw-r--r--src/base/io/ioReadBench.c61
-rw-r--r--src/base/io/ioReadBlif.c113
-rw-r--r--src/base/io/ioReadBlifAig.c77
-rw-r--r--src/base/io/ioReadBlifMv.c380
-rw-r--r--src/base/io/ioReadDsd.c13
-rw-r--r--src/base/io/ioReadEdif.c103
-rw-r--r--src/base/io/ioReadEqn.c31
-rw-r--r--src/base/io/ioReadPla.c45
-rw-r--r--src/base/io/ioReadVerilog.c10
-rw-r--r--src/base/io/ioUtil.c83
-rw-r--r--src/base/io/ioWriteAiger.c12
-rw-r--r--src/base/io/ioWriteBaf.c15
-rw-r--r--src/base/io/ioWriteBblif.c11
-rw-r--r--src/base/io/ioWriteBench.c11
-rw-r--r--src/base/io/ioWriteBlif.c169
-rw-r--r--src/base/io/ioWriteBlifMv.c59
-rw-r--r--src/base/io/ioWriteBook.c99
-rw-r--r--src/base/io/ioWriteCnf.c7
-rw-r--r--src/base/io/ioWriteDot.c67
-rw-r--r--src/base/io/ioWriteEqn.c9
-rw-r--r--src/base/io/ioWriteGml.c5
-rw-r--r--src/base/io/ioWriteList.c5
-rw-r--r--src/base/io/ioWritePla.c11
-rw-r--r--src/base/io/ioWriteSmv.c265
-rw-r--r--src/base/io/ioWriteVerilog.c19
-rw-r--r--src/base/io/module.make3
32 files changed, 1461 insertions, 592 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c
index ecc6302f..eab865d8 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -21,6 +21,8 @@
#include "ioAbc.h"
#include "mainInt.h"
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -41,6 +43,7 @@ static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVer ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -63,6 +66,10 @@ static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv );
+
+extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
extern int glo_fMapped;
@@ -99,6 +106,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_ver", IoCommandReadVer, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_verlib", IoCommandReadVerLib, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_status", IoCommandReadStatus, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write", IoCommandWrite, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 );
@@ -121,6 +129,8 @@ void Io_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "I/O", "write_verlib", IoCommandWriteVerLib, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_truth", IoCommandWriteTruth, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 );
}
/**Function*************************************************************
@@ -134,7 +144,7 @@ void Io_Init( Abc_Frame_t * pAbc )
SeeAlso []
***********************************************************************/
-void Io_End()
+void Io_End( Abc_Frame_t * pAbc )
{
}
@@ -189,6 +199,8 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameCopyLTLDataBase( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
@@ -246,11 +258,12 @@ int IoCommandReadAiger( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_aiger [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
+ fprintf( pAbc->Err, "\t reads the network in the AIGER format (http://fmv.jku.at/aiger)\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" );
@@ -300,11 +313,12 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_baf [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in Binary Aig Format (BAF)\n" );
+ fprintf( pAbc->Err, "\t reads the network in Binary Aig Format (BAF)\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" );
@@ -354,11 +368,12 @@ int IoCommandReadBblif( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_bblif [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in a binary BLIF format\n" );
+ fprintf( pAbc->Err, "\t reads the network in a 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" );
@@ -382,16 +397,21 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
char * pFileName;
int fReadAsAig;
int fCheck;
+ int fUseNewParser;
int c;
extern Abc_Ntk_t * Io_ReadBlifAsAig( char * pFileName, int fCheck );
fCheck = 1;
fReadAsAig = 0;
+ fUseNewParser = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "ach" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nach" ) ) != EOF )
{
switch ( c )
{
+ case 'n':
+ fUseNewParser ^= 1;
+ break;
case 'a':
fReadAsAig ^= 1;
break;
@@ -411,8 +431,9 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
// read the file using the corresponding file reader
if ( fReadAsAig )
pNtk = Io_ReadBlifAsAig( pFileName, fCheck );
+ else if ( fUseNewParser )
+ pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck );
else
-// pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck );
{
Abc_Ntk_t * pTemp;
pNtk = Io_ReadBlif( pFileName, fCheck );
@@ -426,11 +447,14 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
- fprintf( pAbc->Err, "usage: read_blif [-ach] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in binary BLIF format\n" );
+ fprintf( pAbc->Err, "usage: read_blif [-nach] <file>\n" );
+ fprintf( pAbc->Err, "\t reads the network in binary BLIF format\n" );
+ fprintf( pAbc->Err, "\t (if this command does not work, try \"read\")\n" );
+ fprintf( pAbc->Err, "\t-n : toggle using old BLIF parser without hierarchy support [default = %s]\n", !fUseNewParser? "yes":"no" );
fprintf( pAbc->Err, "\t-a : toggle creating AIG while reading the file [default = %s]\n", fReadAsAig? "yes":"no" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
@@ -481,11 +505,13 @@ int IoCommandReadBlifMv( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_blif_mv [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in BLIF-MV format\n" );
+ fprintf( pAbc->Err, "\t reads the network in BLIF-MV format\n" );
+ fprintf( pAbc->Err, "\t (if this command does not work, try \"read\")\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" );
@@ -535,11 +561,12 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
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 reads 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" );
@@ -590,6 +617,7 @@ int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
@@ -650,11 +678,12 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_edif [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in EDIF (works only for ISCAS benchmarks)\n" );
+ fprintf( pAbc->Err, "\t reads the network in EDIF (works only for ISCAS benchmarks)\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" );
@@ -704,11 +733,12 @@ int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_eqn [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in equation format\n" );
+ fprintf( pAbc->Err, "\t reads the network in equation 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" );
@@ -732,7 +762,6 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
char * pFileName;
int c;
- extern void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -773,6 +802,7 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
Io_ReadBenchInit( pNtk, pFileName );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
@@ -844,11 +874,12 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_pla [-zch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in PLA\n" );
+ fprintf( pAbc->Err, "\t reads the network in PLA\n" );
fprintf( pAbc->Err, "\t-z : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" );
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" );
@@ -915,6 +946,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
@@ -973,11 +1005,12 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_verilog [-mch] <file>\n" );
- fprintf( pAbc->Err, "\t read the network in Verilog (IWLS 2002/2005 subset)\n" );
+ fprintf( pAbc->Err, "\t reads the network in Verilog (IWLS 2002/2005 subset)\n" );
fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
@@ -1044,7 +1077,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
fclose( pFile );
// set the new network
- pDesign = Ver_ParseFile( pFileName, Abc_FrameReadLibVer(), fCheck, 1 );
+ pDesign = Ver_ParseFile( pFileName, (Abc_Lib_t *)Abc_FrameReadLibVer(), fCheck, 1 );
if ( pDesign == NULL )
{
fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
@@ -1061,7 +1094,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// derive the AIG network from this design
- pNtkNew = Abc_LibDeriveAig( pNtk, Abc_FrameReadLibVer() );
+ pNtkNew = Abc_LibDeriveAig( pNtk, (Abc_Lib_t *)Abc_FrameReadLibVer() );
Abc_NtkDelete( pNtk );
if ( pNtkNew == NULL )
{
@@ -1070,11 +1103,12 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_ver [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read a network in structural verilog (using current library)\n" );
+ fprintf( pAbc->Err, "\t reads a network in structural verilog (using current library)\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" );
@@ -1144,14 +1178,15 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "The library contains %d gates.\n", st_count(pLibrary->tModules) );
// free old library
if ( Abc_FrameReadLibVer() )
- Abc_LibFree( Abc_FrameReadLibVer(), NULL );
+ Abc_LibFree( (Abc_Lib_t *)Abc_FrameReadLibVer(), NULL );
// read new library
Abc_FrameSetLibVer( pLibrary );
+ Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_verlib [-ch] <file>\n" );
- fprintf( pAbc->Err, "\t read a gate library in structural verilog\n" );
+ fprintf( pAbc->Err, "\t reads a gate library in structural verilog\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" );
@@ -1170,6 +1205,65 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ char * pFileName;
+ FILE * pFile;
+ int c;
+ extern int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex );
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ pFileName = argv[globalUtilOptind];
+ if ( (pFile = fopen( pFileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ Abc_FrameClearVerifStatus( pAbc );
+ pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex );
+ if ( pAbc->pCex )
+ pAbc->nFrames = pAbc->pCex->iFrame;
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_status [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t reads verification log file\n" );
+ fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
+ fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
@@ -1322,7 +1416,7 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" );
- fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
+ fprintf( pAbc->Err, "\t writes the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
@@ -1372,7 +1466,7 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_baf [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
+ fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .baf)\n" );
return 1;
@@ -1420,7 +1514,7 @@ int IoCommandWriteBblif( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_bblif [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the network into a binary BLIF file\n" );
+ fprintf( pAbc->Err, "\t writes the network into a binary BLIF file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bblif)\n" );
return 1;
@@ -1468,7 +1562,7 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_blif [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
+ fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
return 1;
@@ -1516,7 +1610,7 @@ int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_blif_mv [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the network into a BLIF-MV file\n" );
+ fprintf( pAbc->Err, "\t writes the network into a BLIF-MV file\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .mv)\n" );
return 1;
@@ -1580,7 +1674,7 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_bench [-lh] <file>\n" );
- fprintf( pAbc->Err, "\t write the network in BENCH format\n" );
+ fprintf( pAbc->Err, "\t writes the network in BENCH format\n" );
fprintf( pAbc->Err, "\t-l : toggle using LUTs in the output [default = %s]\n", fUseLuts? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" );
@@ -1623,7 +1717,7 @@ int IoCommandWriteBook( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_book [-h] <file> [-options]\n" );
- fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\t-h : prints the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aux, .nodes, .nets)\n" );
fprintf( pAbc->Err, "\t\n" );
fprintf( pAbc->Err, "\tThis command is developed by Myungchul Kim (University of Michigan).\n" );
@@ -1680,7 +1774,7 @@ int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_cellnet [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the network is the cellnet format\n" );
+ fprintf( pAbc->Err, "\t writes the network is the cellnet format\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;
@@ -1750,7 +1844,7 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" );
- fprintf( pAbc->Err, "\t write the miter cone into a CNF file\n" );
+ fprintf( pAbc->Err, "\t writes the miter cone into a CNF file\n" );
fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
@@ -1800,14 +1894,19 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_dot [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the current network into a DOT file\n" );
+ fprintf( pAbc->Err, "\t writes the current network into a DOT 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;
}
+ABC_NAMESPACE_IMPL_END
+
#include "fra.h"
+ABC_NAMESPACE_IMPL_START
+
+
/**Function*************************************************************
Synopsis []
@@ -1862,16 +1961,16 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
// get the input file name
pFileName = argv[globalUtilOptind];
- if ( pNtk->pModel == NULL && pNtk->pSeqModel == NULL )
+ if ( pNtk->pModel == NULL && pAbc->pCex == NULL )
{
fprintf( pAbc->Out, "Counter-example is not available.\n" );
return 0;
}
// write the counter-example into the file
- if ( pNtk->pSeqModel )
+ if ( pAbc->pCex )
{
- Fra_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_Cex_t * pCex = pAbc->pCex;
Abc_Obj_t * pObj;
FILE * pFile;
int i, f;
@@ -1919,7 +2018,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( fNames )
{
- char *cycle_ctr = forceSeq?"@0":"";
+ const char *cycle_ctr = forceSeq?"@0":"";
Abc_NtkForEachPi( pNtk, pObj, i )
// fprintf( pFile, "%s=%c\n", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
fprintf( pFile, "%s%s=%c\n", Abc_ObjName(pObj), cycle_ctr, '0'+(pNtk->pModel[i]==1) );
@@ -1989,7 +2088,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_eqn [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the current network in the equation format\n" );
+ fprintf( pAbc->Err, "\t writes the current network in the equation format\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;
@@ -2037,7 +2136,7 @@ int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_gml [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write network using graph representation formal GML\n" );
+ fprintf( pAbc->Err, "\t writes network using graph representation formal GML\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;
@@ -2100,7 +2199,7 @@ int IoCommandWriteList( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_list [-nh] <file>\n" );
- fprintf( pAbc->Err, "\t write network using graph representation formal GML\n" );
+ fprintf( pAbc->Err, "\t writes network using graph representation formal GML\n" );
fprintf( pAbc->Err, "\t-n : toggle writing host node [default = %s]\n", fUseHost? "yes":"no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
@@ -2149,7 +2248,7 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_pla [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the collapsed network into a PLA file\n" );
+ fprintf( pAbc->Err, "\t writes the collapsed network into a PLA 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;
@@ -2197,7 +2296,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the current network in Verilog format\n" );
+ fprintf( pAbc->Err, "\t writes the current network in Verilog format\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;
@@ -2237,7 +2336,7 @@ int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
// get the input file name
pFileName = argv[globalUtilOptind];
// derive the netlist
- pLibrary = Abc_FrameReadLibVer();
+ pLibrary = (Abc_Lib_t *)Abc_FrameReadLibVer();
if ( pLibrary == NULL )
{
fprintf( pAbc->Out, "Verilog library is not specified.\n" );
@@ -2248,7 +2347,7 @@ int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_verlib [-h] <file>\n" );
- fprintf( pAbc->Err, "\t write the current verilog library\n" );
+ fprintf( pAbc->Err, "\t writes the current verilog library\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;
@@ -2316,7 +2415,7 @@ int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: write_sorter_cnf [-N <num>] [-Q <num>] <file>\n" );
- fprintf( pAbc->Err, "\t write CNF for the sorter\n" );
+ fprintf( pAbc->Err, "\t writes CNF for the sorter\n" );
fprintf( pAbc->Err, "\t-N num : the number of sorter bits [default = %d]\n", nVars );
fprintf( pAbc->Err, "\t-Q num : the number of bits to be asserted to 1 [default = %d]\n", nQueens );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
@@ -2398,7 +2497,7 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
// convert to logic
Abc_NtkToAig( pNtk );
vTruth = Vec_IntAlloc( 0 );
- pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse );
+ pTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse );
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
@@ -2420,8 +2519,102 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * pFileName;
+ int c;
+ extern void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char * pCommand );
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 1 )
+ goto usage;
+ // get the input file name
+ pFileName = argv[globalUtilOptind];
+ Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, NULL );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_status [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t writes verification log 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;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteSmv( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * pFileName;
+ int fUseLuts;
+ int c;
+
+ fUseLuts = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( 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 != globalUtilOptind + 1 )
+ goto usage;
+ // get the output file name
+ pFileName = argv[globalUtilOptind];
+ // call the corresponding file writer
+ Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_SMV );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_smv [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the network in SMV format\n" );
+ fprintf( pAbc->Err, "\t-h : print the help message\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .smv)\n" );
+ return 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index bade17df..b1835dbf 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -21,6 +21,7 @@
#ifndef __IO_H__
#define __IO_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -31,9 +32,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -56,6 +58,7 @@ typedef enum {
IO_FILE_GML,
IO_FILE_LIST,
IO_FILE_PLA,
+ IO_FILE_SMV,
IO_FILE_VERILOG,
IO_FILE_UNKNOWN
} Io_FileType_t;
@@ -82,6 +85,7 @@ extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
extern Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck );
/*=== abcReadBench.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck );
+extern void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcReadEdif.c ===========================================================*/
extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck );
/*=== abcReadEqn.c ============================================================*/
@@ -98,12 +102,12 @@ extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
extern void Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/
extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
-extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
+extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches, int fBb2Wb, int fSeq );
extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
/*=== abcWriteBlifMv.c ==========================================================*/
extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteBench.c =========================================================*/
-extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
+extern int Io_WriteBench( Abc_Ntk_t * pNtk, const char * FileName );
extern int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteBook.c =========================================================*/
extern void Io_WriteBook( Abc_Ntk_t * pNtk, char * FileName );
@@ -121,6 +125,8 @@ extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
extern void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost );
/*=== abcWritePla.c ===========================================================*/
extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteSmv.c ===========================================================*/
+extern int Io_WriteSmv( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteVerilog.c =======================================================*/
extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcUtil.c ===============================================================*/
@@ -136,15 +142,17 @@ extern Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, c
extern Abc_Obj_t * Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv );
extern Abc_Obj_t * Io_ReadCreateResetMux( Abc_Ntk_t * pNtk, char * pResetLO, char * pDataLI, int fBlifMv );
extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs );
-extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
+extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, int fConst1 );
extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/base/io/ioInt.h b/src/base/io/ioInt.h
index 3daf3c75..9ded63e4 100644
--- a/src/base/io/ioInt.h
+++ b/src/base/io/ioInt.h
@@ -21,6 +21,10 @@
#ifndef __IO_INT_H__
#define __IO_INT_H__
+
+ABC_NAMESPACE_HEADER_START
+
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -41,6 +45,10 @@
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_END
+
#endif
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 85475204..61d2967b 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -21,10 +21,13 @@
// The code in this file is developed in collaboration with Mark Jarvin of Toronto.
-#include "ioAbc.h"
#include "bzlib.h"
+#include "ioAbc.h"
#include "zlib.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -190,7 +193,7 @@ static char * Ioa_ReadLoadFileBz2Aig( char * pFileName, int * pFileSize )
static char * Ioa_ReadLoadFileGzAig( char * pFileName, int * pFileSize )
{
const int READ_BLOCK_SIZE = 100000;
- FILE * pFile;
+ gzFile pFile;
char * pContents;
int amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
@@ -340,10 +343,10 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
uLit1 = uLit - Io_ReadAigerDecode( &pCur );
uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
// assert( uLit1 > uLit0 );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
- pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
+ pNode1 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
- Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
+ Vec_PtrPush( vNodes, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pNode0, pNode1) );
}
Extra_ProgressBarStop( pProgress );
@@ -357,14 +360,14 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
}
// read the PO driver literals
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
}
}
@@ -374,14 +377,14 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
{
uLit0 = Vec_IntEntry( vLits, i );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Abc_ObjAddFanin( pObj, pNode0 );
}
// read the PO driver literals
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Abc_ObjAddFanin( pObj, pNode0 );
}
Vec_IntFree( vLits );
@@ -415,7 +418,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
fprintf( stdout, "The number of terminal is out of bound.\n" );
return NULL;
}
- pObj = Vec_PtrEntry( vTerms, iTerm );
+ pObj = (Abc_Obj_t *)Vec_PtrEntry( vTerms, iTerm );
if ( *pType == 'l' )
pObj = Abc_ObjFanout0(pObj);
// assign the name
@@ -481,7 +484,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Vec_PtrFree( vNodes );
// remove the extra nodes
- Abc_AigCleanup( pNtkNew->pManFunc );
+ Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
// check the result
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
@@ -500,3 +503,5 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 495f122b..95c63539 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -128,9 +131,9 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
for ( i = 0; i < nAnds; i++ )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, pBufferNode[2*i+0] >> 1), pBufferNode[2*i+0] & 1 );
- pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, pBufferNode[2*i+1] >> 1), pBufferNode[2*i+1] & 1 );
- Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, pBufferNode[2*i+0] >> 1), pBufferNode[2*i+0] & 1 );
+ pNode1 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, pBufferNode[2*i+1] >> 1), pBufferNode[2*i+1] & 1 );
+ Vec_PtrPush( vNodes, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pNode0, pNode1) );
}
Extra_ProgressBarStop( pProgress );
@@ -143,14 +146,14 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
Abc_ObjSetData( Abc_ObjFanout0(pObj), (void *)(ABC_PTRINT_T)(Num & 3) );
Num >>= 2;
}
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, Num >> 1), Num & 1 );
+ pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, Num >> 1), Num & 1 );
Abc_ObjAddFanin( pObj, pNode0 );
}
ABC_FREE( pContents );
Vec_PtrFree( vNodes );
// remove the extra nodes
-// Abc_AigCleanup( pNtkNew->pManFunc );
+// Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
// check the result
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
@@ -169,3 +172,5 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadBblif.c b/src/base/io/ioReadBblif.c
index 84ef1e29..e2fcca43 100644
--- a/src/base/io/ioReadBblif.c
+++ b/src/base/io/ioReadBblif.c
@@ -22,6 +22,9 @@
#include "dec.h"
#include "bblif.h"
+ABC_NAMESPACE_IMPL_START
+
+
// For description of Binary BLIF format, refer to "abc/src/aig/bbl/bblif.h"
////////////////////////////////////////////////////////////////////////
@@ -70,13 +73,13 @@ Abc_Ntk_t * Bbl_ManToAbc( Bbl_Man_t * p )
pObjNew = Abc_NtkCreateNode( pNtk );
else assert( 0 );
if ( Bbl_ObjIsLut(pObj) )
- pObjNew->pData = Abc_SopRegister( pNtk->pManFunc, Bbl_ObjSop(p, pObj) );
+ pObjNew->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, Bbl_ObjSop(p, pObj) );
Vec_PtrSetEntry( vCopy, Bbl_ObjId(pObj), pObjNew );
}
// connect objects
Bbl_ManForEachObj( p, pObj )
Bbl_ObjForEachFanin( pObj, pFanin )
- Abc_ObjAddFanin( Vec_PtrEntry(vCopy, Bbl_ObjId(pObj)), Vec_PtrEntry(vCopy, Bbl_ObjId(pFanin)) );
+ Abc_ObjAddFanin( (Abc_Obj_t *)Vec_PtrEntry(vCopy, Bbl_ObjId(pObj)), (Abc_Obj_t *)Vec_PtrEntry(vCopy, Bbl_ObjId(pFanin)) );
// finalize
Vec_PtrFree( vCopy );
Abc_NtkAddDummyPiNames( pNtk );
@@ -185,7 +188,7 @@ clk = clock();
// create internal nodes
vNodes = Bbl_ManDfs( p );
vFaninAigs = Vec_PtrAlloc( 100 );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Bbl_Obj_t *, vNodes, pObj, i )
{
// collect fanin AIGs
Vec_PtrClear( vFaninAigs );
@@ -204,10 +207,10 @@ ABC_PRT( "AIG", clock() - clk );
{
if ( !Bbl_ObjIsOutput(pObj) )
continue;
- pObjNew = Vec_PtrEntry( vCopy, Bbl_ObjId(Bbl_ObjFaninFirst(pObj)) );
+ pObjNew = (Abc_Obj_t *)Vec_PtrEntry( vCopy, Bbl_ObjId(Bbl_ObjFaninFirst(pObj)) );
Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pObjNew );
}
- Abc_AigCleanup( pNtk->pManFunc );
+ Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
// clear factored forms
for ( i = Bbl_ManFncSize(p) - 1; i >= 0; i-- )
if ( pFForms[i] )
@@ -340,3 +343,5 @@ Abc_Ntk_t * Io_ReadBblif( char * pFileName, int fCheck )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index e7a2d2fe..681a4e36 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -95,7 +98,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * 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++ )
+ for ( iLine = 0; (vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p)); iLine++ )
{
Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
@@ -108,17 +111,17 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
}
// get the type of the line
- if ( strncmp( vTokens->pArray[0], "INPUT", 5 ) == 0 )
- Io_ReadCreatePi( pNtk, vTokens->pArray[1] );
- else if ( strncmp( vTokens->pArray[0], "OUTPUT", 5 ) == 0 )
- Io_ReadCreatePo( pNtk, vTokens->pArray[1] );
+ if ( strncmp( (char *)vTokens->pArray[0], "INPUT", 5 ) == 0 )
+ Io_ReadCreatePi( pNtk, (char *)vTokens->pArray[1] );
+ else if ( strncmp( (char *)vTokens->pArray[0], "OUTPUT", 5 ) == 0 )
+ Io_ReadCreatePo( pNtk, (char *)vTokens->pArray[1] );
else
{
// get the node name and the node type
- pType = vTokens->pArray[1];
+ pType = (char *)vTokens->pArray[1];
if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE
{
- pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
+ pNode = Io_ReadCreateLatch( pNtk, (char *)vTokens->pArray[2], (char *)vTokens->pArray[0] );
// Abc_LatchSetInit0( pNode );
if ( pType[3] == '0' )
Abc_LatchSetInit0( pNode );
@@ -141,7 +144,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
return NULL;
}
// get the hex string
- pString = vTokens->pArray[2];
+ pString = (char *)vTokens->pArray[2];
if ( strncmp( pString, "0x", 2 ) )
{
printf( "%s: The LUT signature (%s) does not look like a hexadecimal beginning with \"0x\".\n", Extra_FileReaderGetFileName(p), pString );
@@ -172,25 +175,25 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
// check if the node is a constant node
if ( Extra_TruthIsConst0(uTruth, nNames) )
{
- pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 );
- Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
+ pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, 0 );
+ Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" ) );
}
else if ( Extra_TruthIsConst1(uTruth, nNames) )
{
- pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, 0 );
- Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
+ pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, 0 );
+ Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 1\n" ) );
}
else
{
// create the node
- pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
+ pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, nNames );
assert( nNames > 0 );
if ( nNames > 1 )
- Abc_ObjSetData( pNode, Abc_SopCreateFromTruth(pNtk->pManFunc, nNames, uTruth) );
+ Abc_ObjSetData( pNode, Abc_SopCreateFromTruth((Extra_MmFlex_t *)pNtk->pManFunc, nNames, uTruth) );
else if ( pString[0] == '2' )
- Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
+ Abc_ObjSetData( pNode, Abc_SopCreateBuf((Extra_MmFlex_t *)pNtk->pManFunc) );
else if ( pString[0] == '1' )
- Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
+ Abc_ObjSetData( pNode, Abc_SopCreateInv((Extra_MmFlex_t *)pNtk->pManFunc) );
else
{
printf( "%s: Reading truth table (%s) of single-input node has failed.\n", Extra_FileReaderGetFileName(p), pString );
@@ -205,31 +208,31 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
// create a new node and add it to the network
ppNames = (char **)vTokens->pArray + 2;
nNames = vTokens->nSize - 2;
- pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
+ pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, nNames );
// assign the cover
if ( strcmp(pType, "AND") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames, NULL) );
+ Abc_ObjSetData( pNode, Abc_SopCreateAnd((Extra_MmFlex_t *)pNtk->pManFunc, nNames, NULL) );
else if ( strcmp(pType, "OR") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateOr(pNtk->pManFunc, nNames, NULL) );
+ Abc_ObjSetData( pNode, Abc_SopCreateOr((Extra_MmFlex_t *)pNtk->pManFunc, nNames, NULL) );
else if ( strcmp(pType, "NAND") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateNand(pNtk->pManFunc, nNames) );
+ Abc_ObjSetData( pNode, Abc_SopCreateNand((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "NOR") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateNor(pNtk->pManFunc, nNames) );
+ Abc_ObjSetData( pNode, Abc_SopCreateNor((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "XOR") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateXor(pNtk->pManFunc, nNames) );
+ Abc_ObjSetData( pNode, Abc_SopCreateXor((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
else if ( strcmp(pType, "NXOR") == 0 || strcmp(pType, "XNOR") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateNxor(pNtk->pManFunc, nNames) );
+ Abc_ObjSetData( pNode, Abc_SopCreateNxor((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
else if ( strncmp(pType, "BUF", 3) == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
+ Abc_ObjSetData( pNode, Abc_SopCreateBuf((Extra_MmFlex_t *)pNtk->pManFunc) );
else if ( strcmp(pType, "NOT") == 0 )
- Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
+ Abc_ObjSetData( pNode, Abc_SopCreateInv((Extra_MmFlex_t *)pNtk->pManFunc) );
else if ( strncmp(pType, "MUX", 3) == 0 )
// Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
- Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "0-1 1\n11- 1\n") );
+ Abc_ObjSetData( pNode, Abc_SopRegister((Extra_MmFlex_t *)pNtk->pManFunc, "0-1 1\n11- 1\n") );
else if ( strncmp(pType, "gnd", 3) == 0 )
- Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
+ Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" ) );
else if ( strncmp(pType, "vdd", 3) == 0 )
- Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 1\n" ) );
+ Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 1\n" ) );
else
{
printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
@@ -359,3 +362,5 @@ void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName )
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index f2c3e8c2..06920afe 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -22,6 +22,9 @@
#include "main.h"
#include "mio.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -128,7 +131,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
// read the name of the master network
p->vTokens = Io_ReadBlifGetTokens(p);
- if ( p->vTokens == NULL || strcmp( p->vTokens->pArray[0], ".model" ) )
+ if ( p->vTokens == NULL || strcmp( (char *)p->vTokens->pArray[0], ".model" ) )
{
p->LineCur = 0;
sprintf( p->sError, "Wrong input file format." );
@@ -144,7 +147,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
pNtk = Io_ReadBlifNetworkOne( p );
if ( pNtk == NULL )
break;
- if ( p->vTokens && strcmp(p->vTokens->pArray[0], ".exdc") == 0 )
+ if ( p->vTokens && strcmp((char *)p->vTokens->pArray[0], ".exdc") == 0 )
{
pNtk->pExdc = Io_ReadBlifNetworkOne( p );
Abc_NtkFinalizeRead( pNtk->pExdc );
@@ -171,7 +174,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
}
// add the network to the hierarchy
if ( pNtkMaster->tName2Model == NULL )
- pNtkMaster->tName2Model = stmm_init_table(strcmp, stmm_strhash);
+ pNtkMaster->tName2Model = stmm_init_table((int (*)(void))strcmp, (int (*)(void))stmm_strhash);
stmm_insert( pNtkMaster->tName2Model, pNtk->pName, (char *)pNtk );
*/
}
@@ -217,7 +220,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
// create the new network
p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
// read the model name
- if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
+ if ( strcmp( (char *)p->vTokens->pArray[0], ".model" ) == 0 )
{
char * pToken, * pPivot;
if ( Vec_PtrSize(p->vTokens) != 2 )
@@ -227,12 +230,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
Io_ReadBlifPrintErrorMessage( p );
return NULL;
}
- for ( pPivot = pToken = Vec_PtrEntry(p->vTokens, 1); *pToken; pToken++ )
+ for ( pPivot = pToken = (char *)Vec_PtrEntry(p->vTokens, 1); *pToken; pToken++ )
if ( *pToken == '/' || *pToken == '\\' )
pPivot = pToken+1;
pNtk->pName = Extra_UtilStrsav( pPivot );
}
- else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 )
+ else if ( strcmp( (char *)p->vTokens->pArray[0], ".exdc" ) != 0 )
{
printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName,
Extra_FileReaderGetLineNumber(p->pReader, 0), (char*)p->vTokens->pArray[0] );
@@ -252,7 +255,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
// consider different line types
fTokensReady = 0;
- pDirective = p->vTokens->pArray[0];
+ pDirective = (char *)p->vTokens->pArray[0];
if ( !strcmp( pDirective, ".names" ) )
{ fStatus = Io_ReadBlifNetworkNames( p, &p->vTokens ); fTokensReady = 1; }
else if ( !strcmp( pDirective, ".gate" ) )
@@ -282,7 +285,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
{
pNtk->ntkType = ABC_NTK_NETLIST;
pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
- Extra_MmFlexStop( pNtk->pManFunc );
+ Extra_MmFlexStop( (Extra_MmFlex_t *)pNtk->pManFunc );
pNtk->pManFunc = NULL;
}
else
@@ -317,7 +320,7 @@ int Io_ReadBlifNetworkInputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
{
int i;
for ( i = 1; i < vTokens->nSize; i++ )
- Io_ReadCreatePi( p->pNtkCur, vTokens->pArray[i] );
+ Io_ReadCreatePi( p->pNtkCur, (char *)vTokens->pArray[i] );
return 0;
}
@@ -336,7 +339,7 @@ int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
{
int i;
for ( i = 1; i < vTokens->nSize; i++ )
- Io_ReadCreatePo( p->pNtkCur, vTokens->pArray[i] );
+ Io_ReadCreatePo( p->pNtkCur, (char *)vTokens->pArray[i] );
return 0;
}
@@ -355,7 +358,7 @@ int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
{
int i;
for ( i = 1; i < vTokens->nSize; i++ )
- Io_ReadCreateAssert( p->pNtkCur, vTokens->pArray[i] );
+ Io_ReadCreateAssert( p->pNtkCur, (char *)vTokens->pArray[i] );
return 0;
}
@@ -383,13 +386,13 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
return 1;
}
// create the latch
- pLatch = Io_ReadCreateLatch( pNtk, vTokens->pArray[1], vTokens->pArray[2] );
+ pLatch = Io_ReadCreateLatch( pNtk, (char *)vTokens->pArray[1], (char *)vTokens->pArray[2] );
// get the latch reset value
if ( vTokens->nSize == 3 )
Abc_LatchSetInitDc( pLatch );
else
{
- ResetValue = atoi(vTokens->pArray[vTokens->nSize-1]);
+ ResetValue = atoi((char *)vTokens->pArray[vTokens->nSize-1]);
if ( ResetValue != 0 && ResetValue != 1 && ResetValue != 2 )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -447,7 +450,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
{
while ( (vTokens = Io_ReadBlifGetTokens(p)) )
{
- pToken = vTokens->pArray[0];
+ pToken = (char *)vTokens->pArray[0];
if ( pToken[0] == '.' )
break;
// read the cube
@@ -469,7 +472,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
{
while ( (vTokens = Io_ReadBlifGetTokens(p)) )
{
- pToken = vTokens->pArray[0];
+ pToken = (char *)vTokens->pArray[0];
if ( pToken[0] == '.' )
break;
// read the cube
@@ -481,7 +484,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
return 1;
}
// create the cube
- Vec_StrAppend( p->vCubes, vTokens->pArray[0] );
+ Vec_StrPrintStr( p->vCubes, (char *)vTokens->pArray[0] );
// check the char
Char = ((char *)vTokens->pArray[1])[0];
if ( Char != '0' && Char != '1' && Char != 'x' && Char != 'n' )
@@ -507,14 +510,14 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
Vec_StrPush( p->vCubes, 0 );
// set the pointer to the functionality of the node
- Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, p->vCubes->pArray) );
+ Abc_ObjSetData( pNode, Abc_SopRegister((Extra_MmFlex_t *)pNtk->pManFunc, p->vCubes->pArray) );
// check the size
- if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum(Abc_ObjData(pNode)) )
+ if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum((char *)Abc_ObjData(pNode)) )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
sprintf( p->sError, "The number of fanins (%d) of node %s is different from SOP size (%d).",
- Abc_ObjFaninNum(pNode), Abc_ObjName(Abc_ObjFanout(pNode,0)), Abc_SopGetVarNum(Abc_ObjData(pNode)) );
+ Abc_ObjFaninNum(pNode), Abc_ObjName(Abc_ObjFanout(pNode,0)), Abc_SopGetVarNum((char *)Abc_ObjData(pNode)) );
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
@@ -548,7 +551,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate )
{
pNamePin = Mio_PinReadName(pGatePin);
Length = strlen(pNamePin);
- pName = Vec_PtrEntry(vTokens, i+2);
+ pName = (char *)Vec_PtrEntry(vTokens, i+2);
if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
continue;
break;
@@ -562,7 +565,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate )
Length = strlen(pNamePin);
for ( k = 2; k < nSize; k++ )
{
- pName = Vec_PtrEntry(vTokens, k);
+ pName = (char *)Vec_PtrEntry(vTokens, k);
if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
{
Vec_PtrPush( vTokens, pName );
@@ -574,7 +577,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate )
Length = strlen(pNamePin);
for ( k = 2; k < nSize; k++ )
{
- pName = Vec_PtrEntry(vTokens, k);
+ pName = (char *)Vec_PtrEntry(vTokens, k);
if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
{
Vec_PtrPush( vTokens, pName );
@@ -583,7 +586,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate )
}
if ( Vec_PtrSize(vTokens) - nSize != nSize - 2 )
return 0;
- Vec_PtrForEachEntryStart( vTokens, pName, k, nSize )
+ Vec_PtrForEachEntryStart( char *, vTokens, pName, k, nSize )
Vec_PtrWriteEntry( vTokens, k - nSize + 2, pName );
Vec_PtrShrink( vTokens, nSize );
return 1;
@@ -609,7 +612,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
int i, nNames;
// check that the library is available
- pGenlib = Abc_FrameReadLibGen();
+ pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
if ( pGenlib == NULL )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -628,7 +631,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
}
// get the gate
- pGate = Mio_LibraryReadGateByName( pGenlib, vTokens->pArray[1] );
+ pGate = Mio_LibraryReadGateByName( pGenlib, (char *)vTokens->pArray[1] );
if ( pGate == NULL )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -642,7 +645,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
{
assert( p->pNtkCur->ntkFunc == ABC_FUNC_SOP );
p->pNtkCur->ntkFunc = ABC_FUNC_MAP;
- Extra_MmFlexStop( p->pNtkCur->pManFunc );
+ Extra_MmFlexStop( (Extra_MmFlex_t *)p->pNtkCur->pManFunc );
p->pNtkCur->pManFunc = pGenlib;
}
@@ -659,7 +662,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
// remove the formal parameter names
for ( i = 2; i < vTokens->nSize; i++ )
{
- vTokens->pArray[i] = Io_ReadBlifCleanName( vTokens->pArray[i] );
+ vTokens->pArray[i] = Io_ReadBlifCleanName( (char *)vTokens->pArray[i] );
if ( vTokens->pArray[i] == NULL )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -708,7 +711,7 @@ int Io_ReadBlifNetworkSubcircuit( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
// store the names of formal/actual inputs/outputs of the box
vNames = Vec_PtrAlloc( 10 );
- Vec_PtrForEachEntryStart( vTokens, pName, i, 1 )
+ Vec_PtrForEachEntryStart( char *, vTokens, pName, i, 1 )
// Vec_PtrPush( vNames, Abc_NtkRegisterName(p->pNtkCur, pName) );
Vec_PtrPush( vNames, Extra_UtilStrsav(pName) ); // memory leak!!!
@@ -717,7 +720,7 @@ int Io_ReadBlifNetworkSubcircuit( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
// set the pointer to the node names
Abc_ObjSetData( pBox, vNames );
// remember the line of the file
- pBox->pCopy = (void *)(ABC_PTRINT_T)Extra_FileReaderGetLineNumber(p->pReader, 0);
+ pBox->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Extra_FileReaderGetLineNumber(p->pReader, 0);
return 0;
}
@@ -758,9 +761,9 @@ 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 );
+ assert( strncmp( (char *)vTokens->pArray[0], ".input_arrival", 14 ) == 0 );
if ( vTokens->nSize != 4 )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -768,7 +771,7 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
- pNet = Abc_NtkFindNet( p->pNtkCur, vTokens->pArray[1] );
+ pNet = Abc_NtkFindNet( p->pNtkCur, (char *)vTokens->pArray[1] );
if ( pNet == NULL )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -776,8 +779,8 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
- TimeRise = strtod( vTokens->pArray[2], &pFoo1 );
- TimeFall = strtod( vTokens->pArray[3], &pFoo2 );
+ TimeRise = strtod( (char *)vTokens->pArray[2], &pFoo1 );
+ TimeFall = strtod( (char *)vTokens->pArray[3], &pFoo2 );
if ( *pFoo1 != '\0' || *pFoo2 != '\0' )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -807,7 +810,7 @@ int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vToken
double TimeRise, TimeFall;
// make sure this is indeed the .inputs line
- assert( strncmp( vTokens->pArray[0], ".default_input_arrival", 23 ) == 0 );
+ assert( strncmp( (char *)vTokens->pArray[0], ".default_input_arrival", 23 ) == 0 );
if ( vTokens->nSize != 3 )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -815,8 +818,8 @@ int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vToken
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
- TimeRise = strtod( vTokens->pArray[1], &pFoo1 );
- TimeFall = strtod( vTokens->pArray[2], &pFoo2 );
+ TimeRise = strtod( (char *)vTokens->pArray[1], &pFoo1 );
+ TimeFall = strtod( (char *)vTokens->pArray[2], &pFoo2 );
if ( *pFoo1 != '\0' || *pFoo2 != '\0' )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -875,12 +878,12 @@ Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p )
}
// get the new tokens
- vTokens = Extra_FileReaderGetTokens(p->pReader);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p->pReader);
if ( vTokens == NULL )
return vTokens;
// check if there is a transfer to another line
- pLastToken = vTokens->pArray[vTokens->nSize - 1];
+ pLastToken = (char *)vTokens->pArray[vTokens->nSize - 1];
if ( pLastToken[ strlen(pLastToken)-1 ] != '\\' )
return vTokens;
@@ -890,17 +893,17 @@ Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p )
vTokens->nSize--;
// load them into the new array
for ( i = 0; i < vTokens->nSize; i++ )
- Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav(vTokens->pArray[i]) );
+ Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav((char *)vTokens->pArray[i]) );
// load as long as there is the line break
while ( 1 )
{
// get the new tokens
- vTokens = Extra_FileReaderGetTokens(p->pReader);
+ vTokens = (Vec_Ptr_t *)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];
+ pLastToken = (char *)vTokens->pArray[vTokens->nSize - 1];
if ( pLastToken[ strlen(pLastToken)-1 ] == '\\' )
{
// remove the slash
@@ -909,12 +912,12 @@ Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p )
vTokens->nSize--;
// load them into the new array
for ( i = 0; i < vTokens->nSize; i++ )
- Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav(vTokens->pArray[i]) );
+ Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav((char *)vTokens->pArray[i]) );
continue;
}
// otherwise, load them and break
for ( i = 0; i < vTokens->nSize; i++ )
- Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav(vTokens->pArray[i]) );
+ Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav((char *)vTokens->pArray[i]) );
break;
}
return p->vNewTokens;
@@ -993,8 +996,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
int i, Length, Start = -1;
// get the model for this box
- pNames = pBox->pData;
- if ( !stmm_lookup( tName2Model, Vec_PtrEntry(pNames, 0), (char **)&pNtkModel ) )
+ pNames = (Vec_Ptr_t *)pBox->pData;
+ if ( !stmm_lookup( tName2Model, (char *)Vec_PtrEntry(pNames, 0), (char **)&pNtkModel ) )
{
p->LineCur = (int)(ABC_PTRINT_T)pBox->pCopy;
sprintf( p->sError, "Cannot find the model for subcircuit %s.", (char*)Vec_PtrEntry(pNames, 0) );
@@ -1009,7 +1012,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
Start = 1;
else
{
- Vec_PtrForEachEntryStart( pNames, pName, i, 1 )
+ Vec_PtrForEachEntryStart( char *, pNames, pName, i, 1 )
{
pActual = Io_ReadBlifCleanName(pName);
if ( pActual == NULL )
@@ -1047,7 +1050,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
- pObj->pCopy = (void *)pActual;
+ pObj->pCopy = (Abc_Obj_t *)pActual;
// quit if we processed all PIs
if ( i == Abc_NtkPiNum(pNtkModel) )
{
@@ -1059,7 +1062,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
// create the fanins of the box
Abc_NtkForEachPi( pNtkModel, pObj, i )
{
- pActual = (void *)pObj->pCopy;
+ pActual = (char *)pObj->pCopy;
if ( pActual == NULL )
{
p->LineCur = (int)(ABC_PTRINT_T)pBox->pCopy;
@@ -1076,7 +1079,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
// create the fanouts of the box
Abc_NtkForEachPo( pNtkModel, pObj, i )
pObj->pCopy = NULL;
- Vec_PtrForEachEntryStart( pNames, pName, i, Start )
+ Vec_PtrForEachEntryStart( char *, pNames, pName, i, Start )
{
pActual = Io_ReadBlifCleanName(pName);
if ( pActual == NULL )
@@ -1106,12 +1109,12 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
- pObj->pCopy = (void *)pActual;
+ pObj->pCopy = (Abc_Obj_t *)pActual;
}
// create the fanouts of the box
Abc_NtkForEachPo( pNtkModel, pObj, i )
{
- pActual = (void *)pObj->pCopy;
+ pActual = (char *)pObj->pCopy;
if ( pActual == NULL )
{
p->LineCur = (int)(ABC_PTRINT_T)pBox->pCopy;
@@ -1126,9 +1129,9 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
pObj->pCopy = NULL;
// remove the array of names, assign the pointer to the model
- Vec_PtrForEachEntry( pBox->pData, pName, i )
+ Vec_PtrForEachEntry( char *, (Vec_Ptr_t *)pBox->pData, pName, i )
ABC_FREE( pName );
- Vec_PtrFree( pBox->pData );
+ Vec_PtrFree( (Vec_Ptr_t *)pBox->pData );
pBox->pData = pNtkModel;
return 0;
}
@@ -1191,3 +1194,5 @@ int Io_ReadBlifNetworkConnectBoxes( Io_ReadBlif_t * p, Abc_Ntk_t * pNtkMaster )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadBlifAig.c b/src/base/io/ioReadBlifAig.c
index 8d4c77d4..caa776f9 100644
--- a/src/base/io/ioReadBlifAig.c
+++ b/src/base/io/ioReadBlifAig.c
@@ -22,6 +22,9 @@
#include "extra.h"
#include "vecPtr.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -60,7 +63,7 @@ struct Io_BlifMan_t_
// temporary objects
Io_BlifObj_t * pObjects; // the storage for objects
int nObjects; // the number of objects allocated
- int iObjNext; // the next ABC_FREE object
+ int iObjNext; // the next free object
// file lines
char * pModel; // .model line
Vec_Ptr_t * vInputs; // .inputs lines
@@ -347,7 +350,7 @@ static int Io_BlifGetLine( Io_BlifMan_t * p, char * pToken )
{
char * pLine;
int i;
- Vec_PtrForEachEntry( p->vLines, pLine, i )
+ Vec_PtrForEachEntry( char *, p->vLines, pLine, i )
if ( pToken < pLine )
return i;
return -1;
@@ -369,7 +372,7 @@ static int Io_BlifEstimatePiNum( Io_BlifMan_t * p )
char * pCur;
int i, fSpaces;
int Counter = 0;
- Vec_PtrForEachEntry( p->vInputs, pCur, i )
+ Vec_PtrForEachEntry( char *, p->vInputs, pCur, i )
for ( fSpaces = 0; *pCur; pCur++ )
{
if ( Io_BlifCharIsSpace(*pCur) )
@@ -493,7 +496,7 @@ static void Io_BlifReadPreparse( Io_BlifMan_t * p )
}
// unfold the line extensions and sort lines by directive
- Vec_PtrForEachEntry( p->vLines, pCur, i )
+ Vec_PtrForEachEntry( char *, p->vLines, pCur, i )
{
if ( *pCur == 0 )
continue;
@@ -569,19 +572,19 @@ static Abc_Ntk_t * Io_BlifParse( Io_BlifMan_t * p )
if ( !Io_BlifParseModel( p, p->pModel ) )
return NULL;
// parse the inputs
- Vec_PtrForEachEntry( p->vInputs, pLine, i )
+ Vec_PtrForEachEntry( char *, p->vInputs, pLine, i )
if ( !Io_BlifParseInputs( p, pLine ) )
return NULL;
// parse the outputs
- Vec_PtrForEachEntry( p->vOutputs, pLine, i )
+ Vec_PtrForEachEntry( char *, p->vOutputs, pLine, i )
if ( !Io_BlifParseOutputs( p, pLine ) )
return NULL;
// parse the latches
- Vec_PtrForEachEntry( p->vLatches, pLine, i )
+ Vec_PtrForEachEntry( char *, p->vLatches, pLine, i )
if ( !Io_BlifParseLatch( p, pLine ) )
return NULL;
// parse the nodes
- Vec_PtrForEachEntry( p->vNames, pLine, i )
+ Vec_PtrForEachEntry( char *, p->vNames, pLine, i )
if ( !Io_BlifParseNames( p, pLine ) )
return NULL;
// reconstruct the network from the parsed data
@@ -608,14 +611,14 @@ static int Io_BlifParseModel( Io_BlifMan_t * p, char * pLine )
{
char * pToken;
Io_BlifSplitIntoTokens( p->vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry( p->vTokens, 0 );
+ pToken = (char *)Vec_PtrEntry( p->vTokens, 0 );
assert( !strcmp(pToken, "model") );
if ( Vec_PtrSize(p->vTokens) != 2 )
{
sprintf( p->sError, "Line %d: Model line has %d entries while it should have 2.", Io_BlifGetLine(p, pToken), Vec_PtrSize(p->vTokens) );
return 0;
}
- p->pModel = Vec_PtrEntry( p->vTokens, 1 );
+ p->pModel = (char *)Vec_PtrEntry( p->vTokens, 1 );
return 1;
}
@@ -636,9 +639,9 @@ static int Io_BlifParseInputs( Io_BlifMan_t * p, char * pLine )
char * pToken;
int i;
Io_BlifSplitIntoTokens( p->vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry(p->vTokens, 0);
+ pToken = (char *)Vec_PtrEntry(p->vTokens, 0);
assert( !strcmp(pToken, "inputs") );
- Vec_PtrForEachEntryStart( p->vTokens, pToken, i, 1 )
+ Vec_PtrForEachEntryStart( char *, p->vTokens, pToken, i, 1 )
{
pObj = Io_BlifHashFindOrAdd( p, pToken );
if ( pObj->fPi )
@@ -669,9 +672,9 @@ static int Io_BlifParseOutputs( Io_BlifMan_t * p, char * pLine )
char * pToken;
int i;
Io_BlifSplitIntoTokens( p->vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry(p->vTokens, 0);
+ pToken = (char *)Vec_PtrEntry(p->vTokens, 0);
assert( !strcmp(pToken, "outputs") );
- Vec_PtrForEachEntryStart( p->vTokens, pToken, i, 1 )
+ Vec_PtrForEachEntryStart( char *, p->vTokens, pToken, i, 1 )
{
pObj = Io_BlifHashFindOrAdd( p, pToken );
if ( pObj->fPo )
@@ -699,7 +702,7 @@ static int Io_BlifParseLatch( Io_BlifMan_t * p, char * pLine )
char * pToken;
int Init;
Io_BlifSplitIntoTokens( p->vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry(p->vTokens,0);
+ pToken = (char *)Vec_PtrEntry(p->vTokens,0);
assert( !strcmp(pToken, "latch") );
if ( Vec_PtrSize(p->vTokens) < 3 )
{
@@ -708,7 +711,7 @@ static int Io_BlifParseLatch( Io_BlifMan_t * p, char * pLine )
}
// get initial value
if ( Vec_PtrSize(p->vTokens) > 3 )
- Init = atoi( Vec_PtrEntry(p->vTokens,3) );
+ Init = atoi( (char *)Vec_PtrEntry(p->vTokens,3) );
else
Init = 2;
if ( Init < 0 || Init > 2 )
@@ -723,12 +726,12 @@ static int Io_BlifParseLatch( Io_BlifMan_t * p, char * pLine )
else // if ( Init == 2 )
Init = IO_BLIF_INIT_DC;
// get latch input
- pObj = Io_BlifHashFindOrAdd( p, Vec_PtrEntry(p->vTokens,1) );
+ pObj = Io_BlifHashFindOrAdd( p, (char *)Vec_PtrEntry(p->vTokens,1) );
pObj->fLi = 1;
Vec_PtrPush( p->vLis, pObj );
pObj->Init = Init;
// get latch output
- pObj = Io_BlifHashFindOrAdd( p, Vec_PtrEntry(p->vTokens,2) );
+ pObj = Io_BlifHashFindOrAdd( p, (char *)Vec_PtrEntry(p->vTokens,2) );
if ( pObj->fPi )
{
sprintf( p->sError, "Line %d: Primary input (%s) is also defined latch output.", Io_BlifGetLine(p, pToken), (char*)Vec_PtrEntry(p->vTokens,2) );
@@ -761,8 +764,8 @@ static int Io_BlifParseNames( Io_BlifMan_t * p, char * pLine )
Io_BlifObj_t * pObj;
char * pName;
Io_BlifSplitIntoTokens( p->vTokens, pLine, '\0' );
- assert( !strcmp(Vec_PtrEntry(p->vTokens,0), "names") );
- pName = Vec_PtrEntryLast( p->vTokens );
+ assert( !strcmp((char *)Vec_PtrEntry(p->vTokens,0), "names") );
+ pName = (char *)Vec_PtrEntryLast( p->vTokens );
pObj = Io_BlifHashFindOrAdd( p, pName );
if ( pObj->fPi )
{
@@ -811,7 +814,7 @@ static Abc_Obj_t * Io_BlifParseTable( Io_BlifMan_t * p, char * pTable, Vec_Ptr_t
return Abc_ObjNot( Abc_AigConst1(p->pAig) );
if ( Vec_PtrSize(p->vTokens) == 1 )
{
- pOutput = Vec_PtrEntry( p->vTokens, 0 );
+ pOutput = (char *)Vec_PtrEntry( p->vTokens, 0 );
if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
{
sprintf( p->sError, "Line %d: Constant table has wrong output value (%s).", Io_BlifGetLine(p, pOutput), pOutput );
@@ -819,7 +822,7 @@ static Abc_Obj_t * Io_BlifParseTable( Io_BlifMan_t * p, char * pTable, Vec_Ptr_t
}
return Abc_ObjNotCond( Abc_AigConst1(p->pAig), pOutput[0] == '0' );
}
- pProduct = Vec_PtrEntry( p->vTokens, 0 );
+ pProduct = (char *)Vec_PtrEntry( p->vTokens, 0 );
if ( Vec_PtrSize(p->vTokens) % 2 == 1 )
{
sprintf( p->sError, "Line %d: Table has odd number of tokens (%d).", Io_BlifGetLine(p, pProduct), Vec_PtrSize(p->vTokens) );
@@ -829,8 +832,8 @@ static Abc_Obj_t * Io_BlifParseTable( Io_BlifMan_t * p, char * pTable, Vec_Ptr_t
pRes = Abc_ObjNot( Abc_AigConst1(p->pAig) );
for ( i = 0; i < Vec_PtrSize(p->vTokens)/2; i++ )
{
- pProduct = Vec_PtrEntry( p->vTokens, 2*i + 0 );
- pOutput = Vec_PtrEntry( p->vTokens, 2*i + 1 );
+ pProduct = (char *)Vec_PtrEntry( p->vTokens, 2*i + 0 );
+ pOutput = (char *)Vec_PtrEntry( p->vTokens, 2*i + 1 );
if ( strlen(pProduct) != (unsigned)Vec_PtrSize(vFanins) )
{
sprintf( p->sError, "Line %d: Cube (%s) has size different from the fanin count (%d).", Io_BlifGetLine(p, pProduct), pProduct, Vec_PtrSize(vFanins) );
@@ -853,16 +856,16 @@ static Abc_Obj_t * Io_BlifParseTable( Io_BlifMan_t * p, char * pTable, Vec_Ptr_t
for ( k = 0; pProduct[k]; k++ )
{
if ( pProduct[k] == '0' )
- pCube = Abc_AigAnd( p->pAig->pManFunc, pCube, Abc_ObjNot(Vec_PtrEntry(vFanins,k)) );
+ pCube = Abc_AigAnd( (Abc_Aig_t *)p->pAig->pManFunc, pCube, Abc_ObjNot((Abc_Obj_t *)Vec_PtrEntry(vFanins,k)) );
else if ( pProduct[k] == '1' )
- pCube = Abc_AigAnd( p->pAig->pManFunc, pCube, Vec_PtrEntry(vFanins,k) );
+ pCube = Abc_AigAnd( (Abc_Aig_t *)p->pAig->pManFunc, pCube, (Abc_Obj_t *)Vec_PtrEntry(vFanins,k) );
else if ( pProduct[k] != '-' )
{
sprintf( p->sError, "Line %d: Product term (%s) contains character (%c).", Io_BlifGetLine(p, pProduct), pProduct, pProduct[k] );
return NULL;
}
}
- pRes = Abc_AigOr( p->pAig->pManFunc, pRes, pCube );
+ pRes = Abc_AigOr( (Abc_Aig_t *)p->pAig->pManFunc, pRes, pCube );
}
pRes = Abc_ObjNotCond( pRes, Polarity == 0 );
return pRes;
@@ -901,13 +904,13 @@ static Abc_Obj_t * Io_BlifParseConstruct_rec( Io_BlifMan_t * p, char * pName )
}
// check if the AIG is already constructed
if ( pObjIo->pEquiv )
- return pObjIo->pEquiv;
+ return (Abc_Obj_t *)pObjIo->pEquiv;
// mark this node on the path
pObjIo->fLoop = 1;
// construct the AIGs for the fanins
vFanins = Vec_PtrAlloc( 8 );
Io_BlifCollectTokens( vFanins, pObjIo->pName - pObjIo->Offset, pObjIo->pName );
- Vec_PtrForEachEntry( vFanins, pNameFanin, i )
+ Vec_PtrForEachEntry( char *, vFanins, pNameFanin, i )
{
pFaninAbc = Io_BlifParseConstruct_rec( p, pNameFanin );
if ( pFaninAbc == NULL )
@@ -923,7 +926,7 @@ static Abc_Obj_t * Io_BlifParseConstruct_rec( Io_BlifMan_t * p, char * pName )
// unmark this node on the path
pObjIo->fLoop = 0;
// remember the new node
- return pObjIo->pEquiv;
+ return (Abc_Obj_t *)pObjIo->pEquiv;
}
/**Function*************************************************************
@@ -948,24 +951,24 @@ static int Io_BlifParseConstruct( Io_BlifMan_t * p )
pAig->pName = Extra_UtilStrsav( p->pModel );
pAig->pSpec = Extra_UtilStrsav( p->pFileName );
// create PIs
- Vec_PtrForEachEntry( p->vPis, pObjIo, i )
+ Vec_PtrForEachEntry( Io_BlifObj_t *, p->vPis, pObjIo, i )
{
pObj = Abc_NtkCreatePi( pAig );
Abc_ObjAssignName( pObj, pObjIo->pName, NULL );
pObjIo->pEquiv = pObj;
}
// create POs
- Vec_PtrForEachEntry( p->vPos, pObjIo, i )
+ Vec_PtrForEachEntry( Io_BlifObj_t *, p->vPos, pObjIo, i )
{
pObj = Abc_NtkCreatePo( pAig );
Abc_ObjAssignName( pObj, pObjIo->pName, NULL );
}
// create latches
- Vec_PtrForEachEntry( p->vLos, pObjIo, i )
+ Vec_PtrForEachEntry( Io_BlifObj_t *, p->vLos, pObjIo, i )
{
// add the latch input terminal
pObj = Abc_NtkCreateBi( pAig );
- pObjIoInput = Vec_PtrEntry( p->vLis, i );
+ pObjIoInput = (Io_BlifObj_t *)Vec_PtrEntry( p->vLis, i );
Abc_ObjAssignName( pObj, pObjIoInput->pName, NULL );
// add the latch box
@@ -983,7 +986,7 @@ static int Io_BlifParseConstruct( Io_BlifMan_t * p )
pObjIo->pEquiv = pObj;
}
// traverse the nodes from the POs
- Vec_PtrForEachEntry( p->vPos, pObjIo, i )
+ Vec_PtrForEachEntry( Io_BlifObj_t *, p->vPos, pObjIo, i )
{
pObj = Io_BlifParseConstruct_rec( p, pObjIo->pName );
if ( pObj == NULL )
@@ -991,7 +994,7 @@ static int Io_BlifParseConstruct( Io_BlifMan_t * p )
Abc_ObjAddFanin( Abc_NtkPo(p->pAig, i), pObj );
}
// traverse the nodes from the latch inputs
- Vec_PtrForEachEntry( p->vLis, pObjIo, i )
+ Vec_PtrForEachEntry( Io_BlifObj_t *, p->vLis, pObjIo, i )
{
pObj = Io_BlifParseConstruct_rec( p, pObjIo->pName );
if ( pObj == NULL )
@@ -1011,3 +1014,5 @@ static int Io_BlifParseConstruct( Io_BlifMan_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 2e2388d3..c73f8d92 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -23,6 +23,8 @@
#include "vecPtr.h"
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -33,6 +35,8 @@ typedef struct Io_MvVar_t_ Io_MvVar_t; // parsing var
typedef struct Io_MvMod_t_ Io_MvMod_t; // parsing model
typedef struct Io_MvMan_t_ Io_MvMan_t; // parsing manager
+Vec_Ptr_t *vGlobalLtlArray;
+
struct Io_MvVar_t_
{
int nValues; // the number of values
@@ -46,12 +50,15 @@ struct Io_MvMod_t_
Vec_Ptr_t * vInputs; // .inputs lines
Vec_Ptr_t * vOutputs; // .outputs lines
Vec_Ptr_t * vLatches; // .latch lines
+ Vec_Ptr_t * vFlops; // .flop lines
Vec_Ptr_t * vResets; // .reset lines
Vec_Ptr_t * vNames; // .names lines
Vec_Ptr_t * vSubckts; // .subckt lines
Vec_Ptr_t * vShorts; // .short lines
Vec_Ptr_t * vOnehots; // .onehot lines
Vec_Ptr_t * vMvs; // .mv lines
+ Vec_Ptr_t * vConstrs; // .constraint lines
+ Vec_Ptr_t * vLtlProperties;
int fBlackBox; // indicates blackbox model
// the resulting network
Abc_Ntk_t * pNtk;
@@ -97,13 +104,16 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p );
static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine );
+static int Io_MvParseLineConstrs( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine );
+static int Io_MvParseLineFlop( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine );
+static int Io_MvParseLineLtlProperty( Io_MvMod_t * p, char * pLine );
static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens );
static Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar );
@@ -135,6 +145,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
Abc_Lib_t * pDesign = NULL;
char * pDesignName;
int RetValue, i;
+ char * pLtlProp;
// check that the file is available
pFile = fopen( pFileName, "rb" );
@@ -161,10 +172,11 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
p->pDesign = Abc_LibCreate( pDesignName );
ABC_FREE( pDesignName );
// free the HOP manager
- Hop_ManStop( p->pDesign->pManFunc );
+ Hop_ManStop( (Hop_Man_t *)p->pDesign->pManFunc );
p->pDesign->pManFunc = NULL;
// prepare the file for parsing
Io_MvReadPreparse( p );
+ vGlobalLtlArray = Vec_PtrAlloc( 100 );
// parse interfaces of each network and construct the network
if ( Io_MvReadInterfaces( p ) )
pDesign = Io_MvParse( p );
@@ -178,7 +190,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
// make sure that everything is okay with the network structure
if ( fCheck )
{
- Vec_PtrForEachEntry( pDesign->vModules, pNtk, i )
+ Vec_PtrForEachEntry( Abc_Ntk_t *, pDesign->vModules, pNtk, i )
{
if ( !Abc_NtkCheckRead( pNtk ) )
{
@@ -193,7 +205,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
// detect top-level model
RetValue = Abc_LibFindTopLevelModels( pDesign );
- pNtk = Vec_PtrEntry( pDesign->vTops, 0 );
+ pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
if ( RetValue > 1 )
printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
Vec_PtrSize(pDesign->vTops), pNtk->pName );
@@ -217,6 +229,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
//Io_WriteBlifMv( pNtk, "_temp_.mv" );
if ( pNtk->pSpec == NULL )
pNtk->pSpec = Extra_UtilStrsav( pFileName );
+
+ Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i )
+ Vec_PtrPush( pNtk->vLtlProperties, pLtlProp );
return pNtk;
}
@@ -267,7 +282,7 @@ static void Io_MvFree( Io_MvMan_t * p )
Vec_PtrFree( p->vLines );
if ( p->vModels )
{
- Vec_PtrForEachEntry( p->vModels, pMod, i )
+ Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
Io_MvModFree( pMod );
Vec_PtrFree( p->vModels );
}
@@ -296,12 +311,15 @@ static Io_MvMod_t * Io_MvModAlloc()
p->vInputs = Vec_PtrAlloc( 512 );
p->vOutputs = Vec_PtrAlloc( 512 );
p->vLatches = Vec_PtrAlloc( 512 );
+ p->vFlops = Vec_PtrAlloc( 512 );
p->vResets = Vec_PtrAlloc( 512 );
p->vNames = Vec_PtrAlloc( 512 );
p->vSubckts = Vec_PtrAlloc( 512 );
p->vShorts = Vec_PtrAlloc( 512 );
p->vOnehots = Vec_PtrAlloc( 512 );
p->vMvs = Vec_PtrAlloc( 512 );
+ p->vConstrs = Vec_PtrAlloc( 512 );
+ p->vLtlProperties = Vec_PtrAlloc( 512 );
return p;
}
@@ -323,12 +341,14 @@ static void Io_MvModFree( Io_MvMod_t * p )
Vec_PtrFree( p->vInputs );
Vec_PtrFree( p->vOutputs );
Vec_PtrFree( p->vLatches );
+ Vec_PtrFree( p->vFlops );
Vec_PtrFree( p->vResets );
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vSubckts );
Vec_PtrFree( p->vShorts );
Vec_PtrFree( p->vOnehots );
Vec_PtrFree( p->vMvs );
+ Vec_PtrFree( p->vConstrs );
ABC_FREE( p );
}
@@ -484,7 +504,7 @@ static int Io_MvGetLine( Io_MvMan_t * p, char * pToken )
{
char * pLine;
int i;
- Vec_PtrForEachEntry( p->vLines, pLine, i )
+ Vec_PtrForEachEntry( char *, p->vLines, pLine, i )
if ( pToken < pLine )
return i;
return -1;
@@ -570,7 +590,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
}
// unfold the line extensions and sort lines by directive
- Vec_PtrForEachEntry( p->vLines, pCur, i )
+ Vec_PtrForEachEntry( char *, p->vLines, pCur, i )
{
if ( *pCur == 0 )
continue;
@@ -579,7 +599,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
if ( !Io_MvCharIsSpace(*pPrev) )
break;
// if it is the line extender, overwrite it with spaces
- if ( *pPrev == '\\' )
+ if ( pPrev >= p->pBuffer && *pPrev == '\\' )
{
for ( ; *pPrev; pPrev++ )
*pPrev = ' ';
@@ -595,8 +615,12 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
Vec_PtrPush( p->pLatest->vNames, pCur );
else if ( p->fBlifMv && (!strncmp(pCur, "def ", 4) || !strncmp(pCur, "default ", 8)) )
continue;
+ else if ( !strncmp( pCur, "ltlformula", 10 ) )
+ Vec_PtrPush( p->pLatest->vLtlProperties, pCur );
else if ( !strncmp(pCur, "latch", 5) )
Vec_PtrPush( p->pLatest->vLatches, pCur );
+ else if ( !strncmp(pCur, "flop", 4) )
+ Vec_PtrPush( p->pLatest->vFlops, pCur );
else if ( !strncmp(pCur, "r ", 2) || !strncmp(pCur, "reset ", 6) )
Vec_PtrPush( p->pLatest->vResets, pCur );
else if ( !strncmp(pCur, "inputs", 6) )
@@ -611,6 +635,8 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
Vec_PtrPush( p->pLatest->vOnehots, pCur );
else if ( p->fBlifMv && !strncmp(pCur, "mv", 2) )
Vec_PtrPush( p->pLatest->vMvs, pCur );
+ else if ( !strncmp(pCur, "constraint", 10) )
+ Vec_PtrPush( p->pLatest->vConstrs, pCur );
else if ( !strncmp(pCur, "blackbox", 8) )
p->pLatest->fBlackBox = 1;
else if ( !strncmp(pCur, "model", 5) )
@@ -628,7 +654,10 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
else if ( !strncmp(pCur, "exdc", 4) )
{
fprintf( stdout, "Line %d: Skipping EXDC network.\n", Io_MvGetLine(p, pCur) );
- break;
+// break;
+ if ( p->pLatest )
+ Vec_PtrPush( p->vModels, p->pLatest );
+ p->pLatest = NULL;
}
else if ( !strncmp(pCur, "attrib", 6) )
{}
@@ -640,6 +669,8 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
{}
else if ( !strncmp(pCur, "no_merge", 8) )
{}
+ else if ( !strncmp(pCur, "wd", 2) )
+ {}
// else if ( !strncmp(pCur, "inouts", 6) )
// {}
else
@@ -667,9 +698,9 @@ static int Io_MvReadInterfaces( Io_MvMan_t * p )
{
Io_MvMod_t * pMod;
char * pLine;
- int i, k;
+ int i, k, nOutsOld;
// iterate through the models
- Vec_PtrForEachEntry( p->vModels, pMod, i )
+ Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
{
// parse the model
if ( !Io_MvParseLineModel( pMod, pMod->pName ) )
@@ -681,13 +712,22 @@ static int Io_MvReadInterfaces( Io_MvMan_t * p )
return 0;
}
// parse the inputs
- Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vInputs, pLine, k )
if ( !Io_MvParseLineInputs( pMod, pLine ) )
return 0;
// parse the outputs
- Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vOutputs, pLine, k )
if ( !Io_MvParseLineOutputs( pMod, pLine ) )
return 0;
+ // parse the constraints
+ nOutsOld = Abc_NtkPoNum(pMod->pNtk);
+ Vec_PtrForEachEntry( char *, pMod->vConstrs, pLine, k )
+ if ( !Io_MvParseLineConstrs( pMod, pLine ) )
+ return 0;
+ pMod->pNtk->nConstrs = Abc_NtkPoNum(pMod->pNtk) - nOutsOld;
+ Vec_PtrForEachEntry( char *, pMod->vLtlProperties, pLine, k )
+ if ( !Io_MvParseLineLtlProperty( pMod, pLine ) )
+ return 0;
}
return 1;
}
@@ -711,13 +751,13 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
char * pLine;
int i, k;
// iterate through the models
- Vec_PtrForEachEntry( p->vModels, pMod, i )
+ Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
{
// check if there any MV lines
if ( Vec_PtrSize(pMod->vMvs) > 0 )
Abc_NtkStartMvVars( pMod->pNtk );
// parse the mv lines
- Vec_PtrForEachEntry( pMod->vMvs, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vMvs, pLine, k )
if ( !Io_MvParseLineMv( pMod, pLine ) )
return NULL;
// if reset lines are used there should be the same number of them as latches
@@ -733,33 +773,37 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
if ( p->fUseReset )
pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv );
}
+ // parse the flops
+ Vec_PtrForEachEntry( char *, pMod->vFlops, pLine, k )
+ if ( !Io_MvParseLineFlop( pMod, pLine ) )
+ return NULL;
// parse the latches
- Vec_PtrForEachEntry( pMod->vLatches, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vLatches, pLine, k )
if ( !Io_MvParseLineLatch( pMod, pLine ) )
return NULL;
// parse the reset lines
if ( p->fUseReset )
- Vec_PtrForEachEntry( pMod->vResets, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vResets, pLine, k )
if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) )
return NULL;
// parse the nodes
if ( p->fBlifMv )
{
- Vec_PtrForEachEntry( pMod->vNames, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vNames, pLine, k )
if ( !Io_MvParseLineNamesMv( pMod, pLine, 0 ) )
return NULL;
}
else
{
- Vec_PtrForEachEntry( pMod->vNames, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vNames, pLine, k )
if ( !Io_MvParseLineNamesBlif( pMod, pLine ) )
return NULL;
- Vec_PtrForEachEntry( pMod->vShorts, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vShorts, pLine, k )
if ( !Io_MvParseLineShortBlif( pMod, pLine ) )
return NULL;
}
// parse the subcircuits
- Vec_PtrForEachEntry( pMod->vSubckts, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vSubckts, pLine, k )
if ( !Io_MvParseLineSubckt( pMod, pLine ) )
return NULL;
@@ -768,7 +812,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
{
if ( pMod->pNtk->ntkFunc == ABC_FUNC_SOP )
{
- Extra_MmFlexStop( pMod->pNtk->pManFunc );
+ Extra_MmFlexStop( (Extra_MmFlex_t *)pMod->pNtk->pManFunc );
pMod->pNtk->pManFunc = NULL;
pMod->pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
}
@@ -786,7 +830,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
pObj->pNext = (Abc_Obj_t *)(ABC_PTRINT_T)k;
// derive register
pMod->pNtk->vOnehots = Vec_PtrAlloc( Vec_PtrSize(pMod->vOnehots) );
- Vec_PtrForEachEntry( pMod->vOnehots, pLine, k )
+ Vec_PtrForEachEntry( char *, pMod->vOnehots, pLine, k )
{
vLine = Io_MvParseLineOnehot( pMod, pLine );
if ( vLine == NULL )
@@ -799,7 +843,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
pObj->pNext = NULL;
// print the result
printf( "Parsed %d groups of 1-hot registers: { ", Vec_PtrSize(pMod->pNtk->vOnehots) );
- Vec_PtrForEachEntry( pMod->pNtk->vOnehots, vLine, k )
+ Vec_PtrForEachEntry( Vec_Int_t *, pMod->pNtk->vOnehots, vLine, k )
printf( "%d ", Vec_IntSize(vLine) );
printf( "}\n" );
printf( "The total number of 1-hot registers = %d. (%.2f %%)\n",
@@ -812,6 +856,12 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
printf( "One-hotness condition is written into file \"%s\".\n", pFileName );
}
}
+ if ( Vec_PtrSize(pMod->vFlops) )
+ {
+ printf( "Warning: The parser converted %d .flop lines into .latch lines\n", Vec_PtrSize(pMod->vFlops) );
+ printf( "(information about set, reset, enable of the flops may be lost).\n" );
+ }
+
}
if ( p->nNDnodes )
// printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes );
@@ -838,7 +888,7 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
Vec_Ptr_t * vTokens = p->pMan->vTokens;
char * pToken, * pPivot;
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry( vTokens, 0 );
+ pToken = (char *)Vec_PtrEntry( vTokens, 0 );
assert( !strcmp(pToken, "model") );
if ( Vec_PtrSize(vTokens) != 2 )
{
@@ -854,7 +904,7 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
// for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
// if ( *pToken == '/' || *pToken == '\\' )
// pPivot = pToken+1;
- pPivot = pToken = Vec_PtrEntry(vTokens, 1);
+ pPivot = pToken = (char *)Vec_PtrEntry(vTokens, 1);
p->pNtk->pName = Extra_UtilStrsav( pPivot );
return 1;
}
@@ -876,9 +926,9 @@ static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine )
char * pToken;
int i;
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry(vTokens, 0);
+ pToken = (char *)Vec_PtrEntry(vTokens, 0);
assert( !strcmp(pToken, "inputs") );
- Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
+ Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
Io_ReadCreatePi( p->pNtk, pToken );
return 1;
}
@@ -900,15 +950,82 @@ static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine )
char * pToken;
int i;
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry(vTokens, 0);
+ pToken = (char *)Vec_PtrEntry(vTokens, 0);
assert( !strcmp(pToken, "outputs") );
- Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
+ Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
Io_ReadCreatePo( p->pNtk, pToken );
return 1;
}
/**Function*************************************************************
+ Synopsis [Parses the outputs line.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Io_MvParseLineConstrs( Io_MvMod_t * p, char * pLine )
+{
+ Vec_Ptr_t * vTokens = p->pMan->vTokens;
+ char * pToken;
+ int i;
+ Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
+ pToken = (char *)Vec_PtrEntry(vTokens, 0);
+ assert( !strcmp(pToken, "constraint") );
+ Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
+ Io_ReadCreatePo( p->pNtk, pToken );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Parses the LTL property line.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Io_MvParseLineLtlProperty( Io_MvMod_t * p, char * pLine )
+{
+ int i, j;
+ int quoteBegin, quoteEnd;
+ char keyWordLtlFormula[11];
+ char *actualLtlFormula;
+
+ //checking if the line begins with the keyword "ltlformula" and
+ //progressing the pointer forword
+ for( i=0; i<10; i++ )
+ keyWordLtlFormula[i] = pLine[i];
+ quoteBegin = i;
+ keyWordLtlFormula[10] = '\0';
+ assert( strcmp( "ltlformula", keyWordLtlFormula ) == 0 );
+ while( pLine[i] != '"' )
+ i++;
+ quoteBegin = i;
+ i = strlen( pLine );
+ while( pLine[i] != '"' )
+ i--;
+ quoteEnd = i;
+ actualLtlFormula = (char *)malloc( sizeof(char) * (quoteEnd - quoteBegin) );
+ //printf("\nThe input ltl formula = ");
+ for( i = quoteBegin + 1, j = 0; i<quoteEnd; i++, j++ )
+ //printf("%c", pLine[i] );
+ actualLtlFormula[j] = pLine[i];
+ actualLtlFormula[j] = '\0';
+ Vec_PtrPush( vGlobalLtlArray, actualLtlFormula );
+ return 1;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Parses the latches line.]
Description []
@@ -925,7 +1042,7 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
char * pToken;
int Init;
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
- pToken = Vec_PtrEntry(vTokens,0);
+ pToken = (char *)Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "latch") );
if ( Vec_PtrSize(vTokens) < 3 )
{
@@ -935,7 +1052,7 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
// create latch
if ( p->pResetLatch == NULL )
{
- pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Vec_PtrEntry(vTokens,2) );
+ pObj = Io_ReadCreateLatch( p->pNtk, (char *)Vec_PtrEntry(vTokens,1), (char *)Vec_PtrEntry(vTokens,2) );
// get initial value
if ( p->pMan->fBlifMv )
Abc_LatchSetInit0( pObj );
@@ -945,7 +1062,7 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
printf( "Warning: Line %d has .latch directive with unrecognized entries (the total of %d entries).\n",
Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
if ( Vec_PtrSize(vTokens) > 3 )
- Init = atoi( Vec_PtrEntryLast(vTokens) );
+ Init = atoi( (char *)Vec_PtrEntryLast(vTokens) );
else
Init = 2;
if ( Init < 0 || Init > 2 )
@@ -964,11 +1081,11 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
else
{
// get the net corresponding to the output of the latch
- pNet = Abc_NtkFindOrCreateNet( p->pNtk, Vec_PtrEntry(vTokens,2) );
+ pNet = Abc_NtkFindOrCreateNet( p->pNtk, (char *)Vec_PtrEntry(vTokens,2) );
// get the net corresponding to the latch output (feeding into reset MUX)
pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") );
// create latch
- pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) );
+ pObj = Io_ReadCreateLatch( p->pNtk, (char *)Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) );
// Abc_LatchSetInit0( pObj );
Abc_LatchSetInit0( pObj );
}
@@ -977,6 +1094,81 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
/**Function*************************************************************
+ Synopsis [Parses the latches line.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Io_MvParseLineFlop( Io_MvMod_t * p, char * pLine )
+{
+ Vec_Ptr_t * vTokens = p->pMan->vTokens;
+ Abc_Obj_t * pObj;
+ char * pToken, * pOutput, * pInput;
+ int i, Init = 2;
+ assert( !p->pMan->fBlifMv );
+ Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
+ pToken = (char *)Vec_PtrEntry(vTokens,0);
+ assert( !strcmp(pToken, "flop") );
+ // get flop output
+ Vec_PtrForEachEntry( char *, vTokens, pToken, i )
+ if ( pToken[0] == 'Q' && pToken[1] == '=' )
+ break;
+ if ( i == Vec_PtrSize(vTokens) )
+ {
+ sprintf( p->pMan->sError, "Line %d: Cannot find flop output.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
+ return 0;
+ }
+ pOutput = pToken+2;
+ // get flop input
+ Vec_PtrForEachEntry( char *, vTokens, pToken, i )
+ if ( pToken[0] == 'D' && pToken[1] == '=' )
+ break;
+ if ( i == Vec_PtrSize(vTokens) )
+ {
+ sprintf( p->pMan->sError, "Line %d: Cannot find flop input.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
+ return 0;
+ }
+ pInput = pToken+2;
+ // create latch
+ pObj = Io_ReadCreateLatch( p->pNtk, pInput, pOutput );
+ // get the init value
+ Vec_PtrForEachEntry( char *, vTokens, pToken, i )
+ {
+ if ( !strncmp( pToken, "init=", 5 ) )
+ {
+ Init = 0;
+ if ( pToken[5] == '1' )
+ Init = 1;
+ else if ( pToken[5] == '2' )
+ Init = 2;
+ else if ( pToken[5] != '0' )
+ {
+ sprintf( p->pMan->sError, "Line %d: Cannot read flop init value %s.", Io_MvGetLine(p->pMan, pToken), pToken );
+ return 0;
+ }
+ break;
+ }
+ }
+ if ( Init < 0 || Init > 2 )
+ {
+ sprintf( p->pMan->sError, "Line %d: Initial state of the flop is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), (char*)Vec_PtrEntry(vTokens,3) );
+ return 0;
+ }
+ if ( Init == 0 )
+ Abc_LatchSetInit0( pObj );
+ else if ( Init == 1 )
+ Abc_LatchSetInit1( pObj );
+ else // if ( Init == 2 )
+ Abc_LatchSetInitDc( pObj );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Parses the subckt line.]
Description []
@@ -997,11 +1189,19 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
// split the line into tokens
nEquals = Io_MvCountChars( pLine, '=' );
Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
- pToken = Vec_PtrEntry(vTokens,0);
+ pToken = (char *)Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "subckt") );
// get the model for this box
- pName = Vec_PtrEntry(vTokens,1);
+ pName = (char *)Vec_PtrEntry(vTokens,1);
+ // skip instance name for now
+ for ( pToken = pName; *pToken; pToken++ )
+ if ( *pToken == '|' )
+ {
+ *pToken = 0;
+ break;
+ }
+ // find the model
pModel = Abc_LibFindModelByName( p->pMan->pDesign, pName );
if ( pModel == NULL )
{
@@ -1027,7 +1227,7 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
pBox = Abc_NtkCreateWhitebox( p->pNtk );
pBox->pData = pModel;
if ( p->pMan->fBlifMv )
- Abc_ObjAssignName( pBox, Vec_PtrEntry(vTokens,2), NULL );
+ Abc_ObjAssignName( pBox, (char *)Vec_PtrEntry(vTokens,2), NULL );
// go through formal inputs
Abc_NtkForEachPi( pModel, pTerm, i )
{
@@ -1047,7 +1247,7 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
if ( k == nEquals )
{
Abc_Obj_t * pNode = Abc_NtkCreateNode( p->pNtk );
- pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, " 0\n" );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, " 0\n" );
pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNode, "abc") );
Abc_ObjAddFanin( pNet, pNode );
pTerm = Abc_NtkCreateBi( p->pNtk );
@@ -1110,13 +1310,13 @@ static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine )
// split the line into tokens
nEquals = Io_MvCountChars( pLine, '=' );
Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
- pToken = Vec_PtrEntry(vTokens,0);
+ pToken = (char *)Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "onehot") );
// iterate through the register names
// vResult = Vec_PtrAlloc( Vec_PtrSize(vTokens) );
vResult = Vec_IntAlloc( Vec_PtrSize(vTokens) );
- Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
+ Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
{
// check if this register exists
pNet = Abc_NtkFindNet( p->pNtk, pToken );
@@ -1167,7 +1367,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
// count commas and get the tokens
nCommas = Io_MvCountChars( pLine, ',' );
Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', ',' );
- pName = Vec_PtrEntry(vTokens,0);
+ pName = (char *)Vec_PtrEntry(vTokens,0);
assert( !strcmp(pName, "mv") );
// get the number of values
if ( Vec_PtrSize(vTokens) <= nCommas + 2 )
@@ -1175,7 +1375,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
sprintf( p->pMan->sError, "Line %d: The number of values in not specified in .mv line.", Io_MvGetLine(p->pMan, pName) );
return 0;
}
- nValues = atoi( Vec_PtrEntry(vTokens,nCommas+2) );
+ nValues = atoi( (char *)Vec_PtrEntry(vTokens,nCommas+2) );
if ( nValues < 2 || nValues > IO_BLIFMV_MAXVALUES )
{
sprintf( p->pMan->sError, "Line %d: The number of values (%d) is incorrect (should be >= 2 and <= %d).",
@@ -1192,10 +1392,10 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
return 0;
}
// go through variables
- pFlex = Abc_NtkMvVarMan( p->pNtk );
+ pFlex = (Extra_MmFlex_t *)Abc_NtkMvVarMan( p->pNtk );
for ( i = 0; i <= nCommas; i++ )
{
- pName = Vec_PtrEntry( vTokens, i+1 );
+ pName = (char *)Vec_PtrEntry( vTokens, i+1 );
pObj = Abc_NtkFindOrCreateNet( p->pNtk, pName );
// allocate variable
pVar = (Io_MvVar_t *)Extra_MmFlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
@@ -1205,7 +1405,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
if ( Vec_PtrSize(vTokens) > nCommas + 3 )
{
pVar->pNames = (char **)Extra_MmFlexEntryFetch( pFlex, sizeof(char *) * nValues );
- Vec_PtrForEachEntryStart( vTokens, pName, k, nCommas + 3 )
+ Vec_PtrForEachEntryStart( char *, vTokens, pName, k, nCommas + 3 )
{
pVar->pNames[k-(nCommas + 3)] = (char *)Extra_MmFlexEntryFetch( pFlex, strlen(pName) + 1 );
strcpy( pVar->pNames[k-(nCommas + 3)], pName );
@@ -1222,7 +1422,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
for ( k = i+1; k < nValues; k++ )
if ( !strcmp(pVar->pNames[i], pVar->pNames[k]) )
{
- pName = Vec_PtrEntry(vTokens,0);
+ pName = (char *)Vec_PtrEntry(vTokens,0);
sprintf( p->pMan->sError, "Line %d: Symbolic value name \"%s\" is repeated in .mv line.",
Io_MvGetLine(p->pMan, pName), pVar->pNames[i] );
return 0;
@@ -1251,12 +1451,12 @@ static int Io_MvWriteValues( Abc_Obj_t * pNode, Vec_Str_t * vFunc )
Abc_ObjForEachFanin( pNode, pFanin, i )
{
sprintf( Buffer, "%d", Abc_ObjMvVarNum(pFanin) );
- Vec_StrAppend( vFunc, Buffer );
+ Vec_StrPrintStr( vFunc, Buffer );
Vec_StrPush( vFunc, ' ' );
}
// add the node number of values
sprintf( Buffer, "%d", Abc_ObjMvVarNum(Abc_ObjFanout0(pNode)) );
- Vec_StrAppend( vFunc, Buffer );
+ Vec_StrPrintStr( vFunc, Buffer );
Vec_StrPush( vFunc, '\n' );
return 1;
}
@@ -1294,18 +1494,18 @@ static int Io_MvParseLiteralMv( Io_MvMod_t * p, Abc_Obj_t * pNode, char * pToken
}
Vec_StrPush( vFunc, '=' );
sprintf( Buffer, "%d", i );
- Vec_StrAppend( vFunc, Buffer );
+ Vec_StrPrintStr( vFunc, Buffer );
Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
return 1;
}
// consider regular literal
assert( iLit < Abc_ObjFaninNum(pNode) );
pNet = iLit >= 0 ? Abc_ObjFanin(pNode, iLit) : Abc_ObjFanout0(pNode);
- pVar = Abc_ObjMvVar( pNet );
+ pVar = (Io_MvVar_t *)Abc_ObjMvVar( pNet );
// if the var is absent or has no symbolic values quit
if ( pVar == NULL || pVar->pNames == NULL )
{
- Vec_StrAppend( vFunc, pToken );
+ Vec_StrPrintStr( vFunc, pToken );
Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
return 1;
}
@@ -1334,7 +1534,7 @@ static int Io_MvParseLiteralMv( Io_MvMod_t * p, Abc_Obj_t * pNode, char * pToken
}
// value name is found
sprintf( Buffer, "%d", i );
- Vec_StrAppend( vFunc, Buffer );
+ Vec_StrPrintStr( vFunc, Buffer );
// update the pointer
pCur = pNext - 1;
}
@@ -1363,12 +1563,12 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
// write the number of values
// Io_MvWriteValues( pNode, vFunc );
// get the first token
- pFirst = Vec_PtrEntry( vTokens2, 0 );
+ pFirst = (char *)Vec_PtrEntry( vTokens2, 0 );
if ( pFirst[0] == '.' )
{
// write the default literal
Vec_StrPush( vFunc, 'd' );
- pToken = Vec_PtrEntry(vTokens2, 1 + iOut);
+ pToken = (char *)Vec_PtrEntry(vTokens2, 1 + iOut);
if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, -1 ) )
return NULL;
iStart = 1 + nOutputs;
@@ -1381,12 +1581,12 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
// input literals
for ( i = 0; i < nInputs; i++ )
{
- pToken = Vec_PtrEntry( vTokens2, iStart + i );
+ pToken = (char *)Vec_PtrEntry( vTokens2, iStart + i );
if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, i ) )
return NULL;
}
// output literal
- pToken = Vec_PtrEntry( vTokens2, iStart + nInputs + iOut );
+ pToken = (char *)Vec_PtrEntry( vTokens2, iStart + nInputs + iOut );
if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, -1 ) )
return NULL;
// update the counter
@@ -1424,7 +1624,7 @@ static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
// duplicate MV variables
if ( Abc_NtkMvVar(p->pNtk) )
{
- pVar = Abc_ObjMvVar( pOutNet );
+ pVar = (Io_MvVar_t *)Abc_ObjMvVar( pOutNet );
Abc_ObjSetMvVar( pData0Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
Abc_ObjSetMvVar( pData1Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
}
@@ -1439,10 +1639,10 @@ static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
// int nValues = Abc_ObjMvVarNum(pOutNet);
// sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
sprintf( Buffer, "1 - - =1\n0 - - =2\n" );
- pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, Buffer );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, Buffer );
}
else
- pNode->pData = Abc_SopCreateMux( p->pNtk->pManFunc );
+ pNode->pData = Abc_SopCreateMux( (Extra_MmFlex_t *)p->pNtk->pManFunc );
// add nets
Abc_ObjAddFanin( pNode, pResetLONet );
Abc_ObjAddFanin( pNode, pData1Net );
@@ -1466,7 +1666,7 @@ static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Pt
Abc_Obj_t * pNet, * pNode;
char * pName;
// get the output name
- pName = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + iOut );
+ pName = (char *)Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + iOut );
// create the node
if ( fReset )
{
@@ -1503,7 +1703,7 @@ static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Pt
pNode->pData = Io_MvParseTableMv( p, pNode, vTokens2, nInputs, nOutputs, iOut );
if ( pNode->pData == NULL )
return 0;
- pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, pNode->pData );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
//printf( "Finished parsing node \"%s\" with table:\n%s\n", pName, pNode->pData );
return 1;
}
@@ -1537,9 +1737,9 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
// split names line into tokens
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
if ( fReset )
- assert( !strcmp(Vec_PtrEntry(vTokens,0), "r") || !strcmp(Vec_PtrEntry(vTokens,0), "reset") );
+ assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "r") || !strcmp((char *)Vec_PtrEntry(vTokens,0), "reset") );
else
- assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") || !strcmp(Vec_PtrEntry(vTokens,0), "table") );
+ assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "names") || !strcmp((char *)Vec_PtrEntry(vTokens,0), "table") );
// find the number of inputs and outputs
nInputs = Vec_PtrSize(vTokens) - 2;
nOutputs = 1;
@@ -1553,9 +1753,9 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
}
}
// split table into tokens
- pName = Vec_PtrEntryLast( vTokens );
+ pName = (char *)Vec_PtrEntryLast( vTokens );
Io_MvSplitIntoTokensMv( vTokens2, pName + strlen(pName) );
- pFirst = Vec_PtrEntry( vTokens2, 0 );
+ pFirst = (char *)Vec_PtrEntry( vTokens2, 0 );
if ( pFirst[0] == '.' )
{
assert( pFirst[1] == 'd' );
@@ -1576,7 +1776,7 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
// add the outputs to the PIs
for ( i = 0; i < nOutputs; i++ )
{
- pName = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + i );
+ pName = (char *)Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + i );
// get the net corresponding to this node
pNet = Abc_NtkFindOrCreateNet(p->pNtk, pName);
if ( fReset )
@@ -1625,19 +1825,19 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
// get the tokens
Io_MvSplitIntoTokens( vTokens, pTable, '.' );
if ( Vec_PtrSize(vTokens) == 0 )
- return Abc_SopCreateConst0( p->pNtk->pManFunc );
+ return Abc_SopCreateConst0( (Extra_MmFlex_t *)p->pNtk->pManFunc );
if ( Vec_PtrSize(vTokens) == 1 )
{
- pOutput = Vec_PtrEntry( vTokens, 0 );
+ pOutput = (char *)Vec_PtrEntry( vTokens, 0 );
c = pOutput[0];
if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
{
sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Io_MvGetLine(p->pMan, pOutput), pOutput );
return NULL;
}
- return pOutput[0] == '0' ? Abc_SopCreateConst0(p->pNtk->pManFunc) : Abc_SopCreateConst1(p->pNtk->pManFunc);
+ return pOutput[0] == '0' ? Abc_SopCreateConst0((Extra_MmFlex_t *)p->pNtk->pManFunc) : Abc_SopCreateConst1((Extra_MmFlex_t *)p->pNtk->pManFunc);
}
- pProduct = Vec_PtrEntry( vTokens, 0 );
+ pProduct = (char *)Vec_PtrEntry( vTokens, 0 );
if ( Vec_PtrSize(vTokens) % 2 == 1 )
{
sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Io_MvGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) );
@@ -1647,8 +1847,8 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
Vec_StrClear( vFunc );
for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ )
{
- pProduct = Vec_PtrEntry( vTokens, 2*i + 0 );
- pOutput = Vec_PtrEntry( vTokens, 2*i + 1 );
+ pProduct = (char *)Vec_PtrEntry( vTokens, 2*i + 0 );
+ pOutput = (char *)Vec_PtrEntry( vTokens, 2*i + 1 );
if ( strlen(pProduct) != (unsigned)nFanins )
{
sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Io_MvGetLine(p->pMan, pProduct), pProduct, nFanins );
@@ -1668,7 +1868,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
return NULL;
}
// parse one product
- Vec_StrAppend( vFunc, pProduct );
+ Vec_StrPrintStr( vFunc, pProduct );
Vec_StrPush( vFunc, ' ' );
Vec_StrPush( vFunc, pOutput[0] );
Vec_StrPush( vFunc, '\n' );
@@ -1696,11 +1896,11 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
assert( !p->pMan->fBlifMv );
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
// parse the mapped node
- if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") )
+ if ( !strcmp((char *)Vec_PtrEntry(vTokens,0), "gate") )
return Io_MvParseLineGateBlif( p, vTokens );
// parse the regular name line
- assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
- pName = Vec_PtrEntryLast( vTokens );
+ assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "names") );
+ pName = (char *)Vec_PtrEntryLast( vTokens );
pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
if ( Abc_ObjFaninNum(pNet) > 0 )
{
@@ -1713,7 +1913,7 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
pNode->pData = Io_MvParseTableBlif( p, pName + strlen(pName), Abc_ObjFaninNum(pNode) );
if ( pNode->pData == NULL )
return 0;
- pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, pNode->pData );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
return 1;
}
@@ -1737,12 +1937,12 @@ static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine )
Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
if ( Vec_PtrSize(vTokens) != 3 )
{
- sprintf( p->pMan->sError, "Line %d: Expecting three entries in the .short line.", Io_MvGetLine(p->pMan, Vec_PtrEntry(vTokens,0)) );
+ sprintf( p->pMan->sError, "Line %d: Expecting three entries in the .short line.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
return 0;
}
// parse the regular name line
- assert( !strcmp(Vec_PtrEntry(vTokens,0), "short") );
- pName = Vec_PtrEntryLast( vTokens );
+ assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "short") );
+ pName = (char *)Vec_PtrEntryLast( vTokens );
pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
if ( Abc_ObjFaninNum(pNet) > 0 )
{
@@ -1752,7 +1952,7 @@ static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine )
// create fanins
pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), 1 );
// parse the table of this node
- pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, "1 1\n" );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, "1 1\n" );
return 1;
}
@@ -1774,7 +1974,7 @@ Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar )
int i;
if ( pVar == NULL )
return NULL;
- pFlex = Abc_NtkMvVarMan( pNtk );
+ pFlex = (Extra_MmFlex_t *)Abc_NtkMvVarMan( pNtk );
assert( pFlex != NULL );
pVarDup = (Io_MvVar_t *)Extra_MmFlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
pVarDup->nValues = pVar->nValues;
@@ -1790,10 +1990,14 @@ Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar )
return pVarDup;
}
+ABC_NAMESPACE_IMPL_END
#include "mio.h"
#include "main.h"
+ABC_NAMESPACE_IMPL_START
+
+
/**Function*************************************************************
Synopsis []
@@ -1835,10 +2039,10 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
char ** ppNames, * pName;
int i, nNames;
- pName = vTokens->pArray[0];
+ pName = (char *)vTokens->pArray[0];
// check that the library is available
- pGenlib = Abc_FrameReadLibGen();
+ pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
if ( pGenlib == NULL )
{
sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
@@ -1853,7 +2057,7 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
}
// get the gate
- pGate = Mio_LibraryReadGateByName( pGenlib, vTokens->pArray[1] );
+ pGate = Mio_LibraryReadGateByName( pGenlib, (char *)vTokens->pArray[1] );
if ( pGate == NULL )
{
sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
@@ -1865,7 +2069,7 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
{
assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
p->pNtk->ntkFunc = ABC_FUNC_MAP;
- Extra_MmFlexStop( p->pNtk->pManFunc );
+ Extra_MmFlexStop( (Extra_MmFlex_t *)p->pNtk->pManFunc );
p->pNtk->pManFunc = pGenlib;
}
@@ -1879,7 +2083,7 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
// remove the formal parameter names
for ( i = 2; i < vTokens->nSize; i++ )
{
- vTokens->pArray[i] = Io_ReadBlifCleanName( vTokens->pArray[i] );
+ vTokens->pArray[i] = Io_ReadBlifCleanName( (char *)vTokens->pArray[i] );
if ( vTokens->pArray[i] == NULL )
{
sprintf( p->pMan->sError, "Line %d: Invalid gate input assignment.", Io_MvGetLine(p->pMan, pName) );
@@ -1902,3 +2106,5 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c
index 4848e4e9..35bc6aaa 100644
--- a/src/base/io/ioReadDsd.c
+++ b/src/base/io/ioReadDsd.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -183,11 +186,11 @@ Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop )
}
}
if ( pSop )
- pObj->pData = Abc_SopRegister( pNtk->pManFunc, pSop );
+ pObj->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, pSop );
else if ( TypeExor )
- pObj->pData = Abc_SopCreateXorSpecial( pNtk->pManFunc, nParts );
+ pObj->pData = Abc_SopCreateXorSpecial( (Extra_MmFlex_t *)pNtk->pManFunc, nParts );
else
- pObj->pData = Abc_SopCreateAnd( pNtk->pManFunc, nParts, NULL );
+ pObj->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtk->pManFunc, nParts, NULL );
return pObj;
}
if ( *pCur >= 'a' && *pCur <= 'z' )
@@ -248,7 +251,7 @@ Abc_Ntk_t * Io_ReadDsd( char * pForm )
// create PIs
vNames = Abc_NodeGetFakeNames( nInputs );
for ( i = 0; i < nInputs; i++ )
- Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), Vec_PtrEntry(vNames, i), NULL );
+ Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), (char *)Vec_PtrEntry(vNames, i), NULL );
Abc_NodeFreeNames( vNames );
// transform the formula by inserting parantheses
@@ -306,3 +309,5 @@ Abc_Ntk_t * Io_ReadDsd( char * pForm )
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 26e49d0e..8c739e61 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -90,8 +93,8 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
int fTokensReady, iLine, i;
// read the first line
- vTokens = Extra_FileReaderGetTokens(p);
- if ( strcmp( vTokens->pArray[0], "edif" ) != 0 )
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ if ( strcmp( (char *)vTokens->pArray[0], "edif" ) != 0 )
{
printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
return NULL;
@@ -103,19 +106,19 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
// go through the lines of the file
fTokensReady = 0;
pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
- for ( iLine = 1; fTokensReady || (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
+ for ( iLine = 1; fTokensReady || (vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p)); iLine++ )
{
Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
// get the type of the line
fTokensReady = 0;
- if ( strcmp( vTokens->pArray[0], "instance" ) == 0 )
+ if ( strcmp( (char *)vTokens->pArray[0], "instance" ) == 0 )
{
- pNetName = vTokens->pArray[1];
+ pNetName = (char *)vTokens->pArray[1];
pNet = Abc_NtkFindOrCreateNet( pNtk, pNetName );
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- pGateName = vTokens->pArray[1];
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ pGateName = (char *)vTokens->pArray[1];
if ( strncmp( pGateName, "Flip", 4 ) == 0 )
{
pObj = Abc_NtkCreateLatch( pNtk );
@@ -129,63 +132,63 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
}
Abc_ObjAddFanin( pNet, pObj );
}
- else if ( strcmp( vTokens->pArray[0], "net" ) == 0 )
+ else if ( strcmp( (char *)vTokens->pArray[0], "net" ) == 0 )
{
- pNetName = vTokens->pArray[1];
+ pNetName = (char *)vTokens->pArray[1];
if ( strcmp( pNetName, "CK" ) == 0 || strcmp( pNetName, "RESET" ) == 0 )
continue;
if ( strcmp( pNetName + strlen(pNetName) - 4, "_out" ) == 0 )
pNetName[strlen(pNetName) - 4] = 0;
pNet = Abc_NtkFindNet( pNtk, pNetName );
assert( pNet );
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- while ( strcmp( vTokens->pArray[0], "portRef" ) == 0 )
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ while ( strcmp( (char *)vTokens->pArray[0], "portRef" ) == 0 )
{
- if ( strcmp( pNetName, vTokens->pArray[3] ) != 0 )
+ if ( strcmp( pNetName, (char *)vTokens->pArray[3] ) != 0 )
{
- pFanout = Abc_NtkFindNet( pNtk, vTokens->pArray[3] );
+ pFanout = Abc_NtkFindNet( pNtk, (char *)vTokens->pArray[3] );
Abc_ObjAddFanin( Abc_ObjFanin0(pFanout), pNet );
}
- vTokens = Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
}
fTokensReady = 1;
}
- else if ( strcmp( vTokens->pArray[0], "library" ) == 0 )
+ else if ( strcmp( (char *)vTokens->pArray[0], "library" ) == 0 )
{
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- vTokens = Extra_FileReaderGetTokens(p);
- while ( strcmp( vTokens->pArray[0], "port" ) == 0 )
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
+ while ( strcmp( (char *)vTokens->pArray[0], "port" ) == 0 )
{
- pNetName = vTokens->pArray[1];
+ pNetName = (char *)vTokens->pArray[1];
if ( strcmp( pNetName, "CK" ) == 0 || strcmp( pNetName, "RESET" ) == 0 )
{
- vTokens = Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
continue;
}
if ( strcmp( pNetName + strlen(pNetName) - 3, "_PO" ) == 0 )
pNetName[strlen(pNetName) - 3] = 0;
- if ( strcmp( vTokens->pArray[3], "INPUT" ) == 0 )
- Io_ReadCreatePi( pNtk, vTokens->pArray[1] );
- else if ( strcmp( vTokens->pArray[3], "OUTPUT" ) == 0 )
- Io_ReadCreatePo( pNtk, vTokens->pArray[1] );
+ if ( strcmp( (char *)vTokens->pArray[3], "INPUT" ) == 0 )
+ Io_ReadCreatePi( pNtk, (char *)vTokens->pArray[1] );
+ else if ( strcmp( (char *)vTokens->pArray[3], "OUTPUT" ) == 0 )
+ Io_ReadCreatePo( pNtk, (char *)vTokens->pArray[1] );
else
{
printf( "%s (line %d): Wrong interface specification.\n", Extra_FileReaderGetFileName(p), iLine );
Abc_NtkDelete( pNtk );
return NULL;
}
- vTokens = Extra_FileReaderGetTokens(p);
+ vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p);
}
}
- else if ( strcmp( vTokens->pArray[0], "design" ) == 0 )
+ else if ( strcmp( (char *)vTokens->pArray[0], "design" ) == 0 )
{
ABC_FREE( pNtk->pName );
- pNtk->pName = Extra_UtilStrsav( vTokens->pArray[3] );
+ pNtk->pName = (char *)Extra_UtilStrsav( (char *)vTokens->pArray[3] );
break;
}
}
@@ -194,22 +197,22 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
// assign logic functions
Abc_NtkForEachNode( pNtk, pObj, i )
{
- if ( strncmp( pObj->pData, "And", 3 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
- else if ( strncmp( pObj->pData, "Or", 2 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateOr(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
- else if ( strncmp( pObj->pData, "Nand", 4 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateNand(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
- else if ( strncmp( pObj->pData, "Nor", 3 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateNor(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
- else if ( strncmp( pObj->pData, "Exor", 4 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateXor(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
- else if ( strncmp( pObj->pData, "Exnor", 5 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateNxor(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
- else if ( strncmp( pObj->pData, "Inv", 3 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateInv(pNtk->pManFunc) );
- else if ( strncmp( pObj->pData, "Buf", 3 ) == 0 )
- Abc_ObjSetData( pObj, Abc_SopCreateBuf(pNtk->pManFunc) );
+ if ( strncmp( (char *)pObj->pData, "And", 3 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateAnd((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
+ else if ( strncmp( (char *)pObj->pData, "Or", 2 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateOr((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
+ else if ( strncmp( (char *)pObj->pData, "Nand", 4 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateNand((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+ else if ( strncmp( (char *)pObj->pData, "Nor", 3 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateNor((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+ else if ( strncmp( (char *)pObj->pData, "Exor", 4 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateXor((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+ else if ( strncmp( (char *)pObj->pData, "Exnor", 5 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateNxor((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+ else if ( strncmp( (char *)pObj->pData, "Inv", 3 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateInv((Extra_MmFlex_t *)pNtk->pManFunc) );
+ else if ( strncmp( (char *)pObj->pData, "Buf", 3 ) == 0 )
+ Abc_ObjSetData( pObj, Abc_SopCreateBuf((Extra_MmFlex_t *)pNtk->pManFunc) );
else
{
printf( "%s: Unknown gate type \"%s\".\n", Extra_FileReaderGetFileName(p), (char*)pObj->pData );
@@ -233,3 +236,5 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
index f778197b..1e4f5d46 100644
--- a/src/base/io/ioReadEqn.c
+++ b/src/base/io/ioReadEqn.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -100,13 +103,13 @@ Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
// go through the lines of the file
vVars = Vec_PtrAlloc( 100 );
pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
- for ( iLine = 0; (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
+ for ( iLine = 0; (vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p)); iLine++ )
{
Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
// check if the first token contains anything
- Io_ReadEqnStrCompact( vTokens->pArray[0] );
- if ( strlen(vTokens->pArray[0]) == 0 )
+ Io_ReadEqnStrCompact( (char *)vTokens->pArray[0] );
+ if ( strlen((char *)vTokens->pArray[0]) == 0 )
break;
// if the number of tokens is different from two, error
@@ -118,16 +121,16 @@ Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
}
// get the type of the line
- if ( strncmp( vTokens->pArray[0], "INORDER", 7 ) == 0 )
+ if ( strncmp( (char *)vTokens->pArray[0], "INORDER", 7 ) == 0 )
{
- Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
- Vec_PtrForEachEntry( vVars, pVarName, i )
+ Io_ReadEqnStrCutAt( (char *)vTokens->pArray[1], " \n\r\t", 0, vVars );
+ Vec_PtrForEachEntry( char *, vVars, pVarName, i )
Io_ReadCreatePi( pNtk, pVarName );
}
- else if ( strncmp( vTokens->pArray[0], "OUTORDER", 8 ) == 0 )
+ else if ( strncmp( (char *)vTokens->pArray[0], "OUTORDER", 8 ) == 0 )
{
- Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
- Vec_PtrForEachEntry( vVars, pVarName, i )
+ Io_ReadEqnStrCutAt( (char *)vTokens->pArray[1], " \n\r\t", 0, vVars );
+ Vec_PtrForEachEntry( char *, vVars, pVarName, i )
Io_ReadCreatePo( pNtk, pVarName );
}
else
@@ -135,8 +138,8 @@ Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
extern Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVarNames, Hop_Man_t * pMan );
// get hold of the node name and its formula
- pNodeName = vTokens->pArray[0];
- pFormula = vTokens->pArray[1];
+ pNodeName = (char *)vTokens->pArray[0];
+ pFormula = (char *)vTokens->pArray[1];
// compact the formula
Io_ReadEqnStrCompact( pFormula );
@@ -156,7 +159,7 @@ Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
// create the node
pNode = Io_ReadCreateNode( pNtk, pNodeName, (char **)Vec_PtrArray(vVars), Vec_PtrSize(vVars) );
// derive the function
- pNode->pData = Parse_FormulaParserEqn( stdout, pFormula, vVars, pNtk->pManFunc );
+ pNode->pData = Parse_FormulaParserEqn( stdout, pFormula, vVars, (Hop_Man_t *)pNtk->pManFunc );
// remove the cubes
ABC_FREE( pFormulaCopy );
}
@@ -204,7 +207,7 @@ int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName )
{
char * pToken;
int i;
- Vec_PtrForEachEntry( vTokens, pToken, i )
+ Vec_PtrForEachEntry( char *, vTokens, pToken, i )
if ( strcmp( pToken, pName ) == 0 )
return i;
return -1;
@@ -237,3 +240,5 @@ void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t *
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 347d1daa..85029ce8 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -95,12 +98,12 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
// go through the lines of the file
nCubes = 0;
pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
- for ( iLine = 0; (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
+ for ( iLine = 0; (vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p)); iLine++ )
{
Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
// if it is the end of file, quit the loop
- if ( strcmp( vTokens->pArray[0], ".e" ) == 0 )
+ if ( strcmp( (char *)vTokens->pArray[0], ".e" ) == 0 )
break;
if ( vTokens->nSize == 1 )
@@ -111,25 +114,25 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
return NULL;
}
- if ( strcmp( vTokens->pArray[0], ".i" ) == 0 )
- nInputs = atoi(vTokens->pArray[1]);
- else if ( strcmp( vTokens->pArray[0], ".o" ) == 0 )
- nOutputs = atoi(vTokens->pArray[1]);
- else if ( strcmp( vTokens->pArray[0], ".p" ) == 0 )
- nProducts = atoi(vTokens->pArray[1]);
- else if ( strcmp( vTokens->pArray[0], ".ilb" ) == 0 )
+ if ( strcmp( (char *)vTokens->pArray[0], ".i" ) == 0 )
+ nInputs = atoi((char *)vTokens->pArray[1]);
+ else if ( strcmp( (char *)vTokens->pArray[0], ".o" ) == 0 )
+ nOutputs = atoi((char *)vTokens->pArray[1]);
+ else if ( strcmp( (char *)vTokens->pArray[0], ".p" ) == 0 )
+ nProducts = atoi((char *)vTokens->pArray[1]);
+ else if ( strcmp( (char *)vTokens->pArray[0], ".ilb" ) == 0 )
{
if ( vTokens->nSize - 1 != nInputs )
printf( "Warning: Mismatch between the number of PIs on the .i line (%d) and the number of PIs on the .ilb line (%d).\n", nInputs, vTokens->nSize - 1 );
for ( i = 1; i < vTokens->nSize; i++ )
- Io_ReadCreatePi( pNtk, vTokens->pArray[i] );
+ Io_ReadCreatePi( pNtk, (char *)vTokens->pArray[i] );
}
- else if ( strcmp( vTokens->pArray[0], ".ob" ) == 0 )
+ else if ( strcmp( (char *)vTokens->pArray[0], ".ob" ) == 0 )
{
if ( vTokens->nSize - 1 != nOutputs )
printf( "Warning: Mismatch between the number of POs on the .o line (%d) and the number of POs on the .ob line (%d).\n", nOutputs, vTokens->nSize - 1 );
for ( i = 1; i < vTokens->nSize; i++ )
- Io_ReadCreatePo( pNtk, vTokens->pArray[i] );
+ Io_ReadCreatePo( pNtk, (char *)vTokens->pArray[i] );
}
else
{
@@ -189,8 +192,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
Abc_NtkDelete( pNtk );
return NULL;
}
- pCubeIn = vTokens->pArray[0];
- pCubeOut = vTokens->pArray[1];
+ pCubeIn = (char *)vTokens->pArray[0];
+ pCubeOut = (char *)vTokens->pArray[1];
if ( strlen(pCubeIn) != (unsigned)nInputs )
{
printf( "%s (line %d): Input cube length (%zu) differs from the number of inputs (%d).\n",
@@ -211,8 +214,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
{
if ( pCubeOut[i] == '0' )
{
- Vec_StrAppend( ppSops[i], pCubeIn );
- Vec_StrAppend( ppSops[i], " 1\n" );
+ Vec_StrPrintStr( ppSops[i], pCubeIn );
+ Vec_StrPrintStr( ppSops[i], " 1\n" );
}
}
}
@@ -222,8 +225,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
{
if ( pCubeOut[i] == '1' )
{
- Vec_StrAppend( ppSops[i], pCubeIn );
- Vec_StrAppend( ppSops[i], " 1\n" );
+ Vec_StrPrintStr( ppSops[i], pCubeIn );
+ Vec_StrPrintStr( ppSops[i], " 1\n" );
}
}
}
@@ -242,12 +245,12 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
if ( ppSops[i]->nSize == 0 )
{
Abc_ObjRemoveFanins(pNode);
- pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 0\n" );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" );
Vec_StrFree( ppSops[i] );
continue;
}
Vec_StrPush( ppSops[i], 0 );
- pNode->pData = Abc_SopRegister( pNtk->pManFunc, ppSops[i]->pArray );
+ pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, ppSops[i]->pArray );
Vec_StrFree( ppSops[i] );
}
ABC_FREE( ppSops );
@@ -262,3 +265,5 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 9847c2da..94147745 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -19,12 +19,16 @@
***********************************************************************/
#include "ioAbc.h"
+#include "ver.h"
+
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+//extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -54,7 +58,7 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
// detect top-level model
RetValue = Abc_LibFindTopLevelModels( pDesign );
- pNtk = Vec_PtrEntry( pDesign->vTops, 0 );
+ pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
if ( RetValue > 1 )
printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
Vec_PtrSize(pDesign->vTops), pNtk->pName );
@@ -88,3 +92,5 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index c00c3008..a4dbf949 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -19,6 +19,10 @@
***********************************************************************/
#include "ioAbc.h"
+#include "main.h"
+
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -73,6 +77,8 @@ Io_FileType_t Io_ReadFileType( char * pFileName )
return IO_FILE_BLIFMV;
if ( !strcmp( pExt, "pla" ) )
return IO_FILE_PLA;
+ if ( !strcmp( pExt, "smv" ) )
+ return IO_FILE_SMV;
if ( !strcmp( pExt, "v" ) )
return IO_FILE_VERILOG;
return IO_FILE_UNKNOWN;
@@ -156,7 +162,56 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
return pNtk;
}
-
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t *temporaryLtlStore( Abc_Ntk_t *pNtk )
+{
+ Vec_Ptr_t *tempStore;
+ char *pFormula;
+ int i;
+
+ if( pNtk && Vec_PtrSize( pNtk->vLtlProperties ) > 0 )
+ {
+ tempStore = Vec_PtrAlloc( Vec_PtrSize( pNtk->vLtlProperties ) );
+ Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pFormula, i )
+ Vec_PtrPush( tempStore, pFormula );
+ assert( Vec_PtrSize( tempStore ) == Vec_PtrSize( pNtk->vLtlProperties ) );
+ return tempStore;
+ }
+ else
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void updateLtlStoreOfNtk( Abc_Ntk_t *pNtk, Vec_Ptr_t *tempLtlStore )
+{
+ int i;
+ char *pFormula;
+
+ assert( tempLtlStore != NULL );
+ Vec_PtrForEachEntry( char *, tempLtlStore, pFormula, i )
+ Vec_PtrPush( pNtk->vLtlProperties, pFormula );
+}
+
/**Function*************************************************************
Synopsis [Read the network from a file.]
@@ -171,8 +226,10 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck )
{
Abc_Ntk_t * pNtk, * pTemp;
+ Vec_Ptr_t * vLtl;
// get the netlist
pNtk = Io_ReadNetlist( pFileName, FileType, fCheck );
+ vLtl = temporaryLtlStore( pNtk );
if ( pNtk == NULL )
return NULL;
if ( !Abc_NtkIsNetlist(pNtk) )
@@ -217,6 +274,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck )
}
// convert the netlist into the logic network
pNtk = Abc_NtkToLogic( pTemp = pNtk );
+ if( vLtl )
+ updateLtlStoreOfNtk( pNtk, vLtl );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
@@ -331,6 +390,15 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
}
pNtkTemp = Abc_NtkToNetlistBench( pNtk );
}
+ else if ( FileType == IO_FILE_SMV )
+ {
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Writing traditional SMV is available for AIGs only.\n" );
+ return;
+ }
+ pNtkTemp = Abc_NtkToNetlistBench( pNtk );
+ }
else
pNtkTemp = Abc_NtkToNetlist( pNtk );
@@ -344,7 +412,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
{
if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
Abc_NtkToSop( pNtkTemp, 0 );
- Io_WriteBlif( pNtkTemp, pFileName, 1 );
+ Io_WriteBlif( pNtkTemp, pFileName, 1, 0, 0 );
}
else if ( FileType == IO_FILE_BLIFMV )
{
@@ -364,6 +432,8 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
Abc_NtkToAig( pNtkTemp );
Io_WriteEqn( pNtkTemp, pFileName );
}
+ else if ( FileType == IO_FILE_SMV )
+ Io_WriteSmv( pNtkTemp, pFileName );
else if ( FileType == IO_FILE_VERILOG )
{
if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
@@ -459,7 +529,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
{
if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
Abc_NtkToSop( pNtkResult, 0 );
- Io_WriteBlif( pNtkResult, pFileName, 1 );
+ Io_WriteBlif( pNtkResult, pFileName, 1, 0, 0 );
}
else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG )
{
@@ -611,7 +681,7 @@ Abc_Obj_t * Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv )
Abc_LatchSetInit0( pLatch );
// feed the latch with constant1- node
// pNode = Abc_NtkCreateNode( pNtk );
-// pNode->pData = Abc_SopRegister( pNtk->pManFunc, "2\n1\n" );
+// pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, "2\n1\n" );
pNode = Abc_NtkCreateNodeConst1( pNtk );
Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pNode );
return pLatch;
@@ -657,7 +727,7 @@ Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesI
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 )
+Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, int fConst1 )
{
Abc_Obj_t * pNet, * pTerm;
pTerm = fConst1? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
@@ -725,7 +795,6 @@ Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut
FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose )
{
char * t = 0, * c = 0, * i;
- extern char * Abc_FrameReadFlag( char * pFlag );
if ( PathVar == 0 )
{
@@ -768,3 +837,5 @@ FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mo
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 54db0641..3900cf26 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -21,12 +21,16 @@
// The code in this file is developed in collaboration with Mark Jarvin of Toronto.
+#include "bzlib.h"
#include "ioAbc.h"
#include <stdarg.h>
-#include "bzlib.h"
#include "zlib.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
#ifdef _WIN32
#define vsnprintf _vsnprintf
#endif
@@ -137,7 +141,7 @@ Binary Format Definition
static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj ) { return (unsigned)(ABC_PTRINT_T)pObj->pCopy; }
-static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (void *)(ABC_PTRINT_T)Num; }
+static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Num; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -451,7 +455,7 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
// write the nodes into the buffer
Pos = 0;
nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
- pBuffer = ABC_ALLOC( char, nBufferSize );
+ pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_AigForEachAnd( pNtk, pObj, i )
{
@@ -751,3 +755,5 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c
index 1154e218..a65115b3 100644
--- a/src/base/io/ioWriteBaf.c
+++ b/src/base/io/ioWriteBaf.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -126,9 +129,9 @@ void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName )
Abc_NtkCleanCopy( pNtk );
nNodes = 1;
Abc_NtkForEachCi( pNtk, pObj, i )
- pObj->pCopy = (void *)(ABC_PTRINT_T)nNodes++;
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)nNodes++;
Abc_AigForEachAnd( pNtk, pObj, i )
- pObj->pCopy = (void *)(ABC_PTRINT_T)nNodes++;
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)nNodes++;
// write the nodes into the buffer
nAnds = 0;
@@ -138,15 +141,15 @@ void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName )
Abc_AigForEachAnd( pNtk, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
- pBufferNode[nAnds++] = (((int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
- pBufferNode[nAnds++] = (((int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj);
+ pBufferNode[nAnds++] = (((int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | (int)Abc_ObjFaninC0(pObj);
+ pBufferNode[nAnds++] = (((int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy) << 1) | (int)Abc_ObjFaninC1(pObj);
}
// write the COs into the buffer
Abc_NtkForEachCo( pNtk, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
- pBufferNode[nAnds] = (((int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
+ pBufferNode[nAnds] = (((int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | (int)Abc_ObjFaninC0(pObj);
if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) )
pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((int)(ABC_PTRINT_T)Abc_ObjData(Abc_ObjFanout0(pObj)) & 3);
nAnds++;
@@ -166,3 +169,5 @@ void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteBblif.c b/src/base/io/ioWriteBblif.c
index e5bd6503..5cace190 100644
--- a/src/base/io/ioWriteBblif.c
+++ b/src/base/io/ioWriteBblif.c
@@ -21,6 +21,9 @@
#include "ioAbc.h"
#include "bblif.h"
+ABC_NAMESPACE_IMPL_START
+
+
// For description of Binary BLIF format, refer to "abc/src/aig/bbl/bblif.h"
////////////////////////////////////////////////////////////////////////
@@ -63,13 +66,13 @@ Bbl_Man_t * Bbl_ManFromAbc( Abc_Ntk_t * pNtk )
Abc_NtkForEachCi( pNtk, pObj, i )
Bbl_ManCreateObject( p, BBL_OBJ_CI, Abc_ObjId(pObj), 0, NULL );
// create internal nodes
- Vec_PtrForEachEntry( vNodes, pObj, i )
- Bbl_ManCreateObject( p, BBL_OBJ_NODE, Abc_ObjId(pObj), Abc_ObjFaninNum(pObj), pObj->pData );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ Bbl_ManCreateObject( p, BBL_OBJ_NODE, Abc_ObjId(pObj), Abc_ObjFaninNum(pObj), (char *)pObj->pData );
// create combinational outputs
Abc_NtkForEachCo( pNtk, pObj, i )
Bbl_ManCreateObject( p, BBL_OBJ_CO, Abc_ObjId(pObj), 1, NULL );
// create fanin/fanout connections for internal nodes
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
Abc_ObjForEachFanin( pObj, pFanin, k )
Bbl_ManAddFanin( p, Abc_ObjId(pObj), Abc_ObjId(pFanin) );
// create fanin/fanout connections for combinational outputs
@@ -109,3 +112,5 @@ void Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 147976da..4ca1ac0a 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -47,7 +50,7 @@ static int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t *
SeeAlso []
***********************************************************************/
-int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
+int Io_WriteBench( Abc_Ntk_t * pNtk, const char * pFileName )
{
Abc_Ntk_t * pExdc;
FILE * pFile;
@@ -258,8 +261,8 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
nFanins = Abc_ObjFaninNum(pNode);
assert( nFanins <= 8 );
// compute the truth table
- pTruth = Hop_ManConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
- if ( Hop_IsComplement(pNode->pData) )
+ pTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNode->pNtk->pManFunc, Hop_Regular((Hop_Obj_t *)pNode->pData), nFanins, vTruth, 0 );
+ if ( Hop_IsComplement((Hop_Obj_t *)pNode->pData) )
Extra_TruthNot( pTruth, pTruth, nFanins );
// consider simple cases
if ( Extra_TruthIsConst0(pTruth, nFanins) )
@@ -333,3 +336,5 @@ int Io_WriteBenchCheckNames( Abc_Ntk_t * pNtk )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index d1adaf90..7233161b 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -22,12 +22,15 @@
#include "main.h"
#include "mio.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
-static void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
+static void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches, int fBb2Wb, int fSeq );
+static void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches, int fBb2Wb, int fSeq );
static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
static void Io_NtkWriteSubckt( FILE * pFile, Abc_Obj_t * pNode );
@@ -62,7 +65,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
fprintf( stdout, "Writing BLIF has failed.\n" );
return;
}
- Io_WriteBlif( pNtkTemp, FileName, fWriteLatches );
+ Io_WriteBlif( pNtkTemp, FileName, fWriteLatches, 0, 0 );
Abc_NtkDelete( pNtkTemp );
}
@@ -77,7 +80,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
SeeAlso []
***********************************************************************/
-void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
+void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches, int fBb2Wb, int fSeq )
{
FILE * pFile;
Abc_Ntk_t * pNtkTemp;
@@ -92,18 +95,18 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
}
fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
// write the master network
- Io_NtkWrite( pFile, pNtk, fWriteLatches );
+ Io_NtkWrite( pFile, pNtk, fWriteLatches, fBb2Wb, fSeq );
// make sure there is no logic hierarchy
assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
// write the hierarchy if present
if ( Abc_NtkBlackboxNum(pNtk) > 0 )
{
- Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
+ Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNtkTemp, i )
{
if ( pNtkTemp == pNtk )
continue;
fprintf( pFile, "\n\n" );
- Io_NtkWrite( pFile, pNtkTemp, fWriteLatches );
+ Io_NtkWrite( pFile, pNtkTemp, fWriteLatches, fBb2Wb, fSeq );
}
}
fclose( pFile );
@@ -120,21 +123,21 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
SeeAlso []
***********************************************************************/
-void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
+void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches, int fBb2Wb, int fSeq )
{
Abc_Ntk_t * pExdc;
assert( Abc_NtkIsNetlist(pNtk) );
// write the model name
fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
// write the network
- Io_NtkWriteOne( pFile, pNtk, fWriteLatches );
+ Io_NtkWriteOne( pFile, pNtk, fWriteLatches, fBb2Wb, fSeq );
// write EXDC network if it exists
pExdc = Abc_NtkExdc( pNtk );
if ( pExdc )
{
fprintf( pFile, "\n" );
fprintf( pFile, ".exdc\n" );
- Io_NtkWriteOne( pFile, pExdc, fWriteLatches );
+ Io_NtkWriteOne( pFile, pExdc, fWriteLatches, fBb2Wb, fSeq );
}
// finalize the file
fprintf( pFile, ".end\n" );
@@ -148,10 +151,51 @@ void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
SideEffects []
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteConvertedBox( FILE * pFile, Abc_Ntk_t * pNtk, int fSeq )
+{
+ Abc_Obj_t * pObj;
+ int i, v;
+ if ( fSeq )
+ {
+ fprintf( pFile, ".attrib white box seq\n" );
+ }
+ else
+ {
+ fprintf( pFile, ".attrib white box comb\n" );
+ fprintf( pFile, ".delay 1\n" );
+ }
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ // write the .names line
+ fprintf( pFile, ".names" );
+ Io_NtkWritePis( pFile, pNtk, 1 );
+ if ( fSeq )
+ fprintf( pFile, " %s_in\n", Abc_ObjName(Abc_ObjFanin0(pObj)) );
+ else
+ fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanin0(pObj)) );
+ for ( v = 0; v < Abc_NtkPiNum(pNtk); v++ )
+ fprintf( pFile, "1" );
+ fprintf( pFile, " 1\n" );
+ if ( fSeq )
+ fprintf( pFile, ".latch %s_in %s 1\n", Abc_ObjName(Abc_ObjFanin0(pObj)), Abc_ObjName(Abc_ObjFanin0(pObj)) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write one network.]
+
+ Description []
+
+ SideEffects []
+
SeeAlso []
***********************************************************************/
-void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
+void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches, int fBb2Wb, int fSeq )
{
ProgressBar * pProgress;
Abc_Obj_t * pNode, * pLatch;
@@ -167,18 +211,13 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
Io_NtkWritePos( pFile, pNtk, fWriteLatches );
fprintf( pFile, "\n" );
- // write the assertions
- if ( Abc_NtkAssertNum(pNtk) )
- {
- fprintf( pFile, ".asserts" );
- Io_NtkWriteAsserts( pFile, pNtk );
- fprintf( pFile, "\n" );
- }
-
// write the blackbox
if ( Abc_NtkHasBlackbox( pNtk ) )
{
- fprintf( pFile, ".blackbox\n" );
+ if ( fBb2Wb )
+ Io_NtkWriteConvertedBox( pFile, pNtk, fSeq );
+ else
+ fprintf( pFile, ".blackbox\n" );
return;
}
@@ -205,7 +244,7 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
}
// write each internal node
- Length = Abc_NtkHasMapping(pNtk)? Mio_LibraryReadGateNameMax(pNtk->pManFunc) : 0;
+ Length = Abc_NtkHasMapping(pNtk)? Mio_LibraryReadGateNameMax((Mio_Library_t *)pNtk->pManFunc) : 0;
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
@@ -344,46 +383,6 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
/**Function*************************************************************
- Synopsis [Writes the assertion list.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pTerm, * pNet;
- int LineLength;
- int AddedLength;
- int NameCounter;
- int i;
-
- LineLength = 8;
- NameCounter = 0;
-
- Abc_NtkForEachAssert( pNtk, pTerm, i )
- {
- pNet = Abc_ObjFanin0(pTerm);
- // 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 []
@@ -395,7 +394,7 @@ void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk )
***********************************************************************/
void Io_NtkWriteSubckt( FILE * pFile, Abc_Obj_t * pNode )
{
- Abc_Ntk_t * pModel = pNode->pData;
+ Abc_Ntk_t * pModel = (Abc_Ntk_t *)pNode->pData;
Abc_Obj_t * pTerm;
int i;
// write the subcircuit
@@ -487,7 +486,7 @@ void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length )
***********************************************************************/
void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length )
{
- Mio_Gate_t * pGate = pNode->pData;
+ Mio_Gate_t * pGate = (Mio_Gate_t *)pNode->pData;
Mio_Pin_t * pGatePin;
int i;
// write the node
@@ -585,8 +584,52 @@ void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk )
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkConvertBb2Wb( char * pFileNameIn, char * pFileNameOut, int fSeq, int fVerbose )
+{
+ FILE * pFile;
+ Abc_Ntk_t * pNetlist;
+ // check the files
+ pFile = fopen( pFileNameIn, "rb" );
+ if ( pFile == NULL )
+ {
+ printf( "Input file \"%s\" cannot be opened.\n", pFileNameIn );
+ return;
+ }
+ fclose( pFile );
+ // check the files
+ pFile = fopen( pFileNameOut, "wb" );
+ if ( pFile == NULL )
+ {
+ printf( "Output file \"%s\" cannot be opened.\n", pFileNameOut );
+ return;
+ }
+ fclose( pFile );
+ // derive AIG for signal correspondence
+ pNetlist = Io_ReadNetlist( pFileNameIn, Io_ReadFileType(pFileNameIn), 1 );
+ if ( pNetlist == NULL )
+ {
+ printf( "Reading input file \"%s\" has failed.\n", pFileNameIn );
+ return;
+ }
+ Io_WriteBlif( pNetlist, pFileNameOut, 1, 1, fSeq );
+ Abc_NtkDelete( pNetlist );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c
index e1494475..62028606 100644
--- a/src/base/io/ioWriteBlifMv.c
+++ b/src/base/io/ioWriteBlifMv.c
@@ -22,6 +22,9 @@
#include "main.h"
#include "mio.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -72,7 +75,7 @@ void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName )
// write the remaining networks
if ( pNtk->pDesign )
{
- Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
+ Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNtkTemp, i )
{
if ( pNtkTemp == pNtk )
continue;
@@ -135,14 +138,6 @@ void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk )
Io_NtkWriteBlifMvPos( pFile, pNtk );
fprintf( pFile, "\n" );
- // write the assertions
- if ( Abc_NtkAssertNum(pNtk) )
- {
- fprintf( pFile, ".asserts" );
- Io_NtkWriteBlifMvAsserts( pFile, pNtk );
- fprintf( pFile, "\n" );
- }
-
// write the MV directives
fprintf( pFile, "\n" );
Abc_NtkForEachCi( pNtk, pTerm, i )
@@ -286,46 +281,6 @@ void Io_NtkWriteBlifMvPos( FILE * pFile, Abc_Ntk_t * pNtk )
/**Function*************************************************************
- Synopsis [Writes the assertion list.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Io_NtkWriteBlifMvAsserts( FILE * pFile, Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pTerm, * pNet;
- int LineLength;
- int AddedLength;
- int NameCounter;
- int i;
-
- LineLength = 8;
- NameCounter = 0;
-
- Abc_NtkForEachAssert( pNtk, pTerm, i )
- {
- pNet = Abc_ObjFanin0(pTerm);
- // 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 []
@@ -365,7 +320,7 @@ void Io_NtkWriteBlifMvLatch( FILE * pFile, Abc_Obj_t * pLatch )
***********************************************************************/
void Io_NtkWriteBlifMvSubckt( FILE * pFile, Abc_Obj_t * pNode )
{
- Abc_Ntk_t * pModel = pNode->pData;
+ Abc_Ntk_t * pModel = (Abc_Ntk_t *)pNode->pData;
Abc_Obj_t * pTerm;
int i;
// write the MV directives
@@ -436,7 +391,7 @@ void Io_NtkWriteBlifMvNode( FILE * pFile, Abc_Obj_t * pNode )
fprintf( pFile, "\n" );
// write the cubes
- pCur = Abc_ObjData(pNode);
+ pCur = (char *)Abc_ObjData(pNode);
if ( *pCur == 'd' )
{
fprintf( pFile, ".default " );
@@ -517,3 +472,5 @@ void Io_NtkWriteBlifMvNodeFanins( FILE * pFile, Abc_Obj_t * pNode )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteBook.c b/src/base/io/ioWriteBook.c
index 322c3ef4..9d0df473 100644
--- a/src/base/io/ioWriteBook.c
+++ b/src/base/io/ioWriteBook.c
@@ -21,6 +21,9 @@
#include "ioAbc.h"
#include "main.h"
#include "mio.h"
+
+ABC_NAMESPACE_IMPL_START
+
#define NODES 0
#define PL 1
#define coreHeight 1
@@ -33,8 +36,8 @@
static unsigned Io_NtkWriteNodes( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_NtkWritePiPoNodes( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, bool NodesOrPl );
-static unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, bool NodesOrPl );
+static void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, int NodesOrPl );
+static unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, int NodesOrPl );
static unsigned Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode );
static void Io_NtkWriteNets( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_NtkWriteIntNet( FILE * pFile, Abc_Obj_t * pNode );
@@ -42,13 +45,13 @@ static void Io_NtkBuildLayout( FILE * pFile1, FILE *pFile2, Abc_Ntk_t * pNtk, do
static void Io_NtkWriteScl( FILE * pFile, unsigned numCoreRows, double layoutWidth );
static void Io_NtkWritePl( FILE * pFile, Abc_Ntk_t * pNtk, unsigned numTerms, double layoutHeight, double layoutWidth );
static Vec_Ptr_t * Io_NtkOrderingPads( Abc_Ntk_t * pNtk, Vec_Ptr_t * vTerms );
-static Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pCurrEntry, unsigned numTerms, bool * pOrdered );
-static bool Abc_NodeIsNand2( Abc_Obj_t * pNode );
-static bool Abc_NodeIsNor2( Abc_Obj_t * pNode );
-static bool Abc_NodeIsAnd2( Abc_Obj_t * pNode );
-static bool Abc_NodeIsOr2( Abc_Obj_t * pNode );
-static bool Abc_NodeIsXor2( Abc_Obj_t * pNode );
-static bool Abc_NodeIsXnor2( Abc_Obj_t * pNode );
+static Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pCurrEntry, unsigned numTerms, int * pOrdered );
+static int Abc_NodeIsNand2( Abc_Obj_t * pNode );
+static int Abc_NodeIsNor2( Abc_Obj_t * pNode );
+static int Abc_NodeIsAnd2( Abc_Obj_t * pNode );
+static int Abc_NodeIsOr2( Abc_Obj_t * pNode );
+static int Abc_NodeIsXor2( Abc_Obj_t * pNode );
+static int Abc_NodeIsXnor2( Abc_Obj_t * pNode );
static inline double Abc_Rint( double x ) { return (double)(int)x; }
@@ -139,7 +142,7 @@ void Io_WriteBook( Abc_Ntk_t * pNtk, char * FileName )
// write the hierarchy if present
if ( Abc_NtkBlackboxNum(pNtk) > 0 )
{
- Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i )
+ Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNtkTemp, i )
{
if ( pNtkTemp == pNtk )
continue;
@@ -255,7 +258,7 @@ void Io_NtkWritePiPoNodes( FILE * pFile, Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, bool NodesOrPl )
+void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, int NodesOrPl )
{
Abc_Obj_t * pNetLi, * pNetLo;
@@ -278,7 +281,7 @@ void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, bool NodesOrPl )
SeeAlso []
***********************************************************************/
-unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, bool NodesOrPl )
+unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, int NodesOrPl )
{
unsigned sizex=0, sizey=coreHeight, isize=0;
//double nx, ny, xstep, ystep;
@@ -317,7 +320,7 @@ unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, bool NodesOrPl )
else
{
assert( isize > 2 );
- sizex=isize+Abc_SopGetCubeNum(pNode->pData);
+ sizex=isize+Abc_SopGetCubeNum((char *)pNode->pData);
}
}
}
@@ -370,7 +373,7 @@ unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, bool NodesOrPl )
***********************************************************************/
unsigned Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode )
{
- Mio_Gate_t * pGate = pNode->pData;
+ Mio_Gate_t * pGate = (Mio_Gate_t *)pNode->pData;
Mio_Pin_t * pGatePin;
int i;
// write the node gate
@@ -459,7 +462,7 @@ void Io_NtkWriteIntNet( FILE * pFile, Abc_Obj_t * pNet )
Abc_ObjForEachFanout( pFanin, pNeto, j )
fprintf( pFile, "%s_", Abc_ObjName(pNeto) );
if ( Abc_NtkHasMapping(pNet->pNtk) )
- fprintf( pFile, "%s : ", Mio_GateReadName(pFanin->pData) );
+ fprintf( pFile, "%s : ", Mio_GateReadName((Mio_Gate_t *)pFanin->pData) );
else
fprintf( pFile, "name I : " );
}
@@ -487,7 +490,7 @@ void Io_NtkWriteIntNet( FILE * pFile, Abc_Obj_t * pNet )
Abc_ObjForEachFanout( pFanout, pNeto, j )
fprintf( pFile, "%s_", Abc_ObjName(pNeto) );
if ( Abc_NtkHasMapping(pNet->pNtk) )
- fprintf( pFile, "%s : ", Mio_GateReadName(pFanout->pData) );
+ fprintf( pFile, "%s : ", Mio_GateReadName((Mio_Gate_t *)pFanout->pData) );
else
fprintf( pFile, "name O : " );
}
@@ -626,7 +629,7 @@ void Io_NtkWritePl( FILE * pFile, Abc_Ntk_t * pNtk, unsigned numTerms, double la
delta = layoutWidth / termsOnTop;
for(t = 0; t < termsOnTop; t++)
{
- pTerm = Vec_PtrEntry( vOrderedTerms, t );
+ pTerm = (Abc_Obj_t *)Vec_PtrEntry( vOrderedTerms, t );
if( Abc_ObjIsPi(pTerm) )
fprintf( pFile, "i%s_input\t\t", Abc_ObjName(Abc_ObjFanout0(pTerm)) );
else
@@ -642,7 +645,7 @@ void Io_NtkWritePl( FILE * pFile, Abc_Ntk_t * pNtk, unsigned numTerms, double la
delta = layoutWidth / termsOnBottom;
for(;t < termsOnTop+termsOnBottom; t++)
{
- pTerm = Vec_PtrEntry( vOrderedTerms, t );
+ pTerm = (Abc_Obj_t *)Vec_PtrEntry( vOrderedTerms, t );
if( Abc_ObjIsPi(pTerm) )
fprintf( pFile, "i%s_input\t\t", Abc_ObjName(Abc_ObjFanout0(pTerm)) );
else
@@ -658,7 +661,7 @@ void Io_NtkWritePl( FILE * pFile, Abc_Ntk_t * pNtk, unsigned numTerms, double la
delta = layoutHeight / termsOnLeft;
for(;t < termsOnTop+termsOnBottom+termsOnLeft; t++)
{
- pTerm = Vec_PtrEntry( vOrderedTerms, t );
+ pTerm = (Abc_Obj_t *)Vec_PtrEntry( vOrderedTerms, t );
if( Abc_ObjIsPi(pTerm) )
fprintf( pFile, "i%s_input\t\t", Abc_ObjName(Abc_ObjFanout0(pTerm)) );
else
@@ -674,7 +677,7 @@ void Io_NtkWritePl( FILE * pFile, Abc_Ntk_t * pNtk, unsigned numTerms, double la
delta = layoutHeight / termsOnRight;
for(;t < termsOnTop+termsOnBottom+termsOnLeft+termsOnRight; t++)
{
- pTerm = Vec_PtrEntry( vOrderedTerms, t );
+ pTerm = (Abc_Obj_t *)Vec_PtrEntry( vOrderedTerms, t );
if( Abc_ObjIsPi(pTerm) )
fprintf( pFile, "i%s_input\t\t", Abc_ObjName(Abc_ObjFanout0(pTerm)) );
else
@@ -715,8 +718,8 @@ Vec_Ptr_t * Io_NtkOrderingPads( Abc_Ntk_t * pNtk, Vec_Ptr_t * vTerms )
ProgressBar * pProgress;
unsigned numTerms=Vec_PtrSize(vTerms);
unsigned termIdx=0, termCount=0;
- bool * pOrdered = ABC_ALLOC(bool, numTerms);
- bool newNeighbor=1;
+ int * pOrdered = ABC_ALLOC(int, numTerms);
+ int newNeighbor=1;
Vec_Ptr_t * vOrderedTerms = Vec_PtrAlloc ( numTerms );
Abc_Obj_t * pNeighbor, * pNextTerm;
unsigned i;
@@ -724,13 +727,13 @@ Vec_Ptr_t * Io_NtkOrderingPads( Abc_Ntk_t * pNtk, Vec_Ptr_t * vTerms )
for( i=0 ; i<numTerms ; i++ )
pOrdered[i]=0;
- pNextTerm = Vec_PtrEntry(vTerms, termIdx++);
+ pNextTerm = (Abc_Obj_t *)Vec_PtrEntry(vTerms, termIdx++);
pProgress = Extra_ProgressBarStart( stdout, numTerms );
while( termCount < numTerms && termIdx < numTerms )
{
if( pOrdered[Abc_ObjId(pNextTerm)] && !newNeighbor )
{
- pNextTerm = Vec_PtrEntry( vTerms, termIdx++ );
+ pNextTerm = (Abc_Obj_t *)Vec_PtrEntry( vTerms, termIdx++ );
continue;
}
if(!Vec_PtrPushUnique( vOrderedTerms, pNextTerm ))
@@ -746,7 +749,7 @@ Vec_Ptr_t * Io_NtkOrderingPads( Abc_Ntk_t * pNtk, Vec_Ptr_t * vTerms )
pNextTerm=pNeighbor;
}
else if(termIdx < numTerms)
- pNextTerm = Vec_PtrEntry( vTerms, termIdx++ );
+ pNextTerm = (Abc_Obj_t *)Vec_PtrEntry( vTerms, termIdx++ );
Extra_ProgressBarUpdate( pProgress, termCount, NULL );
}
@@ -766,11 +769,11 @@ Vec_Ptr_t * Io_NtkOrderingPads( Abc_Ntk_t * pNtk, Vec_Ptr_t * vTerms )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pTerm, unsigned numTerms, bool * pOrdered )
+Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pTerm, unsigned numTerms, int * pOrdered )
{
Vec_Ptr_t * vNeighbors = Vec_PtrAlloc ( numTerms );
Abc_Obj_t * pNet, * pNode, * pNeighbor;
- bool foundNeighbor=0;
+ int foundNeighbor=0;
int i;
assert(Abc_ObjIsPi(pTerm) || Abc_ObjIsPo(pTerm) );
@@ -791,7 +794,7 @@ Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pTerm, unsigned numTerm
while ( Vec_PtrSize(vNeighbors) >0 )
{
- pNeighbor = Vec_PtrEntry( vNeighbors, 0 );
+ pNeighbor = (Abc_Obj_t *)Vec_PtrEntry( vNeighbors, 0 );
assert( Abc_ObjIsNode(pNeighbor) || Abc_ObjIsTerm(pNeighbor) );
Vec_PtrRemove( vNeighbors, pNeighbor );
@@ -836,7 +839,7 @@ Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pTerm, unsigned numTerm
SeeAlso []
***********************************************************************/
-bool Abc_NodeIsNand2( Abc_Obj_t * pNode )
+int Abc_NodeIsNand2( Abc_Obj_t * pNode )
{
Abc_Ntk_t * pNtk = pNode->pNtk;
assert( Abc_NtkIsNetlist(pNtk) );
@@ -844,11 +847,11 @@ bool Abc_NodeIsNand2( Abc_Obj_t * pNode )
if ( Abc_ObjFaninNum(pNode) != 2 )
return 0;
if ( Abc_NtkHasSop(pNtk) )
- return ( !strcmp((pNode->pData), "-0 1\n0- 1\n") ||
- !strcmp((pNode->pData), "0- 1\n-0 1\n") ||
- !strcmp((pNode->pData), "11 0\n") );
+ return ( !strcmp(((char *)pNode->pData), "-0 1\n0- 1\n") ||
+ !strcmp(((char *)pNode->pData), "0- 1\n-0 1\n") ||
+ !strcmp(((char *)pNode->pData), "11 0\n") );
if ( Abc_NtkHasMapping(pNtk) )
- return pNode->pData == Mio_LibraryReadNand2(Abc_FrameReadLibGen());
+ return pNode->pData == (void *)Mio_LibraryReadNand2((Mio_Library_t *)Abc_FrameReadLibGen());
assert( 0 );
return 0;
}
@@ -864,7 +867,7 @@ bool Abc_NodeIsNand2( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-bool Abc_NodeIsNor2( Abc_Obj_t * pNode )
+int Abc_NodeIsNor2( Abc_Obj_t * pNode )
{
Abc_Ntk_t * pNtk = pNode->pNtk;
assert( Abc_NtkIsNetlist(pNtk) );
@@ -872,7 +875,7 @@ bool Abc_NodeIsNor2( Abc_Obj_t * pNode )
if ( Abc_ObjFaninNum(pNode) != 2 )
return 0;
if ( Abc_NtkHasSop(pNtk) )
- return ( !strcmp((pNode->pData), "00 1\n") );
+ return ( !strcmp(((char *)pNode->pData), "00 1\n") );
assert( 0 );
return 0;
}
@@ -888,7 +891,7 @@ bool Abc_NodeIsNor2( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-bool Abc_NodeIsAnd2( Abc_Obj_t * pNode )
+int Abc_NodeIsAnd2( Abc_Obj_t * pNode )
{
Abc_Ntk_t * pNtk = pNode->pNtk;
assert( Abc_NtkIsNetlist(pNtk) );
@@ -896,9 +899,9 @@ bool Abc_NodeIsAnd2( Abc_Obj_t * pNode )
if ( Abc_ObjFaninNum(pNode) != 2 )
return 0;
if ( Abc_NtkHasSop(pNtk) )
- return Abc_SopIsAndType((pNode->pData));
+ return Abc_SopIsAndType(((char *)pNode->pData));
if ( Abc_NtkHasMapping(pNtk) )
- return pNode->pData == Mio_LibraryReadAnd2(Abc_FrameReadLibGen());
+ return pNode->pData == (void *)Mio_LibraryReadAnd2((Mio_Library_t *)Abc_FrameReadLibGen());
assert( 0 );
return 0;
}
@@ -914,7 +917,7 @@ bool Abc_NodeIsAnd2( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-bool Abc_NodeIsOr2( Abc_Obj_t * pNode )
+int Abc_NodeIsOr2( Abc_Obj_t * pNode )
{
Abc_Ntk_t * pNtk = pNode->pNtk;
assert( Abc_NtkIsNetlist(pNtk) );
@@ -922,10 +925,10 @@ bool Abc_NodeIsOr2( Abc_Obj_t * pNode )
if ( Abc_ObjFaninNum(pNode) != 2 )
return 0;
if ( Abc_NtkHasSop(pNtk) )
- return ( Abc_SopIsOrType((pNode->pData)) ||
- !strcmp((pNode->pData), "01 0\n") ||
- !strcmp((pNode->pData), "10 0\n") ||
- !strcmp((pNode->pData), "00 0\n") );
+ return ( Abc_SopIsOrType(((char *)pNode->pData)) ||
+ !strcmp(((char *)pNode->pData), "01 0\n") ||
+ !strcmp(((char *)pNode->pData), "10 0\n") ||
+ !strcmp(((char *)pNode->pData), "00 0\n") );
//off-sets, too
assert( 0 );
return 0;
@@ -942,7 +945,7 @@ bool Abc_NodeIsOr2( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-bool Abc_NodeIsXor2( Abc_Obj_t * pNode )
+int Abc_NodeIsXor2( Abc_Obj_t * pNode )
{
Abc_Ntk_t * pNtk = pNode->pNtk;
assert( Abc_NtkIsNetlist(pNtk) );
@@ -950,7 +953,7 @@ bool Abc_NodeIsXor2( Abc_Obj_t * pNode )
if ( Abc_ObjFaninNum(pNode) != 2 )
return 0;
if ( Abc_NtkHasSop(pNtk) )
- return ( !strcmp((pNode->pData), "01 1\n10 1\n") || !strcmp((pNode->pData), "10 1\n01 1\n") );
+ return ( !strcmp(((char *)pNode->pData), "01 1\n10 1\n") || !strcmp(((char *)pNode->pData), "10 1\n01 1\n") );
assert( 0 );
return 0;
}
@@ -966,7 +969,7 @@ bool Abc_NodeIsXor2( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-bool Abc_NodeIsXnor2( Abc_Obj_t * pNode )
+int Abc_NodeIsXnor2( Abc_Obj_t * pNode )
{
Abc_Ntk_t * pNtk = pNode->pNtk;
assert( Abc_NtkIsNetlist(pNtk) );
@@ -974,7 +977,7 @@ bool Abc_NodeIsXnor2( Abc_Obj_t * pNode )
if ( Abc_ObjFaninNum(pNode) != 2 )
return 0;
if ( Abc_NtkHasSop(pNtk) )
- return ( !strcmp((pNode->pData), "11 1\n00 1\n") || !strcmp((pNode->pData), "00 1\n11 1\n") );
+ return ( !strcmp(((char *)pNode->pData), "11 1\n00 1\n") || !strcmp(((char *)pNode->pData), "00 1\n11 1\n") );
assert( 0 );
return 0;
}
@@ -984,3 +987,5 @@ bool Abc_NodeIsXnor2( Abc_Obj_t * pNode )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 3df189d1..6cb82a0a 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -21,6 +21,9 @@
#include "ioAbc.h"
#include "satSolver.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -68,7 +71,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
if ( Abc_NtkIsLogic(pNtk) )
Abc_NtkToBdd( pNtk );
// create solver with clauses
- pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
+ pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
if ( pSat == NULL )
{
fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
@@ -113,3 +116,5 @@ void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 64be1425..c1b9befc 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -22,6 +22,9 @@
#include "main.h"
#include "mio.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -105,10 +108,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
}
// mark the nodes from the set
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
pNode->fMarkC = 1;
if ( vNodesShow )
- Vec_PtrForEachEntry( vNodesShow, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
pNode->fMarkB = 1;
// get the levels of nodes
@@ -117,7 +120,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
{
LevelMin = Abc_NtkLevelReverse( pNtk );
assert( LevelMax == LevelMin );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
if ( Abc_ObjIsNode(pNode) )
pNode->Level = LevelMax - pNode->Level + 1;
}
@@ -126,7 +129,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
LevelMin = 10000;
LevelMax = -1;
fHasCos = 0;
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( Abc_ObjIsCo(pNode) )
{
@@ -143,7 +146,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
if ( fHasCos )
{
LevelMax++;
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( Abc_ObjIsCo(pNode) )
pNode->Level = LevelMax;
@@ -247,7 +250,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMax );
// generate the PO nodes
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( !Abc_ObjIsCo(pNode) )
continue;
@@ -273,7 +276,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", Level );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( (int)pNode->Level != Level )
continue;
@@ -296,11 +299,11 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
if ( Abc_NtkIsStrash(pNtk) )
pSopString = "";
else if ( Abc_NtkHasMapping(pNtk) && fGateNames )
- pSopString = Mio_GateReadName(pNode->pData);
+ pSopString = Mio_GateReadName((Mio_Gate_t *)pNode->pData);
else if ( Abc_NtkHasMapping(pNtk) )
- pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
+ pSopString = Abc_NtkPrintSop(Mio_GateReadSop((Mio_Gate_t *)pNode->pData));
else
- pSopString = Abc_NtkPrintSop(pNode->pData);
+ pSopString = Abc_NtkPrintSop((char *)pNode->pData);
fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id,
// SuppSize,
@@ -324,7 +327,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMin );
// generate the PO nodes
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( !Abc_ObjIsCi(pNode) )
{
@@ -356,7 +359,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( (int)pNode->Level != LevelMax )
continue;
@@ -364,7 +367,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
}
// generate edges
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( Abc_ObjIsLatch(pNode) )
continue;
@@ -392,10 +395,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fclose( pFile );
// unmark the nodes from the set
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
pNode->fMarkC = 0;
if ( vNodesShow )
- Vec_PtrForEachEntry( vNodesShow, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
pNode->fMarkB = 0;
// convert the network back into BDDs if this is how it was
@@ -456,10 +459,10 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
}
// mark the nodes from the set
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
pNode->fMarkC = 1;
if ( vNodesShow )
- Vec_PtrForEachEntry( vNodesShow, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
pNode->fMarkB = 1;
// get the levels of nodes
@@ -468,7 +471,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
{
LevelMin = Abc_NtkLevelReverse( pNtk );
assert( LevelMax == LevelMin );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
if ( Abc_ObjIsNode(pNode) )
pNode->Level = LevelMax - pNode->Level + 1;
}
@@ -477,7 +480,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
LevelMin = 10000;
LevelMax = -1;
fHasCos = 0;
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( Abc_ObjIsCo(pNode) )
{
@@ -494,7 +497,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
if ( fHasCos )
{
LevelMax++;
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( Abc_ObjIsCo(pNode) )
pNode->Level = LevelMax;
@@ -598,7 +601,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMax );
// generate the PO nodes
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( !Abc_ObjIsPo(pNode) )
continue;
@@ -629,11 +632,11 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
if ( Abc_NtkIsStrash(pNtk) )
pSopString = "";
else if ( Abc_NtkHasMapping(pNtk) && fGateNames )
- pSopString = Mio_GateReadName(pNode->pData);
+ pSopString = Mio_GateReadName((Mio_Gate_t *)pNode->pData);
else if ( Abc_NtkHasMapping(pNtk) )
- pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
+ pSopString = Abc_NtkPrintSop(Mio_GateReadSop((Mio_Gate_t *)pNode->pData));
else
- pSopString = Abc_NtkPrintSop(pNode->pData);
+ pSopString = Abc_NtkPrintSop((char *)pNode->pData);
fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
fprintf( pFile, ", shape = ellipse" );
@@ -654,7 +657,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMin );
// generate the PO nodes
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( pNode->Level > 0 )
continue;
@@ -685,7 +688,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
}
// fprintf( pFile, "{\n" );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( !Abc_ObjIsLatch(pNode) )
continue;
@@ -702,7 +705,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" );
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( (int)pNode->Level != LevelMax )
continue;
@@ -712,7 +715,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
}
// generate edges
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
if ( Abc_ObjIsBi(pNode) || Abc_ObjIsBo(pNode) )
continue;
@@ -750,10 +753,10 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fclose( pFile );
// unmark the nodes from the set
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
pNode->fMarkC = 0;
if ( vNodesShow )
- Vec_PtrForEachEntry( vNodesShow, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodesShow, pNode, i )
pNode->fMarkB = 0;
// convert the network back into BDDs if this is how it was
@@ -807,7 +810,7 @@ int Abc_NtkCountLogicNodes( Vec_Ptr_t * vNodes )
{
Abc_Obj_t * pObj;
int i, Counter = 0;
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
if ( !Abc_ObjIsNode(pObj) )
continue;
@@ -823,3 +826,5 @@ int Abc_NtkCountLogicNodes( Vec_Ptr_t * vNodes )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c
index 228e4ae9..d3784187 100644
--- a/src/base/io/ioWriteEqn.c
+++ b/src/base/io/ioWriteEqn.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -108,9 +111,9 @@ void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, "%s = ", Abc_ObjName(Abc_ObjFanout0(pNode)) );
// set the input names
Abc_ObjForEachFanin( pNode, pFanin, k )
- Hop_IthVar(pNtk->pManFunc, k)->pData = Abc_ObjName(pFanin);
+ Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData = Abc_ObjName(pFanin);
// write the formula
- Hop_ObjPrintEqn( pFile, pNode->pData, vLevels, 0 );
+ Hop_ObjPrintEqn( pFile, (Hop_Obj_t *)pNode->pData, vLevels, 0 );
fprintf( pFile, ";\n" );
}
Extra_ProgressBarStop( pProgress );
@@ -250,3 +253,5 @@ int Io_NtkWriteEqnCheck( Abc_Ntk_t * pNtk )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteGml.c b/src/base/io/ioWriteGml.c
index d84e5f67..49a90d9c 100644
--- a/src/base/io/ioWriteGml.c
+++ b/src/base/io/ioWriteGml.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -114,3 +117,5 @@ void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c
index c06b39d7..22d0d1af 100644
--- a/src/base/io/ioWriteList.c
+++ b/src/base/io/ioWriteList.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
/*
-------- Original Message --------
Subject: Re: abc release and retiming
@@ -286,3 +289,5 @@ void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 93332793..ce6ee31f 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -20,6 +20,9 @@
#include "ioAbc.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -100,7 +103,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
nProducts++;
continue;
}
- nProducts += Abc_SopGetCubeNum(pDriver->pData);
+ nProducts += Abc_SopGetCubeNum((char *)pDriver->pData);
}
// collect the parameters
@@ -155,11 +158,11 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
}
// make sure the cover is not complemented
- assert( !Abc_SopIsComplement( pDriver->pData ) );
+ assert( !Abc_SopIsComplement( (char *)pDriver->pData ) );
// write the cubes
nFanins = Abc_ObjFaninNum(pDriver);
- Abc_SopForEachCube( pDriver->pData, nFanins, pCube )
+ Abc_SopForEachCube( (char *)pDriver->pData, nFanins, pCube )
{
Abc_ObjForEachFanin( pDriver, pFanin, k )
{
@@ -195,3 +198,5 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteSmv.c b/src/base/io/ioWriteSmv.c
new file mode 100644
index 00000000..c767bcaa
--- /dev/null
+++ b/src/base/io/ioWriteSmv.c
@@ -0,0 +1,265 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteSmv.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write the network in SMV format.]
+
+ Author [Satrajit Chatterjee]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteSmv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ioAbc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Io_WriteSmvCheckNames( Abc_Ntk_t * pNtk );
+
+static int Io_WriteSmvOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static int Io_WriteSmvOneNode( FILE * pFile, Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// This returns a pointer to a static area, so be careful in using results
+// of this function i.e. don't call this twice in the same printf call.
+//
+// This function replaces '|' with '_' I think abc introduces '|' when
+// flattening hierarchy. The '|' is interpreted as a or function by nusmv
+// which is unfortunate. This probably should be fixed elsewhere.
+static char *cleanUNSAFE( const char *s )
+{
+ char *t;
+ static char buffer[1024];
+ assert (strlen(s) < 1024);
+ strcpy(buffer, s);
+ for (t = buffer; *t != 0; ++t) *t = (*t == '|') ? '_' : *t;
+ return buffer;
+}
+
+static int hasPrefix(const char *needle, const char *haystack)
+{
+ return (strncmp(haystack, needle, strlen(needle)) == 0);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the network in SMV format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteSmv( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ Abc_Ntk_t * pExdc;
+ FILE * pFile;
+ assert( Abc_NtkIsSopNetlist(pNtk) );
+ if ( !Io_WriteSmvCheckNames(pNtk) )
+ {
+ fprintf( stdout, "Io_WriteSmv(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the SMV format. Use \"short_names\".\n" );
+ return 0;
+ }
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteSmv(): Cannot open the output file.\n" );
+ return 0;
+ }
+ fprintf( pFile, "-- benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+ // write the network
+ Io_WriteSmvOne( pFile, pNtk );
+ // write EXDC network if it exists
+ pExdc = Abc_NtkExdc( pNtk );
+ if ( pExdc )
+ printf( "Io_WriteSmv: EXDC is not written (warning).\n" );
+ // finalize the file
+ fclose( pFile );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the network in SMV format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteSmvOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ ProgressBar * pProgress;
+ Abc_Obj_t * pNode;
+ int i;
+
+ // write the PIs/POs/latches
+ fprintf( pFile, "MODULE main\n"); // nusmv needs top module to be main
+ fprintf ( pFile, "\n" );
+
+ fprintf( pFile, "VAR -- inputs\n");
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ fprintf( pFile, " %s : boolean;\n",
+ cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
+ fprintf ( pFile, "\n" );
+
+ fprintf( pFile, "VAR -- state variables\n");
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ fprintf( pFile, " %s : boolean;\n",
+ cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))) );
+ fprintf ( pFile, "\n" );
+
+ // No outputs needed for NuSMV:
+ // TODO: Add sepcs by recognizing assume_.* and assert_.*
+ //
+ // Abc_NtkForEachPo( pNtk, pNode, i )
+ // fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
+
+ // write internal nodes
+ fprintf( pFile, "DEFINE\n");
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Io_WriteSmvOneNode( pFile, pNode );
+ }
+ Extra_ProgressBarStop( pProgress );
+ fprintf ( pFile, "\n" );
+
+ fprintf( pFile, "ASSIGN\n");
+ Abc_NtkForEachLatch( pNtk, pNode, i )
+ {
+ int Reset = (int)(ABC_PTRUINT_T)Abc_ObjData( pNode );
+ assert (Reset >= 1);
+ assert (Reset <= 3);
+
+ if (Reset != 3)
+ {
+ fprintf( pFile, " init(%s) := %d;\n",
+ cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))),
+ Reset - 1);
+ }
+ fprintf( pFile, " next(%s) := ",
+ cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))) );
+ fprintf( pFile, "%s;\n",
+ cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode)))) );
+ }
+
+ fprintf ( pFile, "\n" );
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ {
+ const char *n = cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode)));
+ // fprintf( pFile, "-- output %s;\n", n );
+ if (hasPrefix("assume_fair_", n))
+ {
+ fprintf( pFile, "FAIRNESS %s;\n", n );
+ }
+ else if (hasPrefix("Assert_", n) ||
+ hasPrefix("assert_safety_", n))
+ {
+ fprintf( pFile, "INVARSPEC %s;\n", n );
+ }
+ else if (hasPrefix("assert_fair_", n))
+ {
+ fprintf( pFile, "LTLSPEC G F %s;\n", n );
+ }
+ }
+
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the network in SMV format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteSmvOneNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+ int nFanins;
+
+ assert( Abc_ObjIsNode(pNode) );
+ nFanins = Abc_ObjFaninNum(pNode);
+ if ( nFanins == 0 )
+ { // write the constant 1 node
+ assert( Abc_NodeIsConst1(pNode) );
+ fprintf( pFile, " %s", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode)) ) );
+ fprintf( pFile, " := 1;\n" );
+ }
+ else if ( nFanins == 1 )
+ { // write the interver/buffer
+ if ( Abc_NodeIsBuf(pNode) )
+ {
+ fprintf( pFile, " %s := ", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
+ fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) );
+ }
+ else
+ {
+ fprintf( pFile, " %s := !", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
+ fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) );
+ }
+ }
+ else
+ { // write the AND gate
+ fprintf( pFile, " %s", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
+ fprintf( pFile, " := %s & ", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) );
+ fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin1(pNode))) );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the names cannot be written into the bench file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_WriteSmvCheckNames( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj;
+ char * pName;
+ int i;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ for ( pName = Nm_ManFindNameById(pNtk->pManName, i); pName && *pName; pName++ )
+ if ( *pName == '(' || *pName == ')' )
+ return 0;
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index f2ac1b1d..7f9bee95 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -22,6 +22,9 @@
#include "main.h"
#include "mio.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -80,7 +83,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
// write the network first
Io_WriteVerilogInt( pFile, pNtk );
// write other things
- Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNetlist, i )
+ Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNetlist, i )
{
assert( Abc_NtkIsNetlist(pNetlist) );
if ( pNetlist == pNtk )
@@ -495,7 +498,7 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
{
if ( Abc_ObjIsLatch(pObj) )
continue;
- pNtkBox = pObj->pData;
+ pNtkBox = (Abc_Ntk_t *)pObj->pData;
fprintf( pFile, " %s box%0*d", pNtkBox->pName, nDigits, Counter++ );
fprintf( pFile, "(" );
Abc_NtkForEachPi( pNtkBox, pTerm, k )
@@ -513,12 +516,12 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
// write nodes
if ( Abc_NtkHasMapping(pNtk) )
{
- Length = Mio_LibraryReadGateNameMax(pNtk->pManFunc);
+ Length = Mio_LibraryReadGateNameMax((Mio_Library_t *)pNtk->pManFunc);
nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
Counter = 0;
Abc_NtkForEachNode( pNtk, pObj, k )
{
- Mio_Gate_t * pGate = pObj->pData;
+ Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
Mio_Pin_t * pGatePin;
// write the node
fprintf( pFile, " %-*s g%0*d", Length, Mio_GateReadName(pGate), nDigits, Counter++ );
@@ -539,17 +542,17 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
vLevels = Vec_VecAlloc( 10 );
Abc_NtkForEachNode( pNtk, pObj, i )
{
- pFunc = pObj->pData;
+ pFunc = (Hop_Obj_t *)pObj->pData;
fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
// set the input names
Abc_ObjForEachFanin( pObj, pFanin, k )
- Hop_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin)));
+ Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin)));
// write the formula
Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
fprintf( pFile, ";\n" );
// clear the input names
Abc_ObjForEachFanin( pObj, pFanin, k )
- ABC_FREE( Hop_IthVar(pNtk->pManFunc, k)->pData );
+ ABC_FREE( Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData );
}
Vec_VecFree( vLevels );
}
@@ -637,3 +640,5 @@ char * Io_WriteVerilogGetName( char * pName )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 993bd7d2..dee459da 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -25,4 +25,5 @@ SRC += src/base/io/io.c \
src/base/io/ioWriteGml.c \
src/base/io/ioWriteList.c \
src/base/io/ioWritePla.c \
- src/base/io/ioWriteVerilog.c
+ src/base/io/ioWriteVerilog.c \
+ src/base/io/ioWriteSmv.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-11 19:43:41 +0000