Skip to content

fpga(coverage): line, toggle and FSM coverage as a t27 spec (Closes #7578) - #7579

Open
gHashTag wants to merge 1 commit into
masterfrom
feat/fpga-coverage-1483
Open

gHashTag wants to merge 1 commit into
masterfrom
feat/fpga-coverage-1483

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 7, 2026

Copy link
Copy Markdown
Owner

Adds specs/fpga/coverage.t27 — line, toggle and FSM coverage expressed as a t27 spec: 506 lines, 26 tests + 4 invariants, t27c test-report 26/26 with 0 vacuous claims.

Canonical home for the spec the verification course lesson vendors (gHashTag/trinity#1483 — the course branch feat/course-verification-1483 carries the vendored copy; the nightly vendored-sha gate picks it up once this merges).

Closes #7578

🤖 Generated with Claude Code

…nity#1483)

The verification course (gHashTag/trinity#1483) needs a coverage model
for its lesson 16; this is the gHashTag/t27 side. Line/branch points,
toggle points per signal bit and direction, FSM state and transition
points, each with a hit counter; integer percentages that return 0
when nothing was measured; illegal transitions that must stay at 0
hits. 26 tests (t27c test-report: 26/26, 0 vacuous) and 4 invariants,
proved comptime. Flat arrays + count fields, the style of
specs/fpga/simulator.t27 and vcd_trace.t27. trinity vendors the same
file byte-identically.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 7, 2026
This was referenced Oct 8, 2026

This branch has not been deployed

No deployments
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.

fpga: coverage spec (line, toggle, FSM) for the verification course

1 participant