Add opt_addcmp: fuse an adder into the comparator it feeds

[akashlevy]

What

A bound check spelled a + b <cmp> c asks for the order of a sum, never for
the sum itself, but the RTL puts a full carry-propagate adder in front of the
comparator's own carry chain. opt_addcmp reduces the three operands to a sum
and a carry vector in constant depth, leaving one carry chain instead of two:

(a + b) >= c   ->   s >= ~(v << 1)      s = a ^ b ^ ~c
(a + b) >  c   ->   s >  ~(v << 1)      v = maj(a, b, ~c)

Operands are widened to max(|a|,|b|,|c|) + 1 first. That is what makes the
identity exact rather than modular: the carry out of the top column is
maj(0, 0, x) = 0, so the shift drops nothing. Derivation, at width W with
a + b < 2**W:

a + b >= c  <=>  a + b + ~c + 1 >= 2**W       (~c = 2**W-1 - c)
            <=>  s + d + 1 >= 2**W            (a + b + ~c = s + d, d = v << 1)
            <=>  s >= 2**W-1 - d = ~d

The strict form drops the +1, turning >= into >. The other two relations
are these two inverted, and a sum on the comparator's right-hand side is the
mirror image, so all four cell types are covered by choosing a relation and an
inversion.

Soundness conditions, both structural:

• No truncation. The add's Y must be at least max(|a|,|b|) + 1 bits and
  the comparator must read all of it. An add that wraps compares a residue,
  which the carry-save form does not reproduce.
• Unsigned. A signed compare orders the same bits differently.

Profitability: when the comparator is the sum's only reader the adder is dead
after the rewrite, so it is a strict win and always taken. When the sum has
other readers the adder stays and the carry-save level is added area, which
only pays on a critical comparator — that case is behind -timing.

Shared timing model

The -timing guard has to agree with muxpush's on which paths are critical,
so rather than adding a fourth copy of the unit-delay heuristic this lifts
mux_push's arrival/departure model into passes/silimate/unit_delay.h and
derives both workers from it. That half is a pure refactor: mux_push.cc loses
202 lines and gains 3, and the extracted bodies are character-identical modulo
indentation. (opt_timing_balance and opt_carry_select keep their own
variants — those cost a cell in fractional levels against its output width,
which is a different currency.)

Landing order

Nothing invokes opt_addcmp, so this PR is a no-op on its own and safe to merge
first. Silimate/preqorsor adds it to the matcher block in a follow-up, which is
where the behavior change lands atomically.

Timing model scaling

The extracted model memoized per bit, but every output bit of a cell shares one
arrival (the max over all its inputs) and every input bit shares one departure,
so it recomputed the same number once per bit and rescanned the cell's whole
port list each time -- O(width**2) per cell, on a model that exists to be
consulted from wide datapaths. The caches are now keyed on the cell.

Isolated cost of compute_module_depth() on a chain of 800 operators, sweeping
their width (opt_addcmp -timing with a shared, off-critical bound check, so
the guard runs but nothing is rewritten):

operand width	before	after
32	0.036s	0.005s
64	0.116s	0.005s
128	0.410s	0.013s
256	1.585s	0.130s
512	6.316s	0.119s

Before quadruples with each doubling of width; after is flat in it.

The values are unchanged by construction -- the per-bit recurrence and the
per-cell one compute the same max -- and 66 netlists across six timing-guarded
muxpush/opt_addcmp configurations and 11 designs come out byte-identical.
#315 landed the same factoring from the other side -- a lazy longest_path()
and a reset_timing() helper -- so both now live in UnitDelayTiming and
opt_addcmp picks up the lazy depth too. The two changes are complementary:
#315 stopped rebuilding the model per candidate, this one stops the model
itself from costing O(width**2).

opt_addcmp also checks a module has a comparator at all before indexing every
bit in it.

Generalization

• $eq / $ne, off the same pair the ordering relations already build:
  a + b == c iff s + d == 2**W-1, and two values summing to all-ones can
  share no set bit (it would carry and clear one), so that is exactly s == ~d.
