Merge pull request #5190 from YosysHQ/emil/dfflibmap-fix-negated-next_state

dfflibmap: propagate negated next_state to output correctly

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;

tests/techmap/dfflibmap.ys

@@ -81,3 +81,19 @@ clean
 select -assert-count 0 t:dffn
 select -assert-count 5 t:dffsr
 select -assert-count 1 t:dffe
+
+design -load orig
+dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
+clean
+# We have one more _NOT_ than with the regular dffsr
+select -assert-count 6 t:$_NOT_
+select -assert-count 1 t:dffn
+select -assert-count 4 t:dffsr_mixedpol
+select -assert-count 1 t:dffe
+# The additional NOT is on ff2.
+# Originally, ff2.R is an active high "set".
+# dffsr_mixedpol has functionally swapped labels due to the next_state inversion,
+# so we use its CLEAR port for the "set",
+# but we have to invert it because the CLEAR pin is active low.
+# ff2.CLEAR = !R
+select -assert-count 1 c:ff2 %x:+[CLEAR] %ci t:$_NOT_ %i

tests/techmap/dfflibmap_dffr_not_next.lib

@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffr_not_next) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "!D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : L;
+      clear_preset_var2 : L;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}

tests/techmap/dfflibmap_dffsr_mixedpol.lib

@@ -0,0 +1,35 @@
+library(test) {
+  cell (dffsr_mixedpol) {
+    area : 6;
+    ff("IQ", "IQN") {
+      // look here
+      next_state : "!D";
+      clocked_on : "CLK";
+      // look here
+      clear      : "!CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : L;
+      clear_preset_var2 : L;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}

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";
+    }
+  }
+}

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