dfflibmap: fix next_state inversion propagation for DFF flops by inverting reset value polarity

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;

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

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