Skip to content

feat(fpga): eth_rx.t27 -- receive path of the Ethernet job link (E2a) - #8337

Closed
dmitrii-f-t27 wants to merge 3 commits into
masterfrom
spec/eth-rx
Closed

dmitrii-f-t27 wants to merge 3 commits into
masterfrom
spec/eth-rx

Conversation

@dmitrii-f-t27

@dmitrii-f-t27 dmitrii-f-t27 commented Oct 9, 2026 •

Copy link
Copy Markdown
Collaborator

Closes #8333

Part of #8327 (E2: TRI-NET node over UDP on the AX7203). Refs #6655.

Pull Request Checklist

  • PR title follows semantic convention
  • PR body includes Closes #8333
  • Tests added: t27c test-report specs/fpga/eth_rx.t27 passes 8/8
  • Spec sealed: t27c seal specs/fpga/eth_rx.t27 --save, then --verify all MATCH

Description

specs/fpga/eth_rx.t27 (module EthRx) is the receive half of the Ethernet job link. It takes the GMII-style byte stream of one PHY, a valid flag plus one byte per 125 MHz clock, and accepts exactly the UDP datagrams addressed to the node:

  • destination MAC 02:27:00:00:00:01 (the address EthBeacon sends from) or broadcast;
  • EtherType 0x0800, IPv4 with IHL 5, not a fragment, a correct header checksum, protocol 17;
  • destination 192.168.1.227, 192.168.1.255 or 255.255.255.255, UDP port 27028;
  • a UDP length that agrees with the IP length and is at most 1480 (a 1518-byte frame, no jumbo frames);
  • at least 64 bytes and as many as the UDP header needs (padding after the datagram is legal), and an FCS that leaves the CRC-32 residue 0xDEBB20E3.

Payload bytes come out one per clock with their index while the frame is still clean; the consumer buffers them and uses them only when the frame ends with ok = 1. The sender's MAC, IP and port are latched for the reply (E2c), so a host needs no ARP entry: it may send to the broadcast address. Each drop has its own reason code (1 MAC, 2 EtherType/version, 3 protocol, 4 destination IP, 5 port, 6 FCS, 7 runt/truncated, 8 IPv4 checksum, 9 fragment, 10 UDP length) and is counted.

Turning RGMII nibbles into these bytes on silicon is E2d and is not in this PR.

Changes

  • specs/fpga/eth_rx.t27 -- new spec, 8 tests and 1 invariant.
  • .trinity/seals/fpga_EthRx.json -- seal built with t27c 0.5.2 from this tree.
  • docs/reports/t27b_expectations.json -- one pass row for specs/fpga/eth_rx.t27.
  • tools/duplicate_bodies_baseline.txt -- crc_step and crc_byte copied from EthBeacon on purpose: use fpga::eth_beacon::{crc_byte} typechecks and passes the tests, but gen-verilog emits the call without the function body, so the RTL of EthRx would not elaborate.

Fix in 8819b10: the length sums wrapped (review finding)

pay_end and need_len were UDP_POS + udp_len (+ 4) in 16 bits. A 70-byte frame with IP length FF FF, UDP length FF EB and a correct IPv4 checksum (B6 54) and FCS passed the length agreement (65535 - 20 = 65515); need_len wrapped to 17 and the frame was accepted with ok = 1 and no payload byte. Now byte 39 rejects a UDP length above 1480 as reason 10, and pay_end_of / need_of add only below that bound, so the sums are safe on every clock whatever udp_len holds (above it the need is 65535, past POS_CAP).

before (454e08a) after (8819b10)
spec, Zig runner new test panics integer overflow at UDP_POS + udp_len 8/8 pass, 0 vacuous
generated RTL, 20 independent frames FAIL: frames 1 (IP 0xFFFF / UDP 0xFFEB), 5 (UDP 1481) and 6 (IP 19 / UDP 0xFFFF) accepted with ok = 1 PASS 20/20
OOC, seeds 1/2/3 at 125 MHz 139.51 / 138.99 / 128.80 MHz 145.01 / 149.50 / 142.53 MHz

Testing

