Merge branch 'YosysHQ:main' into master

abc

@@ -1 +1 @@
-Subproject commit de0ebae1c5ddbb345871c2e3c4c2a99c9c881ad2
+Subproject commit 180a6adb68e855942e859f3646eff7762c7bc3e6

docs/source/cell/gate_reg_ff.rst

@@ -154,6 +154,10 @@ to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if
 ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` if
 ``SET_LVL`` if ``1``, ``negedge`` otherwise.
 
+When both set and reset are active, the state and output is undefined. The Verilog
+code model does not correspond to this due to limitations
+of synthesizable Verilog.
+
 .. code-block:: verilog
    :force:
 
@@ -187,6 +191,10 @@ types relate to the following Verilog code template, where ``RST_EDGE`` is
 ``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is
 ``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise.
 
+When both set and reset are active, the state and output is undefined. The Verilog
+code model does not correspond to this due to limitations
+of synthesizable Verilog.
+
 .. code-block:: verilog
    :force:
 

docs/source/cell/word_reg.rst

@@ -78,6 +78,7 @@ D-type flip-flops with asynchronous set and reset are represented by `$dffsr`
 cells. As the `$dff` cells they have ``CLK``, ``D`` and ``Q`` ports. In addition
 they also have multi-bit ``SET`` and ``CLR`` input ports and the corresponding
 polarity parameters, like `$sr` cells.
+When both set and reset are active, the state and output is undefined.
 
 D-type flip-flops with enable are represented by `$dffe`, `$adffe`, `$aldffe`,
 `$dffsre`, `$sdffe`, and `$sdffce` cells, which are enhanced variants of `$dff`,

frontends/liberty/liberty.cc

@@ -20,6 +20,7 @@
 #include "passes/techmap/libparse.h"
 #include "kernel/register.h"
 #include "kernel/log.h"
+#include <array>
 
 YOSYS_NAMESPACE_BEGIN
 
@@ -210,7 +211,10 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node)
 	auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node);
 	RTLIL::SigSpec clk_sig, data_sig, clear_sig, preset_sig;
 	bool clk_polarity = true, clear_polarity = true, preset_polarity = true;
+	const std::string name = RTLIL::unescape_id(module->name);
 
+	std::optional<char> clear_preset_var1;
+	std::optional<char> clear_preset_var2;
 	for (auto child : node->children) {
 		if (child->id == "clocked_on")
 			clk_sig = parse_func_expr(module, child->value.c_str());
@@ -220,10 +224,18 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node)
 			clear_sig = parse_func_expr(module, child->value.c_str());
 		if (child->id == "preset")
 			preset_sig = parse_func_expr(module, child->value.c_str());
+
+		for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}})
+			if (child->id == id) {
+				if (child->value.size() != 1)
+					log_error("Unexpected length of clear_preset_var* value %s in FF cell %s\n", child->value, name);
+				*var = child->value[0];
+			}
+
 	}
 
 	if (clk_sig.size() == 0 || data_sig.size() == 0)
-		log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", RTLIL::unescape_id(module->name));
+		log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", name);
 
 	for (bool rerun_invert_rollback = true; rerun_invert_rollback;)
 	{
@@ -248,36 +260,64 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node)
 		}
 	}
 
-	RTLIL::Cell *cell = module->addCell(NEW_ID, ID($_NOT_));
+	for (auto& [out_sig, cp_var, neg] : {tuple{iq_sig, clear_preset_var1, false}, {iqn_sig, clear_preset_var2, true}}) {
-	cell->setPort(ID::A, iq_sig);
+		SigSpec q_sig = out_sig;
-	cell->setPort(ID::Y, iqn_sig);
+		if (neg) {
+			q_sig = module->addWire(NEW_ID, out_sig.as_wire());
+			module->addNotGate(NEW_ID, q_sig, out_sig);
+		}
 
-	cell = module->addCell(NEW_ID, "");
+		RTLIL::Cell* cell = module->addCell(NEW_ID, "");
-	cell->setPort(ID::D, data_sig);
+		cell->setPort(ID::D, data_sig);
-	cell->setPort(ID::Q, iq_sig);
+		cell->setPort(ID::Q, q_sig);
-	cell->setPort(ID::C, clk_sig);
+		cell->setPort(ID::C, clk_sig);
 
-	if (clear_sig.size() == 0 && preset_sig.size() == 0) {
+		if (clear_sig.size() == 0 && preset_sig.size() == 0) {
-		cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N');
+			cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N');
+		}
+
+		if (clear_sig.size() == 1 && preset_sig.size() == 0) {
+			cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
+			cell->setPort(ID::R, clear_sig);
+		}
+
+		if (clear_sig.size() == 0 && preset_sig.size() == 1) {
+			cell->type = stringf("$_DFF_%c%c1_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N');
+			cell->setPort(ID::R, preset_sig);
+		}
+
+		if (clear_sig.size() == 1 && preset_sig.size() == 1) {
+			cell->type = stringf("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
+
+			SigBit s_sig = preset_sig;
+			SigBit r_sig = clear_sig;
+			if (cp_var && *cp_var != 'X') {
+				// Either set or reset dominates
+				bool set_dominates;
+				if (*cp_var == 'L') {
+					set_dominates = neg;
+				} else if (*cp_var == 'H') {
+					set_dominates = !neg;
+				} else {
+					log_error("FF cell %s has unsupported clear&preset behavior \'%c\'.\n", name, *cp_var);
+				}
+				log_debug("cell %s variable %d cp_var %c set dominates? %d\n", name, (int)neg + 1, *cp_var, set_dominates);
+				// S&R priority is well-defined now
+				if (set_dominates) {
+					r_sig = module->AndnotGate(NEW_ID, r_sig, s_sig);
+				} else {
+					s_sig = module->AndnotGate(NEW_ID, s_sig, r_sig);
+				}
+			} else {
+				log_debug("cell %s variable %d undef c&p behavior\n", name, (int)neg + 1);
+			}
+
+			cell->setPort(ID::S, s_sig);
+			cell->setPort(ID::R, r_sig);
+		}
+
+		log_assert(!cell->type.empty());
 	}
-
-	if (clear_sig.size() == 1 && preset_sig.size() == 0) {
-		cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
-		cell->setPort(ID::R, clear_sig);
-	}
-
-	if (clear_sig.size() == 0 && preset_sig.size() == 1) {
-		cell->type = stringf("$_DFF_%c%c1_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N');
-		cell->setPort(ID::R, preset_sig);
-	}
-
-	if (clear_sig.size() == 1 && preset_sig.size() == 1) {
-		cell->type = stringf("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
-		cell->setPort(ID::S, preset_sig);
-		cell->setPort(ID::R, clear_sig);
-	}
-
-	log_assert(!cell->type.empty());
 }
 
 static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool flag_ignore_miss_data_latch)
@@ -797,3 +837,4 @@ skip_cell:;
 
 YOSYS_NAMESPACE_END
 
+

passes/sat/async2sync.cc

@@ -157,6 +157,7 @@ struct Async2syncPass : public Pass {
 
 						SigSpec sig_set = ff.sig_set;
 						SigSpec sig_clr = ff.sig_clr;
+						SigSpec sig_clr_inv = ff.sig_clr;
 
 						if (!ff.pol_set) {
 							if (!ff.is_fine)
@@ -166,24 +167,42 @@ struct Async2syncPass : public Pass {
 						}
 
 						if (ff.pol_clr) {
+							if (!ff.is_fine)
+								sig_clr_inv = module->Not(NEW_ID, sig_clr);
+							else
+								sig_clr_inv = module->NotGate(NEW_ID, sig_clr);
+						} else {
 							if (!ff.is_fine)
 								sig_clr = module->Not(NEW_ID, sig_clr);
 							else
 								sig_clr = module->NotGate(NEW_ID, sig_clr);
 						}
 
+						// At this point, sig_set and sig_clr are now unconditionally
+						// active-high, and sig_clr_inv is inverted sig_clr
+
+						SigSpec set_and_clr;
+						if (!ff.is_fine)
+							set_and_clr = module->And(NEW_ID, sig_set, sig_clr);
+						else
+							set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr);
+
 						if (!ff.is_fine) {
 							SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set);
-							module->addAnd(NEW_ID, tmp, sig_clr, new_d);
+							tmp = module->And(NEW_ID, tmp, sig_clr_inv);
+							module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d);
 
 							tmp = module->Or(NEW_ID, new_q, sig_set);
-							module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q);
+							tmp = module->And(NEW_ID, tmp, sig_clr_inv);
+							module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q);
 						} else {
 							SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set);
-							module->addAndGate(NEW_ID, tmp, sig_clr, new_d);
+							tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv);
+							module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, new_d);
 
 							tmp = module->OrGate(NEW_ID, new_q, sig_set);
-							module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q);
+							tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv);
+							module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q);
 						}
 
 						ff.sig_d = new_d;

passes/sat/clk2fflogic.cc

@@ -123,10 +123,14 @@ struct Clk2fflogicPass : public Pass {
 			return module->Mux(NEW_ID, a, b, s);
 	}
 	SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) {
-		if (is_fine)
+		if (is_fine) {
-			return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r));
+			return module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)), RTLIL::State::Sx, module->AndGate(NEW_ID, s, r));
-		else
+		} else {
-			return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r));
+			std::vector<SigBit> y;
+			for (int i = 0; i < a.size(); i++)
+				y.push_back(module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a[i], s[i]), module->NotGate(NEW_ID, r[i])), RTLIL::State::Sx, module->AndGate(NEW_ID, s[i], r[i])));
+			return y;
+		}
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{

techlibs/common/simcells.v

@@ -1613,6 +1613,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 0 0 - | x
 //-                 - - 0 - | 0
 //-                 - 0 - - | 1
 //-                 \ - - d | d
@@ -1641,6 +1642,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 0 1 - | x
 //-                 - - 1 - | 0
 //-                 - 0 - - | 1
 //-                 \ - - d | d
@@ -1669,6 +1671,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 1 0 - | x
 //-                 - - 0 - | 0
 //-                 - 1 - - | 1
 //-                 \ - - d | d
@@ -1697,6 +1700,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 1 1 - | x
 //-                 - - 1 - | 0
 //-                 - 1 - - | 1
 //-                 \ - - d | d
@@ -1725,6 +1729,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 0 0 - | x
 //-                 - - 0 - | 0
 //-                 - 0 - - | 1
 //-                 / - - d | d
@@ -1753,6 +1758,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 0 1 - | x
 //-                 - - 1 - | 0
 //-                 - 0 - - | 1
 //-                 / - - d | d
@@ -1781,6 +1787,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 1 0 - | x
 //-                 - - 0 - | 0
 //-                 - 1 - - | 1
 //-                 / - - d | d
@@ -1809,6 +1816,7 @@ endmodule
 //-
 //- Truth table:    C S R D | Q
 //-                ---------+---
+//-                 - 1 1 - | x
 //-                 - - 1 - | 0
 //-                 - 1 - - | 1
 //-                 / - - d | d
@@ -1837,6 +1845,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 0 - - - | 1
 //-                 \ - - 0 d | d
@@ -1865,6 +1874,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 0 - - - | 1
 //-                 \ - - 1 d | d
@@ -1893,6 +1903,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 0 - - - | 1
 //-                 \ - - 0 d | d
@@ -1921,6 +1932,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 0 - - - | 1
 //-                 \ - - 1 d | d
@@ -1949,6 +1961,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 1 - - - | 1
 //-                 \ - - 0 d | d
@@ -1977,6 +1990,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 1 - - - | 1
 //-                 \ - - 1 d | d
@@ -2005,6 +2019,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 1 - - - | 1
 //-                 \ - - 0 d | d
@@ -2033,6 +2048,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 1 - - - | 1
 //-                 \ - - 1 d | d
@@ -2061,6 +2077,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 0 - - - | 1
 //-                 / - - 0 d | d
@@ -2089,6 +2106,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 0 - - - | 1
 //-                 / - - 1 d | d
@@ -2117,6 +2135,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 0 - - - | 1
 //-                 / - - 0 d | d
@@ -2145,6 +2164,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 0 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 0 - - - | 1
 //-                 / - - 1 d | d
@@ -2173,6 +2193,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 1 - - - | 1
 //-                 / - - 0 d | d
@@ -2201,6 +2222,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 0 - - | x
 //-                 - - 0 - - | 0
 //-                 - 1 - - - | 1
 //-                 / - - 1 d | d
@@ -2229,6 +2251,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 1 - - - | 1
 //-                 / - - 0 d | d
@@ -2257,6 +2280,7 @@ endmodule
 //-
 //- Truth table:    C S R E D | Q
 //-                -----------+---
+//-                 - 1 1 - - | x
 //-                 - - 1 - - | 0
 //-                 - 1 - - - | 1
 //-                 / - - 1 d | d

tests/techmap/dfflibmap.ys

@@ -64,8 +64,8 @@ select -assert-count 1 t:dffe
 select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
 
 design -load orig
-dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
+dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
-dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
+dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
 clean
 
 select -assert-count 5 t:$_NOT_

tests/techmap/dfflibmap_dffsr_r.lib

@@ -7,8 +7,8 @@ library(test) {
       clear      : "CLEAR";
       preset     : "PRESET";
       clear_preset_var1 : L;
-      clear_preset_var2 : L;
+      clear_preset_var2 : H;
-    } 
+    }
     pin(D) {
       direction : input;
     }
@@ -28,6 +28,6 @@ library(test) {
     pin(QN) {
       direction: output;
       function : "IQN";
-    } 
+    }
   }
 }

tests/techmap/dfflibmap_dffsr_s.lib

@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : H;
+      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_x.lib

@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : X;
+      clear_preset_var2 : X;
+    }
+    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_formal.ys

@@ -8,13 +8,132 @@ $_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
+assume property (~R || ~S);
-// likely due to an equiv_induct assume bug #5196
+$_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]));
 
-// // Workaround for DFFSR bug #5194
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
-// assume property (~R || ~S);
+
-// $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+assign Q[11:6] = ~Q[5:0];
-// $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_s.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_s.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
+
+##################################################################
+
+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]));
+
+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_dffsr_r.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_r.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
+
+##################################################################
+
+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]));
+
+// no assume when mapping to X
+$_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_dffsr_x.lib
+opt
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_x.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+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 -set-assumes assume bug #5196
+
+// no assume when mapping to unset clear_preset_var
+$_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]));
 
@@ -32,12 +151,14 @@ 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
+clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct equiv
+hierarchy -top miter
-equiv_status -assert equiv
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
 
 ##################################################################
 
@@ -50,13 +171,9 @@ $_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
+assume property (~R || ~S);
-// likely due to an equiv_induct assume bug #5196
+$_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]));
-// // 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]));
 
@@ -68,17 +185,21 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffr_not_next.lib
+read_liberty dfflibmap_dffsr_not_next_l.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffr_not_next.lib top
+dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
 
-async2sync
+clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct equiv
+hierarchy -top miter
-equiv_status -assert equiv
+
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
 
 ##################################################################
 
@@ -108,11 +229,11 @@ copy top top_unmapped
 simplemap top
 dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
 
-async2sync
+clk2fflogic
 flatten
 opt_clean -purge
 equiv_make top top_unmapped equiv
-equiv_induct equiv
+equiv_induct -set-assumes equiv
 equiv_status -assert equiv
 
 ##################################################################
@@ -139,9 +260,9 @@ copy top top_unmapped
 simplemap top
 dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top
 
-async2sync
+clk2fflogic
 flatten
 opt_clean -purge
 equiv_make top top_unmapped equiv
-equiv_induct equiv
+equiv_induct -set-assumes equiv
 equiv_status -assert equiv

tests/techmap/dfflibmap_proc_formal.ys

@@ -0,0 +1,100 @@
+##################################################################
+
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [7:0] Q);
+
+	always @( posedge C, posedge S, posedge R)
+		if (R)
+			Q[0] <= 0;
+		else if (S)
+			Q[0] <= 1;
+		else
+			Q[0] <= D;
+
+	always @( posedge C, posedge S, posedge R)
+		if (S)
+			Q[1] <= 1;
+		else if (R)
+			Q[1] <= 0;
+		else
+			Q[1] <= D;
+
+	always @( posedge C, posedge S, posedge R)
+		if (R)
+			Q[2] <= 0;
+		else if (S)
+			Q[2] <= 1;
+		else if (E)
+			Q[2] <= D;
+
+	always @( posedge C, posedge S, posedge R)
+		if (S)
+			Q[3] <= 1;
+		else if (R)
+			Q[3] <= 0;
+		else if (E)
+			Q[3] <= D;
+
+assign Q[7:4] = ~Q[3:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_s.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_s.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+delete top miter
+
+copy top_unmapped top
+dfflibmap -liberty dfflibmap_dffsr_r.lib top
+
+clk2fflogic
+flatten
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+delete top miter
+
+copy top_unmapped top
+dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
+
+clk2fflogic
+flatten
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+delete top miter
+
+copy top_unmapped top
+dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
+
+clk2fflogic
+flatten
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter