Repository navigation
spec(gft_signed_mac): the four on-die clauses, derived as simulation tests - #5662
Merged
dmitrii-f-t27 merged 1 commit intoOct 3, 2026
Conversation
…tests The die check W839 strapped to this operator (DESIGN 13) asks four questions; the spec answered two -- the two the die passed. The two failing clauses, ZERO and COMM, had no simulation counterpart, so nothing cheaper than a bitstream load could have asked them (trinity-fpga#684: the die check is stronger than the suite the spec carries). zero_clause pins the spec's half of W839's registered forecast: with the deliberately unguarded smul, mac(0, live, 0, live2) returns 512 (offset 1, mant 0) -- the operand's magnitude survives at a shifted offset (T596) and the two 'vanished' products add, so the clause cannot hold. The die read c_zero=0 as forecast; simulation agrees. comm_clause asserts the other half, which the die read 0 AGAINST the forecast: smul is commutative by construction (sign XOR over a symmetric RNE magmul, addition order untouched), and a 20000-case randomized operand-swap sweep against the reference semantics found zero divergences. The derived tests pass under icarus-simulate, which lowers to the generated Verilog -- so COMM holds in the simulated RTL too, and the die's c_comm=0 is isolated to the JTAG wrapper's drive pattern, the harness read, or silicon timing. Not the arithmetic. Refs Trinity-S-AI-DNA#5661 Refs Trinity-S-AI-DNA/trinity-fpga#684
dmitrii-f-t27
force-pushed
the
spec/gft-signed-mac-die-clauses-5661
branch
from
October 3, 2026 02:17
adaaedf to
48e55ea
Compare
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.
Refs #5661
Refs Trinity-S-AI-DNA/trinity-fpga#684
Why
trinity-fpga#684 measured the operator red on silicon —
clauses=0011,ok=0— while the spec passes its own two-test suite. The die check (W839, DESIGN 13) asks four questions; the spec answered the two the die passed (cancel↔ CANCEL,pp↔ IND). The two failing clauses had no simulation counterpart, so nothing cheaper than a bitstream load could have asked them.The derivation
zero_clausesmulreturns the operand's magnitude at a shifted offset (T596);mac(0,+1.0,0,+1.0)= 512 (offset 1, mant 0). Simulation now pins the spec's half of W839's registered forecastcomm_clausecancelppWhat the run establishes
All four pass under
t27c icarus-simulate— which lowers the spec to the generated Verilog and simulates that. So COMM holds in the simulated RTL, not only in the reference semantics. The die'sc_comm=0therefore diverges from the spec and from the simulated generated Verilog, isolating the remaining fault to the JTAG wrapper's drive pattern, the harness read, or silicon timing — the exact isolation trinity-fpga#684 asked for.docs/now entry:
docs/now/2026-10-03-gft-signed-mac-die-clauses-derived-as-tests.md— dmitrii-f-t27
On the two red checks (both pre-existing, neither introduced here)
layers_Residual,loss_HuberLossand 10 more seals whose gen hashes predate the current compiler — red on master's own runs of this workflow (2026-10-02 22:43 and 21:51). This PR refreshes the one seal it touches (ternary_GftSignedMac.json, recomputed with t27c 0.4.0 built from this branch); the others are the corpus's existing debt.verify_multitarget.pyfails asgft_sadd.sadd: Zig backend failed to build/run … exited -6 (signal 6) … m.zig:125:20 in magsub. That is a pre-existing defect inspecs/ternary/gft_sadd.t27, not in this PR's spec:saddcallsmagsub(ma, mb)before thema < mbswap, so the discarded call runs with a negative exponent (d = ho − lo_o < 0) and the Zig backend traps on the negative shift while the C/Rust paths happen to tolerate it. The same check was red on master on 2026-08-20 and has not run green since 2026-08-28. Filed separately with the root cause.