Three more primitives enumerated: 50.6M inputs, and a width bug that would have made the tool agree with itself - #2206
Merged
Merged
Conversation
The machinery from #2198/#2200/#2202 is built; this applies it to three more primitives, none of which had any cross-target check before this line of work. full_adder 16,777,216 model == C == Rust; Verilog on a labelled slice maj3 16,777,216 model == C == Rust; Verilog on a labelled slice pack3 16,777,216 model == C == Rust [new] tmul 65,536 four arms, exhaustive xor2 65,536 four arms, exhaustive [new] sign0 65,536 four arms, exhaustive [new] pack2 65,536 model == C == Rust negate 256 four arms, exhaustive 50,594,048 inputs exhaustive across model/C/Rust, of which 196,864 across four independent implementations. A bug caught before it ran, which would have made the tool agree with itself. The Verilog testbench generator sliced every loop variable as i0[7:0], hardcoded to a byte. sign0 takes i16. It would have compiled, run, produced a digest, and compared a NARROWER function than the C and Rust arms evaluated -- Verilog truncating its argument to 8 bits while the others used 16. The digests would then disagree for a reason that has nothing to do with the backends, or agree by luck on some domain and be trusted. The width now comes from the declared type. That is this line's own failure mode, located in the checker rather than the checked: a harness that measures something other than what it reports. pack2 and pack3 return u64. The C and Rust folds take the low 32 bits; a matching Verilog fold needs a 64-bit accumulator. They stay three-way and are labelled, rather than given an arm that quietly compares something narrower -- which is the mistake avoided immediately above. Also corrected in my own issue text: I wrote '262,400 across four implementations', having counted pack2's 65,536 despite it having only three arms. It is 196,864. Closes #2205 Refs #2204 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
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
1 participant
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.
The machinery from #2198 / #2200 / #2202 is built; this applies it. Three more primitives, all previously unchecked cross-target.
full_adder(u8,u8,u8)maj3(u8,u8,u8)pack3(u8,u8,u8)tmul(u8,u8)xor2(u8,u8)sign0(i16)pack2(u8,u8)negate(u8)50,594,048 inputs covered exhaustively by model/C/Rust, of which 196,864 across four independent implementations. At the start of this line of work none of these specs had any cross-target check at all.
A bug caught before it ran, which would have made the tool agree with itself. The Verilog testbench generator sliced every loop variable as
i0[7:0]— hardcoded to a byte.sign0takesi16. It would have compiled, run, produced a digest, and compared a narrower function than the C and Rust arms were evaluating: the Verilog arm truncating its argument to 8 bits while C and Rust used all 16. The digests would then have disagreed for a reason that has nothing to do with the backends — or, worse, agreed by luck on some domain and been trusted. The width now comes from the argument's declared type.That is the same failure this whole line exists to catch, in the checker rather than in the thing checked: a harness that measures something other than what it reports.
pack2andpack3returnu64. The C and Rust folds take the low 32 bits; a matching Verilog fold needs a 64-bit accumulator. They stay three-way and are labelled rather than given an arm that quietly compares something narrower — the exact mistake avoided above.Refs #2204
Closes #2205
🤖 Generated with Claude Code