opt_vps: fold uniform gathers over multi-bit elements - #294
Conversation
The uniform-gather fold only matched WIDTH==1 $bmux, so a variable-index read of anything wider than a bit was skipped and fell through to bmuxmap -pmux + pmuxtree, which expand each selector into a one-hot $eq farm plus a mux tree. A 32-lane sliding window over a 128-entry byte table cost 7.9x the area, 2.2x the logic depth and 21x the wall clock of the same function written as barrel shifts. $bmux is entry-major, so a WIDTH=W cell is W independent gathers over stride-W slices of the table, all sharing one index. Register one candidate per read output bit and let the existing grouping, affine analysis and emission run unchanged: W barrels over M entries cost what one barrel over W*M bits would, so splitting the fold per bit is free. A cell now feeds one group per output bit, so it can no longer be retired by the first group that folds -- later groups still read it for its index and src attribute. Collect the folded cells and remove them once every group has been emitted. Co-authored-by: Cursor <cursoragent@cursor.com>
Greptile SummaryThe PR extends uniform-gather folding to multi-bit
Confidence Score: 5/5The PR appears safe to merge. No blocking failure remains; whole-table grouping ensures that a valid wide
|
| Filename | Overview |
|---|---|
| passes/silimate/opt_vps.cc | Implements whole-table grouping and atomic wide-gather replacement; the previously reported partial-retirement failure is no longer reachable for valid $bmux cells. |
| tests/silimate/opt_vps.ys | Adds equivalence and cell-count coverage for multi-bit gathers and mixed foldability. |
| tests/silimate/opt_vps_gather_mixed.sv | Provides the regression shape that verifies an ineligible gather bank remains intact and driven. |
| tests/silimate/opt_vps_gather_wide.sv | Provides representative multi-bit sliding-window gathers for functional and structural validation. |
Reviews (2): Last reviewed commit: "opt_vps: key gather groups on the whole ..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Grouping per element bit let one bit of a $bmux clear min_gather while another did not. Folding the eligible bit retired the cell, and the skipped bit's output was left undriven -- a silent functional change. Reachable whenever two cells share a table for some element bits but not all of them, since only the matching slices co-group. Key on the whole A port instead, so every element bit of a cell is in one group and folds as a unit, and emit one barrel per element bit inside the group. Same netlist for the homogeneous case that motivated this, one $shr per element bit sharing a single shift amount, but a cell can now only be retired by the group that drives all of its read bits. Bits no candidate reads are skipped rather than folded, so a partially used gather does not pay for barrels nothing consumes. Co-authored-by: Cursor <cursoragent@cursor.com>
|
@greptileai review |
Test 17's two banks read wholly disjoint tables, so a cell folds all-or-nothing whether grouping is keyed on the whole A port or on a stride-WIDTH slice of it. Overlapping-but-not-identical tables are the only shape that separates the two keys, and nothing in the suite had that shape: the per-element-bit keying this branch replaced passes every existing test, test 17 included. The new fixture gives four lanes whose tables agree on element bit 0 and differ on element bit 1. Per-slice keying puts the four bit-0 slices in one group that clears min_gather and each bit-1 slice in a group of one that does not, so folding bit 0 retires all four cells and leaves y_ovl[l][1] undriven. A second bank over a wholly shared table still folds, so the overlap bank's survival is not just the fold never firing. The equivalence arm scopes opt_vps to `gate` -- with a bare opt_vps the pass also optimizes `gold` and the miter compares optimized against optimized, which lets the undriven bits through. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Added a test that pins the grouping key, because the suite as it stood could not tell the two candidate keys apart. The gap. Test 17's two banks read wholly disjoint tables ( The shape that separates them. Tables that overlap but are not identical. The new fixture
A second bank over a wholly shared table still folds to one barrel per element bit, so the overlap bank surviving cannot be explained by the fold simply never firing. Proof that it discriminates. Full suite, same script, two binaries:
On #295 tests 1–17 all pass and test 18 fails. Both arms discriminate on their own:
One note on the equivalence arm. It scopes the pass as That bare- |
Tests 15 and 17 rename `gold` before reading the design a second time and then run a bare `opt_vps`. With no selection argument the pass runs on every module in the design, `gold` included, so the miter compared optimized against optimized. Both solves were degenerate -- 2 variables and 4 clauses -- meaning the only functional proofs of the multi-bit gather fold this branch adds were proving nothing. Scoped, they now solve 10104 and 5026 variables and still pass. Also drop a stale claim from the test 15 header and from the fixture: a cell no longer "lands in W groups and is retired by whichever folds first". That described the per-element-bit keying replaced in bb30219. The same bare-opt_vps pattern predates this branch in tests 2, 3, 8, 10 and 13; those are fixed separately against main. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Follow-up to the note above, now that I have measured it. Split as follows. The bare-
Full suite after all of this,
Note that tests 15 and 17 still pass on the #295 binary even now that they are real proofs — their tables are disjoint, so nothing is ever half-folded. Test 18's overlapping tables remain the only shape that catches it. |
1 participant
Summary
process_uniform_gathers()only matchedWIDTH == 1$bmux, so a variable-index read of anything wider than a bit was skipped entirely and fell through tobmuxmap -pmux+pmuxtree, which expand each selector into a one-hot$eqfarm plus a mux tree.$bmuxis entry-major (Y = A[S*WIDTH +: WIDTH]), so aWIDTH = Wcell is W independent gathers over stride-W slices of the table, all sharing one index. This registers one candidate per read output bit and lets the existing grouping, affine analysis and emission run unchanged. W barrels over M entries cost what one barrel overW*Mbits would, so splitting the fold per element bit is free.One consequence needed handling: a cell now feeds one group per output bit, so it can no longer be retired by the first group that folds — the later groups still read it for its index and
srcattribute, which was a use-after-free (it segfaults without this). Folded cells are collected and removed once every group has been emitted.Only read output bits get a candidate, so a partially-used multi-bit gather does not pay for barrels nothing consumes.
Measured
Two 32-lane sliding windows over a 128-entry table of 8-bit elements — the new
vps_gather_widthregression in Silimate/preqorsor#2282 — post-aigmap, with the fold enabled versus disabled via-min_gather 0:$bmuxleft$_AND_$_NOT_139x fewer AND nodes. All 64 selectors fold to 16
$shr(8 element bits x 2 windows), and through the full Preqorsor flow the result lands 1.4% above the same function written as hand-rolled barrel shifts.Test plan
tests/silimate/opt_vps.ystests 15 and 16 added: SAT self-equivalence for a multi-bit gather, then cell counts pinning 16WIDTH=4$bmux-> 8$shr, with-min_gather 0as the control so the assertion cannot pass on a netlist that had nothing foldable.tests/silimate/opt_vps.ys(16 tests) passes in 18 s.tests/silimatesuite passes. The one failure,mux_push.ys, never invokesopt_vpsand comes from unrelated local work inmux_push.cc.