From 676ac184edf5386f6f9c7d7dfbc9d363179b3142 Mon Sep 17 00:00:00 2001
From: Akash Levy <akash@silimate.com>
Date: Mon, 6 Jul 2026 21:35:51 -0700
Subject: [PATCH 1/2] opt_prienc: guard ConstEval fingerprint inputs against
 constant/aliased bits

The round-robin detector fed sigmap(wire) signals straight into
ConstEval::set() while sweeping test vectors. On real designs a candidate
bus can have bits tied to constants, repeated bits, or a req/start pair
that alias to the same net after sigmap. ConstEval::set() asserts
(current_val[i].wire != NULL || current_val[i] == value[i]) when asked to
re-pin such a bit to a conflicting value, crashing the pass
(consteval.h:83) on designs like veer/picorv32/murax/raygentop under
formal synthesis.

Add clean_set_signals() and reject any fingerprint candidate whose
set-signals contain constant bits, repeated bits, or overlap each other,
in both the priority-encoder and round-robin paths. Skipping an unclean
candidate only forgoes a possible rewrite; it never produces an incorrect
one. Clean candidates (the intended patterns) are unaffected.

Co-authored-by: Cursor <cursoragent@cursor.com>
---
 passes/opt/opt_prienc.cc | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/passes/opt/opt_prienc.cc b/passes/opt/opt_prienc.cc
index 7231db45e..07089283c 100644
--- a/passes/opt/opt_prienc.cc
+++ b/passes/opt/opt_prienc.cc
@@ -243,6 +243,23 @@ struct OptPriEncWorker {
 		return vs;
 	}
 
+	// ConstEval::set() requires every (sigmap-canonical) bit it pins to be a
+	// distinct free wire bit. Real designs can tie parts of a bus to constants
+	// or alias nets together, so guard the fingerprint inputs: reject signals
+	// containing constant or repeated bits, and (across the whole set) any
+	// overlap between them. This prevents a ConstEval assertion; skipping an
+	// unclean candidate only forgoes a possible rewrite, never yields a wrong
+	// one.
+	static bool clean_set_signals(std::initializer_list<const SigSpec*> sigs) {
+		pool<SigBit> seen;
+		for (const SigSpec* sp : sigs)
+			for (auto bit : *sp) {
+				if (bit.wire == nullptr) return false;
+				if (!seen.insert(bit).second) return false;
+			}
+		return true;
+	}
+
 	// Run all candidate test vectors through ConstEval and try to match each of
 	// the four PE variants against the recorded outputs. Returns the matched
 	// variant, or NONE.
