aboutsummaryrefslogtreecommitdiffstats
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.cc8
-rw-r--r--passes/equiv/equiv_make.cc12
-rw-r--r--passes/equiv/equiv_mark.cc4
-rw-r--r--passes/equiv/equiv_miter.cc4
-rw-r--r--passes/equiv/equiv_opt.cc8
-rw-r--r--passes/equiv/equiv_purge.cc8
-rw-r--r--passes/equiv/equiv_remove.cc4
-rw-r--r--passes/equiv/equiv_simple.cc4
-rw-r--r--passes/equiv/equiv_status.cc4
-rw-r--r--passes/equiv/equiv_struct.cc4
11 files changed, 33 insertions, 31 deletions
diff --git a/passes/equiv/equiv_add.cc b/passes/equiv/equiv_add.cc
index cdc74b0b2..2abbb59bb 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") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
bool try_mode = false;
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index ec651193e..37aec50cd 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -65,8 +65,10 @@ struct EquivInductWorker
int ez_a = satgen.importSigBit(bit_a, step);
int ez_b = satgen.importSigBit(bit_b, step);
int cond = ez->IFF(ez_a, ez_b);
- if (satgen.model_undef)
+ if (satgen.model_undef) {
+ cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_b, step)));
cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step));
+ }
ez_equal_terms.push_back(cond);
}
}
@@ -162,7 +164,7 @@ struct EquivInductWorker
struct EquivInductPass : public Pass {
EquivInductPass() : Pass("equiv_induct", "proving $equiv cells using temporal induction") { }
- void help() YS_OVERRIDE
+ void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -192,7 +194,7 @@ struct EquivInductPass : public Pass {
log("after reset.\n");
log("\n");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
int success_counter = 0;
bool model_undef = false;
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 50572ae5c..6923ae3d0 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -114,25 +114,25 @@ struct EquivMakeWorker
Module *gate_clone = gate_mod->clone();
for (auto it : gold_clone->wires().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
wire_names.insert(it->name);
gold_clone->rename(it, it->name.str() + "_gold");
}
for (auto it : gold_clone->cells().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
cell_names.insert(it->name);
gold_clone->rename(it, it->name.str() + "_gold");
}
for (auto it : gate_clone->wires().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
wire_names.insert(it->name);
gate_clone->rename(it, it->name.str() + "_gate");
}
for (auto it : gate_clone->cells().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
cell_names.insert(it->name);
gate_clone->rename(it, it->name.str() + "_gate");
}
@@ -466,7 +466,7 @@ struct EquivMakeWorker
struct EquivMakePass : public Pass {
EquivMakePass() : Pass("equiv_make", "prepare a circuit for equivalence checking") { }
- void help() YS_OVERRIDE
+ void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -491,7 +491,7 @@ struct EquivMakePass : public Pass {
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
EquivMakeWorker worker;
worker.ct.setup(design);
diff --git a/passes/equiv/equiv_mark.cc b/passes/equiv/equiv_mark.cc
index 737de25d9..a722b5ed6 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") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
log_header(design, "Executing EQUIV_MARK pass.\n");
diff --git a/passes/equiv/equiv_miter.cc b/passes/equiv/equiv_miter.cc
index 085970189..e028f806a 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") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
EquivMiterWorker worker;
worker.ct.setup(design);
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 7c6c2e685..4d0400448 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -26,7 +26,7 @@ struct EquivOptPass:public ScriptPass
{
EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { }
- void help() YS_OVERRIDE
+ void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -68,7 +68,7 @@ struct EquivOptPass:public ScriptPass
std::string command, techmap_opts, make_opts;
bool assert, undef, multiclock, async2sync;
- void clear_flags() YS_OVERRIDE
+ void clear_flags() override
{
command = "";
techmap_opts = "";
@@ -79,7 +79,7 @@ struct EquivOptPass:public ScriptPass
async2sync = false;
}
- void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
+ void execute(std::vector < std::string > args, RTLIL::Design * design) override
{
string run_from, run_to;
clear_flags();
@@ -148,7 +148,7 @@ struct EquivOptPass:public ScriptPass
log_pop();
}
- void script() YS_OVERRIDE
+ void script() override
{
if (check_label("run_pass")) {
run("hierarchy -auto-top");
diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc
index 688c20f43..a43ecec5a 100644
--- a/passes/equiv/equiv_purge.cc
+++ b/passes/equiv/equiv_purge.cc
@@ -35,7 +35,7 @@ struct EquivPurgeWorker
{
if (sig.is_wire()) {
Wire *wire = sig.as_wire();
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
if (!wire->port_output) {
log(" Module output: %s (%s)\n", log_signal(wire), log_id(cellname));
wire->port_output = true;
@@ -62,7 +62,7 @@ struct EquivPurgeWorker
{
if (sig.is_wire()) {
Wire *wire = sig.as_wire();
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
if (!wire->port_output) {
log(" Module input: %s\n", log_signal(wire));
wire->port_input = true;
@@ -176,7 +176,7 @@ struct EquivPurgeWorker
struct EquivPurgePass : public Pass {
EquivPurgePass() : Pass("equiv_purge", "purge equivalence checking module") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
log_header(design, "Executing EQUIV_PURGE pass.\n");
diff --git a/passes/equiv/equiv_remove.cc b/passes/equiv/equiv_remove.cc
index 6daa112b5..89442308b 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") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
bool mode_gold = false;
bool mode_gate = false;
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 4d2839f4d..408c5a793 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -273,7 +273,7 @@ struct EquivSimpleWorker
struct EquivSimplePass : public Pass {
EquivSimplePass() : Pass("equiv_simple", "try proving simple $equiv instances") { }
- void help() YS_OVERRIDE
+ void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -298,7 +298,7 @@ struct EquivSimplePass : public Pass {
log(" the max. number of time steps to be considered (default = 1)\n");
log("\n");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
bool verbose = false, short_cones = false, model_undef = false, nogroup = false;
int success_counter = 0;
diff --git a/passes/equiv/equiv_status.cc b/passes/equiv/equiv_status.cc
index 258e2e45b..2db44ea90 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") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
bool assert_mode = false;
int unproven_count = 0;
diff --git a/passes/equiv/equiv_struct.cc b/passes/equiv/equiv_struct.cc
index 1b7bf96a8..9784225db 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") { }
- void help() YS_OVERRIDE
+ void help() 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");
}
- void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, Design *design) override
{
pool<IdString> fwonly_cells({ ID($equiv) });
bool mode_icells = false;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-09 04:26:00 +0000