luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Updating interface of &cec.

This commit is contained in:
Alan Mishchenko 2026-02-24 14:59:13 -08:00
parent ea6be8a51c
commit ef54c1daea
1 changed files with 20 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/base/abci/abc.c
View File

@ -35189,7 +35189,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
// Check if we should write LUT-based Verilog // Check if we should write LUT-based Verilog
if ( fUseLuts || (Gia_ManHasMapping(pAbc->pGia) && !fUseGates) ) if ( fUseLuts )
{ {
if ( !Gia_ManHasMapping(pAbc->pGia) ) if ( !Gia_ManHasMapping(pAbc->pGia) )
{ {
@ -35232,7 +35232,6 @@ usage:
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the file name\n"); Abc_Print( -2, "\t<file> : the file name\n");
Abc_Print( -2, "\tNote: When AIG is mapped and -l is not specified, LUT-based output is automatically used.\n");
return 1; return 1;
} }
@ -42601,7 +42600,7 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, int * pAbc_ReadAigerOrVerilogFileStatus ) static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus )
{ {
FILE * pFile; FILE * pFile;
Gia_Man_t * pGia; Gia_Man_t * pGia;
@ -42637,7 +42636,8 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu
// Save the original filename before changing it // Save the original filename before changing it
pOrigFileName = pFileName; pOrigFileName = pFileName;
snprintf( pCommand, sizeof(pCommand), snprintf( pCommand, sizeof(pCommand),
"yosys -qp \"read_verilog %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; 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\"",
pDefines ? "-D" : "", pDefines ? pDefines : "",
fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" ); fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" );
#if defined(__wasm) #if defined(__wasm)
RetValue = 1; RetValue = 1;
@ -42685,12 +42685,12 @@ 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 ); extern void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars );
Cec_ParCec_t ParsCec, * pPars = &ParsCec; Cec_ParCec_t ParsCec, * pPars = &ParsCec;
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
char ** pArgvNew, * pTopModule = NULL; char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL;
int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0; int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0;
int Abc_ReadAigerOrVerilogFileStatus = 0; int Abc_ReadAigerOrVerilogFileStatus = 0;
Cec_ManCecSetDefaultParams( pPars ); Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTMnmdbasxytvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDnmdbasxytvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -42725,6 +42725,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
pTopModule = argv[globalUtilOptind]; pTopModule = argv[globalUtilOptind];
globalUtilOptind++; globalUtilOptind++;
break; break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by defines.\n" );
goto usage;
}
pDefines = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'n': case 'n':
pPars->fNaive ^= 1; pPars->fNaive ^= 1;
break; break;
@ -42846,7 +42855,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
int n; int n;
for ( n = 0; n < 2; n++ ) for ( n = 0; n < 2; n++ )
{ {
pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, &Abc_ReadAigerOrVerilogFileStatus ); pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
if ( pGias[n] == NULL ) if ( pGias[n] == NULL )
return Abc_ReadAigerOrVerilogFileStatus; return Abc_ReadAigerOrVerilogFileStatus;
} }
@ -42882,7 +42891,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
FileName = pAbc->pGia->pSpec; FileName = pAbc->pGia->pSpec;
} }
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, &Abc_ReadAigerOrVerilogFileStatus ); pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
if ( pGias[1] == NULL ) if ( pGias[1] == NULL )
return Abc_ReadAigerOrVerilogFileStatus; return Abc_ReadAigerOrVerilogFileStatus;
} }
@ -42994,11 +43003,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-nmdbasxytvwh]\n" ); Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-nmdbasxytvwh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\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-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-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 = %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-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); 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-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"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");