opt_balance_tree: do not reassociate across a discarded carry

[akashlevy]

Problem

opt_balance_tree rebalances $add chains, and is_right_type() deliberately
accepts adders that discard their own carry out:

natural_width = std::max(a_width, b_width) + 1;
// SILIMATE: Ignore carry bit for now for more aggressive balancing
natural_width--;

Accepting those cells as chain members is not sound. Flattening a + b into the
summand list of a wider consumer drops the truncation that adder applied, so the
rebuilt tree computes the discarded carry back and lets it reach a bit the
original circuit never saw. Three lines are enough to miscompile:

module top (input [7:0] a, b, input [15:0] c, output [15:0] y);
  wire [7:0] t = a + b;      // carry out of bit 7 is discarded here
  assign y = c + {8'd0, t};  // ... but the rebuilt tree computes it back
endmodule

equiv_opt -assert opt_balance_tree leaves 8 of 16 output bits unproven on this
design today. A random fuzz of small add networks (2-5 adders, widths 2-8, mixed
zero extension and slicing) miscompiles 25 of 400 designs.

Both matchers are affected, for the same reason but through different code:

• the sliced-add extractor flattens a child adder whose carry lands below the
  head's truncation point;
• the plain chain matcher merges a truncating adder into a wider consumer, which
  is the shape you get without any concatenation, since Verilog leaves the width
  extension to the sink's port parameters.

Fix

Keep the aggressive matching, but only follow a carry-dropping link when the
discarded bit is provably still dead afterwards:

• chain_driver() refuses a carry-dropping driver whose consumer is wider.
  Equal or narrower is fine: mod-2^n addition is associative, and mod-2^n
  followed by mod-2^m with m <= n is just mod-2^m.
• the sliced extractor refuses a carry-dropping child whose carry position
  base_offset + pos + width sits below the head's output width, i.e. lands on
  a bit the head still keeps.

Cutting a chain that way would also strand the truncating adder's own subchain,
since head detection would never treat it as a chain end. So a cell whose only
continuation is a link the guard rejects now heads its own tree, and the
subchain below it still gets balanced.

Validation

• tests/opt/opt_balance_tree.ys gains 6 cases (35-40): the plain and sliced
  miscompiles above, a carry-dropping child whose carry does fall off the head's
  truncation (must still balance), a same-width a+b+c+d chain (must still
  balance), and the stranded-subchain recovery.
• The 6 new cases fail on main and pass here; the other 34 are unchanged.
  Test 36 also fails on a build carrying only the two guards, so the
  head-detection half is covered too.
• tests/opt/opt_addcin.ys, tests/opt/opt_parallel_prefix.ys and the whole
  tests/arith_tree/ suite pass.
• Fuzz: 460/460 random add networks equivalent, against 25/400 miscompiles on
  main.

QoR

A/B over 58 Preqorsor designs (add trees, adder chains, compares, barrel
shifters, multipliers, priority encoders, plus non-arithmetic controls). 53 come
out bit-identical. clk is delay in ps, so lower is better:

design	LoL	clk (ps)	area
qor_cmp_onehot_path12	25.25 -> 24.25	345.6 -> 357.8	40.77 -> 39.29
qor_levelsize_pow2_leadone	29.75 -> 29.25	339.4 -> 365.1	125.16 -> 119.64
qor_pow2_tied_msb	32.75 -> 33.50	412.2 -> 451.8	50.99 -> 51.25
qor_pow2_round_size	34.50 -> 36.25	432.3 -> 465.9	53.29 -> 52.05
qor_pow2_round_size_2	34.50 -> 36.25	432.3 -> 465.9	53.29 -> 52.05

qor_pow2_round_size is the honest cost of the guard. Its 6-bit slice adder
truncates, and folding it into the two 7-bit exponent adders reading it is in
fact equivalent -- SAT proves it on the real netlist -- but only because of a
value range the pass cannot establish locally, so the guard conservatively
refuses. Extending the guard to discount constant-zero operand padding was
tried and recovers nothing here, so it is not part of this change.

Its LoL bound is raised in
Silimate/preqorsor#2292,
which should merge before this ships in a wheel.

[greptile-apps]

Greptile Summary

The PR prevents opt_balance_tree from reassociating across an $add truncation when the discarded carry could become observable downstream. It also preserves balancing below rejected links and adds equivalence and structural regressions for plain, sliced, boundary, and same-width cases.

• Adds carry-loss detection and width-aware guards to plain add-chain traversal.
• Rejects sliced-child extraction when a restored carry would fall within the head output.
• Recovers truncated cells as independent tree heads after an unsafe continuation.
• Adds six regression cases covering unsafe and safe reassociation boundaries.

Confidence Score: 5/5

The PR appears safe to merge; the new guards preserve modular-addition boundaries while retaining balancing where discarded bits remain unobservable.

The plain matcher cuts widening links after a truncated add, the sliced matcher compares the restored carry position against the current head width, and the added tests exercise both rejected and permitted boundary cases without leaving a concrete blocking failure.

Important Files Changed

Filename	Overview
passes/opt/opt_balance_tree.cc	Adds correctly bounded carry-truncation guards for plain and sliced add-tree extraction, plus independent subchain-head recovery.
tests/opt/opt_balance_tree.ys	Adds focused equivalence and topology regressions for unsafe widening, safe modular chains, sliced carry boundaries, and stranded-subchain recovery.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Candidate child add] --> B{Child discards carry?}
    B -->|No| C[Allow chain traversal]
    B -->|Yes| D{Plain or sliced link?}
    D -->|Plain| E{Consumer width <= child width?}
    E -->|Yes| C
    E -->|No| F[Cut link and balance child subchain separately]
    D -->|Sliced| G{Carry position >= head width?}
    G -->|Yes| C
    G -->|No| F

Loading

_{Reviews (1): Last reviewed commit: "opt_balance_tree: do not reassociate acr..." | Re-trigger Greptile}