Repository navigation
fix(trit): ternary MAC adder_tree_27 overflow — wrong dot product on dense vectors - #1733
Merged
Merged
Conversation
…verflow) adder_tree_27 declared level-2 as signed [3:0] (range [-8,+7]), but each l2[j] = l1[3j]+l1[3j+1]+l1[3j+2] with l1 in [-3,+3] has range [-9,+9]. A group of 9 same-sign trits (sum +/-9) overflowed, so an all-+1 dot product read -21 instead of +27. Widen l2 to signed [4:0]. Found by a new golden-vector functional testbench (tests/bitnet_compute_mac.rs, iverilog+vvp) that drives pipeline_stage2_compute with known trit chunks and checks the accumulated result. Updated the unit test that had asserted the buggy signed [3:0] width. trit_stdlib.rs is not under the FROZEN_HASH seal; no reseal. Closes #1732 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Aug 5, 2026
Closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Model-critical correctness bug in the ternary MAC core, found by a new functional testbench.
Bug
adder_tree_27(fromgen-trit-stdlib, wrapped bytrit27_dot_product→pipeline_stage2_compute) declared level-2 aswire signed [3:0] l2 [0:2];(range [-8, +7]). But eachl2[j] = l1[3j] + l1[3j+1] + l1[3j+2]withl1 ∈ [-3, +3]has range [-9, +9] — so a group of 9 same-sign trits (sum ±9, or even ±8) overflows.Symptom:
input = {27{+1}}, weight = {27{+1}}→ expected dot product +27, actual −21 (each level-2 group of 9 wrapped +9 → −7; 3 × −7 = −21). Single-trit / sparse cases were correct, so the existing substring asserts never caught it.Fix
Widen
l2tosigned [4:0](range [−16, +15]). Level-1 (signed [2:0]holds [−3,+3]) and level-3 (signed [5:0]holds [−27,+27]) were already correct.Verification
New golden-vector functional testbench
tests/bitnet_compute_mac.rs(iverilog + vvp) drivespipeline_stage2_computewith known trit chunks:allP×allP = +27,allP×allN = −27,allN×allN = +27,allZ = 0, single-trit= +1, multi-chunk+27then−27accumulates to0.All pass after the fix;
−21/+21before it. Skips gracefully without iverilog. The unit test that had codified the buggysigned [3:0]width is updated.trit_stdlib.rsis not under the FROZEN_HASH seal (onlycompiler.rs), so no reseal. Full suite green apart from the pre-existing, unrelatedbitnet_topreds (#1726).This is the functional instrument that makes the engine-top datapath fix (input≡weight aliasing at
bitnet_top.rs:217) provable, per the observability-before-mutation discipline.🤖 Generated with Claude Code
Closes #1732