opt_compact_prefix tests: scope the self-equivalence proofs to gate

[akashlevy]

Sibling of #310, same flaw in a different test file, found by auditing the whole
test suite for the idiom that #310 fixed.

The idiom

A Yosys pass with no selection argument runs on every module in the design. These
tests build gold first and gate second:

proc; opt_clean
rename opt_compact_prefix_pack gold   # gold created FIRST

read -sv opt_compact_prefix_pack.sv
...
opt_compact_prefix                    # BARE -> also optimizes gold
opt_clean
rename opt_compact_prefix_pack gate

miter -equiv -flatten -make_assert gold gate miter
sat -prove-asserts -verify

By the time opt_compact_prefix runs, gold is live, so the bare invocation optimizes
it as well and the miter compares optimized against optimized. gold and gate end up
byte-identical, and the proof is not merely weakened but vacuous.

Order is what matters: an arm that builds gate before gold exists is unaffected.

Affected

All five SAT self-equivalence arms in tests/silimate/opt_compact_prefix.ys:

Arm	Solve size before	Solve size after
Forward dense pack	2 vars / 4 clauses	2241 vars / 6104 clauses
Reverse suffix read	2 vars / 4 clauses	4951 vars / 13563 clauses
Reverse suffix + add-by-minus-one	2 vars / 4 clauses	6405 vars / 17593 clauses
Modulo decimation (MSB-first)	2 vars / 4 clauses	1874 vars / 5125 clauses
Modulo decimation (LSB-first)	2 vars / 4 clauses	1796 vars / 4919 clauses

All five still prove SUCCESS, so opt_compact_prefix is genuinely correct on these
cases — the tests were the only thing broken.

These arms were worthless, not just weak

Injecting a gross miscompile into arm 1 (chtype -map $add $sub, i.e. every adder
becomes a subtractor) and running it the way a buggy pass would run, bare:

• before this change: Solving problem with 2 variables and 4 clauses -> no model found: SUCCESS!, exit 0. The corruption hits gold too, so the miter cannot see it.
• after this change: Solving problem with 2226 variables and 6059 clauses -> model found: FAIL!, exit 1.

The same was independently demonstrated for opt_vps in #310, where a version of the
pass that provably left four output bits undriven still passed a vacuous arm.

Fix

Move rename ... gate ahead of the pass and scope the pass to gate, exactly as #310
does:

rename opt_compact_prefix_pack gate
opt_compact_prefix gate; select -clear; opt_clean

select -clear is needed because handing a pass a selection argument overwrites the
current selection, and the following opt_clean should still see the whole design.

The two modulo-decimation arms keep bmuxmap unscoped: sat needs $bmux lowered on
both arms, and it is a semantics-preserving lowering applied symmetrically, exactly like
the trailing bare opt_clean.

Audit scope

I applied the same detector to the whole tests/ tree. Within tests/silimate this file
was the only remaining instance; everything else is safe, by four distinct mechanisms:

• opt_argmax.ys (7 arms), opt_priority_onehot.ys (8 arms) — already scoped with select -module X / select -clear. Solves run on 2315-14525 and 1839-6732 variables.
• opt_carry_select.ys (2 arms) — pass already given an explicit module selection. 964 and 1912 variables.
• opt_boundary.ys (16 arms), opt_boundary_random.tcl, mux_push.ys (1 equiv_make arm) — snapshot idiom (design -save / -load / -stash), so the reference is not a live module and a bare pass cannot reach it. Structurally immune.
• carvenetlist.ys (6 arms) — the golden reference is a hand-written module read in after the pass runs.
• ~25 files use equiv_opt, which handles gold/gate internally and is unaffected.

Outside tests/silimate, the cd-scoped comparisons in tests/opt/opt_expr_*.ys,
tests/opt/bug1758.ys, tests/fsm/uut_*.ys and tests/sat/splice.ys are all correctly
scoped, and tests/verific/case.ys re-runs prep on gold but is not vacuous (its two
arms come from different Verific configurations; solves run on 180 and 348 variables).

Testing

Full tests/silimate suite: 40 PASS, 1 FAIL. The failure is mux_push.ys, pre-existing
and unrelated (a t:$shr cell-count assertion from in-flight work on mux_push.cc).

Made with Cursor

[greptile-apps]

Greptile Summary

The PR repairs five previously vacuous opt_compact_prefix self-equivalence proofs by preserving the unoptimized gold module and applying the pass only to gate.

• Renames each second imported module to gate before optimization.
• Runs opt_compact_prefix gate, then restores full-design selection for cleanup.
• Keeps $bmux lowering symmetric across both sides of the modulo-decimation proofs.

Confidence Score: 5/5

The PR appears safe to merge; the updated scripts now compare the preserved reference modules against independently optimized gate modules.

The scoped pass argument selects each renamed gate module, select -clear restores full-design processing for subsequent commands, and no blocking or non-blocking defect remains in the changed test flows.

Important Files Changed

Filename	Overview
tests/silimate/opt_compact_prefix.ys	Correctly scopes optimization to gate in all five self-equivalence arms while restoring full selection before shared cleanup and miter construction.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart LR
    SRC[Import source] --> GOLD[Rename first module to gold]
    SRC --> GATE[Import again and rename to gate]
    GATE --> PASS[opt_compact_prefix gate]
    PASS --> CLEAR[select -clear and opt_clean]
    GOLD --> MITER[Equivalence miter]
    CLEAR --> MITER
    MITER --> SAT[SAT proof]

Loading

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