mirror of https://github.com/YosysHQ/yosys.git
242 lines
7.2 KiB
Plaintext
242 lines
7.2 KiB
Plaintext
# =============================================================================
|
|
# 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
|
|
|
|
# =============================================================================
|
|
# Test 7: SAT equivalence — VPS read vs right-shift reference
|
|
# Proves opt_vps produces a logically equivalent circuit to a hand-written
|
|
# right-shift for a 256-bit register with 32-bit read window.
|
|
# =============================================================================
|
|
log -header "SAT equivalence: VPS read vs right-shift 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_read.sv
|
|
verific -import opt_vps_read
|
|
proc; opt_clean
|
|
opt_vps; opt_clean
|
|
rename opt_vps_read gate
|
|
|
|
read -sv opt_vps_read_ref.sv
|
|
verific -import opt_vps_read
|
|
proc; opt_clean
|
|
rename opt_vps_read 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 8: SAT self-equivalence — VPS read before vs after opt_vps
|
|
# Proves opt_vps does not change the functional behavior for VPS reads.
|
|
# =============================================================================
|
|
log -header "SAT self-equivalence: VPS read 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_read.sv
|
|
verific -import opt_vps_read
|
|
proc; opt_clean
|
|
rename opt_vps_read gold
|
|
|
|
read -sv opt_vps_read.sv
|
|
verific -import opt_vps_read
|
|
proc; opt_clean
|
|
opt_vps; opt_clean
|
|
rename opt_vps_read 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 9: Cell count verification — VPS read
|
|
# After opt_vps, the $pmux should be replaced with a $shr.
|
|
# =============================================================================
|
|
log -header "Cell counts: VPS read 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_read.sv
|
|
verific -import opt_vps_read
|
|
proc; opt_clean
|
|
opt_vps; opt_clean
|
|
|
|
select -assert-none t:$pmux
|
|
select -assert-count 1 t:$shr
|
|
select -assert-count 1 t:$dff
|
|
select -assert-count 1 t:$mux
|
|
design -reset
|
|
log -pop
|
|
|
|
|