From 000be270ca3272dd660dcd82b8a142b9fd593411 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:54:46 +0100 Subject: [PATCH] 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++;