From a022ca524ddcd70b52cf768c1d8cf4a5e5918482 Mon Sep 17 00:00:00 2001
From: Akash Levy <akash@silimate.com>
Date: Wed, 8 Jul 2026 23:20:22 -0700
Subject: [PATCH] Fix flaky opt_priokey -strict and cover binary exclusive scan

ASLR-dependent ConstEval seeding let E4 miss OOR counterexamples; use a
deterministic seed and force OOR key collisions. Add I9 (NB=12) for the
thermometer fallback path Greptile flagged.

Co-authored-by: Cursor <cursoragent@cursor.com>
---
 passes/opt/opt_priokey.cc        | 51 ++++++++++++++++++++++++--------
 tests/opt/opt_first_fit_alloc.ys | 39 ++++++++++++++++++++++++
 2 files changed, 78 insertions(+), 12 deletions(-)

diff --git a/passes/opt/opt_priokey.cc b/passes/opt/opt_priokey.cc
index f505c1e7e..5f678b9d6 100644
--- a/passes/opt/opt_priokey.cc
+++ b/passes/opt/opt_priokey.cc
@@ -264,26 +264,21 @@ struct OptPrioKeyWorker {
 			range = 1ULL << cap;
 		}
 		ConstEval ce(module);
-		uint64_t lfsr = 0x9e3779b97f4a7c15ULL ^ (uintptr_t)read;
+		// Deterministic seed (not a Cell*): ASLR made uintptr_t seeding flake
+		// across runs, so -strict could miss the OOR counterexample.
+		uint64_t lfsr = 0x9e3779b97f4a7c15ULL ^ ((uint64_t)S << 1) ^
+		                ((uint64_t)kw << 17) ^ (uint64_t)GetSize(steps);
 		auto rnd = [&]() {
 			lfsr ^= lfsr << 13; lfsr ^= lfsr >> 7; lfsr ^= lfsr << 17;
 			return lfsr;
 		};
-		for (int t = 0; t < fp_trials; t++) {
+		auto trial = [&](int rk, const vector<int> &kv, const vector<int> &gv) -> bool {
 			ce.push();
-			int rk = (int)(rnd() % range);
 			ce.set(read_key, Const(rk, GetSize(read_key)));
-			vector<int> kv(GetSize(steps));
-			vector<int> gv(GetSize(steps));
 			for (int i = 0; i < GetSize(steps); i++) {
-				kv[i] = (int)(rnd() % range);
 				ce.set(steps[i].key, Const(kv[i], GetSize(steps[i].key)));
-				if (steps[i].guard == State::S1) {
-					gv[i] = 1;
-				} else {
-					gv[i] = (int)(rnd() & 1);
+				if (steps[i].guard != State::S1)
 					ce.set(SigSpec(steps[i].guard), Const(gv[i], 1));
-				}
 			}
 			SigSpec out(read->getPort(ID::Y));
 			SigSpec undef;
@@ -293,7 +288,39 @@ struct OptPrioKeyWorker {
 			for (int i = 0; i < GetSize(steps); i++)
 				if (gv[i] && kv[i] == rk) { expect = 1; break; }
 			ce.pop();
-			if (!ok || actual != expect)
+			return ok && actual == expect;
+		};
+		// Strict + non-pow2 S: force OOR key collisions the rewrite would accept
+		// but the S-bit accumulator cannot store (taken[key>=S] is not a set bit).
+		if (strict && range > (uint64_t)S && !steps.empty()) {
+			int oor_n = (int)(range - (uint64_t)S);
+			int forced = oor_n < 16 ? oor_n : 16;
+			for (int f = 0; f < forced; f++) {
+				int rk = S + f;
+				vector<int> kv(GetSize(steps), 0);
+				vector<int> gv(GetSize(steps), 0);
+				kv[0] = rk;
+				gv[0] = 1;
+				for (int i = 1; i < GetSize(steps); i++) {
+					kv[i] = (int)(rnd() % range);
+					gv[i] = steps[i].guard == State::S1 ? 1 : (int)(rnd() & 1);
+				}
+				if (!trial(rk, kv, gv))
+					return false;
+			}
+		}
+		for (int t = 0; t < fp_trials; t++) {
+			int rk = (int)(rnd() % range);
+			vector<int> kv(GetSize(steps));
+			vector<int> gv(GetSize(steps));
+			for (int i = 0; i < GetSize(steps); i++) {
+				kv[i] = (int)(rnd() % range);
+				if (steps[i].guard == State::S1)
+					gv[i] = 1;
+				else
+					gv[i] = (int)(rnd() & 1);
+			}
+			if (!trial(rk, kv, gv))
 				return false;
 		}
 		return true;
diff --git a/tests/opt/opt_first_fit_alloc.ys b/tests/opt/opt_first_fit_alloc.ys
index f4a4b4c7a..470e328fc 100644
--- a/tests/opt/opt_first_fit_alloc.ys
+++ b/tests/opt/opt_first_fit_alloc.ys
@@ -1171,3 +1171,42 @@ design -load postopt
 select -assert-min 1 w:*ffa_*
 design -reset
 log -pop
+
+# I9: exclusive with NB > max_therm_nb (8) — forces the binary saturating
+# Hillis–Steele fallback (emit_scan_exclusive_bin / emit_sat_add) instead of
+# the thermometer scan used by I1–I8.
+log -header "I9: exclusive binary-scan fallback N=16 NB=12 (equiv)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module top #(parameter N=16, NB=12, W=4) (
+  input  logic           mode,
+  input  logic [N-1:0]   req,
+  output logic [N*W-1:0] dsel_flat
+);
+  logic [N-1:0]  en = req & {N{mode}};
+  logic [W-1:0]  dsel [0:N-1];
+  logic [NB-1:0] taken;
+  logic [N-1:0]  done;
+  always_comb begin
+    for (int i=0;i<N;i++) dsel[i] = '0;
+    taken = '0; done = '0;
+    for (int i=0;i<N;i++)
+      if (en[i])
+        for (int j=0;j<NB;j++)
+          if (!taken[j] && !done[i]) begin
+            dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
+          end
+  end
+  for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
+endmodule
+EOF
+hierarchy -top top
+proc
+opt
+check -assert
+equiv_opt -assert opt_first_fit_alloc
+design -load postopt
+select -assert-min 1 w:*ffa_*
+design -reset
+log -pop