satgen, simlib: Consistent x-propagation for `$pmux` cells

This updates satgen and simlib to use a `$pmux` model where the output
is fully X when the S input is not all zero or one-hot with no x bits.

2 files changed, 20 insertions, 18 deletions

diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index 2a1fd1711..3c21a8f99 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -375,29 +375,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 			std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
 			std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
 
-			int maybe_a = ez->CONST_TRUE;
+			int all_undef = ez->CONST_FALSE;
+			int found_active = ez->CONST_FALSE;
 
-			std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
-			std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
+			std::vector<int> undef_tmp = undef_a;
 
 			for (size_t i = 0; i < s.size(); i++)
 			{
-				std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
 				std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
 
-				int maybe_s = ez->OR(s.at(i), undef_s.at(i));
-				int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
-
-				maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
-
-				bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
-				bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
+				undef_tmp = ez->vec_ite(s.at(i), part_of_undef_b, undef_tmp);
+				all_undef = ez->OR(all_undef, undef_s.at(i));
+				all_undef = ez->OR(all_undef, ez->AND(s.at(i), found_active));
+				found_active = ez->OR(found_active, s.at(i));
 			}
 
-			bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
-			bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
+			undef_tmp = ez->vec_or(undef_tmp, std::vector<int>(a.size(), all_undef));
 
-			ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
+			ez->assume(ez->vec_eq(undef_tmp, undef_y));
 			undefGating(y, yy, undef_y);
 		}
 		return true;
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index e64697efb..b5e437d90 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1331,10 +1331,17 @@ always @* begin
 	Y = A;
 	found_active_sel_bit = 0;
 	for (i = 0; i < S_WIDTH; i = i+1)
-		if (S[i]) begin
-			Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
-			found_active_sel_bit = 1;
-		end
+		case (S[i])
+			1'b1: begin
+				Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
+				found_active_sel_bit = 1;
+			end
+			1'b0: ;
+			1'bx: begin
+				Y = 'bx;
+				found_active_sel_bit = 'bx;
+			end
+		endcase
 end
 
 endmodule