Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# NOW -- Port gHashTag/trinity:fpga/openxc7-synth/clock_test.v (Verilog, 1 module) to specs/port/trinity/fpga/openxc7-synth/clock_test.t27 (published 2026-10-03)

## A bee's work on #5819, published from `queen-5819` (Closes #5819)

- The branch changes 1 file(s): `specs/port/trinity/fpga/openxc7-synth/clock_test.t27`.
- `git diff --stat origin/master...queen-5819` reads: 1 file changed, 77 insertions(+)
- This entry is written by the publisher, not by the bee. 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.
- What this entry does NOT establish: that the work is correct. The gates on the
pull request judge that, and they are the same gates every other change meets.
77 changes: 77 additions & 0 deletions specs/port/trinity/fpga/openxc7-synth/clock_test.t27
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
// SPDX-License-Identifier: Apache-2.0
// t27/specs/port/trinity/fpga/openxc7-synth/clock_test.t27
// CLOCK TEST - Verify 50MHz oscillator is working
// Ported from gHashTag/trinity fpga/openxc7-synth/clock_test.v
// Direct connection: T23 LED tied to the clock, R23 LED tied to the inverted clock
// If the clock works, the LEDs show blur (~50MHz too fast to see)
// If an LED is solid, the clock is not working
// phi^2 + 1/phi^2 = 3 | TRINITY

module clock_test {

// === Module constants ===

// 50 MHz on U22
pub const CLK_MHZ : u32 = 50;

// === Output types ===

// The two LEDs the module drives: t23 follows the clock, r23 inverts it.
pub struct ClockOutputs {
t23 : bool,
r23 : bool,
}

// === Combinational surface ===

// The original's two assigns in one decision:
// assign t23 = clk;
// assign r23 = ~clk;
// The parameter becomes the `clk` input, the return the combinational result.
fn on_comb(clk: bool) -> ClockOutputs {
return ClockOutputs{ .t23 = clk, .r23 = !clk };
}

// === Output functions (the individual assigns) ===

// assign t23 = clk; // T23 LED - direct clock connection
fn t23_output(clk: bool) -> bool {
return clk;
}

// assign r23 = ~clk; // R23 LED - inverted clock
fn r23_output(clk: bool) -> bool {
return !clk;
}

// === Tests ===

// T23 LED follows the clock in both states.
test t23_follows_clk
given high = t23_output(true)
then high == true
and t23_output(false) == false

// R23 LED is the inverted clock in both states.
test r23_inverts_clk
given low = r23_output(false)
then low == true
and r23_output(true) == false

// The original's pair of assigns: the two LEDs never agree.
test outputs_complement
given quiet = on_comb(false)
then quiet.t23 == false
and quiet.r23 == true
and t23_output(true) == true
and r23_output(true) == false
and quiet.t23 != quiet.r23

// === Invariants ===

invariant clock_frequency_positive
given mhz = CLK_MHZ
assert mhz > 0
}

// phi^2 + 1/phi^2 = 3 | TRINITY
Loading