summaryrefslogtreecommitdiff
path: root/passes/equiv
diff options
context:
space:
mode:
Diffstat (limited to 'passes/equiv')
-rw-r--r--passes/equiv/equiv_add.cc4
-rw-r--r--passes/equiv/equiv_induct.cc4
-rw-r--r--passes/equiv/equiv_make.cc8
-rw-r--r--passes/equiv/equiv_mark.cc4
-rw-r--r--passes/equiv/equiv_miter.cc4
-rw-r--r--passes/equiv/equiv_purge.cc8
-rw-r--r--passes/equiv/equiv_remove.cc4
-rw-r--r--passes/equiv/equiv_simple.cc59
-rw-r--r--passes/equiv/equiv_status.cc4
-rw-r--r--passes/equiv/equiv_struct.cc4
10 files changed, 67 insertions, 36 deletions
diff --git a/passes/equiv/equiv_add.cc b/passes/equiv/equiv_add.cc
index 0494a724..71599f46 100644
--- a/passes/equiv/equiv_add.cc
+++ b/passes/equiv/equiv_add.cc
@@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN
struct EquivAddPass : public Pass {
EquivAddPass() : Pass("equiv_add", "add a $equiv cell") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -39,7 +39,7 @@ struct EquivAddPass : public Pass {
log("This command adds $equiv cells for the ports of the specified cells.\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 try_mode = false;
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index c958c3de..bcc68d6d 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -162,7 +162,7 @@ struct EquivInductWorker
struct EquivInductPass : public Pass {
EquivInductPass() : Pass("equiv_induct", "proving $equiv cells using temporal induction") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -192,7 +192,7 @@ struct EquivInductPass : public Pass {
log("after reset.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, Design *design)
+ void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
{
int success_counter = 0;
bool model_undef = false;
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 40ca4262..b1f88d55 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -260,11 +260,11 @@ struct EquivMakeWorker
for (int i = 0; i < wire->width; i++) {
if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
- log(" Skipping signal bit %d: undriven on gold side.\n", i);
+ log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
continue;
}
if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
- log(" Skipping signal bit %d: undriven on gate side.\n", i);
+ log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
continue;
}
equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
@@ -390,7 +390,7 @@ struct EquivMakeWorker
struct EquivMakePass : public Pass {
EquivMakePass() : Pass("equiv_make", "prepare a circuit for equivalence checking") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -415,7 +415,7 @@ struct EquivMakePass : public Pass {
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
EquivMakeWorker worker;
worker.ct.setup(design);
diff --git a/passes/equiv/equiv_mark.cc b/passes/equiv/equiv_mark.cc
index 22c50176..135eaf14 100644
--- a/passes/equiv/equiv_mark.cc
+++ b/passes/equiv/equiv_mark.cc
@@ -204,7 +204,7 @@ struct EquivMarkWorker
struct EquivMarkPass : public Pass {
EquivMarkPass() : Pass("equiv_mark", "mark equivalence checking regions") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -216,7 +216,7 @@ struct EquivMarkPass : public Pass {
log("wires and cells.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, Design *design)
+ void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
{
log_header(design, "Executing EQUIV_MARK pass.\n");
diff --git a/passes/equiv/equiv_miter.cc b/passes/equiv/equiv_miter.cc
index eb2e5a17..e06f9515 100644
--- a/passes/equiv/equiv_miter.cc
+++ b/passes/equiv/equiv_miter.cc
@@ -261,7 +261,7 @@ struct EquivMiterWorker
struct EquivMiterPass : public Pass {
EquivMiterPass() : Pass("equiv_miter", "extract miter from equiv circuit") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -282,7 +282,7 @@ struct EquivMiterPass : public Pass {
log(" Create compare logic that handles undefs correctly\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
EquivMiterWorker worker;
worker.ct.setup(design);
diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc
index 163b1009..18b3e7d3 100644
--- a/passes/equiv/equiv_purge.cc
+++ b/passes/equiv/equiv_purge.cc
@@ -80,7 +80,7 @@ struct EquivPurgeWorker
Wire *wire = module->addWire(name, GetSize(sig));
wire->port_input = true;
module->connect(sig, wire);
- log(" Module input: %s\n", log_signal(wire));
+ log(" Module input: %s (%s)\n", log_signal(wire), log_signal(sig));
return module->addWire(NEW_ID, GetSize(sig));
}
}
@@ -142,7 +142,7 @@ struct EquivPurgeWorker
for (auto bit : queue)
visited.insert(bit);
-
+
for (auto bit : queue)
{
auto &cells = up_bit2cells[bit];
@@ -176,7 +176,7 @@ struct EquivPurgeWorker
struct EquivPurgePass : public Pass {
EquivPurgePass() : Pass("equiv_purge", "purge equivalence checking module") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -187,7 +187,7 @@ struct EquivPurgePass : public Pass {
log("ports as needed.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, Design *design)
+ void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
{
log_header(design, "Executing EQUIV_PURGE pass.\n");
diff --git a/passes/equiv/equiv_remove.cc b/passes/equiv/equiv_remove.cc
index 770497a5..c5c28c7d 100644
--- a/passes/equiv/equiv_remove.cc
+++ b/passes/equiv/equiv_remove.cc
@@ -24,7 +24,7 @@ PRIVATE_NAMESPACE_BEGIN
struct EquivRemovePass : public Pass {
EquivRemovePass() : Pass("equiv_remove", "remove $equiv cells") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -40,7 +40,7 @@ struct EquivRemovePass : public Pass {
log(" keep gate circuit\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 mode_gold = false;
bool mode_gate = false;
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();
}
}
diff --git a/passes/equiv/equiv_status.cc b/passes/equiv/equiv_status.cc
index 7b9230b3..b4a93ccf 100644
--- a/passes/equiv/equiv_status.cc
+++ b/passes/equiv/equiv_status.cc
@@ -24,7 +24,7 @@ PRIVATE_NAMESPACE_BEGIN
struct EquivStatusPass : public Pass {
EquivStatusPass() : Pass("equiv_status", "print status of equivalent checking module") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -36,7 +36,7 @@ struct EquivStatusPass : public Pass {
log(" produce an error if any unproven $equiv cell is found\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 assert_mode = false;
int unproven_count = 0;
diff --git a/passes/equiv/equiv_struct.cc b/passes/equiv/equiv_struct.cc
index c4ced6a7..a7973fd0 100644
--- a/passes/equiv/equiv_struct.cc
+++ b/passes/equiv/equiv_struct.cc
@@ -283,7 +283,7 @@ struct EquivStructWorker
struct EquivStructPass : public Pass {
EquivStructPass() : Pass("equiv_struct", "structural equivalence checking") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -314,7 +314,7 @@ struct EquivStructPass : public Pass {
log(" maximum number of iterations to run before aborting\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, Design *design)
+ void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
{
pool<IdString> fwonly_cells({ "$equiv" });
bool mode_icells = false;
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-01 07:14:23 +0000