cargo build --release -p t27c
PATH=<zig 0.16.0>:$PATH ./target/release/t27c test-report specs/fpga/eth_rx.t27 --verbose
./target/release/t27c seal specs/fpga/eth_rx.t27 --verify
  • test-report: 8/8 pass, 0 vacuous. Invariant proved at comptime.
  • seal --verify: all hashes MATCH; tests 8/8 recorded in the seal.
  • Independent oracle. The canonical frame (66 data bytes, 192.168.1.101:50000 to 192.168.1.227:27028, a 24-byte TRI-NET request as payload) was built in Python with struct, the RFC 791 sum and zlib.crc32 before the spec: IPv4 checksum 0xB620, FCS 30 2B 9B E2, payload sum 2199. A test asserts that the spec's own builder and crc_byte reproduce exactly these values.
  • Each drop reason is exercised. One variant per defect, with a correct FCS so only the intended defect is present, plus a corrupted FCS, a runt, broadcast MAC and broadcast IP (accepted), noise before the SFD and two frames back to back. A test also checks that no payload byte leaks out of a frame whose header already failed.
  • Generated RTL, simulated. The gen-verilog output (sha256 2abc54db..., equal to the seal's gen_hash_verilog) runs in Icarus Verilog 13.0 against 20 frames built independently in Python (struct, RFC 791, zlib.crc32): every reason code 1..10, a flipped FCS bit, a runt, broadcast MAC and both broadcast IPs, a padded 2-byte datagram, UDP 1480 in a 1518-byte frame, UDP 1481, the two length-overflow frames and a 64-byte frame that needs 70. why, ok, and for accepted frames the payload count and byte sum all match. The testbench and generator are kept outside the repo (hand-written .v/.py need an owner-approved entry in tools/policy/foreign-exceptions.txt); hashes: generator 482c55df..., testbench a326e94e..., vectors 39008e84....
  • Synthesis and timing, out of context. gen-verilog output, wrapped (not committed) so that all outputs reach one pin, on xc7a200tfbg484-2 with yosys 0.69 (synth_xilinx -flatten -abc9 -nowidelut -nosrl) and nextpnr-xilinx 0.9.7: 1004 cells after the fix, post-route 145.01 / 149.50 / 142.53 MHz on seeds 1, 2, 3 against 125 MHz. The first version reached 85.5 MHz; the verdict now uses only comparisons (the IPv4 checksum fold and the required length are settled at byte 40) and the counters move one clock after done.

Review Notes

  • t27c icarus-simulate does not run tests that call on_clock (Enable of unknown task on_clock); the same happens on master for eth_beacon.t27 and rgmii_sniff.t27. The generated RTL is therefore checked with the separate testbench above.
  • No compiler change, no existing spec touched, no hand-written Verilog in the repo.
  • Not shown here: RGMII capture on silicon and a frame received by the board (E2d). This PR proves the spec and its generated RTL in simulation and out-of-context timing only.

Checks that fail on master too (not caused by this PR)

check cause master
duplicate-bodies has_at in specs/tri/t27b/ast_walk.t27 (#8258) has no ledger row tools/dupe_scan.py on origin/master fails with the same line
scan /Users/playra/ in .claude/skills/t27b-loop/SKILL.md (#8332) same file on master
t27b-native-ratchet 10 UNLISTED specs from master (queen/keyed, math/constants, ...); eth_rx.t27 is no longer among them same 10
Corpus ratchet specs/math/constants.t27 discards improved 386 to 349 (#8209) without a re-bless master change

This PR does not merge while they are red; they need their own fixes on master.


φ² + 1/φ² = 3 | TRINITY

#8333)

E2a of #8327. EthRx takes the GMII-style byte stream of one PHY (valid flag plus
one byte per 125 MHz clock) and accepts exactly the UDP datagrams addressed to
the TRI-NET node on the AX7203: destination MAC 02:27:00:00:00:01 or broadcast,
IPv4 without fragments and with a correct header checksum, UDP to port 27028 at
192.168.1.227 or a broadcast address, a UDP length that agrees with the IP
length, and an FCS that leaves the CRC-32 residue 0xDEBB20E3. Payload bytes go
out one per clock with their index; the sender's MAC, IP and port are latched
for the reply; every drop has its own reason code and is counted.

The canonical test frame was built independently in Python (struct, the RFC 791
sum, zlib.crc32): IPv4 checksum 0xB620, FCS 30 2B 9B E2, payload sum 2199.

Timing: every sum the verdict needs is settled at byte 40, and the counters
move one clock after the verdict, so no adder chain follows the last byte.
Out of context on xc7a200tfbg484-2 (yosys 0.69, nextpnr-xilinx 0.9.7) the
module closes 125 MHz on three seeds: 139.51, 138.99 and 128.80 MHz.
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 20:36:14 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 46
PRs with All Checks Green 4
READY 0
FAILING 46
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 46 + 0 + 0 = 46, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=557cd271f4e3 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

…8333)

t27b-native-ratchet: specs/fpga/eth_rx.t27 passes t27b and the reference,
so it gets a pass row, sorted after eth_crc.t27.

duplicate-bodies: crc_step and crc_byte in EthRx are byte-identical to
EthBeacon on purpose. `use fpga::eth_beacon::{crc_byte}` typechecks and the
7 tests pass, but gen-verilog emits the call without the function body, so
the RTL of EthRx would not elaborate. Each RTL module must carry its own
copy until the Verilog backend inlines imported functions; the baseline
records the two groups.
…ot wrap (#8333)

pay_end and need_len were UDP_POS + udp_len (+ 4) in 16 bits. A 70-byte frame with
IP length 0xFFFF and UDP length 0xFFEB passed the IP/UDP length agreement
(65535 - 20 = 65515), then need_len wrapped to 17 and the frame was accepted with
ok = 1 and no payload. The generated RTL did exactly that; the Zig test runner
panicked with an integer overflow on the same sum.

- Byte 39 rejects a UDP length above MAX_UDP = 1480 (a 1518-byte frame) as reason 10.
- pay_end_of and need_of add only below the bound, so the sums are safe on every
  clock, whatever udp_len holds then; above it the need is 65535, past POS_CAP.
- New test: IP 0xFFFF / UDP 0xFFEB, a padded 2-byte datagram (accepted), UDP 1480 in
  1518 bytes (accepted), UDP 1481, IP length 19 with UDP 0xFFFF, and the canonical
  frame cut to 64 bytes on the wire while it needs 70 (reason 7).

test-report 8/8, 0 vacuous; seal re-saved with the tree's t27c 0.5.2, verify MATCH.
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 21:16:27 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 49
PRs with All Checks Green 1
READY 0
FAILING 49
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 49 + 0 + 0 = 49, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=557cd271f4e3 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@dmitrii-f-t27

Copy link
Copy Markdown
Collaborator Author

Replaced by #8370: the same four files as one commit on current master (ef75683). Two commits here had (#8333) without the keyword that L1 TRACEABILITY requires (run 37991060782, job 114027790002), and a pushed branch is not rewritten. The review findings and the generated-RTL evidence are in #8370's description.

dmitrii-f-t27 added a commit that referenced this pull request Oct 9, 2026
…#8370)

* feat(fpga): eth_rx.t27 -- receive path of the Ethernet job link (E2a)

Closes #8333

EthRx takes the GMII-style byte stream of one PHY and accepts exactly the UDP
datagrams to the TRI-NET node (MAC 02:27:00:00:00:01 or broadcast, IPv4
192.168.1.227/.255/255.255.255.255, port 27028), with a UDP length of at most
1480 that agrees with the IP length, at least 64 bytes and as many as the UDP
header needs, and a CRC-32 residue 0xDEBB20E3. Each drop has its own reason.

The UDP length is bounded before any sum uses it: 34 + 0xFFEB would wrap to 13
in 16 bits and let a 70-byte frame pass the length check (found in review of
#8337; the generated RTL accepted that frame with ok = 1).

- test-report 8/8, 0 vacuous; seal from this tree's t27c 0.5.2, verify MATCH.
- t27b ledger: one pass row. Duplicate baseline: crc_step and crc_byte are
  EthBeacon's on purpose, because gen-verilog emits an imported call without
  its body.

Replaces #8337, whose commits lacked the issue keyword L1 TRACEABILITY needs.

* ci(elab): eth_rx elaborates clean, so it gets a 0 row

Refs #8333

fpga-conformance (tools/check_elab_ratchet.py) read the new EthRx module as
NEW with 0 errors and no row, as it did for eth_beacon and rgmii_sniff with
#7788. iverilog elaborates the gen-verilog output without an error.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

E2a: eth_rx.t27 -- receive path for UDP datagrams to the TRI-NET node (AX7203)

1 participant