@@ -257,6 +274,9 @@ struct OptPriEncWorker {
 		if (!clz_full_ok && !ctz_full_ok && !clz_short_ok && !ctz_short_ok)
 			return PEVariant::NONE;
 
+		if (!clean_set_signals({&T_sig}))
+			return PEVariant::NONE;
+
 		auto vs = gen_test_vectors(N);
 		for (auto& v : vs) {
 			ce.push();
@@ -440,6 +460,8 @@ struct OptPriEncWorker {
 	int fingerprint_rr(SigSpec req_sig, SigSpec start_sig, SigSpec S_sig,
 	                   int N, int W) {
 		ConstEval ce(module);
+		if (!clean_set_signals({&req_sig, &start_sig}))
+			return -1;
 		bool ok0 = true, ok1 = true;
 		auto deck = gen_test_vectors(N);
 		int checks = 0;

From 945e4a403ba50928dfb5837e346c4df8af9b4d68 Mon Sep 17 00:00:00 2001
From: Akash Levy <akash@silimate.com>
Date: Mon, 6 Jul 2026 22:05:50 -0700
Subject: [PATCH 2/2] tests/opt: add generalization coverage for the QoR
 pattern passes

Prove the three pattern detectors work on unseen inputs, not just the RTL
they were derived from. Because detection is functional (ConstEval
fingerprinting over the reachable input space), correctness is established
per case with equiv_opt -assert (full) or a SAT miter clamped to the
reachable range (non-power-of-two), and detection is confirmed with a
w:*tag* probe.

opt_priokey:
  D1-D3  spelling variants (explicit shift-or set, compound derived guard,
         accumulator also exported) -- all fire and prove equivalent.
  E1-E2  parameter sweep P=2..8, S=4..32.
  E3     non-power-of-two S=12 reachable-range equivalence via SAT miter.
  E4     same shape under -strict declines to rewrite (formal-flow safety).
  F1-F2  near-miss negatives (clear accumulator, multi-hot set) -> no rewrite.

opt_prienc (round-robin):
  RR4-RR5 DEPTH sweep 8/32, full sequential equivalence.
  RR6     non-power-of-two DEPTH=7 reachable-range equivalence (SAT miter).
  RR7     an entirely different spelling (upward wrap-scan, first-hit) of the
          same arbiter -- fires and proves equivalent.
  RR8     fixed-priority (no rotating pointer) negative.

opt_first_fit_alloc (coalesce):
  H1      inline same-category compare (no precomputed matrix) spelling.
  H2      different slot/field shape (N=8, NB=8, W=3).

All new cases pass locally; they avoid brittle exact cell-count asserts so
they are robust to upstream optimization drift.

Co-authored-by: Cursor <cursoragent@cursor.com>
---
 tests/opt/opt_first_fit_alloc.ys | 100 +++++++++
 tests/opt/opt_prienc.ys          | 182 ++++++++++++++++
 tests/opt/opt_priokey.ys         | 343 +++++++++++++++++++++++++++++++
 3 files changed, 625 insertions(+)

diff --git a/tests/opt/opt_first_fit_alloc.ys b/tests/opt/opt_first_fit_alloc.ys
index a4bec64b0..4ffe36684 100644
--- a/tests/opt/opt_first_fit_alloc.ys
+++ b/tests/opt/opt_first_fit_alloc.ys
@@ -757,3 +757,103 @@ opt_first_fit_alloc
 select -assert-count 0 w:*ffa_*
 design -reset
 log -pop
+
+# ============================================================================
+# Group H: coalesce generalization (spelling + shape variants)
+# ============================================================================
+#
+# The coalesce variant is detected by functional fingerprinting of the dsel
+# cone, so it should not depend on the exact way the same-category forwarding
+# is written or on the specific N/NB/C shape. These cases vary both.
+
+# H1: coalesce with the same-category forwarding written INLINE (no precomputed
+# same_cat[i][k] matrix) -- the leader compares categories directly in its
+# forward loop. Functionally identical to G1's matrix form; must still detect
+# the enable-independent coalescing variant and prove equivalent.
+log -header "H1: coalesce inline-compare spelling, N=8 (equiv + fires)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module top #(parameter N=8, NB=4, C=2, W=2) (
+  input  logic [N-1:0]   lane_en,
+  input  logic [N*C-1:0] cat_flat,
+  output logic [N*W-1:0] dsel_flat
+);
+  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 (lane_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;
+            for (int k=i;k<N;k++)
+              if (cat_flat[k*C +: C]==cat_flat[i*C +: C]) begin
+                dsel[k] = W'(j); done[k] = 1'b1;
+              end
+          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
+
+# H2: coalesce at a different shape -- N=8 lanes but NB=8 slots (twice G1's
+# slot count, wider dsel W=3). Confirms the coalesce fingerprint generalizes
+# across slot/field widths, not just the N=8/NB=4 shape of G1.
+log -header "H2: coalesce shape N=8 NB=8 W=3 (equiv + fires)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module top #(parameter N=8, NB=8, C=2, W=3) (
+  input  logic [N-1:0]   lane_en,
+  input  logic [N*C-1:0] cat_flat,
+  output logic [N*W-1:0] dsel_flat
+);
+  logic [N-1:0] same_cat [0:N-1];
+  always_comb begin
+    for (int a=0;a<N;a++) begin
+      same_cat[a] = '0;
+      if (lane_en[a])
+        for (int b=a;b<N;b++)
+          if (cat_flat[a*C +: C]==cat_flat[b*C +: C]) same_cat[a][b] = 1'b1;
+    end
+  end
+  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 (lane_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;
+            for (int k=0;k<N;k++)
+              if (same_cat[i][k]) begin dsel[k] = W'(j); done[k] = 1'b1; end
+          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
diff --git a/tests/opt/opt_prienc.ys b/tests/opt/opt_prienc.ys
index 924653e3a..ef60147bf 100644
--- a/tests/opt/opt_prienc.ys
+++ b/tests/opt/opt_prienc.ys
@@ -798,3 +798,185 @@ opt_prienc
 select -assert-count 0 w:*rr*
 design -reset
 log -pop
+
+# RR4: DEPTH sweep, power-of-2 = 8 -- full sequential equivalence.
+log -header "RR4: round-robin arbiter, DEPTH=8 (sequential equiv)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module test #(parameter int DEPTH = 8) (
+    input  logic                    clk,
+    input  logic                    rst_n,
+    input  logic [DEPTH-1:0]        req,
+    output logic [$clog2(DEPTH)-1:0] grant
+);
+    typedef logic [$clog2(DEPTH)-1:0] idx_t;
+    idx_t idx, idx_next, idx_last;
+    always_comb begin
+        idx = idx_last; idx_next = idx_last; grant = '0;
+        for (int i = 0; i < DEPTH; i++) begin
+            if (req[idx]) begin grant = idx; idx_next = idx; end
+            if (idx == 0) idx = idx_t'(DEPTH-1); else idx--;
+        end
+    end
+    always_ff @(posedge clk) begin
+        if (!rst_n) idx_last <= '0;
+        else if (idx_last != idx_next) idx_last <= idx_next;
+    end
+endmodule
+EOF
+hierarchy -top test
+proc
+opt
+equiv_opt -assert -multiclock opt_prienc
+design -load postopt
+select -assert-min 1 w:*rr*
+design -reset
+log -pop
+
+# RR5: DEPTH sweep, power-of-2 = 32 -- larger than any test case, full equiv.
+log -header "RR5: round-robin arbiter, DEPTH=32 (sequential equiv)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module test #(parameter int DEPTH = 32) (
+    input  logic                    clk,
+    input  logic                    rst_n,
+    input  logic [DEPTH-1:0]        req,
+    output logic [$clog2(DEPTH)-1:0] grant
+);
+    typedef logic [$clog2(DEPTH)-1:0] idx_t;
+    idx_t idx, idx_next, idx_last;
+    always_comb begin
+        idx = idx_last; idx_next = idx_last; grant = '0;
+        for (int i = 0; i < DEPTH; i++) begin
+            if (req[idx]) begin grant = idx; idx_next = idx; end
+            if (idx == 0) idx = idx_t'(DEPTH-1); else idx--;
+        end
+    end
+    always_ff @(posedge clk) begin
+        if (!rst_n) idx_last <= '0;
+        else if (idx_last != idx_next) idx_last <= idx_next;
+    end
+endmodule
+EOF
+hierarchy -top test
+proc
+opt
+equiv_opt -assert -multiclock opt_prienc
+design -load postopt
+select -assert-min 1 w:*rr*
+design -reset
+log -pop
+
+# RR6: non-power-of-2 DEPTH=7 -- reachable-range equivalence via SAT miter,
+# mirroring RR2 but at a different (odd) size to confirm the reachable-range
+# handling generalizes across non-pow2 widths, not just DEPTH=13.
+log -header "RR6: round-robin arbiter, DEPTH=7 (reachable-range equiv)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module rr_dut #(parameter int N=7, parameter int W=3) (
+  input  logic [N-1:0] req, input logic [W-1:0] s,
+  output logic [W-1:0] grant, output logic [W-1:0] idx_next
+);
+  always_comb begin
+    logic [W-1:0] idx; idx=s; idx_next=s; grant='0;
+    for (int i=0;i<N;i++) begin
+      if (req[idx]) begin grant=idx; idx_next=idx; end
+      if (idx==0) idx=W'(N-1); else idx--;
+    end
+  end
+endmodule
+EOF
+hierarchy -top rr_dut
+proc
+opt
+design -save rr_gold
+opt_prienc
+select -assert-min 1 w:*rr*
+design -save rr_gate
+design -reset
+design -copy-from rr_gold -as rr_ref rr_dut
+design -copy-from rr_gate -as rr_dut rr_dut
+read_verilog -sv <<EOF
+module tb #(parameter int N=7, parameter int W=3)(input logic [N-1:0] req, input logic [W-1:0] si);
+  logic [W-1:0] s, g1,n1,g2,n2;
+  assign s = (si >= N) ? (si - N) : si;
+  rr_dut #(N,W) u1(.req(req),.s(s),.grant(g1),.idx_next(n1));
+  rr_ref #(N,W) u2(.req(req),.s(s),.grant(g2),.idx_next(n2));
+  always_comb begin
+    assert (g1 == g2);
+    assert (n1 == n2);
+  end
+endmodule
+EOF
+hierarchy -top tb
+flatten
+chformal -lower
+opt -full
+sat -verify -prove-asserts -show-ports tb
+design -reset
+log -pop
+
+# RR7: DIFFERENT RTL SPELLING of the same rotated-priority function. Instead of
+# the customer's downward idx-- last-write-wins loop, scan UPWARD from s+1 with
+# wraparound and keep the FIRST hit. This is a functionally identical arbiter
+# written in an unrelated style; detection is functional so it must still fire
+# and prove equivalent. (Combinational, pointer `s` an input -> full equiv at
+# power-of-2 N over all pointer values.)
+log -header "RR7: upward-scan spelling variant, N=16 (equiv + fires)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module test #(parameter int N=16, parameter int W=4) (
+  input  logic [N-1:0] req, input logic [W-1:0] s,
+  output logic [W-1:0] grant
+);
+  always_comb begin
+    logic [W-1:0] idx; logic found;
+    grant='0; found=1'b0;
+    for (int k=1;k<=N;k++) begin
+      idx = W'((s + k) % N);
+      if (req[idx] && !found) begin grant = idx; found = 1'b1; end
+    end
+  end
+endmodule
+EOF
+hierarchy -top test
+proc
+opt
+equiv_opt -assert opt_prienc
+design -load postopt
+select -assert-min 1 w:*rr*
+design -reset
+log -pop
+
+# RR8: negative -- FIXED-priority arbiter (constant start, no rotating pointer).
+# This is a plain priority encoder, not a round-robin, so no round_robin
+# rewrite may fire (it may still be picked up by the ordinary PE/CTZ path,
+# which is fine; we only forbid a spurious *rr* rewrite).
+log -header "RR8: fixed-priority (no pointer) -> no round-robin rewrite"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module test #(parameter int N=13, parameter int W=4) (
+  input  logic [N-1:0] req,
+  output logic [W-1:0] grant
+);
+  always_comb begin
+    logic [W-1:0] idx; grant='0;
+    for (int i=0;i<N;i++) begin
+      idx = W'(N-1-i);
+      if (req[idx]) grant=idx;   // last-write-wins over a fixed 0..N-1 order
+    end
+  end
+endmodule
+EOF
+hierarchy -top test
+proc
+opt
+opt_prienc
+select -assert-count 0 w:*rr*
+design -reset
+log -pop
diff --git a/tests/opt/opt_priokey.ys b/tests/opt/opt_priokey.ys
index 4e84a9ecd..8260ddc66 100644
--- a/tests/opt/opt_priokey.ys
+++ b/tests/opt/opt_priokey.ys
@@ -238,3 +238,346 @@ opt_priokey
 select -assert-count 0 w:*priokey*
 design -reset
 log -pop
