feat(xilinx7): 7-series configuration packets as a .t27 spec (Closes #5608) - #5609
9 commits merged into
Conversation
…5608) specs/xilinx7/packets.t27 holds the packet grammar, Series-7 register and command numbers, FAR layout, the running CRC and the COR0 field table, each cited from prjxray c9f02d857. 10/10 tests; the CRC oracle is a value Vivado wrote. bitwalk.rs, built from t27c gen-rust, reproduces all 12 CRC checks in 6 Vivado bitstreams, and `resealed` keeps the CRC valid after a COR0 rewrite where rewriting COR0 alone leaves 1 of 2 checks wrong. Closes #5608 Refs #5606 Refs #5607 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
… (Refs #5608) The bitwise CRC (37 bit steps per written word) was ~90% of bitwalk's time. Add CRC32C_TABLE, crc_byte and crc_word (4 lookups + 5 bit steps) and route crc_after through it. crc_step stays as the bitwise definition. The table is not trusted: crc_table_is_derived recomputes all 256 entries from crc_bit, and crc_word_equals_crc_step compares both forms over 4096 xorshift32 pairs. Mutating one table bit or dropping one byte step fails them. 12/12 tests; bitwalk still reproduces all 12 Vivado CRC checks. The docs/now entry withdraws the earlier 0.3-0.9 s figure (taken at load ~45) and records the measured before/after with its load. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
PR DashboardGenerated at: 2026-10-02 16:20:26 UTC
Summary
Seal Status
|
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
…mes (Refs #5608) specs/xilinx7/frames.t27 states the 13-bit ECC in word 50 of every 7-series frame, citing prjxray ecc.cc. Three frames copied from a Vivado bitstream are the in-spec oracle (7/7 tests). bitwalk recomputes the ECC of every FDRI frame through the generated module: 6 Vivado bitstreams, 32,520 frames, bad 0. Four deliberate defects each fail the tests and the sweep. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…efs #5608) The six vectors lromor/fpga-assembler pins in arch-xc7-frame_test.cc for the same function, added as one test. 8/8. They are computed from the rule, not a device; the Vivado frames remain the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
PR DashboardGenerated at: 2026-10-02 16:43:16 UTC
Summary
Seal Status
|
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
PR DashboardGenerated at: 2026-10-02 16:46:03 UTC
Summary
Seal Status
|
…rites, pin tiles and segbits (Refs #5608) far.t27 states the 7-series frame address layout and the order a multi-frame FDRI write visits addresses, with two pad frames after every (block, half, row) group. The xc7a35t part table is generated from prjxray-db part.json between markers and drift-checked. Checked against six Vivado xc7a35t bitstreams: every FDRI write is the walked 5420 frames, all 72 pad frames are empty, 82/82 constrained pins land in IOB frames with data, and 4224/4224 set bits are named by some tile's segbits at the walked frame (bitwalk --pins, --bits). Five mutations fail both the spec tests and the sweep. The FAR layout moves here from packets.t27 (no cross-module use in t27c yet), so the rule keeps one home. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
PR DashboardGenerated at: 2026-10-02 17:09:24 UTC
Summary
Seal Status
|
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
far.t27's part table now covers xc7a35t, xc7a100t and xc7a200t, rendered from prjxray-db part.json/part.yaml by `tri x7-part` and drift-checked on every audit. Every walk function takes the part; bitwalk picks it from the IDCODE the stream writes. - xc7a35t: unchanged against Vivado (5420 frames x6, pins 82/82, segbits 4224/4224, 11/11 mutations caught). - xc7a100t: 9464 frames, equal to hb.bit (xc7frames2bit) and to an in-house openXC7 build. - xc7a200t: 24080 frames, equal to an xc7frames2bit 200T bitstream. The larger parts have no Vivado reference here; the header says so. New test every_part_index_meets_its_walk ties fdri_index to part_fdri_frames for all 24 groups; ignoring the part offset fails it. Refs #5608 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Reviewer bee: evidence and verdict for head What I checked myself. I used a temp clone and a
These claims reproduce. What is still missing:
The other red gates ( |
…o xc7frames2bit (Refs #5608) packets.t27 now holds the 42-step packet sequence xc7frames2bit writes around the frame data, cited to prjxray c9f02d857 and tested against an xc7frames2bit bitstream (57 words before FDRI, 524 after, register words). bitwalk --write places .frames at far.t27's fdri_index, seals ECC with frames.t27 and emits the SEQ steps plus the .bit header. bitwalk --frames dumps a .bit back to .frames. Measured: byte-identical to xc7frames2bit on 8/8 xc7a100t pairs and on frames dumped from 6 Vivado xc7a35t and 2 xc7a200t bitstreams, whose FDRI payload also equals the original's. xc7a100t frames handed over as xc7a200t are refused (192 foreign addresses, exit 1); xc7frames2bit writes them with exit 0 and 192 extra frames. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
PR DashboardGenerated at: 2026-10-02 17:47:25 UTC
Summary
Seal Status
|
Retain original PR5609's nine upstream commits, three specifications, Rust driver, six receipts and test oracles. Resolve the add/add packet conflict to the original sourced grammar and CRC/ECC rules, preserving current master fixes. Add one receipt with this review's actual proof. 35existing Zig tests,37,048original-C++/generated-Rust observations, three meaningful negative controls and full-file COR0/CRC cases pass. Fast corpus95/95CLEAN without ledger edits. Full hardware/Vivado/FASM verification and all-green repository health are not claimed. Closes #5870 Refs #5608, #5609
Closes #5608
Refs #5606, #5607
What
specs/xilinx7/packets.t27: the Xilinx 7-series configuration packet stream as one spec.resealed, which rewrites a CRC word only if the original one passed.specs/xilinx7/bitwalk.rs: a driver built fromt27c gen-rust. It does file I/O and the loop; every decision is a spec function. Build steps are in both file headers. The generatedpackets.rsand the binary are gitignored.docs/now/2026-10-02-xilinx7-packets-spec-reproduces-vivado-crc.md.Measured
t27c test-report specs/xilinx7/packets.t27: 10 pass, 0 fail. The CRC oracle is a value Vivado wrote (0xE3AD7EA5), not one the spec computed.prjxray-db/artix7/harnessbitstreams), all 12 CRC checks reproduce; bad 0.xc7frames2bit) bitstreams contain no CRC write at all.patch_cor0's approach, rewriting only the COR0 word, leaves a Vivado bitstream with 1 of 2 CRC checks wrong (bitwalk --cor0 5 --no-reseal). Withresealed, 2 words change and bad is 0.scripts/dump_bit_config.pyprints for the same files.Limitations
cli/tri/src/fpga.rsis not changed. Movingpatch_cor0andbit_configonto the spec is a follow-up.varin a test (t27c gen: var reassigned in a test block is emitted as a second var (redeclaration) #5606), and bool calls inlined iniffor gen-rust (t27c gen-rust: local bound to a bool-returning call is emitted as if (b) != 0 #5607).Later commits on this branch
Each commit has its own
docs/now/entry with the measurements and the limits.frames.t27). It recomputes the ECC of 32,520 of 32,520 Vivado frames.far.t27, xc7a35t / 100T / 200T, part picked by IDCODE).bitwalk --write). Frames to .bit, byte-identical toxc7frames2biton 16/16.xc7frames2bitaccepts them, see xc7frames2bit: refuse frame addresses the part does not have openXC7/prjxray#27.bitwalk --fasm, segbit positions inframes.t27).fasm2frameson 20/20: 13 real designs, 5 synthetic, and 2 refuse filesrefused for the same reason.
--strictrefuses bits outside their tile.fasm2frameswrites an absent*_SINGsite'sbits into word 100 of the frame, which another tile owns.
fasm2frames.Still not shown: no board has been configured with any output of this branch. No xc7a200t FASM
is in the corpus, and there is no Vivado reference for 100T or 200T.
🤖 Generated with Claude Code