mirror of https://github.com/YosysHQ/abc.git
Add support for second Verilog files in %ysoys and &cec
This commit is contained in:
Alan Mishchenko
parent
6aaf0db1e1
commit
b8059c310a
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -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 <module>] [-D <defines>] [-L <liberty_file>] [-bdisumlcvh] <file_name>\n" );
|
||||
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name>\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" );
|
||||
|
|
|
|||
|
|
@ -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" );
|
||||
|
|
|
|||
Loading…
Reference in New Issue