diff options
Diffstat (limited to 'passes/equiv')
| -rw-r--r-- | passes/equiv/equiv_simple.cc | 51 |
1 files changed, 41 insertions, 10 deletions
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 270200c34..e69e17ac6 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -35,13 +35,14 @@ struct EquivSimpleWorker ezSatPtr ez; SatGen satgen; int max_seq; + bool short_cones; bool verbose; pool<pair<Cell*, int>> imported_cells_cache; - EquivSimpleWorker(const vector<Cell*> &equiv_cells, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool verbose, bool model_undef) : + EquivSimpleWorker(const vector<Cell*> &equiv_cells, SigMap &sigmap, dict<SigBit, Cell*> &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), verbose(verbose) + sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), short_cones(short_cones), verbose(verbose) { satgen.model_undef = model_undef; } @@ -142,22 +143,44 @@ struct EquivSimpleWorker pool<SigBit> short_bits_cone_a, short_bits_cone_b; pool<SigBit> input_bits; - 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); + if (short_cones) + { + 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); - 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); + 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); + } pool<Cell*> 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()); 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)); + + for (auto cell : short_cells_cone_b) + log(" B-side cell: %s\n", log_id(cell)); + #endif + } for (auto cell : problem_cells) { auto key = pair<Cell*, int>(cell, step+1); @@ -264,6 +287,10 @@ struct EquivSimplePass : public Pass { 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"); @@ -273,7 +300,7 @@ struct EquivSimplePass : public Pass { } virtual void execute(std::vector<std::string> args, Design *design) { - bool verbose = false, model_undef = false, nogroup = false; + bool verbose = false, short_cones = false, model_undef = false, nogroup = false; int success_counter = 0; int max_seq = 1; @@ -285,6 +312,10 @@ struct EquivSimplePass : public Pass { verbose = true; continue; } + if (args[argidx] == "-short") { + short_cones = true; + continue; + } if (args[argidx] == "-undef") { model_undef = true; continue; @@ -346,7 +377,7 @@ struct EquivSimplePass : public Pass { for (auto it2 : it.second) cells.push_back(it2.second); - EquivSimpleWorker worker(cells, sigmap, bit2driver, max_seq, verbose, model_undef); + EquivSimpleWorker worker(cells, sigmap, bit2driver, max_seq, short_cones, verbose, model_undef); success_counter += worker.run(); } } |