From: David Shah <dave@ds0.me>
Date: Wed, 11 Sep 2019 12:55:16 +0000 (+0100)
Subject: Add equiv_opt -multiclock
X-Git-Tag: working-ls180~1068^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c43e52d2d7d16c26b1a4a9c20fad83c9f4577910;p=yosys.git

Add equiv_opt -multiclock

Signed-off-by: David Shah <dave@ds0.me>
---

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