From b2fe335b2d3270a565d5b46d7a64d4c8b88800bb Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Tue, 28 Oct 2025 13:01:26 +0100
Subject: [PATCH] dfflibmap: fix next_state inversion propagation for DFF flops
 by inverting reset value polarity

---
 passes/techmap/dfflibmap.cc              |  7 ++++++
 tests/techmap/dfflibmap_dff_not_next.lib | 24 ++++++++++++++++++
 tests/techmap/dfflibmap_formal.ys        | 31 ++++++++++++++++++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 tests/techmap/dfflibmap_dff_not_next.lib

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index f2bd16082..6d55d1b43 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -271,6 +271,13 @@ static void find_cell(std::vector<const LibertyAst *> cells, IdString cell_type,
 			continue;
 		if (!parse_next_state(cell, ff->find("next_state"), cell_next_pin, cell_next_pol, cell_enable_pin, cell_enable_pol) || (has_enable && (cell_enable_pin.empty() || cell_enable_pol != enapol)))
 			continue;
+
+		if (has_reset && !cell_next_pol) {
+			// next_state is negated
+			// we later propagate this inversion to the output,
+			// which requires the negation of the reset value
+			rstval = !rstval;
+		}
 		if (has_reset && rstval == false) {
 			if (!parse_pin(cell, ff->find("clear"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol)
 				continue;
diff --git a/tests/techmap/dfflibmap_dff_not_next.lib b/tests/techmap/dfflibmap_dff_not_next.lib
new file mode 100644
index 000000000..0a0b011de
--- /dev/null
+++ b/tests/techmap/dfflibmap_dff_not_next.lib
@@ -0,0 +1,24 @@
+library (test_not_next) {
+  cell (dff_not_next) {
+    area: 1.0;
+    pin (QN) {
+      direction : output;
+      function : "STATE";
+    }
+    pin (CLK) {
+      direction : input;
+      clock : true;
+    }
+    pin (D) {
+      direction : input;
+    }
+    pin (RN) {
+      direction : input;
+    }
+    ff (STATE, STATEN) {
+      clocked_on: "CLK";
+      next_state: "!D";
+      preset : "!RN";
+    }
+  }
+}
diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys
index 11c90ea6c..71a52a261 100644
--- a/tests/techmap/dfflibmap_formal.ys
+++ b/tests/techmap/dfflibmap_formal.ys
@@ -108,6 +108,37 @@ copy top top_unmapped
 simplemap top
 dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
 
+async2sync
+flatten
+opt_clean -purge
+equiv_make top top_unmapped equiv
+equiv_induct equiv
+equiv_status -assert equiv
+
+##################################################################
+
+design -reset
+read_verilog <<EOT
+
+module top(input C, D, R, output Q);
+  // DFF with preset
+  always @(posedge C or negedge R) begin
+    if (!R) Q <= 1'b1;
+    else Q <= D;
+  end
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffn_dffe.lib
+read_liberty dfflibmap_dff_not_next.lib
+
+copy top top_unmapped
+simplemap top
+dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top
+
 async2sync
 flatten
 opt_clean -purge