opt_vps tests: scope the self-equivalence proofs to gate

[akashlevy]

Summary

Five of the opt_vps self-equivalence tests were proving nothing at all. They were not merely weaker than intended — they were vacuous, and I found it while reconciling two duplicate PRs (#294 / the closed #295).

Tests 2, 3, 8, 10 and 13 all follow this shape:

read -sv foo.sv
...
rename foo gold          # gold exists from here on

read -sv foo.sv
...
opt_vps; opt_clean       # <-- no selection argument
rename foo gate

miter -equiv ... gold gate miter
sat -prove-asserts -verify

opt_vps ends its argument loop with extra_args(...) and then iterates design->selected_modules(). With no selection argument that is every module in the design, gold included. So gold was optimized too, gold and gate ended up as the same netlist, and each miter compared optimized against optimized.

How vacuous

Every one of the ten solves in those five tests ran on 2 variables and 3–5 clauses — the miter had collapsed to nothing. After scoping:

test	before	after
2	2 / 2	3965 / 7764
3	2 / 2	18431 / 36212
8	2 / 2	38697 / 76879
10	2 / 2	45027 / 90052
13	2 / 2	79557 / 159112

(variables, base case / induction step)

Tests 1 and 7 build gate before gold exists, so they were always real proofs against a hand-written reference. Their solve sizes are byte-for-byte unchanged (2182/4229 and 13450/26385), which independently confirms the affected set is exactly {2, 3, 8, 10, 13}.

Direct evidence the pass really was touching the reference — from a replay of test 8's shape:

Module opt_vps_read: 1 VPS group(s), ... 1 VPS reads -> $shr, ...
Module gold:         1 VPS group(s), ... 1 VPS reads -> $shr, ...

and afterwards gold contains gold/$auto$opt_vps.cc:2069:process_vps_reads$vps_rd_shr$2.

What this hid

Worth stating concretely, because it is not hypothetical. Take a build of opt_vps with a known-unsound gather grouping key (the per-element-bit keying from the closed #295), on a netlist where it demonstrably leaves four output bits with no driver at all — check reports Wire ...\y_ovl[3] [1] is used but has no driver four times. An equivalence arm written in the bare style still reports:

SAT proof finished - no model found: SUCCESS!

Scoped to gate, the same arm on the same binary reports model found: FAIL!.

Change

One line per test: rename to gate first, then opt_vps gate; select -clear; opt_clean. 10 insertions, 5 deletions, no fixture or expected-count changes.

Test plan

• Full tests/silimate/opt_vps.ys suite passes, exit 0, with a binary built from main's opt_vps.cc
• Baseline (unscoped) suite on the same binary also exits 0, so this is not fixing a break — it is removing vacuity
• No expected cell counts changed; no previously-green arm turned red
• Solve sizes above confirm every affected arm is now a real proof

The two instances of this pattern in tests 15 and 17 are added by #294, so they are fixed there rather than here.

Made with Cursor

[greptile-apps]

Greptile Summary

The PR repairs five vacuous opt_vps self-equivalence tests by ensuring only the implementation module is transformed.

• Renames the freshly imported implementation to gate before running opt_vps.
• Passes gate as the explicit module selection, preserving the unoptimized gold reference.
• Clears the temporary selection before whole-design cleanup and subsequent equivalence checks.

Confidence Score: 5/5

The PR appears safe to merge and makes the affected equivalence tests meaningfully exercise opt_vps.

The explicit trailing gate selection is accepted by both command forms and limits opt_vps to the implementation module, while select -clear restores the full selection needed by subsequent cleanup and proof commands.

Important Files Changed

Filename	Overview
tests/silimate/opt_vps.ys	Correctly scopes opt_vps to gate in five self-equivalence arms while preserving full-design cleanup and meaningful gold-versus-gate proofs.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart LR
    SRC[Import source] --> GOLD[Rename reference to gold]
    SRC --> GATE[Import again and rename to gate]
    GATE --> VPS[Run opt_vps on gate only]
    GOLD --> MITER[Equivalence miter]
    VPS --> MITER
    MITER --> SAT[SAT proof]

Loading

_{Reviews (1): Last reviewed commit: "opt_vps tests: scope the self-equivalenc..." | Re-trigger Greptile}