mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-15 19:55:41 +00:00
Merge pull request #204 from Silimate/akashlevy/opt_prienc-consteval-fix
opt_prienc: fix ConstEval crash on constant/aliased fingerprint inputs
This commit is contained in:
Akash Levy
GitHub
commit
a4fa9c31e8
4 changed files with 647 additions and 0 deletions
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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