diff --git a/docs/now/2026-10-03-published-port-ghashtag-trinity-fpga-openxc7-synth-clock-test-v-verilo.md b/docs/now/2026-10-03-published-port-ghashtag-trinity-fpga-openxc7-synth-clock-test-v-verilo.md new file mode 100644 index 0000000000..4a3830ded9 --- /dev/null +++ b/docs/now/2026-10-03-published-port-ghashtag-trinity-fpga-openxc7-synth-clock-test-v-verilo.md @@ -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. diff --git a/specs/port/trinity/fpga/openxc7-synth/clock_test.t27 b/specs/port/trinity/fpga/openxc7-synth/clock_test.t27 new file mode 100644 index 0000000000..94e0c231a5 --- /dev/null +++ b/specs/port/trinity/fpga/openxc7-synth/clock_test.t27 @@ -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