From c43e52d2d7d16c26b1a4a9c20fad83c9f4577910 Mon Sep 17 00:00:00 2001
From: David Shah <dave@ds0.me>
Date: Wed, 11 Sep 2019 13:55:16 +0100
Subject: [PATCH] Add equiv_opt -multiclock
Signed-off-by: David Shah <dave@ds0.me>
---
passes/equiv/equiv_opt.cc | 12 +++++++++++-
tests/various/equiv_opt_multiclock.ys | 12 ++++++++++++
2 files changed, 23 insertions(+), 1 deletion(-)
create mode 100644 tests/various/equiv_opt_multiclock.ys
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 19d1c25ac..d4c7f7953 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -46,6 +46,9 @@ struct EquivOptPass:public ScriptPass
log(" -assert\n");
log(" produce an error if the circuits are not equivalent.\n");
log("\n");
+ log(" -multiclock\n");
+ log(" run clk2fflogic before equivalence checking.\n");
+ log("\n");
log(" -undef\n");
log(" enable modelling of undef states during equiv_induct.\n");
log("\n");
@@ -55,7 +58,7 @@ struct EquivOptPass:public ScriptPass
}
std::string command, techmap_opts;
- bool assert, undef;
+ bool assert, undef, multiclock;
void clear_flags() YS_OVERRIDE
{
@@ -63,6 +66,7 @@ struct EquivOptPass:public ScriptPass
techmap_opts = "";
assert = false;
undef = false;
+ multiclock = false;
}
void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@@ -92,6 +96,10 @@ struct EquivOptPass:public ScriptPass
undef = true;
continue;
}
+ if (args[argidx] == "-multiclock") {
+ multiclock = true;
+ continue;
+ }
break;
}
@@ -146,6 +154,8 @@ struct EquivOptPass:public ScriptPass
}
if (check_label("prove")) {
+ if (multiclock || help_mode)
+ run("clk2fflogic", "(only with -multiclock)");
run("equiv_make gold gate equiv");
if (help_mode)
run("equiv_induct [-undef] equiv");
diff --git a/tests/various/equiv_opt_multiclock.ys b/tests/various/equiv_opt_multiclock.ys
new file mode 100644
index 000000000..81e36d018
--- /dev/null
+++ b/tests/various/equiv_opt_multiclock.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+module top(input clk, pre, d, output reg q);
+ always @(posedge clk, posedge pre)
+ if (pre)
+ q <= 1'b1;
+ else
+ q <= d;
+endmodule
+EOT
+
+prep
+equiv_opt -assert -multiclock -map +/simcells.v synth