opt_shift -expand: do not distribute $add/$sub over a right shift

[akashlevy]

The bug

peepopt_expand_shifts rewrote (a OP b) >> c into (a >> c) OP (b >> c) for
every operator it matched, including $add and $sub. Distribution is only
valid for a left shift, which is a multiply by 2^c and so distributes mod
2^width. A right shift discards a low window that the carry crosses, and
shifting each operand first throws that carry away.

Minimal counterexample, 9-bit operands, a = 255, b = 1, c = 8:

	value
(a + b) >> c	256 >> 8 = 1
(a >> c) + (b >> c)	0 + 0 = 0

This is reachable from ordinary RTL. A shifted saturating decrement,
({3'd0, w} + 17'd1) >> lv, hits it directly, and Preqorsor runs
opt_shift -combine -expand in the default synthesis flow, where the
per-pass equivalence check is only active under options.formal. On the
design this was found on, Preqorsor's own formal mode fails with 14 unproven
$equiv cells before this change and proves equivalence after it.

The fix

One filter line in the pattern: $add/$sub only match $shl/$sshl.
Bitwise operators keep all four shift types, including the sign fill of
$sshr, where the fill of a OP b is the same OP of the two fills.

Exhaustively SAT-checked all 5 operators x 4 shift types with miter -equiv +
sat -prove-asserts, before and after:

OP	<<	>>	<<<	>>>
& | ^	sound	sound	sound	sound
+ -	sound	was unsound	sound	was unsound

After the fix the 16 sound combinations still fire and still prove equivalent;
the 4 unsound ones no longer fire.

Test coverage gap this closes

tests/silimate/opt_expand_shifts.ys already used equiv_opt -assert, but it
covered SHL across all five operators and SHR across the bitwise ones only,
so the broken combinations were never exercised. This adds the four missing
negatives plus the widened-operand shifted increment the bug was found on. The
new negatives fail on main and pass here; the five sibling opt_shift test
files (-combine, -descale, -sink, -fuse, -chain) stay green.

Blast radius

Scanned all 391 Preqorsor regression designs by running the pass and
classifying every rewrite it reports. Four designs make an unsound rewrite
standalone; in the full synthesis flow only one still does, and it is a new
unregistered case, so no tracked LoL bound moves. The other three
(qor_descale_edges, qor_mip_pack_barrel, qor_mip_pack_barrel_trunc) come
out bit-identical on lol/clk/area. Other right-shifted sums in the
corpus (ibex/azadirtl multdiv_slow, or1200, LU32PEEng) use constant shift
amounts, which fold to bit-slices before the pass sees a $shr.

Removing an invalid rewrite costs depth where it was firing: the affected
design goes from LoL 26.5 to 27.75. That shortcut was a miscompile, and the
sound rewrite for that shape is opt_shift -descale, which is being extended
separately.

This is on by default rather than flag-gated: it removes an incorrect
transform, so there is no configuration in which the old behavior is wanted.

Made with Cursor

[greptile-apps]

Greptile Summary

This PR prevents opt_shift -expand from distributing addition and subtraction across logical or arithmetic right shifts while retaining valid bitwise and left-shift rewrites.

• Restricts arithmetic expansion to $shl and $sshl.
• Documents why right-shift arithmetic distribution loses carry or borrow information.
• Adds equivalence-backed negative tests for $shr/$sshr with $add/$sub and a widened increment regression.

Confidence Score: 5/5

The PR appears safe to merge, with no actionable defects identified in the changed behavior.

The new filter precisely excludes arithmetic expansion across right shifts, and the added tests retain both the arithmetic and shift cells while checking equivalence for the affected cases.

Important Files Changed

Filename	Overview
passes/silimate/peepopt_expand_shifts.pmg	Adds a focused match filter that blocks the four unsound arithmetic right-shift combinations while preserving bitwise and left-shift expansion.
passes/silimate/opt_shift.cc	Extends user-facing pass documentation with the carry-loss rationale and a concrete counterexample.
tests/silimate/opt_expand_shifts.ys	Adds equivalence and post-optimization shape checks covering unsigned and signed right-shift arithmetic cases plus the motivating widened-increment shape.

_{Reviews (1): Last reviewed commit: "opt_shift -expand: do not distribute $ad..." | Re-trigger Greptile}

[akashlevy]

Closing in favour of #299, which was opened two minutes after this one and fixes the same bug plus two more.

Both PRs correctly identify that $add/$sub only distribute over a left shift. The difference is what happens to the left-shift cases that remain. The operator truncates at its own width while the expanded form truncates at the shift's, so a bit the operator dropped can reappear underneath a wider shifted result. That case passes the filter here, because it is a left shift:

module top(input [7:0] a, input [7:0] b, input [1:0] c, output [15:0] y);
  wire [7:0] d = a - b;
  assign y = d << c;
endmodule

On main, equiv_opt -assert opt_shift -expand expands this and leaves 8 unproven $equiv cells. #299's width guard rejects it and equivalence proves; the filter in this PR permits it.

#299 also adds a signedness guard, for a narrow operand that the operator pads with its own signedness while the expanded form hands it to a shift that pads with the shift's.

#299 has been rebased onto current main, is mergeable, and I verified it closes all three holes with all six opt_shift suites passing and no measurable QoR change across 38 shift/arith regressions. Nothing here is lost by closing it.

[akashlevy]

Superseded by #299 (see comparison above).