diff --git a/kernel/satgen.h b/kernel/satgen.h index 2c8cbda13..996eaf9fb 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -64,7 +64,7 @@ struct ezSatPtr : public std::unique_ptr { struct SatGen { ezSAT *ez; - SigMap *sigmap; + const SigMap *sigmap; std::string prefix; SigPool initial_state; std::map asserts_a, asserts_en; @@ -75,12 +75,12 @@ struct SatGen bool model_undef; bool def_formal = false; - SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) : + SatGen(ezSAT *ez, const SigMap *sigmap, std::string prefix = std::string()) : ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false) { } - void setContext(SigMap *sigmap, std::string prefix = std::string()) + void setContext(const SigMap *sigmap, std::string prefix = std::string()) { this->sigmap = sigmap; this->prefix = prefix; diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index 8d882ae83..1995be3cd 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -37,14 +37,15 @@ struct EquivInductWorker 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) : module(module), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), - satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0) + satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes) { satgen.model_undef = model_undef; } @@ -77,6 +78,16 @@ struct EquivInductWorker } } + if (set_assumes) { + if (step == 1) { + RTLIL::SigSpec assumes_a, assumes_en; + satgen.getAssumes(assumes_a, assumes_en, step); + for (int i = 0; i < GetSize(assumes_a); i++) + log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); + } + ez->assume(satgen.importAssumes(step)); + } + if (satgen.model_undef) { for (auto bit : undriven_signals.export_all()) ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step))); @@ -184,6 +195,9 @@ struct EquivInductPass : public Pass { 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"); + 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"); log("\n"); @@ -200,7 +214,7 @@ struct EquivInductPass : public Pass { void execute(std::vector args, Design *design) override { int success_counter = 0; - bool model_undef = false; + bool model_undef = false, set_assumes = false; int max_seq = 4; log_header(design, "Executing EQUIV_INDUCT pass.\n"); @@ -215,6 +229,10 @@ struct EquivInductPass : public Pass { max_seq = atoi(args[++argidx].c_str()); continue; } + if (args[argidx] == "-set-assumes") { + set_assumes = true; + continue; + } break; } extra_args(args, argidx, design); @@ -222,6 +240,7 @@ struct EquivInductPass : public Pass { for (auto module : design->selected_modules()) { pool unproven_equiv_cells; + vector assume_cells; for (auto cell : module->selected_cells()) if (cell->type == ID($equiv)) { @@ -234,7 +253,7 @@ struct EquivInductPass : public Pass { continue; } - EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq); + EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes); worker.run(); success_counter += worker.success_counter; } diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 59974a1e6..8ba42595e 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -27,215 +27,345 @@ struct EquivSimpleWorker { Module *module; const vector &equiv_cells; - Cell *equiv_cell; + const vector &assume_cells; + struct Cone { + pool cells; + pool bits; + void clear() { + cells.clear(); + bits.clear(); + } + }; - SigMap &sigmap; - dict &bit2driver; + struct DesignModel { + const SigMap &sigmap; + dict &bit2driver; + }; + DesignModel model; ezSatPtr ez; SatGen satgen; - int max_seq; - bool short_cones; - bool verbose; + + 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, SigMap &sigmap, dict &bit2driver, int max_seq, bool short_cones, bool verbose, bool model_undef) : - module(equiv_cells.front()->module), equiv_cells(equiv_cells), equiv_cell(nullptr), - sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), short_cones(short_cones), verbose(verbose) + 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 = model_undef; + satgen.model_undef = cfg.model_undef; } - bool find_input_cone(pool &next_seed, pool &cells_cone, pool &bits_cone, const pool &cells_stop, const pool &bits_stop, pool *input_bits, Cell *cell) - { - if (cells_cone.count(cell)) + struct ConeFinder { + DesignModel model; + // Bits we should also analyze in a later iteration (flop inputs) + pool &next_seed; + // Cells and bits we've seen so far while traversing + Cone& cone; + // We're not allowed to traverse past cells and bits in `stop` + const Cone& stop; + // Input bits are bits that no longer can be traversed + // Tracking these is optional + pool* input_bits; + + // Recursively traverses backwards from a cell to find all cells in its input cone + // Adds cell to cone.cells, stops at cells in 'stop' set + // Returns true if stopped on a stop cell + bool find_input_cone(Cell *cell) + { + if (cone.cells.count(cell)) + return false; + + cone.cells.insert(cell); + + if (stop.cells.count(cell)) + return true; + + for (auto &conn : cell->connections()) + if (yosys_celltypes.cell_input(cell->type, conn.first)) + for (auto bit : model.sigmap(conn.second)) { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { + if (!conn.first.in(ID::CLK, ID::C)) + next_seed.insert(bit); + } else + find_input_cone(bit); + } return false; + } + void find_input_cone(SigBit bit) + { + if (cone.bits.count(bit)) + return; - cells_cone.insert(cell); + cone.bits.insert(bit); - if (cells_stop.count(cell)) - return true; + if (stop.bits.count(bit)) { + if (input_bits != nullptr) input_bits->insert(bit); + return; + } - for (auto &conn : cell->connections()) - if (yosys_celltypes.cell_input(cell->type, conn.first)) - for (auto bit : sigmap(conn.second)) { - if (RTLIL::builtin_ff_cell_types().count(cell->type)) { - if (!conn.first.in(ID::CLK, ID::C)) - next_seed.insert(bit); - } else - find_input_cone(next_seed, cells_cone, bits_cone, cells_stop, bits_stop, input_bits, bit); - } - return false; - } + if (!model.bit2driver.count(bit)) + return; - void find_input_cone(pool &next_seed, pool &cells_cone, pool &bits_cone, const pool &cells_stop, const pool &bits_stop, pool *input_bits, SigBit bit) + // If the input cone of the driver cell reaches a stop bit, + // then `bit` is an "input bit" + if (find_input_cone(model.bit2driver.at(bit))) + if (input_bits != nullptr) input_bits->insert(bit); + } + void find_input_cone(pool bits) + { + for (auto bit : bits) + find_input_cone(bit); + } + }; + + // Builds (full or short) input cones from the seeds + // Creates full cones (no stops) and optionally short cones (stop at other side's cone) + // Updates seed_a/seed_b with next iteration's FF inputs + // Returns input bits and cone structures for SAT problem construction + std::tuple, Cone, Cone> init_iter(pool& seed_a, pool& seed_b) const { - if (bits_cone.count(bit)) - return; + // Empty, never inserted to, to traverse full cones + const Cone no_stop; + Cone full_cone_a, full_cone_b; - bits_cone.insert(bit); + // Values of seed_* for the next iteration + pool next_seed_a, next_seed_b; - if (bits_stop.count(bit)) { - if (input_bits != nullptr) input_bits->insert(bit); - return; + { + ConeFinder finder_a {model, next_seed_a, full_cone_a, no_stop, nullptr}; + finder_a.find_input_cone(seed_a); + + ConeFinder finder_b {model, next_seed_b, full_cone_b, no_stop, nullptr}; + finder_b.find_input_cone(seed_b); } - if (!bit2driver.count(bit)) - return; + Cone short_cone_a, short_cone_b; + pool input_bits; - if (find_input_cone(next_seed, cells_cone, bits_cone, cells_stop, bits_stop, input_bits, bit2driver.at(bit))) - if (input_bits != nullptr) input_bits->insert(bit); + if (cfg.short_cones) + { + // Rebuild cones with the knowledge of the full cones. + // Avoids stuffing overlaps in input cones into the solver + // e.g. for A by using the full B cone as stops + next_seed_a.clear(); + ConeFinder short_finder_a = {model, next_seed_a, short_cone_a, short_cone_b, &input_bits}; + short_finder_a.find_input_cone(seed_a); + next_seed_a.swap(seed_a); + + next_seed_b.clear(); + ConeFinder short_finder_b = {model, next_seed_b, short_cone_b, short_cone_a, &input_bits}; + short_finder_b.find_input_cone(seed_b); + next_seed_b.swap(seed_b); + } + else + { + short_cone_a = full_cone_a; + next_seed_a.swap(seed_a); + + short_cone_b = full_cone_b; + next_seed_b.swap(seed_b); + } + return std::make_tuple(input_bits, short_cone_a, short_cone_b); } - bool run_cell() + void report_new_cells(const pool& cells, const Cone& cone_a, const Cone& cone_b) const { - SigBit bit_a = sigmap(equiv_cell->getPort(ID::A)).as_bit(); - SigBit bit_b = sigmap(equiv_cell->getPort(ID::B)).as_bit(); - int ez_context = ez->frozen_literal(); + log(" Adding %d new cells to the problem (%d A, %d B, %d shared).\n", + GetSize(cells), GetSize(cone_a.cells), GetSize(cone_b.cells), + (GetSize(cone_a.cells) + GetSize(cone_b.cells)) - GetSize(cells)); + #if 0 + for (auto cell : short_cells_cone_a) + log(" A-side cell: %s\n", log_id(cell)); + for (auto cell : short_cells_cone_b) + log(" B-side cell: %s\n", log_id(cell)); + #endif + } + void report_new_assume_cells(const pool& extra_problem_cells, int old_size, const pool& problem_cells) const + { + if (cfg.verbose) { + log(" Adding %d new cells to check assumptions (and reusing %d).\n", + GetSize(problem_cells) - old_size, + old_size - (GetSize(problem_cells) - GetSize(extra_problem_cells))); + #if 0 + for (auto cell : extra_problem_cells) + log(" cell: %s\n", log_id(cell)); + #endif + } + } + + // Ensure the input cones of $assume cells get modelled by the problem + pool add_assumes_to_problem(const Cone& cone_a, const Cone& cone_b) const + { + pool extra_problem_cells; + for (auto assume : assume_cells) { + pool assume_seed, dummy_next_seed, overlap_bits; + assume_seed.insert(model.sigmap(assume->getPort(ID::A)).as_bit()); + assume_seed.insert(model.sigmap(assume->getPort(ID::EN)).as_bit()); + + for (auto& cone : {cone_a, cone_b}) { + Cone assume_cone; + ConeFinder{model, dummy_next_seed, assume_cone, cone, &overlap_bits} + .find_input_cone(assume_seed); + if (GetSize(overlap_bits)) { + extra_problem_cells.insert(assume); + extra_problem_cells.insert(assume_cone.cells.begin(), assume_cone.cells.end()); + overlap_bits.clear(); + } + assume_cone.clear(); + dummy_next_seed.clear(); + } + } + return extra_problem_cells; + } + + static void report_missing_model(Cell* cell) + { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + 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) { - int ez_a = satgen.importSigBit(bit_a, max_seq+1); - int ez_b = satgen.importDefSigBit(bit_b, max_seq+1); - int ez_undef_a = satgen.importUndefSigBit(bit_a, max_seq+1); + int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1); + int ez_b = satgen.importDefSigBit(bit_b, cfg.max_seq+1); + int ez_undef_a = satgen.importUndefSigBit(bit_a, cfg.max_seq+1); ez->assume(ez->XOR(ez_a, ez_b), ez_context); ez->assume(ez->NOT(ez_undef_a), ez_context); } else { - 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); ez->assume(ez->XOR(ez_a, ez_b), ez_context); } + } + void construct_ezsat(const pool& input_bits, int step) + { + if (cfg.set_assumes) { + if (cfg.verbose && step == cfg.max_seq) { + RTLIL::SigSpec assumes_a, assumes_en; + satgen.getAssumes(assumes_a, assumes_en, step+1); + for (int i = 0; i < GetSize(assumes_a); i++) + log(" Import constraint from assume cell: %s when %s (%d).\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]), step); + } + ez->assume(satgen.importAssumes(step+1)); + } + if (satgen.model_undef) { + for (auto bit : input_bits) + ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1))); + } + + if (cfg.verbose) + log(" Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses()); + } + + bool prove_equiv_cell(Cell* cell) + { + SigBit bit_a = model.sigmap(cell->getPort(ID::A)).as_bit(); + SigBit bit_b = model.sigmap(cell->getPort(ID::B)).as_bit(); + int ez_context = ez->frozen_literal(); + + prepare_ezsat(ez_context, bit_a, bit_b); + + // Two bits, bit_a, and bit_b, have been marked equivalent in the design + // We will be traversing the input cones for each of them + // In the first iteration, we will using those as starting points pool seed_a = { bit_a }; pool seed_b = { bit_b }; - if (verbose) { - log(" Trying to prove $equiv cell %s:\n", log_id(equiv_cell)); - log(" A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(equiv_cell->getPort(ID::Y))); + if (cfg.verbose) { + log(" Trying to prove $equiv cell %s:\n", log_id(cell)); + log(" A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(cell->getPort(ID::Y))); } else { - log(" Trying to prove $equiv for %s:", log_signal(equiv_cell->getPort(ID::Y))); + log(" Trying to prove $equiv for %s:", log_signal(cell->getPort(ID::Y))); } - int step = max_seq; + int step = cfg.max_seq; while (1) { - pool no_stop_cells; - pool no_stop_bits; - - pool full_cells_cone_a, full_cells_cone_b; - pool full_bits_cone_a, full_bits_cone_b; - - pool next_seed_a, next_seed_b; - - for (auto bit_a : seed_a) - find_input_cone(next_seed_a, full_cells_cone_a, full_bits_cone_a, no_stop_cells, no_stop_bits, nullptr, bit_a); - - for (auto bit_b : seed_b) - find_input_cone(next_seed_b, full_cells_cone_b, full_bits_cone_b, no_stop_cells, no_stop_bits, nullptr, bit_b); - - pool short_cells_cone_a, short_cells_cone_b; - pool short_bits_cone_a, short_bits_cone_b; - pool input_bits; - - if (short_cones) - { - next_seed_a.clear(); - for (auto bit_a : seed_a) - find_input_cone(next_seed_a, short_cells_cone_a, short_bits_cone_a, full_cells_cone_b, full_bits_cone_b, &input_bits, bit_a); - next_seed_a.swap(seed_a); - - next_seed_b.clear(); - for (auto bit_b : seed_b) - find_input_cone(next_seed_b, short_cells_cone_b, short_bits_cone_b, full_cells_cone_a, full_bits_cone_a, &input_bits, bit_b); - next_seed_b.swap(seed_b); - } - else - { - short_cells_cone_a = full_cells_cone_a; - short_bits_cone_a = full_bits_cone_a; - next_seed_a.swap(seed_a); - - short_cells_cone_b = full_cells_cone_b; - short_bits_cone_b = full_bits_cone_b; - next_seed_b.swap(seed_b); - } + // Traverse input cones of seed_a and seed_b, potentially finding new seeds + auto [input_bits, cone_a, cone_b] = init_iter(seed_a, seed_b); + // Cells to model in SAT solver pool problem_cells; - problem_cells.insert(short_cells_cone_a.begin(), short_cells_cone_a.end()); - problem_cells.insert(short_cells_cone_b.begin(), short_cells_cone_b.end()); + problem_cells.insert(cone_a.cells.begin(), cone_a.cells.end()); + problem_cells.insert(cone_b.cells.begin(), cone_b.cells.end()); - if (verbose) - { - log(" Adding %d new cells to the problem (%d A, %d B, %d shared).\n", - GetSize(problem_cells), GetSize(short_cells_cone_a), GetSize(short_cells_cone_b), - (GetSize(short_cells_cone_a) + GetSize(short_cells_cone_b)) - GetSize(problem_cells)); - #if 0 - for (auto cell : short_cells_cone_a) - log(" A-side cell: %s\n", log_id(cell)); + if (cfg.verbose) + report_new_cells(problem_cells, cone_a, cone_b); - for (auto cell : short_cells_cone_b) - log(" B-side cell: %s\n", log_id(cell)); - #endif + if (cfg.set_assumes) { + auto extras = add_assumes_to_problem(cone_a, cone_b); + if (GetSize(extras)) { + auto old_size = GetSize(problem_cells); + problem_cells.insert(extras.begin(), extras.end()); + report_new_assume_cells(extras, old_size, problem_cells); + } } for (auto cell : problem_cells) { auto key = pair(cell, step+1); if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) { - if (RTLIL::builtin_ff_cell_types().count(cell->type)) - 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)); + report_missing_model(cell); } imported_cells_cache.insert(key); } - if (satgen.model_undef) { - for (auto bit : input_bits) - ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1))); - } - - if (verbose) - log(" Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses()); + construct_ezsat(input_bits, step); if (!ez->solve(ez_context)) { - log(verbose ? " Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n"); - equiv_cell->setPort(ID::B, equiv_cell->getPort(ID::A)); + log(cfg.verbose ? " Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n"); + // Replace $equiv cell with a short + cell->setPort(ID::B, cell->getPort(ID::A)); ez->assume(ez->NOT(ez_context)); return true; } - if (verbose) - log(" Failed to prove equivalence with sequence length %d.\n", max_seq - step); + if (cfg.verbose) + log(" Failed to prove equivalence with sequence length %d.\n", cfg.max_seq - step); if (--step < 0) { - if (verbose) + if (cfg.verbose) log(" Reached sequence limit.\n"); break; } if (seed_a.empty() && seed_b.empty()) { - if (verbose) + if (cfg.verbose) log(" No nets to continue in previous time step.\n"); break; } if (seed_a.empty()) { - if (verbose) + if (cfg.verbose) log(" No nets on A-side to continue in previous time step.\n"); break; } if (seed_b.empty()) { - if (verbose) + if (cfg.verbose) log(" No nets on B-side to continue in previous time step.\n"); break; } - if (verbose) { + if (cfg.verbose) { #if 0 log(" Continuing analysis in previous time step with the following nets:\n"); for (auto bit : seed_a) @@ -248,7 +378,7 @@ struct EquivSimpleWorker } } - if (!verbose) + if (!cfg.verbose) log(" failed.\n"); ez->assume(ez->NOT(ez_context)); @@ -260,14 +390,13 @@ struct EquivSimpleWorker if (GetSize(equiv_cells) > 1) { SigSpec sig; for (auto c : equiv_cells) - sig.append(sigmap(c->getPort(ID::Y))); + sig.append(model.sigmap(c->getPort(ID::Y))); log(" Grouping SAT models for %s:\n", log_signal(sig)); } int counter = 0; for (auto c : equiv_cells) { - equiv_cell = c; - if (run_cell()) + if (prove_equiv_cell(c)) counter++; } return counter; @@ -301,35 +430,41 @@ struct EquivSimplePass : public Pass { 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"); + log("\n"); } void execute(std::vector args, Design *design) override { - bool verbose = false, short_cones = false, model_undef = false, nogroup = false; + EquivSimpleWorker::Config cfg = {}; int success_counter = 0; - int max_seq = 1; log_header(design, "Executing EQUIV_SIMPLE pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { if (args[argidx] == "-v") { - verbose = true; + cfg.verbose = true; continue; } if (args[argidx] == "-short") { - short_cones = true; + cfg.short_cones = true; continue; } if (args[argidx] == "-undef") { - model_undef = true; + cfg.model_undef = true; continue; } if (args[argidx] == "-nogroup") { - nogroup = true; + cfg.nogroup = true; continue; } if (args[argidx] == "-seq" && argidx+1 < args.size()) { - max_seq = atoi(args[++argidx].c_str()); + cfg.max_seq = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-set-assumes") { + cfg.set_assumes = true; continue; } break; @@ -347,17 +482,21 @@ struct EquivSimplePass : public Pass { SigMap sigmap(module); dict bit2driver; dict> unproven_equiv_cells; + vector assumes; int unproven_cells_counter = 0; - for (auto cell : module->selected_cells()) + for (auto cell : module->selected_cells()) { 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 (!nogroup && bit_group.wire) + if (!cfg.nogroup && bit_group.wire) bit_group.offset = 0; unproven_equiv_cells[bit_group][bit] = cell; unproven_cells_counter++; + } else if (cell->type == ID($assume)) { + assumes.push_back(cell); } + } if (unproven_equiv_cells.empty()) continue; @@ -375,15 +514,16 @@ struct EquivSimplePass : public Pass { } unproven_equiv_cells.sort(); - for (auto it : unproven_equiv_cells) + for (auto [_, d] : unproven_equiv_cells) { - it.second.sort(); + d.sort(); vector cells; - for (auto it2 : it.second) - cells.push_back(it2.second); + for (auto [_, cell] : d) + cells.push_back(cell); - EquivSimpleWorker worker(cells, sigmap, bit2driver, max_seq, short_cones, verbose, model_undef); + EquivSimpleWorker::DesignModel model {sigmap, bit2driver}; + EquivSimpleWorker worker(cells, assumes, model, cfg); success_counter += worker.run(); } } diff --git a/tests/various/equiv_assume.ys b/tests/various/equiv_assume.ys new file mode 100644 index 000000000..7ca572c8c --- /dev/null +++ b/tests/various/equiv_assume.ys @@ -0,0 +1,141 @@ +read_verilog -sv <