From b8059c310a6aa32fe70f49e04d640f099d87fee8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 27 Mar 2026 19:24:31 -0700 Subject: [PATCH 1/5] Add support for second Verilog files in %ysoys and &cec --- src/base/abci/abc.c | 70 ++++++++++++++++++++++++++++++++++++------- src/base/wln/wlnCom.c | 49 ++++++++++++++++++++++++++---- src/base/wln/wlnRtl.c | 35 +++++++++++++++++++--- 3 files changed, 133 insertions(+), 21 deletions(-) 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" ); From bef23270f8ad9c8d2c14f6e6adc4a15fc2ba047f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 27 Mar 2026 20:09:54 -0700 Subject: [PATCH 2/5] Improvements to command "history". --- src/base/cmd/cmd.c | 44 ++++++++++++++++++----------------- src/base/cmd/cmdUtils.c | 50 ++++++++++++++++++++++++++++++++++++---- src/base/main/mainReal.c | 7 ++++++ 3 files changed, 75 insertions(+), 26 deletions(-) diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index bbe3b7d8e..aae2f47d8 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -98,6 +98,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "quit", CmdCommandQuit, 0 ); Cmd_CommandAdd( pAbc, "Basic", "abcrc", CmdCommandAbcrc, 0 ); Cmd_CommandAdd( pAbc, "Basic", "history", CmdCommandHistory, 0 ); + Cmd_CommandAdd( pAbc, "Basic", "hi", CmdCommandHistory, 0 ); Cmd_CommandAdd( pAbc, "Basic", "alias", CmdCommandAlias, 0 ); Cmd_CommandAdd( pAbc, "Basic", "unalias", CmdCommandUnalias, 0 ); Cmd_CommandAdd( pAbc, "Basic", "help", CmdCommandHelp, 0 ); @@ -441,38 +442,31 @@ int CmdCommandAbcrc( Abc_Frame_t * pAbc, int argc, char **argv ) int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pName, * pStr = NULL; - int i, c; + char ** ppMatches = NULL; + int * pIds = NULL; + int i; int nPrints = 20; int nPrinted = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) - { - switch ( c ) - { - case 'h': - goto usage; - default : - goto usage; - } - } - if ( argc > globalUtilOptind + 2 ) + if ( argc == 2 && !strcmp(argv[1], "-h") ) + goto usage; + if ( argc > 3 ) goto usage; // parse arguments: can be [substring] [number] in either order - if ( argc == globalUtilOptind + 1 ) + if ( argc == 2 ) { // one argument: either number or substring - pStr = argv[globalUtilOptind]; + pStr = argv[1]; if ( pStr && pStr[0] >= '1' && pStr[0] <= '9' ) { nPrints = atoi(pStr); pStr = NULL; } } - else if ( argc == globalUtilOptind + 2 ) + else if ( argc == 3 ) { // two arguments: substring and number - char * arg1 = argv[globalUtilOptind]; - char * arg2 = argv[globalUtilOptind + 1]; + char * arg1 = argv[1]; + char * arg2 = argv[2]; // Try to parse second argument as number if ( arg2[0] >= '1' && arg2[0] <= '9' ) @@ -500,14 +494,22 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) fprintf( pAbc->Out, "%4d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); } else { - // Search string provided, show up to nPrints matching entries - Vec_PtrForEachEntry( char *, pAbc->aHistory, pName, i ) + // Search string provided, select up to nPrints most recent matching entries + ppMatches = ABC_ALLOC( char *, nPrints ); + pIds = ABC_ALLOC( int, nPrints ); + Vec_PtrForEachEntryReverse( char *, pAbc->aHistory, pName, i ) if ( strstr(pName, pStr) ) { - fprintf( pAbc->Out, "%4d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); + pIds[nPrinted] = Vec_PtrSize(pAbc->aHistory)-i; + ppMatches[nPrinted] = pName; if ( ++nPrinted >= nPrints ) break; } + // Print the selected entries in reverse so larger history indices appear first + for ( i = nPrinted - 1; i >= 0; i-- ) + fprintf( pAbc->Out, "%4d : %s\n", pIds[i], ppMatches[i] ); + ABC_FREE( pIds ); + ABC_FREE( ppMatches ); } return 0; diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index e8e28078f..f0d8fc2dd 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -25,7 +25,6 @@ #include ABC_NAMESPACE_IMPL_START - // proper declaration of isspace //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -393,9 +392,51 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop ) ***********************************************************************/ char * CmdHistorySubstitution( Abc_Frame_t * pAbc, char *line, int *changed ) { - // as of today, no history substitution - *changed = 0; - return line; + char * pBeg = line, * pEnd, * pStr; + int iRecall, nSize; + while ( *pBeg && isspace((unsigned char)*pBeg) ) + pBeg++; + if ( *pBeg == 0 ) + { + *changed = 0; + return line; + } + pEnd = pBeg; + while ( *pEnd && !isspace((unsigned char)*pEnd) ) + pEnd++; + if ( *pEnd ) + { + char * pTemp = pEnd; + while ( *pTemp && isspace((unsigned char)*pTemp) ) + pTemp++; + if ( *pTemp ) + { + *changed = 0; + return line; + } + } + if ( *pBeg < '1' || *pBeg > '9' ) + { + *changed = 0; + return line; + } + for ( pStr = pBeg; pStr < pEnd; pStr++ ) + if ( *pStr < '0' || *pStr > '9' ) + { + *changed = 0; + return line; + } + iRecall = atoi( pBeg ); + nSize = Vec_PtrSize( pAbc->aHistory ); + if ( iRecall < 1 || iRecall > nSize ) + { + fprintf( pAbc->Err, "History entry %d does not exist.\n", iRecall ); + line[0] = 0; + *changed = 0; + return line; + } + *changed = 1; + return (char *)Vec_PtrEntry( pAbc->aHistory, nSize - iRecall ); } /**Function************************************************************* @@ -905,4 +946,3 @@ void Cmd_CommandSGen( Abc_Frame_t * pAbc, int nParts, int nIters, int fVerbose ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index 3c5d67b3f..9589d5239 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -56,6 +56,7 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS. #endif #include "base/abc/abc.h" +#include "base/cmd/cmdInt.h" #include "mainInt.h" #include "base/wlc/wlc.h" @@ -363,9 +364,15 @@ int Abc_RealMain( int argc, char * argv[] ) // execute commands given by the user while ( !feof(stdin) ) { + int did_subst; // print command line prompt and // get the command from the user sCommand = Abc_UtilsGetUsersInput( pAbc ); + sCommand = CmdHistorySubstitution( pAbc, sCommand, &did_subst ); + if ( sCommand == NULL ) + break; + if ( did_subst ) + fprintf( pAbc->Out, "%s\n", sCommand ); // execute the user's command fStatus = Cmd_CommandExecute( pAbc, sCommand ); From cd2998b5c75a8cb7e14e5ce9f71b538e69896910 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 Apr 2026 21:18:41 -0700 Subject: [PATCH 3/5] Adding name-based input reordering in &cec. --- src/aig/gia/giaGen.c | 4 +- src/base/abci/abc.c | 92 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 94 insertions(+), 2 deletions(-) diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c index c22cb21f8..426409c70 100644 --- a/src/aig/gia/giaGen.c +++ b/src/aig/gia/giaGen.c @@ -1480,10 +1480,10 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, for ( k = 1; k < nVars; k++ ) if ( pStore[i][k] >= 0 ) Gia_ManGenPrefix( p, &pLits[2*k], &pLits[2*k+1], pLits[2*pStore[i][k]], pLits[2*pStore[i][k]+1] ); - for ( k = 0; k < nVars; k++ ) - Gia_ManAppendCo( p, k ? Gia_ManHashXor(p, pLitsI[2*k], pLits[2*(k-1)+1]) : pLitsI[2*k] ); if ( fCarries ) Gia_ManAppendCo( p, pLits[2*(k-1)+1] ); + for ( k = 0; k < nVars; k++ ) + Gia_ManAppendCo( p, k ? Gia_ManHashXor(p, pLitsI[2*k], pLits[2*(k-1)+1]) : pLitsI[2*k] ); ABC_FREE( pStore ); ABC_FREE( pLitsI ); ABC_FREE( pLits ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6cc8df18f..e31b15da4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42589,6 +42589,86 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Vec_Ptr_t * Abc_GiaDupNameVec( Vec_Ptr_t * vNames ) +{ + Vec_Ptr_t * vNew; + char * pName; + int i; + if ( vNames == NULL ) + return NULL; + vNew = Vec_PtrAlloc( Vec_PtrSize(vNames) ); + Vec_PtrForEachEntry( char *, vNames, pName, i ) + Vec_PtrPush( vNew, pName ? Abc_UtilStrsav(pName) : NULL ); + return vNew; +} + +static Gia_Man_t * Abc_GiaReorderInputsByName( Gia_Man_t * pFirst, Gia_Man_t * pSecond ) +{ + Vec_Int_t * vPiPerm; + Gia_Man_t * pNew; + char * pName1, * pName2; + int * pUsed; + int i, k, nPis, fDiff = 0; + if ( pFirst == NULL || pSecond == NULL || pFirst->vNamesIn == NULL || pSecond->vNamesIn == NULL ) + return NULL; + nPis = Gia_ManPiNum( pFirst ); + if ( nPis != Gia_ManPiNum(pSecond) ) + return NULL; + if ( Vec_PtrSize(pFirst->vNamesIn) < nPis || Vec_PtrSize(pSecond->vNamesIn) < nPis ) + return NULL; + vPiPerm = Vec_IntAlloc( nPis ); + pUsed = ABC_CALLOC( int, nPis ); + for ( i = 0; i < nPis; i++ ) + { + pName1 = (char *)Vec_PtrEntry( pFirst->vNamesIn, i ); + if ( pName1 == NULL ) + break; + for ( k = 0; k < nPis; k++ ) + { + pName2 = (char *)Vec_PtrEntry( pSecond->vNamesIn, k ); + if ( pName2 && !pUsed[k] && !strcmp(pName1, pName2) ) + break; + } + if ( k == nPis ) + break; + pUsed[k] = 1; + Vec_IntPush( vPiPerm, k ); + fDiff |= (k != i); + } + ABC_FREE( pUsed ); + if ( i < nPis || !fDiff ) + { + Vec_IntFree( vPiPerm ); + return NULL; + } + pNew = Gia_ManDupPerm( pSecond, vPiPerm ); + Vec_IntFree( vPiPerm ); + pNew->vNamesIn = Vec_PtrAlloc( Vec_PtrSize(pSecond->vNamesIn) ); + for ( i = 0; i < nPis; i++ ) + { + pName1 = (char *)Vec_PtrEntry( pFirst->vNamesIn, i ); + Vec_PtrPush( pNew->vNamesIn, pName1 ? Abc_UtilStrsav(pName1) : NULL ); + } + for ( i = nPis; i < Vec_PtrSize(pSecond->vNamesIn); i++ ) + { + pName2 = (char *)Vec_PtrEntry( pSecond->vNamesIn, i ); + Vec_PtrPush( pNew->vNamesIn, pName2 ? Abc_UtilStrsav(pName2) : NULL ); + } + pNew->vNamesOut = Abc_GiaDupNameVec( pSecond->vNamesOut ); + return pNew; +} + /**Function************************************************************* Synopsis [] @@ -42942,6 +43022,18 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pGias[1] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } + if ( pGias[0] && pGias[1] ) + { + Gia_Man_t * pTemp = Abc_GiaReorderInputsByName( pGias[0], pGias[1] ); + if ( pTemp ) + { + if ( pPars->fVerbose ) + Abc_Print( 1, "Reordered primary inputs of the second network using input names.\n" ); + if ( pGias[1] != pAbc->pGia && pGias[1] != pAbc->pGiaSaved ) + Gia_ManStop( pGias[1] ); + pGias[1] = pTemp; + } + } pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL; pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL; pPars->vNamesIn = pGias[0] ? pGias[0]->vNamesIn : NULL; From ca2a410095b4530dd9359482bbdb75854f60a640 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 4 Apr 2026 09:04:24 -0700 Subject: [PATCH 4/5] Add log dump to %ufar. --- src/opt/ufar/UfarCmd.cpp | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp index 6ac2320ff..f4bd70b20 100755 --- a/src/opt/ufar/UfarCmd.cpp +++ b/src/opt/ufar/UfarCmd.cpp @@ -41,6 +41,39 @@ static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); } static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; } +static string Ufar_GetStatusName( Wlc_Ntk_t * pNtk ) +{ + if ( pNtk == NULL || Wlc_NtkPoNum(pNtk) == 0 ) + return "result"; + if ( Wlc_NtkPoNum(pNtk) == 1 ) + return Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)) ); + + string Name0 = Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)) ); + string Name1 = Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 1)) ); + return Name0 + "_xor_" + Name1; +} + +static void Ufar_DumpStatusLog( const string & FileName, int RetValue, const string & StatusName ) +{ + FILE * pFile; + if ( FileName.empty() || FileName == "none" ) + return; + pFile = fopen( FileName.c_str(), "wb" ); + if ( pFile == NULL ) + { + cout << "Cannot open file \"" << FileName << "\" for writing." << endl; + return; + } + if ( RetValue == 1 ) + fprintf( pFile, "STATUS: UNSAT " ); + else if ( RetValue == 0 ) + fprintf( pFile, "STATUS: SAT " ); + else + fprintf( pFile, "STATUS: ABORTED " ); + fprintf( pFile, "%s\n", StatusName.c_str() ); + fclose( pFile ); +} + void Ufar_Init(Abc_Frame_t *pAbc) { @@ -146,6 +179,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter"); opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit"); opt_mgr.AddOpt("--dump", "none", "str", "specify file name"); + opt_mgr.AddOpt("--dump-log", "none", "str", "write status log"); opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit"); opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name"); opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers"); @@ -254,6 +288,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv // ufar_manager.DumpParams(); LogT::prefix = "UIF_PROVE"; + string dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : ""; + string statusName = Ufar_GetStatusName( Wlc_AbcGetNtk(pAbc) ); set set_op_types; set_op_types.insert(WLC_OBJ_ARI_MULTI); @@ -372,6 +408,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv } else { LOG(0) << "Undecided by UIF."; } + Ufar_DumpStatusLog( dumpLogFile, ret, statusName ); gettimeofday(&t2, NULL); unsigned tTotal = elapsed_time_usec(t1, t2); From 80c8a9a1928ef8148a6b504e9590ec07c55c8bcf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 6 Apr 2026 20:42:44 -0700 Subject: [PATCH 5/5] Bug fix in %blast. --- src/base/wlc/wlcBlast.c | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 7e90863d8..e09868472 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1856,29 +1856,26 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) Wlc_Obj_t * pFanin = Wlc_ObjFanin0(p, pObj); int End = Wlc_ObjRangeEnd(pObj); int Beg = Wlc_ObjRangeBeg(pObj); - if ( End >= Beg ) + int Low = Abc_MinInt( End, Beg ); + int High = Abc_MaxInt( End, Beg ); + assert( nRange == High - Low + 1 ); + if ( pFanin->End >= pFanin->Beg ) { - if ( pFanin->End >= pFanin->Beg ) + assert( pFanin->Beg <= Low && High <= pFanin->End ); + for ( k = 0; k < nRange; k++ ) { - assert( nRange == End - Beg + 1 ); - assert( pFanin->Beg <= Beg && End <= pFanin->End ); - for ( k = Beg; k <= End; k++ ) - Vec_IntPush( vRes, pFans0[k - pFanin->Beg] ); - } - else - { - assert( nRange == End - Beg + 1 ); - assert( pFanin->End <= Beg && End <= pFanin->Beg ); - for ( k = Beg; k <= End; k++ ) - Vec_IntPush( vRes, pFans0[k - pFanin->End] ); + int Label = End >= Beg ? Beg + k : Beg - k; + Vec_IntPush( vRes, pFans0[Label - pFanin->Beg] ); } } else { - assert( nRange == Beg - End + 1 ); - assert( pFanin->End <= End && Beg <= pFanin->Beg ); - for ( k = End; k <= Beg; k++ ) - Vec_IntPush( vRes, pFans0[k - pFanin->End] ); + assert( pFanin->End <= Low && High <= pFanin->Beg ); + for ( k = 0; k < nRange; k++ ) + { + int Label = End >= Beg ? Beg + k : Beg - k; + Vec_IntPush( vRes, pFans0[pFanin->Beg - Label] ); + } } } else if ( pObj->Type == WLC_OBJ_BIT_CONCAT )