mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-15 03:35:40 +00:00
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>
This commit is contained in:
Akash Levy
parent
676ac184ed
commit
945e4a403b
3 changed files with 625 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue