From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- src/base/io/io.c | 279 ++++++++++++++++++++++++++----- src/base/io/ioAbc.h | 26 ++- src/base/io/ioInt.h | 8 + src/base/io/ioReadAiger.c | 27 +-- src/base/io/ioReadBaf.c | 15 +- src/base/io/ioReadBblif.c | 15 +- src/base/io/ioReadBench.c | 61 +++---- src/base/io/ioReadBlif.c | 113 +++++++------ src/base/io/ioReadBlifAig.c | 77 +++++---- src/base/io/ioReadBlifMv.c | 380 +++++++++++++++++++++++++++++++++---------- src/base/io/ioReadDsd.c | 13 +- src/base/io/ioReadEdif.c | 103 ++++++------ src/base/io/ioReadEqn.c | 31 ++-- src/base/io/ioReadPla.c | 45 ++--- src/base/io/ioReadVerilog.c | 10 +- src/base/io/ioUtil.c | 83 +++++++++- src/base/io/ioWriteAiger.c | 12 +- src/base/io/ioWriteBaf.c | 15 +- src/base/io/ioWriteBblif.c | 11 +- src/base/io/ioWriteBench.c | 11 +- src/base/io/ioWriteBlif.c | 169 ++++++++++++------- src/base/io/ioWriteBlifMv.c | 59 +------ src/base/io/ioWriteBook.c | 99 +++++------ src/base/io/ioWriteCnf.c | 7 +- src/base/io/ioWriteDot.c | 67 ++++---- src/base/io/ioWriteEqn.c | 9 +- src/base/io/ioWriteGml.c | 5 + src/base/io/ioWriteList.c | 5 + src/base/io/ioWritePla.c | 11 +- src/base/io/ioWriteSmv.c | 265 ++++++++++++++++++++++++++++++ src/base/io/ioWriteVerilog.c | 19 ++- src/base/io/module.make | 3 +- 32 files changed, 1461 insertions(+), 592 deletions(-) create mode 100644 src/base/io/ioWriteSmv.c (limited to 'src/base/io') 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] \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] \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] \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] \n" ); - fprintf( pAbc->Err, "\t read the network in binary BLIF format\n" ); + fprintf( pAbc->Err, "usage: read_blif [-nach] \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] \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] \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] \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] \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] \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] \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] \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] \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" ); @@ -1159,6 +1194,65 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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] \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 [] @@ -1322,7 +1416,7 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) usage: fprintf( pAbc->Err, "usage: write_aiger [-sch] \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] \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] \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] \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] \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] \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] [-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] \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] \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] \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] \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] \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] \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] \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] \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] \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 ] [-Q ] \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] \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] \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,13 +950,80 @@ 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; ipResetLatch == 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,17 +1081,92 @@ 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 ); } return 1; } +/**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.] @@ -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 -#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,26 +123,67 @@ 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" ); } +/**Function************************************************************* + + Synopsis [Write one network.] + + Description [] + + 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.] @@ -151,7 +195,7 @@ void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches ) 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 ) { @@ -342,46 +381,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.] @@ -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 ) @@ -284,46 +279,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.] @@ -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 ; i0 ) { - 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 -- cgit v1.2.3