Skip to content

verified: the die's 57-bit DNA read over JTAG -- R3-2 slice 1 (Closes #7439) - #7446

Merged
gHashTag merged 2 commits into
masterfrom
claude/device-dna-7439
Oct 7, 2026
Merged

verified: the die's 57-bit DNA read over JTAG -- R3-2 slice 1 (Closes #7439)#7446
gHashTag merged 2 commits into
masterfrom
claude/device-dna-7439

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 7, 2026

Copy link
Copy Markdown
Owner

Closes #7439
Refs #6655

What

specs/verified/device_dna.t27 (module VerifiedDeviceDna) is R3-2 slice 1 of the Verified Compute epic. It is the device-rooted identity: the XC7A200T's 57-bit device DNA, read live over JTAG with no user bitstream. Every decision about that read is written in t27:

  • IR length 6. FUSE_DNA 0x32 is a 64-bit register. XSC_DNA 0x17 is a 57-bit register that must sit between ISC_ENABLE 0x10 and ISC_DISABLE 0x16; without ISC_ENABLE it reads all ones.
  • Decode: the first shifted bit is the most significant (reverse57). This is the order openFPGALoader --read-dna prints.
    • XSC: the low 57 bits of the raw read.
    • FUSE: the raw read shifted right by 7. The upper 57 bits are the same as XSC, and the 7-bit tail is 0x4F.
  • Well-formedness: not all zero; not all one; XSC fill ones present when TDI is held high; FUSE tail as observed.
  • Agreement: when a FUSE read and an XSC read name the same die (exact equality).
  • The DNA as 15-digit lowercase hex, written by dna_hex_char and checked by dna_hex_matches.

Oracle (live, 2026-10-07, one board, USB bus 000 dev 002)

instruction raw decoded DNA
FUSE_DNA 0x32 0x2a19bf1841ab0a4f 050d58218fd9854
XSC_DNA 0x17 (TDI high) 0xfe54337e30835614 050d58218fd9854
  • 14 reads of each instruction over two independent transports (libftdi MPSSE and openocd 0.12.0). All 14 were identical.
  • openFPGALoader --read-dna prints 0x0050d58218fd9854, which confirms the decode independently.
  • Register lengths were measured with fill ones: FUSE 64, XSC 57, BYPASS 1.
  • The reader is the openocd command line in the spec header.

Verification

  • t27c test-report on the Railway lab: 13 tests, 13 pass, 0 vacuous.
  • Seal .trinity/seals/verified_VerifiedDeviceDna.json was written by t27c seal --save on the lab.
  • Mutation: 20 of 20 hand mutants killed by runtime asserts on the lab. The mutants were copies beside the spec under specs/verified/, deleted afterwards; the list is in the spec header.

Hand-foreign lines: 0

The task allowed up to 40 lines of Python I/O glue under tools/jtag. The Only-t27 gate on master denies any added or modified .py (checked with the compiled gen/c/policy/own_language.c), and the 40/80 budget (#7371) has not landed. The read needs no new code, so the reader is the openocd command line documented in the spec header.

Pending

🤖 Generated with Claude Code

gHashTag and others added 2 commits October 7, 2026 16:43
@gHashTag @claude
verified: the die's 57-bit DNA, read over JTAG -- R3-2 slice 1 spec (…
410c111 
…Refs #7439)

specs/verified/device_dna.t27 pins every decision about the 7-series
device DNA read with no user bitstream: IR length 6, FUSE_DNA 0x32 (64-bit
register) and XSC_DNA 0x17 between ISC_ENABLE 0x10 and ISC_DISABLE 0x16
(57-bit register); how the raw shift decodes to the DNA (first shifted bit
is the most significant, the order openFPGALoader --read-dna prints);
well-formedness (not all zero, not all one, XSC fill ones, FUSE tail as
observed); fixed-width hex; and when a FUSE read and an XSC read name one
die.

Oracle: 14 live reads of each instruction on the attached XC7A200T over two
transports (libftdi MPSSE and openocd), all identical; decoded DNA
050d58218fd9854. 13 tests, 0 vacuous; 20 of 20 hand mutants killed on the
Railway lab.

The reader is the openocd command line in the spec header: the Only-t27 gate
refuses a new or edited .py, and the read needs no new code.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@gHashTag @claude
seal: specs/verified/device_dna.t27 on the Railway lab (Refs #7439)
5ca382e 
t27c test-report: 13 tests, 13 pass, 0 vacuous. Seal written by
t27c seal --save on the lab (t27c-bootstrap@0.4.0+cfda070b2).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@gHashTag
gHashTag enabled auto-merge (squash) October 7, 2026 09:47
@gHashTag gHashTag mentioned this pull request Oct 7, 2026
Closed
7 tasks
This was referenced Oct 7, 2026
Merged
Merged
Merged
This was referenced Oct 7, 2026
Closed
Closed
Open
This was referenced Oct 7, 2026
Merged
Draft
Merged
Draft
Draft
Merged
Merged
Merged
Merged
Closed
Merged
Closed
Open
Merged
Merged
@gHashTag gHashTag mentioned this pull request Oct 7, 2026
Merged
@github-actions

github-actions Bot commented Oct 7, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-07 11:00:46 UTC

Summary

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

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

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=c3821827b257 != 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).

@gHashTag
gHashTag merged commit c523d30 into master Oct 7, 2026
24 of 29 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

R3-2 slice 1: read the die's DNA over JTAG (Refs #6655)

1 participant

@gHashTag