riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Fix equiv_simple, old behavior now available with "equiv_simple -short"

This commit is contained in:
Clifford Wolf 2017-04-28 18:54:53 +02:00
parent f0db8ffdbc
commit 3bbac5c141
1 changed files with 41 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
passes/equiv/equiv_simple.cc
View File

@ -35,13 +35,14 @@ struct EquivSimpleWorker
ezSatPtr ez; ezSatPtr ez;
SatGen satgen; SatGen satgen;
int max_seq; int max_seq;
bool short_cones;
bool verbose; bool verbose;
pool<pair<Cell*, int>> imported_cells_cache; 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), 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; satgen.model_undef = model_undef;
} }
@ -142,22 +143,44 @@ struct EquivSimpleWorker
pool<SigBit> short_bits_cone_a, short_bits_cone_b; pool<SigBit> short_bits_cone_a, short_bits_cone_b;
pool<SigBit> input_bits; pool<SigBit> input_bits;
for (auto bit_a : seed_a) if (short_cones)
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_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) 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); 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); 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; pool<Cell*> problem_cells;
problem_cells.insert(short_cells_cone_a.begin(), short_cells_cone_a.end()); 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(short_cells_cone_b.begin(), short_cells_cone_b.end());
if (verbose) if (verbose)
{
log(" Adding %d new cells to the problem (%d A, %d B, %d shared).\n", 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(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)); (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) { for (auto cell : problem_cells) {
auto key = pair<Cell*, int>(cell, step+1); auto key = pair<Cell*, int>(cell, step+1);
@ -264,6 +287,10 @@ struct EquivSimplePass : public Pass {
log(" -undef\n"); log(" -undef\n");
log(" enable modelling of undef states\n"); log(" enable modelling of undef states\n");
log("\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(" -nogroup\n");
log(" disabling grouping of $equiv cells by output wire\n"); log(" disabling grouping of $equiv cells by output wire\n");
log("\n"); log("\n");
@ -273,7 +300,7 @@ struct EquivSimplePass : public Pass {
} }
virtual void execute(std::vector<std::string> args, Design *design) 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 success_counter = 0;
int max_seq = 1; int max_seq = 1;
@ -285,6 +312,10 @@ struct EquivSimplePass : public Pass {
verbose = true; verbose = true;
continue; continue;
} }
if (args[argidx] == "-short") {
short_cones = true;
continue;
}
if (args[argidx] == "-undef") { if (args[argidx] == "-undef") {
model_undef = true; model_undef = true;
continue; continue;
@ -346,7 +377,7 @@ struct EquivSimplePass : public Pass {
for (auto it2 : it.second) for (auto it2 : it.second)
cells.push_back(it2.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(); success_counter += worker.run();
} }
} }