From 1d468962b7be1c494e999ae5ec00077f00c60adb Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Wed, 21 Jan 2026 11:50:45 +0100
Subject: [PATCH] satgen, calc: $priority perform more x-bit horrors

---
 kernel/calc.cc   | 27 ++++++++++++++-------------
 kernel/satgen.cc | 13 ++++++++++---
 2 files changed, 24 insertions(+), 16 deletions(-)

diff --git a/kernel/calc.cc b/kernel/calc.cc
index a1ba5f7c8..feaca4cc6 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -660,21 +660,22 @@ RTLIL::Const RTLIL::const_bmux(const RTLIL::Const &arg1, const RTLIL::Const &arg
 
 RTLIL::Const RTLIL::const_priority(const RTLIL::Const &arg, const RTLIL::Const &polarity)
 {
-	std::vector<State> t;
-	std::optional<State> first_non_zero = std::nullopt;
-	for (int i = 0; i < GetSize(arg); i++)
+	std::vector<RTLIL::State> t;
+	RTLIL::State previous;
+	if (GetSize(arg)) {
+		RTLIL::State s = arg.at(0);
+		t.push_back(s);
+		previous = polarity[0] ? s : const_not(s, Const(), false, false, 1)[0];
+	}
+	for (int i = 1; i < GetSize(arg); i++)
 	{
 		RTLIL::State s = arg.at(i);
-		if (first_non_zero && s != State::Sx) {
-			auto inactive = polarity[i] == State::S0 ? State::S1 : State::S0;
-			auto val = *first_non_zero == State::Sx ? State::Sx : inactive;
-			t.push_back(val);
-		} else {
-			t.push_back(s);
-		}
-		if ((!first_non_zero && s == polarity[i]) || s == State::Sx) {
-			first_non_zero = s;
-		}
+		RTLIL::State is_active = const_xnor(s, polarity[i], false, false, 1)[0];
+		RTLIL::State next = const_or(is_active, previous, false, false, 1)[0];
+		RTLIL::State inactive_polarity = const_not(polarity[i], Const(), false, false, 1)[0];
+		RTLIL::State y = const_mux(s, inactive_polarity, previous)[0];
+		t.push_back(y);
+		previous = next;
 	}
 	return t;
 }
diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index bfbf6d77e..ce0c62819 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -460,13 +460,20 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 			}
 			for (size_t i = 1; i < a.size(); i++) {
 				int inactive_val = !polarity[i] ? ez->CONST_TRUE : ez->CONST_FALSE;
-				// $mux emulation
 				int is_active = ez->XOR(inactive_val, a[i]);
-				int undef_because_s = ez->AND(any_previous_undef, ez->OR(is_active, undef_a[i]));
+				int is_not_inactive = ez->OR(is_active, undef_a[i]);
+				int is_not_active = ez->OR(ez->NOT(is_active), undef_a[i]);
+
+				// $mux
+				int undef_because_s = ez->AND(any_previous_undef, is_not_inactive);
 				int undef_because_a = ez->AND(ez->OR(any_previous_undef, ez->NOT(active_so_far[i-1])), undef_a[i]);
 				int undef = ez->OR(undef_because_s, undef_because_a);
-				any_previous_undef = ez->AND(ez->NOT(is_active), ez->OR(any_previous_undef, undef_a[i]));
 				ez->assume(ez->IFF(undef_y[i], undef));
+
+				// $or
+				int next_previous_undef_because_previous = ez->AND(any_previous_undef, is_not_active);
+				int next_previous_undef_because_a = ez->AND(ez->NOT(active_so_far[i-1]), undef_a[i]);
+				any_previous_undef = ez->OR(next_previous_undef_because_previous, next_previous_undef_because_a);
 			}
 			undefGating(y, yy, undef_y);
 		}