From e918d1200992b83c83f74fab3daaa4c5b971ca07 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 27 Aug 2026 12:51:55 -0700 Subject: [PATCH] opt_vps tests: scope the self-equivalence proofs to `gate` Tests 2, 3, 8, 10 and 13 rename `gold` before reading the design a second time and then run a bare `opt_vps`. With no selection argument the pass runs on every module in the design, so `gold` was optimized too and each miter compared optimized against optimized. These were not merely weaker than intended, they were vacuous. Every one of the ten solves ran on 2 variables and 3-5 clauses, because gold and gate were the same netlist. Scoping the pass to `gate` gives 3965, 7764, 18431, 36212, 38697, 76879, 45027, 90052, 79557 and 159112 variables respectively, and all five tests still pass. Tests 1 and 7 build `gate` before `gold` exists and were always real proofs; their solve sizes are unchanged, which confirms the affected set. Worth stating how much this hid: run the same arm in the bare style against a build of opt_vps with a known unsound gather grouping key, one that leaves four output bits with no driver at all, and it still reports "no model found: SUCCESS!". Co-authored-by: Cursor --- tests/silimate/opt_vps.ys | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) 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