Skip to content

opt_vps tests: scope the self-equivalence proofs to gate #310

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
akashlevy merged 1 commit into from
Aug 27, 2026
Merged

opt_vps tests: scope the self-equivalence proofs to gate #310

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 10 additions & 5 deletions tests/silimate/opt_vps.ys
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,11 @@ log -pop
# =============================================================================
# Test 2: SAT self-equivalence — byte-write before vs after opt_vps
# Proves opt_vps does not change the functional behavior.
#
# The pass is scoped to `gate` here and in every other self-equivalence test
# below. `gold` already exists by this point, and with no selection argument
# opt_vps runs on every module in the design, so a bare `opt_vps` optimizes
# `gold` too and the miter compares optimized against optimized.
# =============================================================================
log -header "SAT self-equivalence: byte-write before vs after opt_vps"
log -push
Expand All @@ -46,8 +51,8 @@ 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
opt_vps gate; select -clear; opt_clean

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
Expand Down Expand Up @@ -75,8 +80,8 @@ 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
opt_vps gate; select -clear; opt_clean

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
Expand Down Expand Up @@ -208,8 +213,8 @@ 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
opt_vps gate; select -clear; opt_clean

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
Expand Down Expand Up @@ -262,8 +267,8 @@ rename opt_vps_gather gold
read -sv opt_vps_gather.sv
verific -import opt_vps_gather
proc; opt_clean
opt_vps; opt_clean
rename opt_vps_gather gate
opt_vps gate; select -clear; opt_clean

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
Expand Down Expand Up @@ -388,8 +393,8 @@ rename opt_vps_gather_negidx gold
read -sv opt_vps_gather_negidx.sv
verific -import opt_vps_gather_negidx
proc; opt_clean
opt_vps -msb-inv-sext; opt_clean
rename opt_vps_gather_negidx gate
opt_vps -msb-inv-sext gate; select -clear; opt_clean

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
Expand Down
Loading