+
+# ============================================================================
+# Group D: RTL-spelling variants (generalization across surface syntax)
+# ============================================================================
+#
+# Detection is functional (the pass traces the set-accumulator structurally
+# and then ConstEval-validates each read over the reachable key range), so it
+# is independent of how the conflict scan is spelled. Each variant below is a
+# DIFFERENT way to write the same "first source per key wins" resolution; for
+# every one we require both that the rewrite fires (w:*priokey*) and that
+# equiv_opt -assert proves it equivalent to the original elaboration. This is
+# the core generalization claim: unseen but functionally-equivalent RTL is
+# handled, not just the one spelling from the QoR case.
+
+# D1: explicit `taken = taken | (1 << sel[i])` set (instead of the bit-select
+# write taken[sel[i]]=1) and a separate `conflict` temporary for the guard.
+log -header "D1: explicit shift-or set + temp guard (equiv + fires)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=4, S=16, SW=4)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] taken;
+  logic         conflict;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++) begin
+      conflict = taken[sel[i]];
+      if (act[i] && !conflict) begin
+        win[i] = 1'b1;
+        taken  = taken | (S'(1) << sel[i]);
+      end
+    end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+check -assert
+equiv_opt -assert opt_priokey
+design -load postopt
+select -assert-min 1 w:*priokey*
+design -reset
+log -pop
+
+# D2: compound guard (act[i] & en[i]) -- the per-step guard the pass keys off
+# is a derived net, not a primary input. The fingerprint drives it as a free
+# variable, so proving read == OR(guard & key==read_key) over free guards is
+# strictly stronger than the real (correlated) guards need.
+log -header "D2: compound derived guard (equiv + fires)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=5, S=32, SW=5)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0]         en,
+  input  logic [P-1:0][SW-1:0] sel,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if ((act[i] & en[i]) && !taken[sel[i]]) begin
+        taken[sel[i]] = 1'b1;
+        win[i] = 1'b1;
+      end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+check -assert
+equiv_opt -assert opt_priokey
+design -load postopt
+select -assert-min 1 w:*priokey*
+design -reset
+log -pop
+
+# D3: the final accumulator state is ALSO a module output. Only the guarded
+# dynamic reads are rewritten; the set-writes that build `taken` are left
+# intact. equiv_opt must still prove the (untouched) taken output and the
+# rewritten win outputs all match.
+log -header "D3: accumulator also exported as output (equiv + fires)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=4, S=16, SW=4)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  output logic [P-1:0]         win,
+  output logic [S-1:0]         taken_o
+);
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && !taken[sel[i]]) begin
+        taken[sel[i]] = 1'b1;
+        win[i] = 1'b1;
+      end
+    taken_o = taken;
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+check -assert
+equiv_opt -assert opt_priokey
+design -load postopt
+select -assert-min 1 w:*priokey*
+design -reset
+log -pop
+
+# ============================================================================
+# Group E: parameter sweep + non-power-of-two accumulator width
+# ============================================================================
+
+# E1: tiny shape P=2 S=4 -- lower edge of the pattern.
+log -header "E1: P=2 S=4 (equiv, edge)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=2, S=4, SW=2)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  input  logic [P-1:0]         src,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && !taken[sel[i]]) begin
+        taken[sel[i]] = 1'b1; win[i] = src[i];
+      end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+check -assert
+equiv_opt -assert opt_priokey
+design -load postopt
+select -assert-min 1 w:*priokey*
+design -reset
+log -pop
+
+# E2: deep shape P=8 S=32 -- more sources than any QoR case, longer chain.
+log -header "E2: P=8 S=32 (equiv, deep chain)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=8, S=32, SW=5)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  input  logic [P-1:0]         src,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && !taken[sel[i]]) begin
+        taken[sel[i]] = 1'b1; win[i] = src[i];
+      end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+check -assert
+equiv_opt -assert opt_priokey
+design -load postopt
+select -assert-min 1 w:*priokey*
+design -reset
+log -pop
+
+# E3: NON-power-of-two accumulator S=12 (SW=4, so the key bus spans [0,16) but
+# only [0,12) are valid slots). The default (non-strict) rewrite is guaranteed
+# only over the REACHABLE key range [0,S); it is NOT unconditionally equivalent
+# (reads for keys in [12,16) index out of range). We prove the reachable-range
+# guarantee rigorously with a SAT miter that clamps every key into [0,S) and
+# compares the rewritten copy against an untouched reference (cf. RR2). The
+# rewrite must fire AND agree with the reference for all in-range keys.
+log -header "E3: non-pow2 S=12 reachable-range equivalence (SAT miter)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module pk_dut #(parameter int P=4, S=12, SW=4)(
+  input  logic [P-1:0]      act,
+  input  logic [P*SW-1:0]   sel_flat,
+  output logic [P-1:0]      win
+);
+  logic [SW-1:0] sel [0:P-1];
+  for (genvar g=0; g<P; g++) assign sel[g] = sel_flat[g*SW +: SW];
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && !taken[sel[i]]) begin
+        taken[sel[i]] = 1'b1; win[i] = 1'b1;
+      end
+  end
+endmodule
+EOF
+hierarchy -top pk_dut
+proc
+opt
+design -save pk_gold
+opt_priokey
+select -assert-min 1 w:*priokey*
+opt_clean
+design -save pk_gate
+design -reset
+design -copy-from pk_gold -as pk_ref  pk_dut
+design -copy-from pk_gate -as pk_dut  pk_dut
+read_verilog -sv <<EOF
+module tb #(parameter int P=4, S=12, SW=4)(
+  input logic [P-1:0] act, input logic [P*SW-1:0] sel_raw
+);
+  logic [P*SW-1:0] sel_c;
+  for (genvar g=0; g<P; g++) begin : clamp
+    wire [SW-1:0] k = sel_raw[g*SW +: SW];
+    assign sel_c[g*SW +: SW] = (k >= SW'(S)) ? (k - SW'(S)) : k;  // into [0,S)
+  end
+  logic [P-1:0] w1, w2;
+  pk_dut #(P,S,SW) u1(.act(act), .sel_flat(sel_c), .win(w1));
+  pk_ref #(P,S,SW) u2(.act(act), .sel_flat(sel_c), .win(w2));
+  always_comb assert (w1 == w2);
+endmodule
+EOF
+hierarchy -top tb
+flatten
+chformal -lower
+opt -full
+sat -verify -prove-asserts -show-ports tb
+design -reset
+log -pop
+
+# E4: SAME non-pow2 S=12 under -strict. Strict validation sweeps the FULL key
+# range and rejects rewrites that only hold via out-of-range don't-cares, so
+# the pass must decline to rewrite. This is the safety mode used by formal
+# synthesis flows: no reliance on out-of-range freedom.
+log -header "E4: non-pow2 S=12 -strict -> no rewrite (safety)"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=4, S=12, SW=4)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && !taken[sel[i]]) begin
+        taken[sel[i]] = 1'b1; win[i] = 1'b1;
+      end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+opt_priokey -strict
+select -assert-count 0 w:*priokey*
+design -reset
+log -pop
+
+# ============================================================================
+# Group F: additional near-miss negatives (no false rewrites)
+# ============================================================================
+
+# F1: CLEAR accumulator -- `avail` starts all-ones and bits are cleared. The
+# read cone does not bottom out at constant zero, so the accumulator trace
+# fails and nothing is rewritten.
+log -header "F1: clear-accumulator (rooted at all-ones) -> no rewrite"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=4, S=16, SW=4)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] avail;
+  always_comb begin
+    avail = '1; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && avail[sel[i]]) begin
+        avail[sel[i]] = 1'b0; win[i] = 1'b1;
+      end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+opt_priokey
+select -assert-count 0 w:*priokey*
+design -reset
+log -pop
+
+# F2: MULTI-hot set mask -- each source sets two adjacent slots (3 << sel).
+# The set arm is not a single one-hot (1 << key), so decode_onehot_key fails
+# and the accumulator is not recognized as a priority-by-key set chain.
+log -header "F2: multi-hot set mask -> no rewrite"
+log -push
+design -reset
+read_verilog -sv <<EOF
+module t #(parameter int P=3, S=16, SW=4)(
+  input  logic [P-1:0]         act,
+  input  logic [P-1:0][SW-1:0] sel,
+  output logic [P-1:0]         win
+);
+  logic [S-1:0] taken;
+  always_comb begin
+    taken = '0; win = '0;
+    for (int i=0;i<P;i++)
+      if (act[i] && !taken[sel[i]]) begin
+        taken = taken | (S'(3) << sel[i]);
+        win[i] = 1'b1;
+      end
+  end
+endmodule
+EOF
+hierarchy -top t
+proc
+opt
+opt_priokey
+select -assert-count 0 w:*priokey*
+design -reset
+log -pop