From ca5b910296c05c95f3bc7f2d1d2b7db19d6328e2 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 1 Apr 2022 21:03:20 +0200
Subject: 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.
---
 passes/opt/opt.cc       |  1 +
 passes/opt/opt_merge.cc | 22 ++++++++++++++++++++--
 2 files changed, 21 insertions(+), 2 deletions(-)

(limited to 'passes')

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;
 		}
 
-- 
cgit v1.2.3