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