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 19d1c25acbfcc9fe2cac6d6fb5513d636ee75d97..d4c7f79535b58696d38bace618a72ccd124443d0 100644 (file)
--- 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 (file)
index 0000000..81e36d0
--- /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