summaryrefslogtreecommitdiff
path: root/passes/equiv/equiv_simple.cc
diff options
context:
space:
mode:
authorRuben Undheim <ruben.undheim@gmail.com>2018-08-30 20:46:20 +0200
committerRuben Undheim <ruben.undheim@gmail.com>2018-08-30 20:46:20 +0200
commit5033b51947a6ef02cb785b5622e993335efa750a (patch)
tree7bed18c526bd94917fa2f08e3df12209863698a1 /passes/equiv/equiv_simple.cc
parentfefe0fc0430f4f173a25e674708aa0f4f0854b31 (diff)
New upstream version 0.7+20180830git0b7a184
Diffstat (limited to 'passes/equiv/equiv_simple.cc')
-rw-r--r--passes/equiv/equiv_simple.cc59
1 files changed, 45 insertions, 14 deletions
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 49963ed6..c2fab26f 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;
}
@@ -59,7 +60,7 @@ struct EquivSimpleWorker
for (auto &conn : cell->connections())
if (yosys_celltypes.cell_input(cell->type, conn.first))
for (auto bit : sigmap(conn.second)) {
- if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) {
+ if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) {
if (!conn.first.in("\\CLK", "\\C"))
next_seed.insert(bit);
} else
@@ -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);
@@ -250,7 +273,7 @@ struct EquivSimpleWorker
struct EquivSimplePass : public Pass {
EquivSimplePass() : Pass("equiv_simple", "try proving simple $equiv instances") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -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");
@@ -271,9 +298,9 @@ struct EquivSimplePass : public Pass {
log(" the max. number of time steps to be considered (default = 1)\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, Design *design)
+ void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
{
- 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;
@@ -329,7 +360,7 @@ struct EquivSimplePass : public Pass {
unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module));
for (auto cell : module->cells()) {
- if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
+ if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
continue;
for (auto &conn : cell->connections())
if (yosys_celltypes.cell_output(cell->type, conn.first))
@@ -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();
}
}