satgen: Add support for dffe, sdff, sdffe, sdffce cells.

2 files changed, 67 insertions, 4 deletions

diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index b90b43fb7..73839d37a 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -18,6 +18,7 @@
  */
 
 #include "kernel/satgen.h"
+#include "kernel/ff.h"
 
 USING_YOSYS_NAMESPACE
 
@@ -1075,8 +1076,14 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		return true;
 	}
 
-	if (timestep > 0 && cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
+	if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type))
 	{
+		FfData ff(nullptr, cell);
+
+		// Latches and FFs with async inputs are not supported — use clk2fflogic or async2sync first.
+		if (!ff.has_d || ff.has_arst || ff.has_sr || (ff.has_en && !ff.has_clk))
+			return false;
+
 		if (timestep == 1)
 		{
 			initial_state.add((*sigmap)(cell->getPort(ID::Q)));
@@ -1084,6 +1091,51 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		else
 		{
 			std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
+			std::vector<int> undef_d;
+			if (model_undef)
+				undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
+			if (ff.has_srst && ff.has_en && ff.ce_over_srst) {
+				int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+				std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+				int undef_srst;
+				std::vector<int> undef_rval;
+				if (model_undef) {
+					undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+					undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+				}
+				if (ff.pol_srst)
+					std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+				else
+					std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+			}
+			if (ff.has_en) {
+				int en = importDefSigSpec(ff.sig_en, timestep-1).at(0);
+				std::vector<int> old_q = importDefSigSpec(ff.sig_q, timestep-1);
+				int undef_en;
+				std::vector<int> undef_old_q;
+				if (model_undef) {
+					undef_en = importUndefSigSpec(ff.sig_en, timestep-1).at(0);
+					undef_old_q = importUndefSigSpec(ff.sig_q, timestep-1);
+				}
+				if (ff.pol_en)
+					std::tie(d, undef_d) = mux(en, undef_en, old_q, undef_old_q, d, undef_d);
+				else
+					std::tie(d, undef_d) = mux(en, undef_en, d, undef_d, old_q, undef_old_q);
+			}
+			if (ff.has_srst && !(ff.has_en && ff.ce_over_srst)) {
+				int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+				std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+				int undef_srst;
+				std::vector<int> undef_rval;
+				if (model_undef) {
+					undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+					undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+				}
+				if (ff.pol_srst)
+					std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+				else
+					std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+			}
 			std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
 
 			std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
@@ -1091,7 +1143,6 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 
 			if (model_undef)
 			{
-				std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
 				std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
 
 				ez->assume(ez->vec_eq(undef_d, undef_q));
@@ -1182,7 +1233,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		return true;
 	}
 
-	// Unsupported internal cell types: $pow $lut
-	// .. and all sequential cells except $dff and $_DFF_[NP]_
+	// Unsupported internal cell types: $pow $fsm $mem*
+	// .. and all sequential cells with asynchronous inputs
 	return false;
 }
diff --git a/kernel/satgen.h b/kernel/satgen.h
index bd6259ba1..cf2db733f 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -262,6 +262,18 @@ struct SatGen
 		}
 	}
 
+	std::pair<std::vector<int>, std::vector<int>> mux(int s, int undef_s, const std::vector<int> &a, const std::vector<int> &undef_a, const std::vector<int> &b, const std::vector<int> &undef_b) {
+		std::vector<int> res;
+		std::vector<int> undef_res;
+		res = ez->vec_ite(s, b, a);
+		if (model_undef) {
+			std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
+			std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
+			undef_res = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
+		}
+		return std::make_pair(res, undef_res);
+	}
+
 	void undefGating(int y, int yy, int undef)
 	{
 		ez->assume(ez->OR(undef, ez->IFF(y, yy)));