diff --git a/tests/silimate/opt_vps.ys b/tests/silimate/opt_vps.ys index 33434d7ff0b..e21e9dad626 100644 --- a/tests/silimate/opt_vps.ys +++ b/tests/silimate/opt_vps.ys @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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