From 0e56ca02ed99bacd6668e64de2dc054dd256d9f1 Mon Sep 17 00:00:00 2001
From: nella <simontupy64@gmail.com>
Date: Mon, 6 Jul 2026 13:47:10 +0200
Subject: [PATCH] Make opt_dff -sat conflict with -keepdc.

---
 passes/opt/opt_dff.cc       | 13 +++++++++++--
 tests/opt/opt_dff_eqbits.ys | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc
index 1b1c3bf0e..fcb961125 100644
--- a/passes/opt/opt_dff.cc
+++ b/passes/opt/opt_dff.cc
@@ -1071,7 +1071,7 @@ struct OptDffWorker
 			ff_for_cell.emplace(cell, ff);
 
 			for (int i = 0; i < ff.width; i++) {
-				// Skip bits whose reset drives an undefined (x) value
+				// Skip bits whose reset value is undefined (x)
 				if (ff.has_srst && !is_def(ff.val_srst[i])) continue;
 				if (ff.has_arst && !is_def(ff.val_arst[i])) continue;
 
@@ -1424,7 +1424,9 @@ struct OptDffPass : public Pass {
 		log("\n");
 		log("    -sat\n");
 		log("        additionally invoke SAT solver to detect and remove flip-flops (with\n");
-		log("        non-constant inputs) that can also be replaced with a constant driver\n");
+		log("        non-constant inputs) that can also be replaced with a constant driver,\n");
+		log("        or merged with equivalent flip-flops. this reasons in 2-valued logic\n");
+		log("        and may resolve don't-care bits, so it is incompatible with -keepdc.\n");
 		log("\n");
 		log("    -keepdc\n");
 		log("        some optimizations change the behavior of the circuit with respect to\n");
@@ -1456,6 +1458,13 @@ struct OptDffPass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
+		// The SAT engine reasons in 2-valued logic (a constant x is treated as
+		// 0), so it can resolve don't-care bits to concrete values -- exactly
+		// what -keepdc promises not to do. Refuse the combination rather than
+		// silently ignore -keepdc.
+		if (opt.sat && opt.keepdc)
+			log_cmd_error("The -sat and -keepdc options are mutually exclusive.\n");
+
 		bool did_something = false;
 		for (auto mod : design->selected_modules()) {
 			OptDffWorker worker(opt, mod);
diff --git a/tests/opt/opt_dff_eqbits.ys b/tests/opt/opt_dff_eqbits.ys
index 10e9045e4..f990fe71a 100644
--- a/tests/opt/opt_dff_eqbits.ys
+++ b/tests/opt/opt_dff_eqbits.ys
@@ -54,3 +54,36 @@ design -copy-from gate -as gate test_case
 equiv_make gold gate equiv
 equiv_induct equiv
 equiv_status -assert
+
+# verify keepdc exclusivity
+design -reset
+read_verilog -sv <<EOT
+module test_case(input clk, input d, output reg a, output reg b);
+	initial a = 1'b0;
+	initial b = 1'b0;
+	always @(posedge clk) a <= d;
+	always @(posedge clk) b <= d | 1'bx;
+endmodule
+EOT
+hierarchy -top test_case
+proc
+techmap
+opt_dff -sat
+opt_clean -purge
+select -assert-count 1 t:$_DFF_P_
+
+
+design -reset
+read_verilog -sv <<EOT
+module test_case(input clk, input d, output reg a, output reg b);
+	initial a = 1'b0;
+	initial b = 1'b0;
+	always @(posedge clk) a <= d;
+	always @(posedge clk) b <= d | 1'bx;
+endmodule
+EOT
+hierarchy -top test_case
+proc
+techmap
+logger -expect error "The -sat and -keepdc options are mutually exclusive." 1
+opt_dff -sat -keepdc