opt_merge: Add `-keepdc` option required for formal verification

The `-keepdc` option prevents merging flipflops with dont-care bits in
their initial value, as, in general, this is not a valid transform for
formal verification.

The keepdc option of `opt` is passed along to `opt_merge` now.

diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index c3e418c075de481cd25b765a40c37f9144f10619..dc88563c23633fa596bd7e161c87272f406075ec 100644 (file)
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -114,6 +114,7 @@ struct OptPass : public Pass {
                        if (args[argidx] == "-keepdc") {
                                opt_expr_args += " -keepdc";
                                opt_dff_args += " -keepdc";
+                               opt_merge_args += " -keepdc";
                                continue;
                        }
                        if (args[argidx] == "-nodffe") {

diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc
index 115eb97a92366eb24c9bca4cd84943a8962a6368..e9d98cd4304c811eef78feccdb94cf994af76b49 100644 (file)
--- a/passes/opt/opt_merge.cc
+++ b/passes/opt/opt_merge.cc
@@ -219,7 +219,15 @@ struct OptMergeWorker
                return conn1 == conn2;
        }
 
-       OptMergeWorker(RTLIL::Design *design, RTLIL::Module *module, bool mode_nomux, bool mode_share_all) :
+       bool has_dont_care_initval(const RTLIL::Cell *cell)
+       {
+               if (!RTLIL::builtin_ff_cell_types().count(cell->type))
+                       return false;
+
+               return !initvals(cell->getPort(ID::Q)).is_fully_def();
+       }
+
+       OptMergeWorker(RTLIL::Design *design, RTLIL::Module *module, bool mode_nomux, bool mode_share_all, bool mode_keepdc) :
                design(design), module(module), assign_map(module), mode_share_all(mode_share_all)
        {
                total_count = 0;
@@ -253,6 +261,8 @@ struct OptMergeWorker
                        for (auto &it : module->cells_) {
                                if (!design->selected(module, it.second))
                                        continue;
+                               if (mode_keepdc && has_dont_care_initval(it.second))
+                                       continue;
                                if (ct.cell_known(it.second->type) || (mode_share_all && it.second->known()))
                                        cells.push_back(it.second);
                        }
@@ -319,6 +329,9 @@ struct OptMergePass : public Pass {
                log("    -share_all\n");
                log("        Operate on all cell types, not just built-in types.\n");
                log("\n");
+               log("    -keepdc\n");
+               log("        Do not merge flipflops with don't-care bits in their initial value.\n");
+               log("\n");
        }
        void execute(std::vector<std::string> args, RTLIL::Design *design) override
        {
@@ -326,6 +339,7 @@ struct OptMergePass : public Pass {
 
                bool mode_nomux = false;
                bool mode_share_all = false;
+               bool mode_keepdc = false;
 
                size_t argidx;
                for (argidx = 1; argidx < args.size(); argidx++) {
@@ -338,13 +352,17 @@ struct OptMergePass : public Pass {
                                mode_share_all = true;
                                continue;
                        }
+                       if (arg == "-keepdc") {
+                               mode_keepdc = true;
+                               continue;
+                       }
                        break;
                }
                extra_args(args, argidx, design);
 
                int total_count = 0;
                for (auto module : design->selected_modules()) {
-                       OptMergeWorker worker(design, module, mode_nomux, mode_share_all);
+                       OptMergeWorker worker(design, module, mode_nomux, mode_share_all, mode_keepdc);
                        total_count += worker.total_count;
                }
 

diff --git a/tests/opt/opt_merge_init.ys b/tests/opt/opt_merge_init.ys
index 20b6cabee160ad6df44601136b3a42155d5638bb..7ee7d3dd748883b212e9e1fb470e6f4a69cf4178 100644 (file)
--- a/tests/opt/opt_merge_init.ys
+++ b/tests/opt/opt_merge_init.ys
@@ -75,3 +75,53 @@ EOT
 
 opt_merge
 select -assert-count 2 t:$dff
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, (* init = 1'b0 *) output o, p);
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ffo  (
+    .CLK(clk),
+    .D(i),
+    .Q(o)
+  );
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ffp  (
+    .CLK(clk),
+    .D(i),
+    .Q(p)
+  );
+endmodule
+EOT
+
+opt_merge -keepdc
+select -assert-count 1 t:$dff
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, output o, p);
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ffo  (
+    .CLK(clk),
+    .D(i),
+    .Q(o)
+  );
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ffp  (
+    .CLK(clk),
+    .D(i),
+    .Q(p)
+  );
+endmodule
+EOT
+
+opt_merge -keepdc
+select -assert-count 2 t:$dff