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");