From: Jannis Harder <me@jix.one>
Date: Fri, 1 Apr 2022 19:03:20 +0000 (+0200)
Subject: opt_merge: Add `-keepdc` option required for formal verification
X-Git-Tag: yosys-0.16~5^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca5b910296c05c95f3bc7f2d1d2b7db19d6328e2;p=yosys.git

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 c3e418c07..dc88563c2 100644
--- 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 115eb97a9..e9d98cd43 100644
--- 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 20b6cabee..7ee7d3dd7 100644
--- 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