From 778079b058a54c3d935bb4e39a8aa26957fb14dd Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Tue, 24 Jun 2025 12:01:12 +0200
Subject: [PATCH] dfflibmap: propagate negated next_state to output correctly

---
 passes/techmap/dfflibmap.cc                |  18 +++-
 tests/techmap/dfflibmap_dffsr_not_next.lib |  28 +++++
 tests/techmap/dfflibmap_formal.ys          | 116 +++++++++++++++++++++
 3 files changed, 160 insertions(+), 2 deletions(-)
 create mode 100644 tests/techmap/dfflibmap_dffsr_not_next.lib
 create mode 100644 tests/techmap/dfflibmap_formal.ys

diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index d00fee83b..f0b0ef20b 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -392,9 +392,21 @@ static void find_cell_sr(std::vector<const LibertyAst *> cells, IdString cell_ty
 			continue;
 		if (!parse_next_state(cell, ff->find("next_state"), cell_next_pin, cell_next_pol, cell_enable_pin, cell_enable_pol))
 			continue;
-		if (!parse_pin(cell, ff->find("preset"), cell_set_pin, cell_set_pol) || cell_set_pol != setpol)
+
+		if (!parse_pin(cell, ff->find("preset"), cell_set_pin, cell_set_pol))
 			continue;
-		if (!parse_pin(cell, ff->find("clear"), cell_clr_pin, cell_clr_pol) || cell_clr_pol != clrpol)
+		if (!parse_pin(cell, ff->find("clear"), cell_clr_pin, cell_clr_pol))
+			continue;
+		if (!cell_next_pol) {
+			// next_state is negated
+			// we later propagate this inversion to the output,
+			// which requires the swap of set and reset
+			std::swap(cell_set_pin, cell_clr_pin);
+			std::swap(cell_set_pol, cell_clr_pol);
+		}
+		if (cell_set_pol != setpol)
+			continue;
+		if (cell_clr_pol != clrpol)
 			continue;
 
 		std::map<std::string, char> this_cell_ports;
@@ -432,12 +444,14 @@ static void find_cell_sr(std::vector<const LibertyAst *> cells, IdString cell_ty
 				for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t"))
 					value.erase(pos, 1);
 				if (value == ff->args[0]) {
+					// next_state negation propagated to output
 					this_cell_ports[pin->args[0]] = cell_next_pol ? 'Q' : 'q';
 					if (cell_next_pol)
 						found_noninv_output = true;
 					found_output = true;
 				} else
 				if (value == ff->args[1]) {
+					// next_state negation propagated to output
 					this_cell_ports[pin->args[0]] = cell_next_pol ? 'q' : 'Q';
 					if (!cell_next_pol)
 						found_noninv_output = true;
diff --git a/tests/techmap/dfflibmap_dffsr_not_next.lib b/tests/techmap/dfflibmap_dffsr_not_next.lib
new file mode 100644
index 000000000..579dedb10
--- /dev/null
+++ b/tests/techmap/dfflibmap_dffsr_not_next.lib
@@ -0,0 +1,28 @@
+library (test_not_next) {
+  cell (dffsr_not_next) {
+    area : 1.0;
+    pin (Q) {
+      direction : output;
+      function : "STATE";
+    }
+    pin (CLK) {
+      clock : true;
+      direction : input;
+    }
+    pin (D) {
+      direction : input;
+    }
+    pin (RN) {
+      direction : input;
+    }
+    pin (SN) {
+      direction : input;
+    }
+    ff (STATE,STATEN) {
+      clear : "!SN";
+      clocked_on : "CLK";
+      next_state : "!D";
+      preset : "!RN";
+    }
+  }
+}
\ No newline at end of file
diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys
new file mode 100644
index 000000000..11c90ea6c
--- /dev/null
+++ b/tests/techmap/dfflibmap_formal.ys
@@ -0,0 +1,116 @@
+##################################################################
+
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+// Formal checking of directly instantiated DFFSR doesn't work at the moment
+// likely due to an equiv_induct assume bug #5196
+
+// // Workaround for DFFSR bug #5194
+// assume property (~R || ~S);
+// $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+// $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffn_dffe.lib
+read_liberty dfflibmap_dffsr_not_next.lib
+
+copy top top_unmapped
+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 -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+// Formal checking of directly instantiated DFFSR doesn't work at the moment
+// likely due to an equiv_induct assume bug #5196
+
+// // Workaround for DFFSR bug #5194
+// assume property (~R || ~S);
+// $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+// $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffr_not_next.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffr_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, E, S, R, output Q);
+// DFFSR with priority R over S
+always @(posedge C, posedge R, posedge S)
+    if (R == 1)
+        Q <= 0;
+    else if (S == 1)
+        Q <= 1;
+    else
+        Q <= D;
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffn_dffe.lib
+read_liberty dfflibmap_dffsr_not_next.lib
+
+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
\ No newline at end of file