Repository navigation
Derive gft_signed_mac's four on-die clauses as simulation tests (W839, trinity-fpga#684) #5661
Description
trinity-fpga#684 measured gft_signed_mac red on silicon — clauses=0011, ok=0 — while the spec passes its own two-test suite. The die check asks four questions; the spec answered only the two that 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 (W839's clause list, as tests)
| clause | die | derived test | expectation under the spec |
|---|---|---|---|
ZERO — mac(0,live,0,live2)==0 |
0 (as forecast) | zero_clause |
cannot hold: the deliberately unguarded smul returns the operand's magnitude at a shifted offset (T596), and the two "vanished" magnitudes add to 512 (offset 1, mant 0). Simulation pins the spec's half of W839's registered forecast |
COMM — mac(live,TWO,live2,ONE)==mac(TWO,live,ONE,live2) |
0 (against forecast) | comm_clause |
holds exactly: sign-XOR + symmetric RNE magmul, addition order untouched. Verified against the reference semantics by a 20000-case randomized operand-swap sweep — zero divergences |
| CANCEL | 1 | existing cancel |
already covered |
| IND | 1 | existing pp |
already covered |
What the run says
All four pass under t27c icarus-simulate — which lowers the spec to the generated Verilog and simulates that, not just the reference semantics. So COMM holds in the generated Verilog too. The die's c_comm=0 therefore diverges from the spec AND from the simulated RTL, isolating the remaining fault to the JTAG wrapper's drive pattern, the on-die harness read, or silicon timing — not to the arithmetic. That is exactly the isolation trinity-fpga#684 asked for and could not get without these tests.
— dmitrii-f-t27
User Scenarios
- Given the
gft_signed_macspec passes its existing two-test suite but the die check fails on clauses ZERO and COMM, When the spec is extended with simulation tests for those two clauses, Thent27c icarus-simulateruns all four clause tests against the generated Verilog and reports the same pass/fail pattern as the die measurement, isolating the fault to the JTAG wrapper, on-die harness, or silicon timing.
Requirements
- FR-001: The spec
specs/ternary/gft_signed_mac.t27MUST define azero_clausetest that assertsmac(0, live, 0, live2) == 0under the generated Verilog simulation. - FR-002: The spec
specs/ternary/gft_signed_mac.t27MUST define acomm_clausetest that assertsmac(live, TWO, live2, ONE) == mac(TWO, live, ONE, live2)under the generated Verilog simulation. - FR-003: The four clause tests (existing
cancel, existingpp, newzero_clause, newcomm_clause) MUST all execute undert27c icarus-simulatewithout tooling changes.
Success Criteria
t27c icarus-simulate specs/ternary/gft_signed_mac.t27exits 0 and runs exactly 4 tests.- The simulation output shows
zero_clauseFAIL (matching die clause ZERO = 0) andcomm_clausePASS (matching die clause COMM = 0 per the issue's forecast), whilecancelandppremain PASS.
Boundary
- specs/ternary/gft_signed_mac.t27
Activity
spec(gft_signed_mac): the four on-die clauses, derived as simulation …
gHashTag commentedon Oct 7, 2026
Reopened 2026-10-07: the bulk close of issues without a
## Boundarysection was reverted by the owner. Nothing to do here; this comment replaces the earlier close notice.dmitrii-f-t27 commentedon Oct 10, 2026
Completed by #5662, merged 2026-10-03 as bb0aa9f. That PR said
Refs, so this issue did not close automatically.specs/ternary/gft_signed_mac.t27on master carries all four on-die clauses as tests:pp(IND),cancel(CANCEL),zero_clause(ZERO),comm_clause(COMM). The later sadd fix in #5737 (34849f5) kept them.Re-checked locally on master 295b2c5, with t27c 0.5.2 built from that tree:
t27c icarus-simulate specs/ternary/gft_signed_mac.t27: exit 0, 4 tests, all PASSED (zero_clauseprobe = 512,comm_clauseprobes = 20480 / 20480).t27c seal specs/ternary/gft_signed_mac.t27 --verify: all hashes MATCH.Note on the queen-shaped sections: FR-001 and the Success Criteria describe ZERO as
== 0/ "zero_clause FAIL". The derivation is intentional and follows the issue body: under the spec ZERO cannot hold (deliberately unguardedsmul, T596), sozero_clausepins the spec's actual value 512 (W839's forecast) and passes. COMM holds in the simulated generated Verilog, so the die's COMM=0 points at the JTAG wrapper drive, the harness read or silicon timing, not at the arithmetic.gHashTag/trinity-fpga#684 (the on-die fault itself) stays open; this issue covered only the simulation tests.
Dmitrii Fedorov (@dmitrii-f-t27)