• Add trees. run_csa() reduces n summands back to the two the identity
  expects. Working at max(|o_i|) + ceil(log2 n) bits keeps the running total
  below 2**W, so every value in the tree is too, which is what makes each
  carry shift exact rather than modular. Only a child add its parent solely
  reads is absorbed, so every adder the walk takes in is dead afterwards; a
  truncating child stays an operand, since its wrapped result is not the sum of
  its own operands.
• $sub deliberately stays out. No width condition makes an unsigned
  subtract exact the way one does an add: a - b wraps whenever a < b, and
  ruling that out needs a value range the pass cannot establish locally.

New tests: SAT equivalence for equality and disequality on both sides, SAT
equivalence for three- and four-summand trees, a structural check that a
three-summand tree leaves both adders dead, and negatives for a shared child, a
truncating child, and $sub.

qor_cmp_onehot_path12 is byte-identical before and after this second commit
(its inner pid + off_q truncates, so it is correctly left as an operand), and
equiv_opt -assert still proves the fusion on it.

Test plan

tests/silimate/opt_addcmp.ys (auto-discovered by generate_mk.py) covers:

• SAT equivalence for all four relations with the sum on the left
• SAT equivalence for all four relations with the sum on the right
• SAT equivalence for mismatched operand widths with the sum also escaping
• Structural: sole reader leaves the adder dead ($add gone, one $ge and
  two $xor left)
• Negative: shared sum without -timing
• Negative: shared sum on a comparator well off the critical path
• Negative: truncating add
• Negative: signed compare
• Negative: adder narrower than -min-width

mux_push.ys, mux_push_types.ys, mux_push_farm_gain.ys and opt_vps.ys
pass unchanged against the refactor.

Downstream, on Preqorsor's qor_cmp_onehot_path12 (address bound check feeding
a one-hot decode): lol 24.25 -> 20.75, clk 358 -> 324, area 39.3 -> 45.4. An
A/B over 15 mixed designs (compares, adders, carry-save, barrel shifters, ibex)
leaves the other 14 identical in lol and clk. Each rewrite in that run was also
proved by equiv_opt -assert in Preqorsor's formal mode.

Made with Cursor

[akashlevy]

@greptileai review

[greptile-apps]

Greptile Summary

The PR adds an unsigned, non-truncating add-compare fusion pass and extracts mux_push’s unit-delay analysis into a shared helper.

• Registers opt_addcmp as an optimization pass with timing- and width-based profitability guards.
• Rewrites comparisons against mathematical sums into carry-save logic followed by one comparator.
• Reuses the extracted timing model in both opt_addcmp and mux_push.
• Adds SAT-equivalence, structural, and negative coverage for relation direction, operand widths, sharing, signedness, and truncation.

Confidence Score: 5/5

The PR appears safe to merge; no concrete correctness, build, security, or selection-boundary failure was identified.

The rewrite checks unsignedness, mathematical-sum width, complete comparator consumption, sharing, and timing eligibility, while the timing extraction preserves mux_push’s existing implementation and the tests exercise the principal semantic and structural boundaries.

Important Files Changed

Filename	Overview
passes/opt/opt_addcmp.cc	Adds guarded recognition and carry-save replacement for unsigned, non-truncating add-compare regions; no actionable defect was established.
passes/silimate/unit_delay.h	Extracts the existing iterative unit-delay arrival/departure model into a reusable worker base.
passes/silimate/mux_push.cc	Replaces the local timing implementation with inheritance from the character-equivalent shared helper.
tests/silimate/opt_addcmp.ys	Covers nominal equivalence, mirrored relations, width variation, structural results, and guarded rejection cases.
passes/opt/CMakeLists.txt	Registers the new optimization pass in the CMake component list.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart LR
    A[Unsigned non-truncating add] --> B[Relational comparator]
    B --> C{Sum shared?}
    C -->|No| D[Apply fusion]
    C -->|Yes| E{Timing mode and critical path?}
    E -->|Yes| D
    E -->|No| F[Keep original structure]
    D --> G[Carry-save XOR/majority level]
    G --> H[Single relational comparator]

Loading

_{Reviews (1): Last reviewed commit: "Add opt_addcmp: fuse an adder into the c..." | Re-trigger Greptile}