mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-23 15:42:32 +00:00
Merge remote-tracking branch 'silimate/main' into update_from_upstream
This commit is contained in:
Mohamed Gaber
commit
0217efb67d
12 changed files with 2120 additions and 46 deletions
|
|
@ -55,6 +55,42 @@ module opt_argmax_w32 (
|
|||
end
|
||||
endmodule
|
||||
|
||||
module opt_argmax_identity_w8 (
|
||||
input wire [7:0] valid_in,
|
||||
input wire [7:0][4:0] val_in,
|
||||
output reg [2:0] best_idx
|
||||
);
|
||||
always_comb begin
|
||||
best_idx = '0;
|
||||
for (int k = 1; k < 8; k++) begin
|
||||
if (!valid_in[best_idx] && valid_in[k]) begin
|
||||
best_idx = k;
|
||||
end else if (valid_in[best_idx] && valid_in[k] &&
|
||||
(val_in[best_idx] < val_in[k])) begin
|
||||
best_idx = k;
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
module opt_argmax_identity_w16 (
|
||||
input wire [15:0] valid_in,
|
||||
input wire [15:0][7:0] val_in,
|
||||
output reg [3:0] best_idx
|
||||
);
|
||||
always_comb begin
|
||||
best_idx = '0;
|
||||
for (int k = 1; k < 16; k++) begin
|
||||
if (!valid_in[best_idx] && valid_in[k]) begin
|
||||
best_idx = k;
|
||||
end else if (valid_in[best_idx] && valid_in[k] &&
|
||||
(val_in[best_idx] < val_in[k])) begin
|
||||
best_idx = k;
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
module opt_argmax_flat (
|
||||
input wire [7:0] sig,
|
||||
input wire [23:0] sig3,
|
||||
|
|
|
|||
|
|
@ -74,6 +74,49 @@ sat -prove-asserts -verify
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Identity-index masked argmax self-equivalence"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_argmax.sv
|
||||
verific -import opt_argmax_identity_w8
|
||||
proc; opt_clean
|
||||
rename opt_argmax_identity_w8 gold
|
||||
|
||||
read -sv opt_argmax.sv
|
||||
verific -import opt_argmax_identity_w8
|
||||
proc; opt_clean
|
||||
select -module opt_argmax_identity_w8
|
||||
opt_argmax
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*argmax*
|
||||
rename opt_argmax_identity_w8 gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Identity-index masked argmax structural rewrite"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_argmax.sv
|
||||
verific -import opt_argmax_identity_w16
|
||||
proc; opt_clean
|
||||
opt_argmax
|
||||
opt_clean
|
||||
select -assert-min 1 w:*argmax*
|
||||
select -assert-none c:*argmax_val*
|
||||
select -assert-none c:LessThan_*
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Scaled masked argmax: 8 entries structural"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
|
|||
|
|
@ -114,6 +114,23 @@ select -assert-count 32 t:$gt
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Renamed ports: forward dense pack"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_renamed.sv
|
||||
verific -import opt_compact_prefix_pack_renamed
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
select -assert-none t:$shl
|
||||
select -assert-none t:$mux
|
||||
select -assert-count 7 t:$add
|
||||
select -assert-count 8 t:$gt
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Exact regression size: 16-entry reverse suffix read"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
@ -131,6 +148,53 @@ select -assert-min 1 t:$eq
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Renamed ports: reverse suffix read"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_renamed.sv
|
||||
verific -import opt_compact_prefix_sub_renamed
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
select -assert-none t:$sub
|
||||
select -assert-none t:$mux
|
||||
select -assert-min 1 t:$add
|
||||
select -assert-min 1 t:$eq
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Yosys frontend: forward dense pack"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -sv opt_compact_prefix_yosys_frontend.v
|
||||
hierarchy -top opt_compact_prefix_yosys_pack
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
select -assert-none t:$shl
|
||||
select -assert-none t:$mux
|
||||
select -assert-count 7 t:$add
|
||||
select -assert-count 8 t:$gt
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Yosys frontend: reverse suffix read"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -sv opt_compact_prefix_yosys_frontend.v
|
||||
hierarchy -top opt_compact_prefix_yosys_sub
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
select -assert-none t:$sub
|
||||
select -assert-none t:$mux
|
||||
select -assert-min 1 t:$add
|
||||
select -assert-min 1 t:$eq
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Reverse suffix read with add-by-minus-one decrement"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
@ -286,3 +350,117 @@ select -assert-none opt_compact_prefix_multi_match/t:$mux
|
|||
select -assert-count 1 opt_compact_prefix_multi_keep/t:$mux
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Modulo decimation self-equivalence (MSB-first)"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod8
|
||||
proc; opt_clean
|
||||
rename opt_compact_prefix_mod8 gold
|
||||
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod8
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
bmuxmap
|
||||
rename opt_compact_prefix_mod8 gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Modulo decimation self-equivalence (LSB-first)"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod_lsb8
|
||||
proc; opt_clean
|
||||
rename opt_compact_prefix_mod_lsb8 gold
|
||||
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod_lsb8
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
bmuxmap
|
||||
rename opt_compact_prefix_mod_lsb8 gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Modulo decimation structural rewrite"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod16
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
select -assert-none t:$mux
|
||||
select -assert-none t:$sub
|
||||
select -assert-min 1 t:$add
|
||||
select -assert-min 1 t:$eq
|
||||
select -assert-min 1 t:$bmux
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Modulo decimation: opt_parallel_prefix collapses the popcount cascade"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod16
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
opt_clean
|
||||
opt_parallel_prefix -arith
|
||||
opt_clean
|
||||
select -assert-none t:$mux
|
||||
select -assert-none t:$sub
|
||||
select -assert-min 1 t:$add
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative: modulo off-by-one near miss unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod_offbyone
|
||||
proc; opt_clean
|
||||
opt_compact_prefix
|
||||
select -assert-none w:*compact*
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Max width: modulo decimation left unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_compact_prefix_mod.sv
|
||||
verific -import opt_compact_prefix_mod16
|
||||
proc; opt_clean
|
||||
select -assert-min 1 t:$mux
|
||||
opt_compact_prefix -max_width 8
|
||||
select -assert-min 1 t:$mux
|
||||
select -assert-none w:*compact*
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
86
tests/silimate/opt_compact_prefix_mod.sv
Normal file
86
tests/silimate/opt_compact_prefix_mod.sv
Normal file
|
|
@ -0,0 +1,86 @@
|
|||
// Modulo-n decimation loops: scanning the enable vector, mark every n-th
|
||||
// enabled bit. Exercised by opt_compact_prefix's modulo decimation rewrite
|
||||
// (cf. the qor_spi_ra_add_chain2 regression).
|
||||
|
||||
module opt_compact_prefix_mod8 (
|
||||
input logic [7:0] en,
|
||||
input logic [3:0] n,
|
||||
output logic [7:0] mask
|
||||
);
|
||||
always_comb begin
|
||||
mask = '0;
|
||||
for (int I = 7, cnt = 0; I >= 0; I--) begin
|
||||
if (en[I] && (n > 0)) begin
|
||||
if (cnt == (n - 1)) begin
|
||||
mask[I] = 1'b1;
|
||||
cnt = 0;
|
||||
end else begin
|
||||
cnt++;
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
module opt_compact_prefix_mod16 (
|
||||
input logic [15:0] en,
|
||||
input logic [4:0] n,
|
||||
output logic [15:0] mask
|
||||
);
|
||||
always_comb begin
|
||||
mask = '0;
|
||||
for (int I = 15, cnt = 0; I >= 0; I--) begin
|
||||
if (en[I] && (n > 0)) begin
|
||||
if (cnt == (n - 1)) begin
|
||||
mask[I] = 1'b1;
|
||||
cnt = 0;
|
||||
end else begin
|
||||
cnt++;
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Same function, but scanned LSB-first (exercises the mirrored direction).
|
||||
module opt_compact_prefix_mod_lsb8 (
|
||||
input logic [7:0] en,
|
||||
input logic [3:0] n,
|
||||
output logic [7:0] mask
|
||||
);
|
||||
always_comb begin
|
||||
mask = '0;
|
||||
for (int I = 0, cnt = 0; I < 8; I++) begin
|
||||
if (en[I] && (n > 0)) begin
|
||||
if (cnt == (n - 1)) begin
|
||||
mask[I] = 1'b1;
|
||||
cnt = 0;
|
||||
end else begin
|
||||
cnt++;
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Negative near-miss: marks every (n+1)-th enabled bit (reset on cnt == n),
|
||||
// a different function that must NOT be rewritten.
|
||||
module opt_compact_prefix_mod_offbyone (
|
||||
input logic [7:0] en,
|
||||
input logic [3:0] n,
|
||||
output logic [7:0] mask
|
||||
);
|
||||
always_comb begin
|
||||
mask = '0;
|
||||
for (int I = 7, cnt = 0; I >= 0; I--) begin
|
||||
if (en[I] && (n > 0)) begin
|
||||
if (cnt == n) begin
|
||||
mask[I] = 1'b1;
|
||||
cnt = 0;
|
||||
end else begin
|
||||
cnt++;
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
32
tests/silimate/opt_compact_prefix_renamed.sv
Normal file
32
tests/silimate/opt_compact_prefix_renamed.sv
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
module opt_compact_prefix_pack_renamed (
|
||||
input logic [7:0] in_bits,
|
||||
output logic [7:0] packed_bits
|
||||
);
|
||||
always_comb begin
|
||||
packed_bits = '0;
|
||||
for (int I = 0, indx = 0; I < 8; I++) begin
|
||||
if (in_bits[I]) begin
|
||||
packed_bits[indx] = in_bits[I];
|
||||
indx += 1;
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
module opt_compact_prefix_sub_renamed (
|
||||
input logic [15:0] stall_vec,
|
||||
input logic [15:0] payload_vec,
|
||||
output logic [15:0] allow_mask
|
||||
);
|
||||
always_comb begin
|
||||
allow_mask = '0;
|
||||
for (int I = 8, indx = 8; I > 0; I--) begin
|
||||
if (stall_vec[I-1]) begin
|
||||
allow_mask[I-1] = 1'b0;
|
||||
end else begin
|
||||
allow_mask[I-1] = payload_vec[indx-1];
|
||||
indx = indx - 1;
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
38
tests/silimate/opt_compact_prefix_yosys_frontend.v
Normal file
38
tests/silimate/opt_compact_prefix_yosys_frontend.v
Normal file
|
|
@ -0,0 +1,38 @@
|
|||
module opt_compact_prefix_yosys_pack (
|
||||
input wire [7:0] in_bits,
|
||||
output reg [7:0] packed_bits
|
||||
);
|
||||
integer I;
|
||||
integer indx;
|
||||
always @* begin
|
||||
packed_bits = 8'b0;
|
||||
indx = 0;
|
||||
for (I = 0; I < 8; I = I + 1) begin
|
||||
if (in_bits[I]) begin
|
||||
packed_bits[indx] = in_bits[I];
|
||||
indx = indx + 1;
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
module opt_compact_prefix_yosys_sub (
|
||||
input wire [15:0] stall_vec,
|
||||
input wire [15:0] payload_vec,
|
||||
output reg [15:0] allow_mask
|
||||
);
|
||||
integer I;
|
||||
integer indx;
|
||||
always @* begin
|
||||
allow_mask = 16'b0;
|
||||
indx = 8;
|
||||
for (I = 8; I > 0; I = I - 1) begin
|
||||
if (stall_vec[I-1]) begin
|
||||
allow_mask[I-1] = 1'b0;
|
||||
end else begin
|
||||
allow_mask[I-1] = payload_vec[indx-1];
|
||||
indx = indx - 1;
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
235
tests/silimate/opt_priority_onehot.sv
Normal file
235
tests/silimate/opt_priority_onehot.sv
Normal file
|
|
@ -0,0 +1,235 @@
|
|||
// Test designs for opt_priority_onehot.
|
||||
//
|
||||
// Each "positive" module computes a lowest/highest-index priority select of a
|
||||
// per-lane index field and scatters the winning field into a one-hot output,
|
||||
// mirroring the qor_spi_ra_binary_tree shape. The "negative" modules look
|
||||
// similar but compute a different function and must be left untouched.
|
||||
|
||||
// Main shape: N=16 lanes, 5-bit id lanes, 4-bit field id[*][4:1], LSB-first.
|
||||
module pri_onehot_basic (
|
||||
input wire [15:0] req,
|
||||
input wire [15:0][4:0] id,
|
||||
output reg [15:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [15:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 16; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][4:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// One-based ports [N:1] / id[I][IDX_W:1], matching the qor_spi_ra_binary_tree
|
||||
// regression exactly (Verific splits id into id[1]..id[16]).
|
||||
module pri_onehot_onebased (
|
||||
input wire [16:1] req,
|
||||
input wire [16:1][4:0] id,
|
||||
output reg [15:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [16:1] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 1; I <= 16; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][4:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Packed field: no per-lane gap (ID_W == IDX_W == 4), field id[*][3:0].
|
||||
module pri_onehot_packed (
|
||||
input wire [15:0] req,
|
||||
input wire [15:0][3:0] id,
|
||||
output reg [15:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [15:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 16; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][3:0]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Scaled down: N=8, 4-bit id lanes, 3-bit field id[*][3:1], W=8.
|
||||
module pri_onehot_w8 (
|
||||
input wire [7:0] req,
|
||||
input wire [7:0][3:0] id,
|
||||
output reg [7:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [7:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 8; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][3:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Scaled up: N=32, 6-bit id lanes, 5-bit field id[*][5:1], W=32.
|
||||
module pri_onehot_w32 (
|
||||
input wire [31:0] req,
|
||||
input wire [31:0][5:0] id,
|
||||
output reg [31:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [31:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 32; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][5:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Lane count != output width: N=8 lanes, 4-bit field, W=16.
|
||||
module pri_onehot_n8_w16 (
|
||||
input wire [7:0] req,
|
||||
input wire [7:0][4:0] id,
|
||||
output reg [15:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [7:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 8; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][4:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// MSB-first priority: highest set index wins (W=8 to keep SAT cheap).
|
||||
module pri_onehot_msb (
|
||||
input wire [7:0] req,
|
||||
input wire [7:0][3:0] id,
|
||||
output reg [7:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [7:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 7; I >= 0; I--) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][3:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Two independent priority-onehot regions in one module.
|
||||
module pri_onehot_two_regions (
|
||||
input wire [7:0] req_a,
|
||||
input wire [7:0][3:0] id_a,
|
||||
input wire [7:0] req_b,
|
||||
input wire [7:0][3:0] id_b,
|
||||
output reg [7:0] oneh_a,
|
||||
output reg [7:0] oneh_b
|
||||
);
|
||||
always_comb begin
|
||||
reg [7:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh_a = '0;
|
||||
for (int I = 0; I < 8; I++) begin
|
||||
sel[I] = req_a[I] & ~(|acc);
|
||||
acc[I] = req_a[I];
|
||||
oneh_a[id_a[I][3:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
always_comb begin
|
||||
reg [7:0] acc2, sel2;
|
||||
acc2 = '0; sel2 = '0; oneh_b = '0;
|
||||
for (int I = 0; I < 8; I++) begin
|
||||
sel2[I] = req_b[I] & ~(|acc2);
|
||||
acc2[I] = req_b[I];
|
||||
oneh_b[id_b[I][3:1]] |= sel2[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// One-hot output also consumed by a downstream parity output.
|
||||
module pri_onehot_shared_consumer (
|
||||
input wire [7:0] req,
|
||||
input wire [7:0][3:0] id,
|
||||
output reg [7:0] oneh,
|
||||
output wire par
|
||||
);
|
||||
always_comb begin
|
||||
reg [7:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 8; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][3:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
assign par = ^oneh;
|
||||
endmodule
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Negative / near-miss modules: must NOT be rewritten.
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
// No priority: OR of all decoded fields (output is generally not one-hot).
|
||||
module pri_onehot_orall (
|
||||
input wire [15:0] req,
|
||||
input wire [15:0][4:0] id,
|
||||
output reg [15:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
oneh = '0;
|
||||
for (int I = 0; I < 16; I++)
|
||||
oneh[id[I][4:1]] |= req[I];
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Nonzero default when no request: function is not "0 when all-invalid".
|
||||
module pri_onehot_nonzero_default (
|
||||
input wire [15:0] req,
|
||||
input wire [15:0][4:0] id,
|
||||
output reg [15:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [15:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '1;
|
||||
for (int I = 0; I < 16; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][4:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Non-power-of-two output width.
|
||||
module pri_onehot_nonpow2 (
|
||||
input wire [11:0] req,
|
||||
input wire [11:0][3:0] id,
|
||||
output reg [11:0] oneh
|
||||
);
|
||||
always_comb begin
|
||||
reg [11:0] acc, sel;
|
||||
acc = '0; sel = '0; oneh = '0;
|
||||
for (int I = 0; I < 12; I++) begin
|
||||
sel[I] = req[I] & ~(|acc);
|
||||
acc[I] = req[I];
|
||||
oneh[id[I][3:1]] |= sel[I];
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Unrelated mux logic.
|
||||
module pri_onehot_unrelated (
|
||||
input wire [15:0] a,
|
||||
input wire [15:0] b,
|
||||
input wire s,
|
||||
output wire [15:0] y
|
||||
);
|
||||
assign y = s ? a : b;
|
||||
endmodule
|
||||
301
tests/silimate/opt_priority_onehot.ys
Normal file
301
tests/silimate/opt_priority_onehot.ys
Normal file
|
|
@ -0,0 +1,301 @@
|
|||
# Tests for opt_priority_onehot.
|
||||
|
||||
# Helper pattern per positive module: import a gold copy, import a gate copy,
|
||||
# rewrite the gate, assert the rewrite fired, then prove gold == gate by SAT.
|
||||
|
||||
log -header "Basic priority-onehot self-equivalence (N=16, field id[*][4:1])"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_basic
|
||||
proc; opt_clean
|
||||
rename pri_onehot_basic gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_basic
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_basic
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_basic gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "One-based [N:1] ports self-equivalence (regression shape)"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_onebased
|
||||
proc; opt_clean
|
||||
rename pri_onehot_onebased gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_onebased
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_onebased
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_onebased gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Packed field self-equivalence (ID_W == IDX_W, no gap)"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_packed
|
||||
proc; opt_clean
|
||||
rename pri_onehot_packed gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_packed
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_packed
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_packed gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Scaled N=8 self-equivalence"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_w8
|
||||
proc; opt_clean
|
||||
rename pri_onehot_w8 gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_w8
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_w8
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_w8 gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Lane count != output width self-equivalence (N=8, W=16)"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_n8_w16
|
||||
proc; opt_clean
|
||||
rename pri_onehot_n8_w16 gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_n8_w16
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_n8_w16
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_n8_w16 gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "MSB-first priority self-equivalence"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_msb
|
||||
proc; opt_clean
|
||||
rename pri_onehot_msb gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_msb
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_msb
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_msb gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Two independent regions self-equivalence"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_two_regions
|
||||
proc; opt_clean
|
||||
rename pri_onehot_two_regions gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_two_regions
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_two_regions
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 2 w:*prionehot*
|
||||
rename pri_onehot_two_regions gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Shared consumer of one-hot output stays equivalent"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_shared_consumer
|
||||
proc; opt_clean
|
||||
rename pri_onehot_shared_consumer gold
|
||||
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_shared_consumer
|
||||
proc; opt_clean
|
||||
select -module pri_onehot_shared_consumer
|
||||
opt_priority_onehot
|
||||
select -clear
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
rename pri_onehot_shared_consumer gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
sat -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Scaled N=32 structural rewrite"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_w32
|
||||
proc; opt_clean
|
||||
opt_priority_onehot
|
||||
opt_clean
|
||||
select -assert-min 1 w:*prionehot*
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative: OR-of-all (no priority) unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_orall
|
||||
proc; opt_clean
|
||||
opt_priority_onehot
|
||||
select -assert-none w:*prionehot*
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative: nonzero all-invalid default unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_nonzero_default
|
||||
proc; opt_clean
|
||||
opt_priority_onehot
|
||||
select -assert-none w:*prionehot*
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative: non-power-of-two output width unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_nonpow2
|
||||
proc; opt_clean
|
||||
opt_priority_onehot
|
||||
select -assert-none w:*prionehot*
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative: unrelated mux logic unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_unrelated
|
||||
proc; opt_clean
|
||||
select -assert-count 1 t:$mux
|
||||
opt_priority_onehot
|
||||
select -assert-none w:*prionehot*
|
||||
select -assert-count 1 t:$mux
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Max-width below lane count leaves design unchanged"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
read -sv opt_priority_onehot.sv
|
||||
verific -import pri_onehot_basic
|
||||
proc; opt_clean
|
||||
opt_priority_onehot -max_width 8
|
||||
select -assert-none w:*prionehot*
|
||||
design -reset
|
||||
log -pop
|
||||
Loading…
Add table
Add a link
Reference in a new issue