Skip to content

Port fpga/vivado/uart_detect_top.v (Verilog, 1 module) to specs/port/fpga/vivado/uart_detect_top.t27 - #6534

Merged
gHashTag merged 1 commit into
masterfrom
claude/bee-4969
Oct 5, 2026
Merged

gHashTag merged 1 commit into
masterfrom
claude/bee-4969

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 5, 2026

Copy link
Copy Markdown
Owner

Closes #4969

Ports fpga/vivado/uart_detect_top.v (46 lines, 1 module) to specs/port/fpga/vivado/uart_detect_top.t27 as module uart_detect_top { ... }. One file, .t27 only.

What the original computes, and where it is in the spec

Verilog .t27
LUT1 #(.INIT(2'b01)): O = INIT[I0], which is an inverter lut1(init, i0)
chain[0] = ~chain[19], chain[i] = LUT1(chain[i-1]) ring_step(chain)
counter <= counter + 1 (23 bits) counter_next
rx_sync <= rx; rx_prev <= rx_sync; if (rx_prev && !rx_sync) pulse_count++ falling_edge, pulse_next, clock_edge (non-blocking: every RHS reads the old state)
led_r23 = ~counter[20], led_t23 = pulse_count > 0 ? ~counter[19] : 1, uart_tx_pin = 1 led_r23, led_t23, uart_tx_pin, outputs
module ports for gen-verilog on_comb(counter, pulse_count) -> u8, which packs the three output pins

An honest note in the header comment: the ring has 20 inversions, an even number. In zero-delay logic the alternating pattern is therefore a fixed point (test ring_has_a_fixed_point_in_zero_delay_logic). Whether the placed ring oscillates depends on routing delay, which this model does not carry. pulse_count has no initialiser in the original, so the spec starts it at 0, the FPGA's GSR value.

Cross-checked against the original

I simulated the original .v under iverilog with a behavioural LUT1 and a forced osc. It gives the same values the spec's tests assert:

  • for rx = 1,1,0,0,0,1,1: pulse_count is 0, 0, 1 after 2, 3 and 4 edges, and 1 after 7 edges, with counter 7 and led_t23 1;
  • for rx = 1,0,0,1,1,0,0,1: pulse_count is 2.

I also simulated the generated Verilog's result port for (counter, pulse_count) = (0,0), (0x100000,0), (0x080000,0), (0x080000,1) and (0x180000,2). It gives 7 5 7 3 1, the same as test on_comb_packs_the_same_pins_as_outputs, and iverilog -g2012 accepts the generated file.

Acceptance criteria

These were run on the Railway t27c lab, with t27c built from origin/master e7afb32.

$ test -f specs/port/fpga/vivado/uart_detect_top.t27 && echo present
present
$ grep -cE '^\s*(pub )?module uart_detect_top\b' specs/port/fpga/vivado/uart_detect_top.t27
1
$ t27c gen-verilog specs/port/fpga/vivado/uart_detect_top.t27 | grep -cE '^module uart_detect_top ?\('
1
$ t27c spec-status specs/port/fpga/vivado/uart_detect_top.t27
IMPLEMENTED
$ grep -cE '^[[:space:]]*test[[:space:]]+("|[A-Za-z_])' specs/port/fpga/vivado/uart_detect_top.t27
11
$ t27c test-report specs/port/fpga/vivado/uart_detect_top.t27 2>&1 | grep -c BLOCKED
0
$ t27c test-report specs/port/fpga/vivado/uart_detect_top.t27
  tests       11
  pass        11
  FAIL        0
  rate    100.0%
$ t27c typecheck specs/port/fpga/vivado/uart_detect_top.t27
Typecheck OK (0 errors, 0 warnings)

Negative control. I flipped three expectations (the pulse count after 4 edges, the LUT1 inverter output, and one on_comb value). test-report then printed pass 8, FAIL 3, naming those three tests.

Two t27c defects I worked around (details on #4969)

  1. In a brace-form test body, the first x = f(x); after var x : T = ...; is emitted to Zig as var x = f(x);, which is a redeclaration and BLOCKs the build. Function bodies are unaffected. Workaround: the edge sequence is driven by run_edges (a fn).
  2. gen-verilog lowers fn osc(chain: [20]bool) -> bool { return chain[19]; } with no input and a body of osc = c2[19];, a name taken from the test call site, and iverilog rejects it. Workaround: osc = chain[19] is read inline.

🤖 Generated with Claude Code

…art_detect_top.t27

module uart_detect_top: the LUT1 (INIT 2'b01, an inverter) ring step,
the 23-bit counter, the two-flop RX synchroniser with falling-edge
pulse count, the three output assigns, and an on_comb surface that
gen-verilog lowers to a module of the same name. Edge sequences were
cross-checked against the original under iverilog.

Closes #4969

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-05 16:18:18 UTC

Summary

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

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

Seal Status

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

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 fpga/vivado/uart_detect_top.v (Verilog, 1 module) to specs/port/fpga/vivado/uart_detect_top.t27

1 participant