mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-21 14:45:50 +00:00
opt_vps
This commit is contained in:
Akash Levy
parent
9a099f73b3
commit
1820526a9a
7 changed files with 834 additions and 0 deletions
159
tests/silimate/opt_vps.ys
Normal file
159
tests/silimate/opt_vps.ys
Normal file
|
|
@ -0,0 +1,159 @@
|
|||
# =============================================================================
|
||||
# Test 1: SAT equivalence — VPS byte-write vs case-statement reference
|
||||
# Proves opt_vps produces a logically equivalent circuit to hand-written
|
||||
# case statements for a 32-bit register with 4 byte lanes.
|
||||
# =============================================================================
|
||||
log -header "SAT equivalence: byte-write VPS vs case-statement ref"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
|
||||
read -sv opt_vps_byte_write.sv
|
||||
verific -import opt_vps_byte_write
|
||||
proc; opt_clean
|
||||
opt_vps; opt_clean
|
||||
rename opt_vps_byte_write gate
|
||||
|
||||
read -sv opt_vps_byte_write_ref.sv
|
||||
verific -import opt_vps_byte_write
|
||||
proc; opt_clean
|
||||
rename opt_vps_byte_write gold
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
clk2fflogic
|
||||
sat -set-init-zero -tempinduct -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 2: SAT self-equivalence — byte-write before vs after opt_vps
|
||||
# Proves opt_vps does not change the functional behavior.
|
||||
# =============================================================================
|
||||
log -header "SAT self-equivalence: byte-write before vs after opt_vps"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
|
||||
read -sv opt_vps_byte_write.sv
|
||||
verific -import opt_vps_byte_write
|
||||
proc; opt_clean
|
||||
rename opt_vps_byte_write gold
|
||||
|
||||
read -sv opt_vps_byte_write.sv
|
||||
verific -import opt_vps_byte_write
|
||||
proc; opt_clean
|
||||
opt_vps; opt_clean
|
||||
rename opt_vps_byte_write gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
clk2fflogic
|
||||
sat -set-init-zero -tempinduct -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 3: SAT self-equivalence — wide (128-bit, 16-bit lanes)
|
||||
# Ensures opt_vps is correct on a larger design with 8 lanes.
|
||||
# =============================================================================
|
||||
log -header "SAT self-equivalence: wide 128-bit VPS"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
|
||||
read -sv opt_vps_wide.sv
|
||||
verific -import opt_vps_wide
|
||||
proc; opt_clean
|
||||
rename opt_vps_wide gold
|
||||
|
||||
read -sv opt_vps_wide.sv
|
||||
verific -import opt_vps_wide
|
||||
proc; opt_clean
|
||||
opt_vps; opt_clean
|
||||
rename opt_vps_wide gate
|
||||
|
||||
miter -equiv -flatten -make_assert gold gate miter
|
||||
hierarchy -top miter
|
||||
proc; opt; memory; opt
|
||||
clk2fflogic
|
||||
sat -set-init-zero -tempinduct -prove-asserts -verify
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 4: Cell count verification — byte-write
|
||||
# After opt_vps, all $pmux and $reduce_or cells should be eliminated and
|
||||
# replaced with per-lane $eq/$and/$mux cells.
|
||||
# =============================================================================
|
||||
log -header "Cell counts: byte-write post-opt_vps"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
|
||||
read -sv opt_vps_byte_write.sv
|
||||
verific -import opt_vps_byte_write
|
||||
proc; opt_clean
|
||||
opt_vps; opt_clean
|
||||
|
||||
select -assert-none t:$pmux
|
||||
select -assert-none t:$reduce_or
|
||||
select -assert-count 4 t:$eq
|
||||
select -assert-count 4 t:$and
|
||||
select -assert-count 4 t:$mux
|
||||
select -assert-count 1 t:$dff
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 5: Cell count verification — wide
|
||||
# Same as above but for the wider 128-bit / 8-lane case.
|
||||
# =============================================================================
|
||||
log -header "Cell counts: wide post-opt_vps"
|
||||
log -push
|
||||
design -reset
|
||||
verific -cfg veri_optimize_wide_selector 1
|
||||
verific -cfg db_infer_wide_muxes_post_elaboration 0
|
||||
|
||||
read -sv opt_vps_wide.sv
|
||||
verific -import opt_vps_wide
|
||||
proc; opt_clean
|
||||
opt_vps; opt_clean
|
||||
|
||||
select -assert-none t:$pmux
|
||||
select -assert-none t:$reduce_or
|
||||
select -assert-count 1 t:$dff
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 6: Negative case — no VPS pattern
|
||||
# A simple mux-based register should not trigger opt_vps.
|
||||
# =============================================================================
|
||||
log -header "Negative: non-VPS 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_vps_no_match.sv
|
||||
verific -import opt_vps_no_match
|
||||
proc; opt_clean
|
||||
|
||||
stat
|
||||
opt_vps
|
||||
stat
|
||||
|
||||
select -assert-none t:$pmux
|
||||
select -assert-none t:$eq w:*vps*
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-count 1 t:$dff
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
14
tests/silimate/opt_vps_byte_write.sv
Normal file
14
tests/silimate/opt_vps_byte_write.sv
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
// 32-bit register with byte-lane writes indexed by a 2-bit selector (VPS).
|
||||
module opt_vps_byte_write (
|
||||
input logic clk,
|
||||
input logic wr_en,
|
||||
input logic [1:0] lane,
|
||||
input logic [7:0] wdata,
|
||||
output logic [31:0] q
|
||||
);
|
||||
logic [31:0] reg_data;
|
||||
always_ff @(posedge clk)
|
||||
if (wr_en)
|
||||
reg_data[((lane + 1) * 8) - 1 -: 8] <= wdata;
|
||||
assign q = reg_data;
|
||||
endmodule
|
||||
19
tests/silimate/opt_vps_byte_write_ref.sv
Normal file
19
tests/silimate/opt_vps_byte_write_ref.sv
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
// Reference: equivalent design WITHOUT variable-part-select.
|
||||
module opt_vps_byte_write (
|
||||
input logic clk,
|
||||
input logic wr_en,
|
||||
input logic [1:0] lane,
|
||||
input logic [7:0] wdata,
|
||||
output logic [31:0] q
|
||||
);
|
||||
logic [31:0] reg_data;
|
||||
always_ff @(posedge clk)
|
||||
if (wr_en)
|
||||
case (lane)
|
||||
2'd0: reg_data[ 7: 0] <= wdata;
|
||||
2'd1: reg_data[15: 8] <= wdata;
|
||||
2'd2: reg_data[23:16] <= wdata;
|
||||
2'd3: reg_data[31:24] <= wdata;
|
||||
endcase
|
||||
assign q = reg_data;
|
||||
endmodule
|
||||
12
tests/silimate/opt_vps_no_match.sv
Normal file
12
tests/silimate/opt_vps_no_match.sv
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
// Simple mux-based register -- no VPS pattern, opt_vps should not fire.
|
||||
module opt_vps_no_match (
|
||||
input logic clk,
|
||||
input logic sel,
|
||||
input logic [7:0] a, b,
|
||||
output logic [7:0] q
|
||||
);
|
||||
logic [7:0] reg_data;
|
||||
always_ff @(posedge clk)
|
||||
reg_data <= sel ? a : b;
|
||||
assign q = reg_data;
|
||||
endmodule
|
||||
14
tests/silimate/opt_vps_wide.sv
Normal file
14
tests/silimate/opt_vps_wide.sv
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
// 128-bit register with 16-bit lane writes indexed by a 3-bit selector (VPS).
|
||||
module opt_vps_wide (
|
||||
input logic clk,
|
||||
input logic wr_en,
|
||||
input logic [2:0] lane,
|
||||
input logic [15:0] wdata,
|
||||
output logic [127:0] q
|
||||
);
|
||||
logic [127:0] reg_data;
|
||||
always_ff @(posedge clk)
|
||||
if (wr_en)
|
||||
reg_data[((lane + 1) * 16) - 1 -: 16] <= wdata;
|
||||
assign q = reg_data;
|
||||
endmodule
|
||||
Loading…
Add table
Add a link
Reference in a new issue