Skip to content

spec(led-d5): connect the clocked counter and LED output - #5854

Merged
dmitrii-f-t27 merged 3 commits into
gHashTag:masterfrom
dmitrii-f-t27:codex/led-d5-executable-rtl
Oct 4, 2026
Merged

dmitrii-f-t27 merged 3 commits into
gHashTag:masterfrom
dmitrii-f-t27:codex/led-d5-executable-rtl

Conversation

@dmitrii-f-t27

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

Copy link
Copy Markdown
Collaborator

Closes #5846. Supersedes the source in PR #5847 after actual code/RTL review; no change to scoring rules.

The Queen-published port passes three Zig tests, but gen-verilog declares clk twice, assigns an undeclared on_clock, and provides no led port. Icarus rejects it. The judged and published commits contain identical .t27 blobs, so this was a source defect rather than a later code change.

The source now declares counter/LED state and uses on_clock() as a void clocked update. The bit-23 LED is computed from the next count before the host counter changes, preserving both sequential Zig and nonblocking RTL behavior. The original bee helpers and commit metadata remain in this branch, which incorporates canonical master facfd819. One corrected NOW receipt includes a portable bench and truthful limits; no compiler/generated output/seal/failure ledger changed.

Verification: 4 Zig tests, 3/3 covered functions, zero discarded tokens/type errors/warnings; generated RTL compiles. A documented bench passes 547 observations (540 differential comparisons with pinned original Verilog plus 7 reset/hold checks). Three independently changed source copies compile but are rejected for LED lag, wrap loss and stuck counter. No new duplicate body/group.

The compiler adds reset/enable/ready and exposes a masked 32-bit counter. The original has undefined power-on state; differential cases seed both counters explicitly. No board, synthesis or timing validation is claimed. Full corpus verification completed:96primary failures versus95ledger; only existing xilinx7/packets.t27[parse] unexpected. This source introduces no new primary failure.

{
  "version": 1,
  "head_sha": "fec122de879865949ba8ddf88c0f38c257ecd74f",
  "summary": "Repair a reviewed LED D5 port whose host tests passed but generated RTL did not compile or expose the LED.",
  "changes": [
    "Keep the bee next-count and bit-23 helpers; declare actual state and a void clock entry that preserves host and nonblocking RTL ordering.",
    "Expose counter and LED output state through the documented reset/enable backend adapter; add a real clock-entry test.",
    "Retain original bee/publisher commit metadata and one truthful NOW receipt; no compiler, generated file, seal or ledger edits."
  ],
  "tests": [
    {
      "command": "t27c test-report / parse-complete / typecheck / coverage specs/port/trinity/fpga/openxc7-synth/led_d5_test.t27",
      "status": "passed",
      "result": "4 tests pass; zero discard and type errors/warnings; all 3 functions covered.",
      "evidence": "Source and the NOW receipt."
    },
    {
      "command": "iverilog -g2012 -s tb <generated RTL, pinned reference and documented bench>; vvp",
      "status": "passed",
      "result": "547 observations pass: 540 defined-state comparisons against original Verilog and 7 reset/hold observations.",
      "evidence": "Complete portable differential bench is in the NOW receipt."
    },
    {
      "command": "Generate and simulate source mutants: LED lag, missing 24-bit wrap, stuck counter",
      "status": "passed",
      "result": "All three mutants compile but the same RTL bench rejects each.",
      "evidence": "Local queen-ledd5-mutations.json/logs; defects and outcomes documented in the NOW receipt."
    },
    {
      "command": "python3 tools/dupe_scan.py; NOW shape; git diff --check",
      "status": "passed",
      "result": "590/4750 bodies in 169 groups: no new or enlarged duplicate group; one valid NOW entry; clean whitespace.",
      "evidence": "PR diff and reproducible repository tools."
    },
    {
      "command": "t27c suite --repo-root . --ratchet --corpus-only",
      "status": "failed",
      "result": "96 primary corpus failures versus95ledger: only xilinx7/packets.t27[parse] unexpected. No new discard, unexpected pass, gate drift or ledger expansion.",
      "evidence": "Full local led-d5-suite.json/log at this HEAD; spec absent from primary failures."
    }
  ],
  "limitations": [
    "No physical board, synthesis, bitstream or timing/inference validation.",
    "Original power-on count is uninitialized; comparisons explicitly seed both implementations. Reset/enable/ready plus the masked 32-bit counter port are the compiler adapter, not the original board pinout.",
    "Existing independent packets parse, conflicted type names and ring/spec drift remain visible; no failure ledger enlarged."
  ],
  "tags": [
    "Engineering",
    "Verification"
  ],
  "blog": {
    "title": "A passing host test can hide a disconnected hardware port",
    "summary": "Explicit clocked state restores a real LED port and makes generated RTL agree with the original counter in 547 observations.",
    "outline": [
      "The accepted port passed three host tests while generated RTL duplicated clk and exposed no LED.",
      "Declare real state, respect nonblocking clock semantics and exercise the generated module against the pinned original.",
      "Mutation checks distinguish LED lag, wrap loss and stuck counter; physical board validation remains."
    ]
  }
}

Trinity Bee and others added 3 commits October 3, 2026 23:22
Re-author the 30-line hand-written Verilog LED D5 test as
specs/port/trinity/fpga/openxc7-synth/led_d5_test.t27, so t27c gen-verilog
generates module trinity_top instead of the module being written by hand.

The original's decisions, carried as code:
- reg [23:0] blink_counter and its wrap at 2^24 (BLINK_COUNTER_BITS,
  BLINK_COUNT_MAX)
- always @(posedge clk) blink_counter <= blink_counter + 1'b1
  (next_count, lowered by the on_clock boundary to an always block)
- assign led = blink_counter[23] (led_value, LED_BIT)
- the 50 MHz QMTECH XC7A100T-1FGG676C clock note (CLK_HZ)

Three tests assert the increment, the 24-bit wrap and the LED following
bit 23; they run green under t27c test-report (3 pass, 0 FAIL, 0 BLOCKED).

Closes gHashTag#5846
A pull request must add exactly one docs/now entry and a bee has no way
to know that: its brief names a boundary file and acceptance criteria,
and docs/now/ is neither. The publisher adds it rather than failing the
gate.

Closes gHashTag#5846

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Preserve the bee source history while integrating current master. Verify four host tests and 547 RTL observations against original behavior.

Closes gHashTag#5846
@dmitrii-f-t27
dmitrii-f-t27 merged commit 11dd81e into gHashTag:master Oct 4, 2026
30 of 33 checks passed
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.

Port gHashTag/trinity:fpga/openxc7-synth/led_d5_test.v (Verilog, 1 module) to specs/port/trinity/fpga/openxc7-synth/led_d5_test.t27

2 participants