From 000be270ca3272dd660dcd82b8a142b9fd593411 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:54:46 +0100 Subject: [PATCH 01/10] equiv_simple, equiv_induct: refactor --- passes/equiv/equiv.h | 73 ++++++++++++++++++++++ passes/equiv/equiv_induct.cc | 66 +++++--------------- passes/equiv/equiv_simple.cc | 118 ++++++++++++++--------------------- 3 files changed, 136 insertions(+), 121 deletions(-) create mode 100644 passes/equiv/equiv.h diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h new file mode 100644 index 000000000..b255042ba --- /dev/null +++ b/passes/equiv/equiv.h @@ -0,0 +1,73 @@ +#ifndef EQUIV_H +#define EQUIV_H + +#include "kernel/log.h" +#include "kernel/yosys_common.h" +#include "kernel/sigtools.h" +#include "kernel/satgen.h" + +YOSYS_NAMESPACE_BEGIN + +static void report_missing_model(bool warn_only, RTLIL::Cell* cell) +{ + std::string s; + if (cell->is_builtin_ff()) + s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); + else + s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); + + if (warn_only) { + log_formatted_warning_noprefix(s); + } else { + log_formatted_error(s); + } +} + +struct EquivWorker { + RTLIL::Module *module; + + ezSatPtr ez; + SatGen satgen; + + struct Config { + bool model_undef = false; + int max_seq = 1; + bool set_assumes = false; + + bool parse(const std::vector& args, size_t& idx) { + if (args[idx] == "-undef") { + model_undef = true; + return true; + } + if (args[idx] == "-seq" && idx+1 < args.size()) { + max_seq = atoi(args[++idx].c_str()); + return true; + } + if (args[idx] == "-set-assumes") { + set_assumes = true; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return stringf( + " -undef\n" + " enable modelling of undef states\n" + "\n" + " -seq \n" + " the max. number of time steps to be considered (default = %s)\n" + "\n" + " -set-assumes\n" + " set all assumptions provided via $assume cells\n" + , default_seq); + } + }; + Config cfg; + + EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) { + satgen.model_undef = cfg.model_undef; + } +}; + +YOSYS_NAMESPACE_END +#endif // EQUIV_H diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index e1a3a7990..c91501719 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -18,49 +18,34 @@ */ #include "kernel/yosys.h" -#include "kernel/satgen.h" -#include "kernel/sigtools.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivInductWorker +struct EquivInductWorker : public EquivWorker { - Module *module; SigMap sigmap; vector cells; pool workset; - ezSatPtr ez; - SatGen satgen; - - int max_seq; int success_counter; - bool set_assumes; dict ez_step_is_consistent; - pool cell_warn_cache; SigPool undriven_signals; - EquivInductWorker(Module *module, const pool &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, Config cfg) : EquivWorker(module, &sigmap, cfg), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), - satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes) - { - satgen.model_undef = model_undef; - } + success_counter(0) {} void create_timestep(int step) { vector ez_equal_terms; for (auto cell : cells) { - if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) { - if (cell->is_builtin_ff()) - log_warning("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - cell_warn_cache.insert(cell); + if (!satgen.importCell(cell, step)) { + report_missing_model(true, cell); } if (cell->type == ID($equiv)) { SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit(); @@ -78,7 +63,7 @@ struct EquivInductWorker } } - if (set_assumes) { + if (cfg.set_assumes) { if (step == 1) { RTLIL::SigSpec assumes_a, assumes_en; satgen.getAssumes(assumes_a, assumes_en, step); @@ -123,7 +108,7 @@ struct EquivInductWorker GetSize(satgen.initial_state), GetSize(undriven_signals)); } - for (int step = 1; step <= max_seq; step++) + for (int step = 1; step <= cfg.max_seq; step++) { ez->assume(ez_step_is_consistent[step]); @@ -146,7 +131,7 @@ struct EquivInductWorker return; } - log(" Proof for induction step failed. %s\n", step != max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset."); + log(" Proof for induction step failed. %s\n", step != cfg.max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset."); } workset.sort(); @@ -158,12 +143,12 @@ struct EquivInductWorker log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort(ID::Y)))); - int ez_a = satgen.importSigBit(bit_a, max_seq+1); - int ez_b = satgen.importSigBit(bit_b, max_seq+1); + int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1); + int ez_b = satgen.importSigBit(bit_b, cfg.max_seq+1); int cond = ez->XOR(ez_a, ez_b); if (satgen.model_undef) - cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1))); + cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, cfg.max_seq+1))); if (!ez->solve(cond)) { log(" success!\n"); @@ -189,14 +174,7 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); - log(" -undef\n"); - log(" enable modelling of undef states\n"); - log("\n"); - log(" -seq \n"); - log(" the max. number of time steps to be considered (default = 4)\n"); - log("\n"); - log(" -set-assumes\n"); - log(" set all assumptions provided via $assume cells\n"); + EquivWorker::Config::help("4"); log("\n"); log("This command is very effective in proving complex sequential circuits, when\n"); log("the internal state of the circuit quickly propagates to $equiv cells.\n"); @@ -214,25 +192,15 @@ struct EquivInductPass : public Pass { void execute(std::vector args, Design *design) override { int success_counter = 0; - bool model_undef = false, set_assumes = false; - int max_seq = 4; + EquivWorker::Config cfg; + cfg.max_seq = 4; log_header(design, "Executing EQUIV_INDUCT pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-undef") { - model_undef = true; + if (cfg.parse(args, argidx)) continue; - } - if (args[argidx] == "-seq" && argidx+1 < args.size()) { - max_seq = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-set-assumes") { - set_assumes = true; - continue; - } break; } extra_args(args, argidx, design); @@ -253,7 +221,7 @@ struct EquivInductPass : public Pass { continue; } - EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes); + EquivInductWorker worker(module, unproven_equiv_cells, cfg); worker.run(); success_counter += worker.success_counter; } diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 97f95ac63..0749d18aa 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -17,15 +17,52 @@ * */ +#include "kernel/log.h" #include "kernel/yosys.h" -#include "kernel/satgen.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivSimpleWorker +struct EquivSimpleWorker : public EquivWorker { - Module *module; + struct Config : EquivWorker::Config { + bool verbose = false; + bool short_cones = false; + bool group = true; + bool parse(const std::vector& args, size_t& idx) { + if (EquivWorker::Config::parse(args, idx)) + return true; + if (args[idx] == "-v") { + verbose = true; + return true; + } + if (args[idx] == "-short") { + short_cones = true; + return true; + } + if (args[idx] == "-nogroup") { + group = false; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return EquivWorker::Config::help(default_seq) + + " -v\n" + " verbose output\n" + "\n" + " -short\n" + " create shorter input cones that stop at shared nodes. This yields\n" + " simpler SAT problems but sometimes fails to prove equivalence.\n" + "\n" + " -nogroup\n" + " disabling grouping of $equiv cells by output wire\n" + "\n"; + } + }; + Config cfg; + const vector &equiv_cells; const vector &assume_cells; struct Cone { @@ -43,27 +80,11 @@ struct EquivSimpleWorker }; DesignModel model; - ezSatPtr ez; - SatGen satgen; - - struct Config { - bool verbose = false; - bool short_cones = false; - bool model_undef = false; - bool nogroup = false; - bool set_assumes = false; - int max_seq = 1; - }; - Config cfg; - pool> imported_cells_cache; EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, Config cfg) : - module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells), - model(model), satgen(ez.get(), &model.sigmap), cfg(cfg) - { - satgen.model_undef = cfg.model_undef; - } + EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), + model(model) {} struct ConeFinder { DesignModel model; @@ -229,14 +250,6 @@ struct EquivSimpleWorker return extra_problem_cells; } - static void report_missing_model(Cell* cell) - { - if (cell->is_builtin_ff()) - log_cmd_error("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - } - void prepare_ezsat(int ez_context, SigBit bit_a, SigBit bit_b) { if (satgen.model_undef) @@ -323,7 +336,7 @@ struct EquivSimpleWorker for (auto cell : problem_cells) { auto key = pair(cell, step+1); if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) { - report_missing_model(cell); + report_missing_model(true, cell); } imported_cells_cache.insert(key); } @@ -414,24 +427,7 @@ struct EquivSimplePass : public Pass { log("\n"); log("This command tries to prove $equiv cells using a simple direct SAT approach.\n"); log("\n"); - log(" -v\n"); - log(" verbose output\n"); - log("\n"); - log(" -undef\n"); - log(" enable modelling of undef states\n"); - log("\n"); - log(" -short\n"); - log(" create shorter input cones that stop at shared nodes. This yields\n"); - log(" simpler SAT problems but sometimes fails to prove equivalence.\n"); - log("\n"); - log(" -nogroup\n"); - log(" disabling grouping of $equiv cells by output wire\n"); - log("\n"); - log(" -seq \n"); - log(" the max. number of time steps to be considered (default = 1)\n"); - log("\n"); - log(" -set-assumes\n"); - log(" set all assumptions provided via $assume cells\n"); + EquivSimpleWorker::Config::help("1"); log("\n"); } void execute(std::vector args, Design *design) override @@ -443,30 +439,8 @@ struct EquivSimplePass : public Pass { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-v") { - cfg.verbose = true; + if (cfg.parse(args, argidx)) continue; - } - if (args[argidx] == "-short") { - cfg.short_cones = true; - continue; - } - if (args[argidx] == "-undef") { - cfg.model_undef = true; - continue; - } - if (args[argidx] == "-nogroup") { - cfg.nogroup = true; - continue; - } - if (args[argidx] == "-seq" && argidx+1 < args.size()) { - cfg.max_seq = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-set-assumes") { - cfg.set_assumes = true; - continue; - } break; } extra_args(args, argidx, design); @@ -489,7 +463,7 @@ struct EquivSimplePass : public Pass { if (cell->type == ID($equiv) && cell->getPort(ID::A) != cell->getPort(ID::B)) { auto bit = sigmap(cell->getPort(ID::Y).as_bit()); auto bit_group = bit; - if (!cfg.nogroup && bit_group.wire) + if (cfg.group && bit_group.wire) bit_group.offset = 0; unproven_equiv_cells[bit_group][bit] = cell; unproven_cells_counter++; From 8e73e2a306809369c2f71d6037f1671e36e69d4e Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:56:10 +0100 Subject: [PATCH 02/10] sat: add -ignore-unknown-cells instead of -ignore_unknown_cells for consistency --- passes/sat/sat.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 90b85d709..ffebdd01c 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -961,10 +961,10 @@ struct SatPass : public Pass { log(" -show-regs, -show-public, -show-all\n"); log(" show all registers, show signals with 'public' names, show all signals\n"); log("\n"); - log(" -ignore_div_by_zero\n"); + log(" -ignore-div-by-zero\n"); log(" ignore all solutions that involve a division by zero\n"); log("\n"); - log(" -ignore_unknown_cells\n"); + log(" -ignore-unknown-cells\n"); log(" ignore all cells that can not be matched to a SAT model\n"); log("\n"); log("The following options can be used to set up a sequential problem:\n"); @@ -1141,7 +1141,7 @@ struct SatPass : public Pass { stepsize = max(1, atoi(args[++argidx].c_str())); continue; } - if (args[argidx] == "-ignore_div_by_zero") { + if (args[argidx] == "-ignore-div-by-zero" || args[argidx] == "-ignore_div_by_zero") { ignore_div_by_zero = true; continue; } @@ -1316,7 +1316,7 @@ struct SatPass : public Pass { show_all = true; continue; } - if (args[argidx] == "-ignore_unknown_cells") { + if (args[argidx] == "-ignore-unknown-cells" || args[argidx] == "-ignore_unknown_cells") { ignore_unknown_cells = true; continue; } From 8d1c1faf82ec085c9756a31010ed9d50d06334d3 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:59:31 +0100 Subject: [PATCH 03/10] equiv_simple, equiv_induct: error by default on missing model, add -ignore-unknown-cells --- passes/equiv/equiv.h | 8 ++++++++ passes/equiv/equiv_induct.cc | 2 +- passes/equiv/equiv_simple.cc | 2 +- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h index b255042ba..8a24b2fcd 100644 --- a/passes/equiv/equiv.h +++ b/passes/equiv/equiv.h @@ -33,6 +33,7 @@ struct EquivWorker { bool model_undef = false; int max_seq = 1; bool set_assumes = false; + bool ignore_unknown_cells = false; bool parse(const std::vector& args, size_t& idx) { if (args[idx] == "-undef") { @@ -47,6 +48,10 @@ struct EquivWorker { set_assumes = true; return true; } + if (args[idx] == "-ignore-unknown-cells") { + ignore_unknown_cells = true; + return true; + } return false; } static std::string help(const char* default_seq) { @@ -59,6 +64,9 @@ struct EquivWorker { "\n" " -set-assumes\n" " set all assumptions provided via $assume cells\n" + "\n" + " -ignore-unknown-cells\n" + " ignore all cells that can not be matched to a SAT model\n" , default_seq); } }; diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index c91501719..f7ceb78a3 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -45,7 +45,7 @@ struct EquivInductWorker : public EquivWorker for (auto cell : cells) { if (!satgen.importCell(cell, step)) { - report_missing_model(true, cell); + report_missing_model(cfg.ignore_unknown_cells, cell); } if (cell->type == ID($equiv)) { SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit(); diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 0749d18aa..f345e9794 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -336,7 +336,7 @@ struct EquivSimpleWorker : public EquivWorker for (auto cell : problem_cells) { auto key = pair(cell, step+1); if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) { - report_missing_model(true, cell); + report_missing_model(cfg.ignore_unknown_cells, cell); } imported_cells_cache.insert(key); } From d199195785fb058eb1c92502787e79be3ea56943 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:00:45 +0100 Subject: [PATCH 04/10] satgen: cover $input_port --- kernel/satgen.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/satgen.cc b/kernel/satgen.cc index f2c1e00c2..b8b850bb3 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -1378,7 +1378,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } - if (cell->type == ID($scopeinfo)) + if (cell->type == ID($scopeinfo) || cell->type == ID($input_port)) { return true; } From 2efd0247a10192fb1240c0c7a6778b2979b3377d Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:09:51 +0100 Subject: [PATCH 05/10] opt_hier: fix test --- tests/opt/opt_hier.tcl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/opt/opt_hier.tcl b/tests/opt/opt_hier.tcl index 65d8f9809..d006759f5 100644 --- a/tests/opt/opt_hier.tcl +++ b/tests/opt/opt_hier.tcl @@ -27,7 +27,7 @@ foreach fn [glob opt_hier_*.v] { design -copy-from gate -as gate A:top yosys rename -hide equiv_make gold gate equiv - equiv_induct equiv + equiv_induct -ignore-unknown-cells equiv equiv_status -assert equiv log -pop From c768e55983f2077da5d0a7d1798f73a35055af8b Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:10:02 +0100 Subject: [PATCH 06/10] ice40: fix dsp_const test --- tests/arch/ice40/ice40_dsp_const.ys | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/arch/ice40/ice40_dsp_const.ys b/tests/arch/ice40/ice40_dsp_const.ys index c9c76a1ac..735f945a1 100644 --- a/tests/arch/ice40/ice40_dsp_const.ys +++ b/tests/arch/ice40/ice40_dsp_const.ys @@ -74,6 +74,7 @@ EOT techmap -wb -D EQUIV -autoproc -map +/ice40/cells_sim.v +async2sync equiv_make top ref equiv select -assert-any -module equiv t:$equiv equiv_induct From ed53ff2f4988c6fc49cefafa85b6a82ef2ca1871 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:37:39 +0100 Subject: [PATCH 07/10] equiv_simple, equiv_induct: fix config --- passes/equiv/equiv.h | 89 ++++++++++++++++++------------------ passes/equiv/equiv_induct.cc | 8 ++-- passes/equiv/equiv_simple.cc | 81 ++++++++++++++++---------------- 3 files changed, 90 insertions(+), 88 deletions(-) diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h index 8a24b2fcd..9641e65a7 100644 --- a/passes/equiv/equiv.h +++ b/passes/equiv/equiv.h @@ -23,54 +23,55 @@ static void report_missing_model(bool warn_only, RTLIL::Cell* cell) } } +struct EquivBasicConfig { + bool model_undef = false; + int max_seq = 1; + bool set_assumes = false; + bool ignore_unknown_cells = false; + + bool parse(const std::vector& args, size_t& idx) { + if (args[idx] == "-undef") { + model_undef = true; + return true; + } + if (args[idx] == "-seq" && idx+1 < args.size()) { + max_seq = atoi(args[++idx].c_str()); + return true; + } + if (args[idx] == "-set-assumes") { + set_assumes = true; + return true; + } + if (args[idx] == "-ignore-unknown-cells") { + ignore_unknown_cells = true; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return stringf( + " -undef\n" + " enable modelling of undef states\n" + "\n" + " -seq \n" + " the max. number of time steps to be considered (default = %s)\n" + "\n" + " -set-assumes\n" + " set all assumptions provided via $assume cells\n" + "\n" + " -ignore-unknown-cells\n" + " ignore all cells that can not be matched to a SAT model\n" + , default_seq); + } +}; + +template struct EquivWorker { RTLIL::Module *module; - ezSatPtr ez; + ezSatPtr ez; SatGen satgen; - - struct Config { - bool model_undef = false; - int max_seq = 1; - bool set_assumes = false; - bool ignore_unknown_cells = false; - - bool parse(const std::vector& args, size_t& idx) { - if (args[idx] == "-undef") { - model_undef = true; - return true; - } - if (args[idx] == "-seq" && idx+1 < args.size()) { - max_seq = atoi(args[++idx].c_str()); - return true; - } - if (args[idx] == "-set-assumes") { - set_assumes = true; - return true; - } - if (args[idx] == "-ignore-unknown-cells") { - ignore_unknown_cells = true; - return true; - } - return false; - } - static std::string help(const char* default_seq) { - return stringf( - " -undef\n" - " enable modelling of undef states\n" - "\n" - " -seq \n" - " the max. number of time steps to be considered (default = %s)\n" - "\n" - " -set-assumes\n" - " set all assumptions provided via $assume cells\n" - "\n" - " -ignore-unknown-cells\n" - " ignore all cells that can not be matched to a SAT model\n" - , default_seq); - } - }; - Config cfg; + Config cfg; EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) { satgen.model_undef = cfg.model_undef; diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index f7ceb78a3..d843fef67 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -23,7 +23,7 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivInductWorker : public EquivWorker +struct EquivInductWorker : public EquivWorker<> { SigMap sigmap; @@ -35,7 +35,7 @@ struct EquivInductWorker : public EquivWorker dict ez_step_is_consistent; SigPool undriven_signals; - EquivInductWorker(Module *module, const pool &unproven_equiv_cells, Config cfg) : EquivWorker(module, &sigmap, cfg), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, EquivBasicConfig cfg) : EquivWorker<>(module, &sigmap, cfg), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), success_counter(0) {} @@ -174,7 +174,7 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); - EquivWorker::Config::help("4"); + EquivBasicConfig::help("4"); log("\n"); log("This command is very effective in proving complex sequential circuits, when\n"); log("the internal state of the circuit quickly propagates to $equiv cells.\n"); @@ -192,7 +192,7 @@ struct EquivInductPass : public Pass { void execute(std::vector args, Design *design) override { int success_counter = 0; - EquivWorker::Config cfg; + EquivBasicConfig cfg {}; cfg.max_seq = 4; log_header(design, "Executing EQUIV_INDUCT pass.\n"); diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index f345e9794..ff6df295c 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -24,45 +24,44 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivSimpleWorker : public EquivWorker -{ - struct Config : EquivWorker::Config { - bool verbose = false; - bool short_cones = false; - bool group = true; - bool parse(const std::vector& args, size_t& idx) { - if (EquivWorker::Config::parse(args, idx)) - return true; - if (args[idx] == "-v") { - verbose = true; - return true; - } - if (args[idx] == "-short") { - short_cones = true; - return true; - } - if (args[idx] == "-nogroup") { - group = false; - return true; - } - return false; +struct EquivSimpleConfig : EquivBasicConfig { + bool verbose = false; + bool short_cones = false; + bool group = true; + bool parse(const std::vector& args, size_t& idx) { + if (EquivBasicConfig::parse(args, idx)) + return true; + if (args[idx] == "-v") { + verbose = true; + return true; } - static std::string help(const char* default_seq) { - return EquivWorker::Config::help(default_seq) + - " -v\n" - " verbose output\n" - "\n" - " -short\n" - " create shorter input cones that stop at shared nodes. This yields\n" - " simpler SAT problems but sometimes fails to prove equivalence.\n" - "\n" - " -nogroup\n" - " disabling grouping of $equiv cells by output wire\n" - "\n"; + if (args[idx] == "-short") { + short_cones = true; + return true; } - }; - Config cfg; + if (args[idx] == "-nogroup") { + group = false; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return EquivBasicConfig::help(default_seq) + + " -v\n" + " verbose output\n" + "\n" + " -short\n" + " create shorter input cones that stop at shared nodes. This yields\n" + " simpler SAT problems but sometimes fails to prove equivalence.\n" + "\n" + " -nogroup\n" + " disabling grouping of $equiv cells by output wire\n" + "\n"; + } +}; +struct EquivSimpleWorker : public EquivWorker +{ const vector &equiv_cells; const vector &assume_cells; struct Cone { @@ -82,8 +81,8 @@ struct EquivSimpleWorker : public EquivWorker pool> imported_cells_cache; - EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, Config cfg) : - EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), + EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, EquivSimpleConfig cfg) : + EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), model(model) {} struct ConeFinder { @@ -270,7 +269,9 @@ struct EquivSimpleWorker : public EquivWorker } void construct_ezsat(const pool& input_bits, int step) { + log("ezsat\n"); if (cfg.set_assumes) { + log("yep assume\n"); if (cfg.verbose && step == cfg.max_seq) { RTLIL::SigSpec assumes_a, assumes_en; satgen.getAssumes(assumes_a, assumes_en, step+1); @@ -427,12 +428,12 @@ struct EquivSimplePass : public Pass { log("\n"); log("This command tries to prove $equiv cells using a simple direct SAT approach.\n"); log("\n"); - EquivSimpleWorker::Config::help("1"); + EquivSimpleConfig::help("1"); log("\n"); } void execute(std::vector args, Design *design) override { - EquivSimpleWorker::Config cfg = {}; + EquivSimpleConfig cfg {}; int success_counter = 0; log_header(design, "Executing EQUIV_SIMPLE pass.\n"); From 91b226b4d40815109f0ac1223bc2fafdf0aa0d03 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:40:32 +0100 Subject: [PATCH 08/10] specify: fix test --- tests/various/specify.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/various/specify.ys b/tests/various/specify.ys index d7260d524..86471de5e 100644 --- a/tests/various/specify.ys +++ b/tests/various/specify.ys @@ -43,7 +43,7 @@ select n:C_* -assert-count 2 equiv_make gold gate equiv hierarchy -top equiv equiv_struct -equiv_induct -seq 5 +equiv_induct -ignore-unknown-cells -seq 5 equiv_status -assert design -reset @@ -57,7 +57,7 @@ select n:B_* -assert-count 2 equiv_make gold gate equiv hierarchy -top equiv equiv_struct -equiv_induct -seq 5 +equiv_induct -ignore-unknown-cells -seq 5 equiv_status -assert design -reset From 81ea922512a5ce7e6fdba1f4ff0c23ce4c3b743a Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 16 Feb 2026 16:54:26 +0100 Subject: [PATCH 09/10] sat: use the same cell import warnings as equiv --- passes/sat/sat.cc | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index ffebdd01c..c143e938e 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -27,6 +27,7 @@ #include "kernel/satgen.h" #include "kernel/yosys.h" #include "kernel/log_help.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -227,16 +228,12 @@ struct SatHelper int import_cell_counter = 0; for (auto cell : module->cells()) if (design->selected(module, cell)) { - // log("Import cell: %s\n", RTLIL::id2cstr(cell->name)); if (satgen.importCell(cell, timestep)) { for (auto &p : cell->connections()) if (ct.cell_output(cell->type, p.first)) show_drivers.insert(sigmap(p.second), cell); import_cell_counter++; - } else if (ignore_unknown_cells) - log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); - else - log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); + } else report_missing_model(ignore_unknown_cells, cell); } log("Imported %d cells to SAT database.\n", import_cell_counter); From 77f64de9979e957452be2a4f2f428f0607791b63 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 16 Feb 2026 17:01:09 +0100 Subject: [PATCH 10/10] satgen: move report_missing_model here from equiv.h --- kernel/satgen.cc | 20 ++++++++++++++++++++ kernel/satgen.h | 2 ++ passes/equiv/equiv.h | 15 --------------- passes/sat/sat.cc | 1 - 4 files changed, 22 insertions(+), 16 deletions(-) diff --git a/kernel/satgen.cc b/kernel/satgen.cc index b8b850bb3..7fbcba1b2 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -19,6 +19,7 @@ #include "kernel/satgen.h" #include "kernel/ff.h" +#include "kernel/yosys_common.h" USING_YOSYS_NAMESPACE @@ -1387,3 +1388,22 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) // .. and all sequential cells with asynchronous inputs return false; } + +namespace Yosys { + +void report_missing_model(bool warn_only, RTLIL::Cell* cell) +{ + std::string s; + if (cell->is_builtin_ff()) + s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); + else + s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); + + if (warn_only) { + log_formatted_warning_noprefix(s); + } else { + log_formatted_error(s); + } +} + +} diff --git a/kernel/satgen.h b/kernel/satgen.h index 7815847b3..9ad940585 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -292,6 +292,8 @@ struct SatGen bool importCell(RTLIL::Cell *cell, int timestep = -1); }; +void report_missing_model(bool warn_only, RTLIL::Cell* cell); + YOSYS_NAMESPACE_END #endif diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h index 9641e65a7..95d4b25e9 100644 --- a/passes/equiv/equiv.h +++ b/passes/equiv/equiv.h @@ -8,21 +8,6 @@ YOSYS_NAMESPACE_BEGIN -static void report_missing_model(bool warn_only, RTLIL::Cell* cell) -{ - std::string s; - if (cell->is_builtin_ff()) - s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - - if (warn_only) { - log_formatted_warning_noprefix(s); - } else { - log_formatted_error(s); - } -} - struct EquivBasicConfig { bool model_undef = false; int max_seq = 1; diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index c143e938e..203147172 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -27,7 +27,6 @@ #include "kernel/satgen.h" #include "kernel/yosys.h" #include "kernel/log_help.h" -#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN