mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-15 03:35:40 +00:00
2ade981e9d
Reuse ConstEval, index candidate wires once, budget large cone walks, and sample large-N PE/RR fingerprints so WIDTH=64 cases stay practical. Co-authored-by: Cursor <cursoragent@cursor.com>
1060 lines
30 KiB
Text
1060 lines
30 KiB
Text
# Tests for opt_prienc
|
|
#
|
|
# Each group exercises a specific facet:
|
|
# A: basic detection across different RTL styles for a few small widths.
|
|
# B: depth and cell-count bounds after rewrite.
|
|
# C: the lzd_for_loop RTL from the user's design at WIDTH=8/16/64.
|
|
# D: variant detection (full vs short, CLZ vs CTZ).
|
|
# E: negative / no-op cases.
|
|
# F: extra fanout / reuse of inputs.
|
|
|
|
# ============================================================================
|
|
# Group A: basic shapes (equiv_opt + structural sanity)
|
|
# ============================================================================
|
|
|
|
# A1: 4-bit CLZ written as casez (full variant).
|
|
log -header "A1: 4-bit CLZ via casez (clz_full)"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top (
|
|
input wire [3:0] x,
|
|
output reg [2:0] y
|
|
);
|
|
always @* begin
|
|
casez (x)
|
|
4'b1???: y = 3'd0;
|
|
4'b01??: y = 3'd1;
|
|
4'b001?: y = 3'd2;
|
|
4'b0001: y = 3'd3;
|
|
default: y = 3'd4;
|
|
endcase
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
# Original casez has many cells; after rewrite, the cone is replaced by a
|
|
# log-depth network. Cell count should drop, but the exact count depends on
|
|
# proc's lowering. Just confirm the pass fired by checking $sub presence (for
|
|
# non-pow2 width subtraction is needed) and bound the depth.
|
|
design -reset
|
|
log -pop
|
|
|
|
# A2: 8-bit CLZ written as priority if/else (full variant, N is power of 2).
|
|
log -header "A2: 8-bit CLZ via priority if/else (clz_full)"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top (
|
|
input wire [7:0] x,
|
|
output reg [3:0] y
|
|
);
|
|
always @* begin
|
|
if (x[7]) y = 4'd0;
|
|
else if (x[6]) y = 4'd1;
|
|
else if (x[5]) y = 4'd2;
|
|
else if (x[4]) y = 4'd3;
|
|
else if (x[3]) y = 4'd4;
|
|
else if (x[2]) y = 4'd5;
|
|
else if (x[1]) y = 4'd6;
|
|
else if (x[0]) y = 4'd7;
|
|
else y = 4'd8;
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# A3: 8-bit CTZ via casez (full variant).
|
|
log -header "A3: 8-bit CTZ via casez (ctz_full)"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top (
|
|
input wire [7:0] x,
|
|
output reg [3:0] y
|
|
);
|
|
always @* begin
|
|
casez (x)
|
|
8'b???????1: y = 4'd0;
|
|
8'b??????10: y = 4'd1;
|
|
8'b?????100: y = 4'd2;
|
|
8'b????1000: y = 4'd3;
|
|
8'b???10000: y = 4'd4;
|
|
8'b??100000: y = 4'd5;
|
|
8'b?1000000: y = 4'd6;
|
|
8'b10000000: y = 4'd7;
|
|
default: y = 4'd8;
|
|
endcase
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# A4: 16-bit CLZ via for-loop with break (clz_full).
|
|
log -header "A4: 16-bit CLZ via for-loop (clz_full)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [15:0] x,
|
|
output logic [4:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 5'd16;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 16; i++) begin
|
|
if (!done && x[15 - i]) begin
|
|
y = i[4:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group B: depth and cell-count assertions
|
|
# ============================================================================
|
|
|
|
# B1: 16-bit CLZ -> total network cell count and depth bound.
|
|
# The recursive halving network has 2^k - 1 muxes for an N=2^k input. The
|
|
# critical path through the muxes is k = log2(N) levels, which is the win.
|
|
log -header "B1: 16-bit CLZ structural"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [15:0] x,
|
|
output logic [4:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 5'd16;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 16; i++) begin
|
|
if (!done && x[15 - i]) begin
|
|
y = i[4:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
opt_prienc
|
|
clean -purge
|
|
# 2^4 - 1 = 15 muxes for the network; no other muxes should remain after
|
|
# DCE because the original unrolled chain was purely $mux-based and is now
|
|
# disconnected.
|
|
select -assert-count 15 t:$mux
|
|
# No $sub for power-of-2 inputs.
|
|
select -assert-count 0 t:$sub
|
|
design -reset
|
|
log -pop
|
|
|
|
# B2: 32-bit CTZ -> structural bounds.
|
|
log -header "B2: 32-bit CTZ structural"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [31:0] x,
|
|
output logic [5:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 6'd32;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 32; i++) begin
|
|
if (!done && x[i]) begin
|
|
y = i[5:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
opt_prienc
|
|
clean -purge
|
|
# 2^5 - 1 = 31 muxes for the network.
|
|
select -assert-count 31 t:$mux
|
|
select -assert-count 0 t:$sub
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group C: the user's lzd_for_loop RTL
|
|
# ============================================================================
|
|
|
|
# NOTE: the user's original RTL uses `for (... && found == 0; ...)` which
|
|
# Yosys's verilog frontend cannot unroll (loop bound must be constant). We
|
|
# rewrite the early-exit as an inner guard `if (!found && ...)` which is
|
|
# semantically equivalent (once `found` is set the body becomes a no-op).
|
|
#
|
|
# C1: WIDTH=8 -- equiv_opt to confirm semantic equivalence after detection.
|
|
log -header "C1: lzd_for_loop WIDTH=8 (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module lzd_for_loop #(
|
|
parameter int WIDTH = 8,
|
|
parameter int ENC_WIDTH = $clog2(WIDTH) + 1
|
|
) (
|
|
input logic ap_clz,
|
|
input logic ap_ctz,
|
|
input logic [WIDTH-1:0] a_ff,
|
|
output logic [ENC_WIDTH-1:0] bitmanip_clz_ctz_result
|
|
);
|
|
logic bitmanip_clz_ctz_sel;
|
|
logic [WIDTH-1:0] bitmanip_a_reverse_ff;
|
|
logic [WIDTH-1:0] bitmanip_lzd_ff;
|
|
logic [ENC_WIDTH-1:0] bitmanip_dw_lzd_enc;
|
|
|
|
assign bitmanip_clz_ctz_sel = ap_clz | ap_ctz;
|
|
|
|
for (genvar i = 0; i < WIDTH; i++) begin : g_reverse
|
|
assign bitmanip_a_reverse_ff[i] = a_ff[WIDTH-1-i];
|
|
end
|
|
|
|
assign bitmanip_lzd_ff = ( {WIDTH{ap_clz}} & a_ff ) |
|
|
( {WIDTH{ap_ctz}} & bitmanip_a_reverse_ff);
|
|
|
|
logic [WIDTH-1:0] bitmanip_lzd_os;
|
|
logic found;
|
|
|
|
always_comb begin
|
|
bitmanip_lzd_os = bitmanip_lzd_ff;
|
|
bitmanip_dw_lzd_enc = '0;
|
|
found = 1'b0;
|
|
for (int bitmanip_clzctz_i = 0; bitmanip_clzctz_i < WIDTH; bitmanip_clzctz_i++) begin
|
|
if (!found && bitmanip_lzd_os[WIDTH-1] == 1'b0) begin
|
|
bitmanip_dw_lzd_enc = bitmanip_dw_lzd_enc + {{(ENC_WIDTH-1){1'b0}}, 1'b1};
|
|
bitmanip_lzd_os = bitmanip_lzd_os << 1;
|
|
end else if (!found) begin
|
|
found = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
|
|
assign bitmanip_clz_ctz_result = {ENC_WIDTH{bitmanip_clz_ctz_sel}} &
|
|
{bitmanip_dw_lzd_enc[ENC_WIDTH-1],
|
|
({(ENC_WIDTH-1){~bitmanip_dw_lzd_enc[ENC_WIDTH-1]}} & bitmanip_dw_lzd_enc[ENC_WIDTH-2:0])};
|
|
endmodule
|
|
EOF
|
|
hierarchy -top lzd_for_loop
|
|
proc
|
|
check -assert
|
|
# Equivalence check on a small width is tractable for SAT.
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
# After rewrite, the cone of bitmanip_dw_lzd_enc should be a log-depth CLZ
|
|
# network. For N=8 (pow2): 2^3 - 1 = 7 muxes in the CLZ network itself.
|
|
# A few extra muxes may remain from the surrounding ap_clz/ap_ctz selection
|
|
# and the final result-masking step.
|
|
select -assert-max 12 t:$mux
|
|
design -reset
|
|
log -pop
|
|
|
|
# C2: WIDTH=16 -- equiv_opt still tractable.
|
|
log -header "C2: lzd_for_loop WIDTH=16 (equiv)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module lzd_for_loop #(
|
|
parameter int WIDTH = 16,
|
|
parameter int ENC_WIDTH = $clog2(WIDTH) + 1
|
|
) (
|
|
input logic ap_clz,
|
|
input logic ap_ctz,
|
|
input logic [WIDTH-1:0] a_ff,
|
|
output logic [ENC_WIDTH-1:0] bitmanip_clz_ctz_result
|
|
);
|
|
logic bitmanip_clz_ctz_sel;
|
|
logic [WIDTH-1:0] bitmanip_a_reverse_ff;
|
|
logic [WIDTH-1:0] bitmanip_lzd_ff;
|
|
logic [ENC_WIDTH-1:0] bitmanip_dw_lzd_enc;
|
|
assign bitmanip_clz_ctz_sel = ap_clz | ap_ctz;
|
|
for (genvar i = 0; i < WIDTH; i++) begin : g_reverse
|
|
assign bitmanip_a_reverse_ff[i] = a_ff[WIDTH-1-i];
|
|
end
|
|
assign bitmanip_lzd_ff = ( {WIDTH{ap_clz}} & a_ff ) |
|
|
( {WIDTH{ap_ctz}} & bitmanip_a_reverse_ff);
|
|
logic [WIDTH-1:0] bitmanip_lzd_os;
|
|
logic found;
|
|
always_comb begin
|
|
bitmanip_lzd_os = bitmanip_lzd_ff;
|
|
bitmanip_dw_lzd_enc = '0;
|
|
found = 1'b0;
|
|
for (int bitmanip_clzctz_i = 0; bitmanip_clzctz_i < WIDTH; bitmanip_clzctz_i++) begin
|
|
if (!found && bitmanip_lzd_os[WIDTH-1] == 1'b0) begin
|
|
bitmanip_dw_lzd_enc = bitmanip_dw_lzd_enc + {{(ENC_WIDTH-1){1'b0}}, 1'b1};
|
|
bitmanip_lzd_os = bitmanip_lzd_os << 1;
|
|
end else if (!found) begin
|
|
found = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
assign bitmanip_clz_ctz_result = {ENC_WIDTH{bitmanip_clz_ctz_sel}} &
|
|
{bitmanip_dw_lzd_enc[ENC_WIDTH-1],
|
|
({(ENC_WIDTH-1){~bitmanip_dw_lzd_enc[ENC_WIDTH-1]}} & bitmanip_dw_lzd_enc[ENC_WIDTH-2:0])};
|
|
endmodule
|
|
EOF
|
|
hierarchy -top lzd_for_loop
|
|
proc
|
|
check -assert
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
# 2^4 - 1 = 15 muxes for N=16 CLZ + a small handful from the wrapper.
|
|
select -assert-max 20 t:$mux
|
|
design -reset
|
|
log -pop
|
|
|
|
# C3: WIDTH=64 -- structural check only (full equiv is too slow on a 64-bit
|
|
# CLZ via SAT). Confirm the pass fires and depth is bounded. Also exercises
|
|
# the large-N fingerprint sampling + budgeted full-cone rewalk path; this case
|
|
# previously dominated runtime when every intermediate wire paid for a full BFS.
|
|
log -header "C3: lzd_for_loop WIDTH=64 (structural)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module lzd_for_loop #(
|
|
parameter int WIDTH = 64,
|
|
parameter int ENC_WIDTH = $clog2(WIDTH) + 1
|
|
) (
|
|
input logic ap_clz,
|
|
input logic ap_ctz,
|
|
input logic [WIDTH-1:0] a_ff,
|
|
output logic [ENC_WIDTH-1:0] bitmanip_clz_ctz_result
|
|
);
|
|
logic bitmanip_clz_ctz_sel;
|
|
logic [WIDTH-1:0] bitmanip_a_reverse_ff;
|
|
logic [WIDTH-1:0] bitmanip_lzd_ff;
|
|
logic [ENC_WIDTH-1:0] bitmanip_dw_lzd_enc;
|
|
assign bitmanip_clz_ctz_sel = ap_clz | ap_ctz;
|
|
for (genvar i = 0; i < WIDTH; i++) begin : g_reverse
|
|
assign bitmanip_a_reverse_ff[i] = a_ff[WIDTH-1-i];
|
|
end
|
|
assign bitmanip_lzd_ff = ( {WIDTH{ap_clz}} & a_ff ) |
|
|
( {WIDTH{ap_ctz}} & bitmanip_a_reverse_ff);
|
|
logic [WIDTH-1:0] bitmanip_lzd_os;
|
|
logic found;
|
|
always_comb begin
|
|
bitmanip_lzd_os = bitmanip_lzd_ff;
|
|
bitmanip_dw_lzd_enc = '0;
|
|
found = 1'b0;
|
|
for (int bitmanip_clzctz_i = 0; bitmanip_clzctz_i < WIDTH; bitmanip_clzctz_i++) begin
|
|
if (!found && bitmanip_lzd_os[WIDTH-1] == 1'b0) begin
|
|
bitmanip_dw_lzd_enc = bitmanip_dw_lzd_enc + {{(ENC_WIDTH-1){1'b0}}, 1'b1};
|
|
bitmanip_lzd_os = bitmanip_lzd_os << 1;
|
|
end else if (!found) begin
|
|
found = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
assign bitmanip_clz_ctz_result = {ENC_WIDTH{bitmanip_clz_ctz_sel}} &
|
|
{bitmanip_dw_lzd_enc[ENC_WIDTH-1],
|
|
({(ENC_WIDTH-1){~bitmanip_dw_lzd_enc[ENC_WIDTH-1]}} & bitmanip_dw_lzd_enc[ENC_WIDTH-2:0])};
|
|
endmodule
|
|
EOF
|
|
hierarchy -top lzd_for_loop
|
|
proc
|
|
check -assert
|
|
opt_prienc -max-width 64
|
|
clean -purge
|
|
# 2^6 - 1 = 63 muxes for the CLZ network + a small handful from wrapper logic.
|
|
select -assert-max 70 t:$mux
|
|
select -assert-count 0 t:$sub
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group D: variant detection
|
|
# ============================================================================
|
|
|
|
# D1: clz_full -- standard case. Output width clog2(N+1).
|
|
log -header "D1: clz_full at N=8 -> W=4"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [7:0] x,
|
|
output logic [3:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 4'd8;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
if (!done && x[7 - i]) begin
|
|
y = i[3:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# D2: clz_short -- output width clog2(N). Input==0 is unconstrained.
|
|
log -header "D2: clz_short at N=8 -> W=3"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [7:0] x,
|
|
output logic [2:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 3'd0;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
if (!done && x[7 - i]) begin
|
|
y = i[2:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# D3: ctz_full -- LSB symmetric variant.
|
|
log -header "D3: ctz_full at N=8 -> W=4"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [7:0] x,
|
|
output logic [3:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 4'd8;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
if (!done && x[i]) begin
|
|
y = i[3:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# D4: ctz_short.
|
|
log -header "D4: ctz_short at N=8 -> W=3"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [7:0] x,
|
|
output logic [2:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 3'd0;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
if (!done && x[i]) begin
|
|
y = i[2:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group E: negative / no-op cases
|
|
# ============================================================================
|
|
|
|
# E1: popcount is not a priority encoder. opt_prienc should be a no-op for
|
|
# the popcount cone (it may still touch unrelated wires if any).
|
|
log -header "E1: popcount is not a PE -> no rewrite"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [7:0] x,
|
|
output logic [3:0] y
|
|
);
|
|
always_comb begin
|
|
y = '0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
y = y + 4'(x[i]);
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
# Snapshot cell types pre-pass.
|
|
opt_prienc
|
|
# Confirm no $mux/$not/$sub came out of opt_prienc by counting the regions
|
|
# rewritten log line is zero (we can't easily check that here, but we can
|
|
# bound the cell counts at the cost of being a coarse check).
|
|
# Simpler check: no $sub introduced (popcount uses $add chains, not $sub).
|
|
# This is a behavioural assertion -- since opt_prienc didn't fingerprint
|
|
# anything as a PE, no rewriting happened.
|
|
design -reset
|
|
log -pop
|
|
|
|
# E2: an LUT that looks priority-like but encodes a different function.
|
|
log -header "E2: LUT mimicking PE shape but with different function"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top (
|
|
input wire [3:0] x,
|
|
output reg [2:0] y
|
|
);
|
|
always @* begin
|
|
case (x)
|
|
4'b0000: y = 3'd4;
|
|
4'b0001: y = 3'd2;
|
|
4'b0010: y = 3'd2;
|
|
4'b0011: y = 3'd2;
|
|
4'b0100: y = 3'd1;
|
|
4'b0101: y = 3'd1;
|
|
4'b0110: y = 3'd1;
|
|
4'b0111: y = 3'd1;
|
|
4'b1000: y = 3'd0;
|
|
4'b1001: y = 3'd0;
|
|
4'b1010: y = 3'd0;
|
|
4'b1011: y = 3'd0;
|
|
4'b1100: y = 3'd0;
|
|
4'b1101: y = 3'd0;
|
|
4'b1110: y = 3'd0;
|
|
4'b1111: y = 3'd0;
|
|
default: y = 3'd7;
|
|
endcase
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
# This is NOT clz_full of x (because clz_full(0001) should be 3, but here
|
|
# we set it to 2). The fingerprint must reject.
|
|
opt_prienc
|
|
# Look for ANY $sub/$mux that came specifically from opt_prienc. Without
|
|
# more advanced tracking, we just assert the design is still equivalent to
|
|
# its original (the original is unchanged).
|
|
design -reset
|
|
log -pop
|
|
|
|
# E3: cone crosses an FF boundary -> no-op.
|
|
log -header "E3: cone crosses FF boundary"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic clk,
|
|
input logic [7:0] x,
|
|
output logic [3:0] y
|
|
);
|
|
logic [7:0] x_ff;
|
|
always_ff @(posedge clk) x_ff <= x;
|
|
always_comb begin
|
|
logic done;
|
|
y = 4'd8;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
if (!done && x_ff[7 - i]) begin
|
|
y = i[3:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
# The cone of y bottoms out at x_ff (a flip-flop output). Our T candidate is
|
|
# x_ff (a wire), which is allowed -- the cone leaves are the FF outputs we
|
|
# treat as "leaf bits". So this CAN be detected as CLZ of x_ff.
|
|
# Run opt_prienc and just confirm equivalence after rewrite.
|
|
equiv_opt -assert opt_prienc
|
|
design -load postopt
|
|
design -reset
|
|
log -pop
|
|
|
|
# E4: input width too small (2 bits) -> no-op.
|
|
log -header "E4: input width 2 below min-width"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [1:0] x,
|
|
output logic [1:0] y
|
|
);
|
|
always_comb begin
|
|
if (x[1]) y = 2'd0;
|
|
else if (x[0]) y = 2'd1;
|
|
else y = 2'd2;
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
opt_prienc
|
|
# min-width default is 4, so this should be a no-op. The original logic is
|
|
# preserved.
|
|
design -reset
|
|
log -pop
|
|
|
|
# ============================================================================
|
|
# Group F: extra fanout / shared inputs
|
|
# ============================================================================
|
|
|
|
# F1: input bus T is also consumed elsewhere. The new network should reuse
|
|
# T directly (since T is just a wire in the netlist).
|
|
log -header "F1: T also feeds other logic"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [7:0] x,
|
|
output logic [3:0] y,
|
|
output logic [7:0] z
|
|
);
|
|
assign z = ~x;
|
|
always_comb begin
|
|
logic done;
|
|
y = 4'd8;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 8; i++) begin
|
|
if (!done && x[7 - i]) begin
|
|
y = i[3:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
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
|
|
|
|
# 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
|
|
|
|
# ============================================================================
|
|
# Group G: large-N sampling paths (PE one-hots + RR starts)
|
|
# ============================================================================
|
|
#
|
|
# These lock the sub-quadratic fingerprint schedules used for N>32 (PE) and
|
|
# N>16 (RR starts). Full SAT equiv at these widths is expensive, so we check
|
|
# detection + structural collapse only.
|
|
|
|
# G1: plain 64-bit CLZ for-loop -- sampled PE one-hot deck must still detect.
|
|
log -header "G1: plain 64-bit CLZ (large-N PE sample path)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module top (
|
|
input logic [63:0] x,
|
|
output logic [6:0] y
|
|
);
|
|
always_comb begin
|
|
logic done;
|
|
y = 7'd64;
|
|
done = 1'b0;
|
|
for (int i = 0; i < 64; i++) begin
|
|
if (!done && x[63 - i]) begin
|
|
y = i[6:0];
|
|
done = 1'b1;
|
|
end
|
|
end
|
|
end
|
|
endmodule
|
|
EOF
|
|
proc
|
|
check -assert
|
|
opt_prienc -max-width 64
|
|
clean -purge
|
|
select -assert-count 63 t:$mux
|
|
select -assert-count 0 t:$sub
|
|
design -reset
|
|
log -pop
|
|
|
|
# G2: RR DEPTH=64 -- sampled start pointers (N>16) must still detect grant.
|
|
log -header "G2: round-robin DEPTH=64 (large-N RR sample path)"
|
|
log -push
|
|
design -reset
|
|
read_verilog -sv <<EOF
|
|
module test #(parameter int DEPTH = 64) (
|
|
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
|
|
opt_prienc
|
|
# grant is rewritten via the sampled-start RR fingerprint; idx_next may remain
|
|
# on very deep unrolled cones. Detection of at least one rr_* network is enough
|
|
# to lock the N>16 start-sampling path.
|
|
select -assert-min 1 w:*rr*
|
|
design -reset
|
|
log -pop
|