diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1fb12e7f1..6cc8df18f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42600,7 +42600,7 @@ usage: SeeAlso [] ***********************************************************************/ -static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus ) +static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus ) { FILE * pFile; Gia_Man_t * pGia; @@ -42631,14 +42631,20 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu fVerilog = fSystemVerilog || Extra_FileIsType( pFileName, ".v", NULL, NULL ); if ( fVerilog ) { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = NULL; char pCommand[2000]; int RetValue; + int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL ); // Save the original filename before changing it pOrigFileName = pFileName; snprintf( pCommand, sizeof(pCommand), - "yosys -qp \"read_verilog %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"", + "yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols _temp_.aig\"", pDefines ? "-D" : "", pDefines ? pDefines : "", - fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" ); + (fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName, + pFileName2 ? " " : "", pFileName2 ? pFileName2 : "", + pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", + pFileName2 ? "delete t:\\$scopeinfo; " : "" ); #if defined(__wasm) RetValue = 1; #else @@ -42649,10 +42655,32 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand ); return NULL; } - pFileName = "_temp_.aig"; + if ( pFileName2 ) + { + Abc_Ntk_t * pNtk = Io_Read( "_temp_.aig", IO_FILE_AIGER, 1, 0 ); + if ( pNtk == NULL ) + { + Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", "_temp_.aig" ); + return NULL; + } + pAig = Abc_NtkToDar( pNtk, 0, 1 ); + Abc_NtkDelete( pNtk ); + if ( pAig == NULL ) + { + Abc_Print( -1, "Converting the AIGER network into an internal AIG has failed.\n" ); + return NULL; + } + pGia = Gia_ManFromAig( pAig ); + Aig_ManStop( pAig ); + } + else + { + pFileName = "_temp_.aig"; + pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); + } } - - pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); + else + pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName ); @@ -42684,13 +42712,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars ); Cec_ParCec_t ParsCec, * pPars = &ParsCec; + FILE * pFile; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; - char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL; + char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL, * pFileName2 = NULL; int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0; int Abc_ReadAigerOrVerilogFileStatus = 0; Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDnmdbasxytvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDFnmdbasxytvwh" ) ) != EOF ) { switch ( c ) { @@ -42734,6 +42763,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) pDefines = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + pFileName2 = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'n': pPars->fNaive ^= 1; break; @@ -42778,6 +42816,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 0, "It looks like the current AIG is derived by &st -m. Such AIG contains XOR gates and cannot be verified before &st is applied.\n" ); return 1; } + if ( pFileName2 ) + { + if ( (pFile = fopen( pFileName2, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\".\n", pFileName2 ); + return 1; + } + fclose( pFile ); + } pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; if ( fMiter ) @@ -42855,7 +42902,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) int n; for ( n = 0; n < 2; n++ ) { - pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); + pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[n] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } @@ -42891,7 +42938,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } FileName = pAbc->pGia->pSpec; } - pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); + pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[1] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } @@ -43003,12 +43050,13 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-nmdbasxytvwh]\n" ); + Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-F str] [-nmdbasxytvwh]\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-M str : top module name if Verilog file(s) are used [default = \"not used\"]\n" ); Abc_Print( -2, "\t-D str : defines to be used by Yosys for Verilog files [default = \"not used\"]\n" ); + Abc_Print( -2, "\t-F str : second Verilog/SystemVerilog file read together with each Verilog input [default = \"not used\"]\n" ); Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index 1b76fab8f..2436932cd 100644 --- a/src/base/wln/wlnCom.c +++ b/src/base/wln/wlnCom.c @@ -93,11 +93,12 @@ void Wln_End( Abc_Frame_t * pAbc ) int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ); - extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); + extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ); FILE * pFile; char * pFileName = NULL; + char * pFileName2= NULL; char * pTopModule= NULL; char * pDefines = NULL; char * pLibrary = NULL; @@ -111,7 +112,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSetUndef = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLbdisumlcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLFbdisumlcvh" ) ) != EOF ) { switch ( c ) { @@ -151,6 +152,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) pLibrary = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + pFileName2 = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'b': fBlast ^= 1; break; @@ -200,10 +210,24 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } fclose( pFile ); + if ( pFileName2 ) + { + if ( (pFile = fopen( pFileName2, "r" )) == NULL ) + { + Abc_Print( 1, "Cannot open input file \"%s\".\n", pFileName2 ); + return 0; + } + fclose( pFile ); + } // perform reading if ( pLibrary ) { + if ( pFileName2 ) + { + Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); + return 0; + } Abc_Ntk_t * pNtk = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose ); @@ -220,11 +244,18 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pNew = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + { + if ( pFileName2 ) + { + Abc_Print( 1, "Command line switch \"-F\" is only supported when the main input is Verilog/SystemVerilog.\n" ); + return 0; + } + pNew = Wln_BlastSystemVerilog( pFileName, NULL, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + } else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); @@ -234,6 +265,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { + if ( pFileName2 ) + { + Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); + return 0; + } Rtl_Lib_t * pLib = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); @@ -250,12 +286,13 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) } return 0; usage: - Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-bdisumlcvh] \n" ); + Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-F ] [-bdisumlcvh] \n" ); Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" ); Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" ); Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" ); Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" ); Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" ); + Abc_Print( -2, "\t-F : specify a second Verilog/SystemVerilog file for the default bit-blasting flow (default \"not used\")\n" ); Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" ); Abc_Print( -2, "\t-d : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" ); diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index 5b9f05c45..ffe8e457d 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -19,6 +19,9 @@ ***********************************************************************/ #include "wln.h" +#include "aig/aig/aig.h" +#include "aig/gia/giaAig.h" +#include "base/io/ioAbc.h" #include "base/main/main.h" #ifdef WIN32 @@ -171,30 +174,54 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p unlink( pFileTemp ); return pNtk; } -Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) +Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) { Gia_Man_t * pGia = NULL; char Command[1000]; char * pFileTemp = "_temp_.aig"; int fRtlil = strstr(pFileName, ".rtl") != NULL; - int fSVlog = strstr(pFileName, ".sv") != NULL; - sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols %s\"", + int fSVlog = strstr(pFileName, ".sv") != NULL || (pFileName2 && strstr(pFileName2, ".sv") != NULL); + sprintf( Command, "%s -qp \"%s %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", Wln_GetYosysName(), fRtlil ? "read_rtlil" : "read_verilog", pDefines ? "-D" : "", pDefines ? pDefines : "", fSVlog ? "-sv " : "", pFileName, + pFileName2 ? " " : "", + pFileName2 ? pFileName2 : "", pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "", fSetUndef ? "setundef -init -zero; " : "", + pFileName2 ? "delete t:\\$scopeinfo; " : "", pFileTemp ); if ( fVerbose ) printf( "%s\n", Command ); if ( !Wln_ConvertToRtl(Command, pFileTemp) ) return NULL; - pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 ); + if ( pFileName2 ) + { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = NULL; + Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); + if ( pNtk == NULL ) + { + printf( "Reading AIGER from file \"%s\" has failed.\n", pFileTemp ); + return NULL; + } + pAig = Abc_NtkToDar( pNtk, 0, 1 ); + Abc_NtkDelete( pNtk ); + if ( pAig == NULL ) + { + printf( "Converting the AIGER network into an internal AIG has failed.\n" ); + return NULL; + } + pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig); + Aig_ManStop( pAig ); + } + else + pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 ); if ( pGia == NULL ) { printf( "Converting to AIG has failed.\n" );