3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-20 06:05:50 +00:00

Merge pull request #202 from Silimate/akashlevy/qor-pattern-passes

opt: recognize three QoR logic-depth patterns
This commit is contained in:
Akash Levy 2026-07-06 13:56:29 -07:00 committed by GitHub
commit 087f5bd254
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 1384 additions and 14 deletions

View file

@ -590,3 +590,170 @@ 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

View file

@ -672,3 +672,129 @@ equiv_opt -assert opt_prienc
design -load postopt
design -reset
log -pop
# ============================================================================
# Group RR: round-robin (rotated priority) arbiters
# ============================================================================
#
# grant / idx_next = first set request bit scanning upward (wrapping) from
# just after a stored pointer idx_last. RTL spells this as a DEPTH-iteration
# idx-- loop over req[idx] that elaborates into a serial mux/shift chain; the
# pass replaces it with a log-depth threshold-mask + CTZ network.
# RR1: power-of-2 DEPTH -- full sequential equivalence. Both grant and
# idx_next collapse and every serial req[idx] $shiftx is removed.
log -header "RR1: round-robin arbiter, DEPTH=16 (sequential equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int DEPTH = 16) (
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*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# RR2: non-power-of-2 DEPTH -- combinational equivalence over the reachable
# pointer range (idx_last in [0,DEPTH)). We rewrite one copy of the arbiter,
# leave a reference copy untouched, and SAT-prove they agree once the pointer
# input is mapped into [0,DEPTH).
log -header "RR2: round-robin arbiter, DEPTH=13 (reachable-range equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module rr_dut #(parameter int N=13, parameter int W=4) (
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
# The serial chain collapsed into the log-depth network.
select -assert-min 1 w:*rr*
select -assert-count 0 t:$shiftx
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=13, parameter int W=4)(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
# RR3: negative -- a downward-scanning arbiter (opposite rotation) is a
# different function and must not be rewritten as round-robin.
log -header "RR3: downward-scan arbiter -> 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, input logic [W-1:0] s,
output logic [W-1:0] grant
);
always_comb begin
logic [W-1:0] idx; idx=s; grant='0;
for (int i=0;i<N;i++) begin
if (req[idx]) grant=idx;
if (idx==W'(N-1)) idx='0; else idx++; // scans the other way
end
end
endmodule
EOF
hierarchy -top test
proc
opt
opt_prienc
select -assert-count 0 w:*rr*
design -reset
log -pop

240
tests/opt/opt_priokey.ys Normal file
View file

@ -0,0 +1,240 @@
# Tests for opt_priokey
#
# The pass detects a serial "priority-by-key" set accumulator: several sources
# each carry a small key and claim it if no earlier source already did. This
# elaborates into a chain of dynamic-index reads/writes ($shiftx / $shift) into
# a wide one-hot "taken" vector, whose depth grows with both the number of
# sources P and the accumulator width S. Every dynamic read taken[key[j]] is
# provably equal to the pairwise reduction
#
# OR over i<j of ( set_guard[i] & key[i] == key[j] )
#
# so the pass replaces each read with that compare reduction and drops the wide
# dynamic indexing. Correctness of every rewrite is validated by an in-pass
# ConstEval fingerprint over the reachable key range [0,S).
#
# Each group exercises a specific facet:
# A: formal equivalence across (P,S) shapes (power-of-two S -> full equiv).
# B: structural win -- the $shiftx chain is gone after the rewrite.
# C: negative / no-op cases (no false rewrites).
#
# Convention: every object the pass emits is named with a `priokey_` suffix, so
# `select w:*priokey*` is a reliable "did the rewrite fire" probe.
# ============================================================================
# Group A: formal equivalence (equiv_opt -assert)
# ============================================================================
# A1: P=3 sources into a 64-slot accumulator (SW=6, all keys reachable).
log -header "A1: priority-by-key dedup P=3 S=64 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=3, parameter int S=64, parameter int SW=6)(
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*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# A2: P=4 sources into a 16-slot accumulator (SW=4).
log -header "A2: priority-by-key dedup P=4 S=16 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4, parameter int S=16, parameter int SW=4)(
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*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# A3: P=5 sources into an 8-slot accumulator (SW=3) -- deeper source chain.
log -header "A3: priority-by-key dedup P=5 S=8 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=5, parameter int S=8, parameter int SW=3)(
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*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# ============================================================================
# Group B: structural win (the dynamic-index chain disappears)
# ============================================================================
# B1: P=6 sources, 64-slot accumulator. Before the rewrite the serial scan uses
# per-source dynamic reads ($shiftx). After the rewrite those reads are gone,
# replaced by pairwise $eq comparisons -- the QoR (depth) win.
log -header "B1: priority-by-key structural, P=6 S=64"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=6, parameter int S=64, parameter int SW=6)(
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
# Serial baseline: the dynamic-index reads are present.
select -assert-min 1 t:$shiftx
opt_priokey
opt_clean
# The wide dynamic indexing is gone, replaced by pairwise key comparisons.
select -assert-count 0 t:$shiftx
select -assert-min 1 t:$eq
select -assert-min 1 w:*priokey*
design -reset
log -pop
# ============================================================================
# Group C: negative / no-op cases (no false rewrites)
# ============================================================================
# C1: the "taken" vector is a primary input, not a set accumulator rooted at 0.
# The dynamic read has no traceable set history, so the pass must not fire.
log -header "C1: non-accumulator dynamic read -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int S=64, parameter int SW=6)(
input logic [S-1:0] taken,
input logic [SW-1:0] sel,
output logic hit
);
assign hit = taken[sel];
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop
# C2: a plain per-lane passthrough -- no dynamic indexing at all.
log -header "C2: per-lane passthrough -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4)(
input logic [P-1:0] a,
input logic [P-1:0] b,
output logic [P-1:0] y
);
assign y = a & b;
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop
# C3: a dynamic write accumulator with NO conflict check -- every source
# unconditionally sets its key and reads are absent (win is a direct index).
# There is no taken[]-guarded read chain to rewrite.
log -header "C3: unconditional writes, no guarded read -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=3, parameter int S=16, parameter int SW=4)(
input logic [P-1:0][SW-1:0] sel,
output logic [S-1:0] taken
);
always_comb begin
taken = '0;
for (int i=0;i<P;i++)
taken[sel[i]] = 1'b1;
end
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop