mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-17 12:45:44 +00:00
945e4a403b
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>
859 lines
27 KiB
Text
859 lines
27 KiB
Text
# Tests for opt_first_fit_alloc
|
|
#
|
|
# The pass detects greedy first-fit "running-rank" resource allocators (the
|
|
# serial taken[]/done[] loop) and replaces the loop-carried cone with a
|
|
# log-depth priority-encode + all-pairs category-equality + prefix-sum + gather
|
|
# network. Where a per-slot field table (an "xbar") is driven from the same
|
|
# allocation, it is rewritten from the shared scan.
|
|
#
|
|
# Each group exercises a specific facet:
|
|
# A: basic detection + formal equivalence across allocator shapes (N=8).
|
|
# B: depth / cell-count bounds after rewrite (the actual QoR win).
|
|
# C: the customer slice (dsel + xbar) at N=8 (equiv) and N=16 (structural).
|
|
# D: variant detection (bc on/off, LSB/MSB-first scan).
|
|
# E: negative / no-op cases (no false rewrites).
|
|
# F: extra fanout / input reuse.
|
|
#
|
|
# Convention: every object the pass emits is named with an `ffa_` suffix, so
|
|
# `select w:*ffa_*` is a reliable "did the rewrite fire" probe.
|
|
|
|
# ============================================================================
|
|
# Group A: basic shapes (equiv_opt -assert)
|
|
# ============================================================================
|
|
|
|
# A1: dsel-only first-fit allocator, N=8 NB=4 (W=2) C=2, LSB-first, with bc.
|
|
log -header "A1: dsel-only allocator N=8 (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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
|
|
# Confirm the rewrite actually fired.
|
|
select -assert-min 1 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# A2: dsel + xbar (per-slot field gather) allocator, N=8.
|
|
log -header "A2: dsel + xbar allocator N=8 (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
input logic [N-1:0] sw,
|
|
output logic [N*W-1:0] dsel_flat,
|
|
output logic [NB*4*5-1:0] xbar_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [4:0] xbar [0:NB*4-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
for (int i=0;i<NB*4;i++) xbar[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int l=0;l<4;l++)
|
|
xbar[(j*4)+l] = (5'(({3'b0,cat_flat[i*C +: C]}*4)+l)) ^ {3'b0, sw[i], 1'b0};
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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];
|
|
for (genvar g=0;g<NB*4;g++) assign xbar_flat[g*5 +: 5] = xbar[g];
|
|
endmodule
|
|
EOF
|
|
hierarchy -top top
|
|
proc
|
|
memory -nomap -norom -nordff
|
|
opt
|
|
check -assert
|
|
equiv_opt -assert opt_first_fit_alloc
|
|
design -load postopt
|
|
select -assert-min 1 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# A3: dsel-only, no broadcast lanes (bc absent), N=8.
|
|
log -header "A3: dsel-only allocator without bc, N=8 (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if ((k!=i) && en[k] && (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
|
|
|
|
# ============================================================================
|
|
# Group B: depth / cell-count bounds (the QoR win)
|
|
# ============================================================================
|
|
|
|
# B1: N=8 allocator. The serial taken[]/done[] scan lowers to ~1000 $mux cells
|
|
# (a deep loop-carried chain). After the rewrite the rank gather is a log-depth
|
|
# network: the long mux chain is gone, replaced by all-pairs $eq + prefix-sum
|
|
# $add. Bounding the surviving $mux count is a robust proxy for the depth win.
|
|
log -header "B1: N=8 allocator structural bounds"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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
|
|
# Serial baseline: hundreds of muxes in the loop-carried chain.
|
|
select -assert-min 200 t:$mux
|
|
opt_first_fit_alloc
|
|
opt_clean
|
|
# The deep mux chain is replaced by the log-depth scan (measured ~17 muxes).
|
|
select -assert-max 60 t:$mux
|
|
# All-pairs category equality and the prefix-sum cascade are present.
|
|
select -assert-min 1 t:$eq
|
|
select -assert-min 1 t:$add
|
|
select -assert-min 1 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group C: the customer slice (dsel + xbar) and scaling
|
|
# ============================================================================
|
|
|
|
# C1: N=16 dsel-only allocator -- structural (full equiv at N=16 is SAT-hard,
|
|
# matching the serial-vs-parallel allocator equivalence cost; covered formally
|
|
# at N=8 in group A and by the in-pass fingerprint here).
|
|
log -header "C1: N=16 allocator structural"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=16, NB=8, C=3, W=3) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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
|
|
select -assert-min 1000 t:$mux
|
|
opt_first_fit_alloc
|
|
opt_clean
|
|
select -assert-max 120 t:$mux
|
|
select -assert-min 1 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# C2: N=16 dsel + xbar -- both deep cones must collapse from the shared scan.
|
|
log -header "C2: N=16 dsel + xbar structural"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=16, NB=8, C=3, W=3) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
input logic [N-1:0] sw,
|
|
output logic [N*W-1:0] dsel_flat,
|
|
output logic [NB*4*5-1:0] xbar_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [4:0] xbar [0:NB*4-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
for (int i=0;i<NB*4;i++) xbar[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int l=0;l<4;l++)
|
|
xbar[(j*4)+l] = (5'(({2'b0,cat_flat[i*C +: C]}*4)+l)) ^ {3'b0, sw[i], 1'b0};
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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];
|
|
for (genvar g=0;g<NB*4;g++) assign xbar_flat[g*5 +: 5] = xbar[g];
|
|
endmodule
|
|
EOF
|
|
hierarchy -top top
|
|
proc
|
|
memory -nomap -norom -nordff
|
|
opt
|
|
select -assert-min 1000 t:$mux
|
|
opt_first_fit_alloc
|
|
opt_clean
|
|
# Both the dsel and the xbar field gather were rewritten from one scan: the
|
|
# deep mux chains collapse (measured ~41 muxes) and the xbar per-slot field
|
|
# gather emits $bmux table-lookups (only the xbar path emits $bmux).
|
|
select -assert-min 1 w:*ffa_*
|
|
select -assert-max 120 t:$mux
|
|
select -assert-min 1 t:$bmux
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group D: variant detection (scan direction, category width)
|
|
# ============================================================================
|
|
|
|
# D1: MSB-first scan -- lanes processed from the high index down. The pass must
|
|
# detect the reversed priority and stay equivalent.
|
|
log -header "D1: MSB-first allocator (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=N-1;i>=0;i--)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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
|
|
|
|
# D2: a wider category (C=3, up to 8 distinct categories) with NB=8 slots.
|
|
log -header "D2: wider category C=3, NB=8 (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=8, C=3, W=3) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if ((k!=i) && en[k] && (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
|
|
|
|
# ============================================================================
|
|
# Group E: negative / no-op cases (no false rewrites)
|
|
# ============================================================================
|
|
|
|
# E1: a per-lane passthrough (dsel[i] = cat[i]) -- no allocation, no taken[]
|
|
# scan. There is no enable bus and the function is not a running rank.
|
|
log -header "E1: per-lane passthrough -> no rewrite"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, C=2, W=2) (
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [W-1:0] dsel [0:N-1];
|
|
always_comb
|
|
for (int i=0;i<N;i++) dsel[i] = W'(cat_flat[i*C +: C]);
|
|
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
|
|
endmodule
|
|
EOF
|
|
hierarchy -top top
|
|
proc
|
|
opt
|
|
opt_first_fit_alloc
|
|
select -assert-count 0 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# E2: a "last-fit" allocator (scans free slots from NB-1 down to 0) -- the same
|
|
# loop shape as first-fit but the OPPOSITE slot choice. The fingerprint must
|
|
# reject it as it is not the first-fit running rank.
|
|
log -header "E2: last-fit allocator near-miss -> no rewrite"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=NB-1;j>=0;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 ((k!=i) && en[k] && (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
|
|
opt_first_fit_alloc
|
|
select -assert-count 0 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# E3: input width below min (N=2 < default min-width 4) -> no candidate root.
|
|
log -header "E3: width below min-width -> no rewrite"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=2, NB=2, C=1, W=1) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
end
|
|
end
|
|
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
|
|
endmodule
|
|
EOF
|
|
hierarchy -top top
|
|
proc
|
|
opt
|
|
opt_first_fit_alloc
|
|
select -assert-count 0 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# E4: a plain unrelated mux feeding a small output -- nothing allocator-shaped.
|
|
log -header "E4: unrelated logic -> no rewrite"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top(input wire sel, input wire [7:0] a, b, output wire [7:0] y);
|
|
assign y = sel ? a : b;
|
|
endmodule
|
|
EOF
|
|
proc
|
|
opt
|
|
opt_first_fit_alloc
|
|
select -assert-count 0 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group F: extra fanout / shared inputs
|
|
# ============================================================================
|
|
|
|
# F1: the request and category inputs also feed unrelated outputs. The pass
|
|
# must still rewrite the allocator and stay equivalent (inputs are just wires).
|
|
log -header "F1: shared inputs / extra fanout (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=8, NB=4, C=2, W=2) (
|
|
input logic mode,
|
|
input logic [N-1:0] req,
|
|
input logic [N-1:0] oob,
|
|
input logic [N*C-1:0] cat_flat,
|
|
output logic [N*W-1:0] dsel_flat,
|
|
output logic [N-1:0] req_dbg,
|
|
output logic [N*C-1:0] cat_dbg
|
|
);
|
|
logic [N-1:0] en = req & {N{mode}};
|
|
logic [N-1:0] bc = oob & {N{mode}};
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
taken = '0; done = '0;
|
|
for (int i=0;i<N;i++)
|
|
if (en[i])
|
|
for (int j=0;j<NB;j++)
|
|
if (!taken[j] && !done[i]) begin
|
|
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
|
|
for (int k=0;k<N;k++)
|
|
if (((k!=i) && en[k] && (cat_flat[k*C +: C]==cat_flat[i*C +: C])) || bc[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];
|
|
assign req_dbg = ~req;
|
|
assign cat_dbg = cat_flat ^ {(N*C){mode}};
|
|
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
|
|
|
|
# ============================================================================
|
|
# Group G: coalesce-matrix variant (precomputed same_cat[i][k], raw-input en)
|
|
# ============================================================================
|
|
#
|
|
# Some RTL precomputes a per-leader "same_cat[i][k]" mask (gated ONLY on the
|
|
# leader's enable) and forward-coalesces the leader's slot into lane k without
|
|
# re-checking en[k]. Disabled lanes after a same-category leader therefore
|
|
# inherit that leader's slot (rather than 0). The pass detects this as the
|
|
# enable-independent forward-coalescing variant. These modules also drive the
|
|
# scan straight from a top-level request port (lane_en), exercising the
|
|
# primary-input enable/broadcast candidate path.
|
|
|
|
# G1: coalesce-matrix dsel-only, raw-input enable, N=8 (equiv).
|
|
log -header "G1: coalesce-matrix allocator, raw-input enable, N=8 (equiv)"
|
|
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 [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
|
|
# The coalesce variant fired (log shows "coalesce").
|
|
select -assert-min 1 w:*ffa_*
|
|
design -reset
|
|
log -pop
|
|
|
|
# G2: coalesce-matrix dsel + xbar, N=16 -- structural. Both deep cones must
|
|
# collapse from the shared scan (dsel via the coalesce gather, xbar via the
|
|
# per-slot field gather); full equiv at N=16 is SAT-hard (see group C).
|
|
log -header "G2: coalesce-matrix dsel + xbar, N=16 structural"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top #(parameter N=16, NB=8, C=3, W=3, A=5) (
|
|
input logic [N-1:0] lane_en,
|
|
input logic [N*C-1:0] cat_flat,
|
|
input logic [N-1:0] swap_bit,
|
|
output logic [N*W-1:0] dsel_flat,
|
|
output logic [32*A-1:0] xbar_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 [NB-1:0] taken;
|
|
logic [N-1:0] done;
|
|
logic [W-1:0] dsel [0:N-1];
|
|
logic [A-1:0] xbar [0:31];
|
|
always_comb begin
|
|
for (int i=0;i<N;i++) dsel[i] = '0;
|
|
for (int i=0;i<32;i++) xbar[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 l=0;l<4;l++)
|
|
xbar[(j*4)+l] = (A'(({2'b0,cat_flat[i*C +: C]}*4)+l)) ^ {3'b0, swap_bit[i], 1'b0};
|
|
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];
|
|
for (genvar g=0;g<32;g++) assign xbar_flat[g*A +: A] = xbar[g];
|
|
endmodule
|
|
EOF
|
|
hierarchy -top top
|
|
proc
|
|
memory -nomap -norom -nordff
|
|
opt
|
|
select -assert-min 1000 t:$mux
|
|
opt_first_fit_alloc
|
|
opt_clean
|
|
select -assert-min 1 w:*ffa_*
|
|
# The deep mux chains collapse and the xbar emits $bmux table-lookups.
|
|
select -assert-max 200 t:$mux
|
|
select -assert-min 1 t:$bmux
|
|
design -reset
|
|
log -pop
|
|
|
|
# G3: coalesce-matrix but LAST-fit slot choice (scans free slots NB-1..0). The
|
|
# same_cat coalescing is present but the slot assignment is not first-fit, so
|
|
# neither the standard nor the coalesce fingerprint may match.
|
|
log -header "G3: coalesce-matrix last-fit near-miss -> no rewrite"
|
|
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 [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=NB-1;j>=0;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
|
|
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
|