aboutsummaryrefslogtreecommitdiffstats
path: root/passes/equiv
diff options
context:
space:
mode:
Diffstat (limited to 'passes/equiv')
-rw-r--r--passes/equiv/equiv_simple.cc51
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();
}
}