diff --git a/docs/now/2026-10-04-published-port-ghashtag-trinity-fpga-openxc7-synth-d-oscillator-v-veri.md b/docs/now/2026-10-04-published-port-ghashtag-trinity-fpga-openxc7-synth-d-oscillator-v-veri.md new file mode 100644 index 0000000000..f4904d8236 --- /dev/null +++ b/docs/now/2026-10-04-published-port-ghashtag-trinity-fpga-openxc7-synth-d-oscillator-v-veri.md @@ -0,0 +1,11 @@ +# NOW -- Port gHashTag/trinity:fpga/openxc7-synth/d_oscillator.v (Verilog, 1 module) to specs/port/trinity/fpga/openxc7-synth/d_oscillator.t27 (published 2026-10-04) + +## A bee's work on #5877, published from `queen-5877` (Closes #5877) + +- The branch changes 1 file(s): `specs/port/trinity/fpga/openxc7-synth/d_oscillator.t27`. +- `git diff --stat origin/master...queen-5877` reads: 1 file changed, 231 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/d_oscillator.t27 b/specs/port/trinity/fpga/openxc7-synth/d_oscillator.t27 new file mode 100644 index 0000000000..c0731822a9 --- /dev/null +++ b/specs/port/trinity/fpga/openxc7-synth/d_oscillator.t27 @@ -0,0 +1,231 @@ +// SPDX-License-Identifier: Apache-2.0 +// t27/specs/port/trinity/fpga/openxc7-synth/d_oscillator.t27 +// +// Ported from gHashTag/trinity `fpga/openxc7-synth/d_oscillator.v` +// (hand-written Verilog, 31 lines, 1 module: `trinity_top`). +// +// What the original computes: `trinity_top` drives one LED from a 4-bit LUT +// cascade (`slow_chain`). It is meant to run off the STARTUPE2 internal +// configuration clock; the `clk` input is declared but never read +// ("Not used!"). The cascade is purely combinational: +// +// assign next_chain[0] = ~slow_chain[0]; +// assign next_chain[1] = slow_chain[0] ^ slow_chain[1]; +// assign next_chain[2] = slow_chain[1] ^ slow_chain[2]; +// assign next_chain[3] = slow_chain[2] ^ slow_chain[3]; +// assign led = next_chain[0]; +// +// so `led` is simply the inverse of `slow_chain[0]`, and each other cascade +// bit XORs two neighbouring chain bits. `t27c gen-verilog` lowers this spec +// back to a `module trinity_top`. +// +// Decisions kept as code: the 4-bit chain width, the 24-bit (unused) counter +// register, the XOR cascade, and `led = next_chain[0]`. + +module trinity_top { + + // reg [3:0] slow_chain -- four cascade bits; index 0 is the Verilog LSB. + pub const CHAIN_WIDTH : u32 = 4; + + // reg [23:0] counter = 24'd0 -- declared in the original but never used + // by its logic; the width is kept here for the record. + pub const COUNTER_WIDTH : u32 = 24; + + invariant chain_width_is_four { + assert(CHAIN_WIDTH == 4); + } + + invariant counter_width_is_24 { + assert(COUNTER_WIDTH == 24); + } + + // === Data moving in or out === + + pub struct Inputs { + clk : bool, // input wire clk; "Not used!" -- never read by the logic. + } + + pub struct Outputs { + led : bool, // output wire led; assign led = next_chain[0]; + } + + // === Internal state: the LUT cascade === + + pub struct OscillatorState { + slow_chain : [4]u32, + } + + // === Constructors === + + fn inputs(clk: bool) -> Inputs { + return Inputs{ .clk = clk }; + } + + fn outputs(led: bool) -> Outputs { + return Outputs{ .led = led }; + } + + // reg [3:0] slow_chain = 4'b0000; + fn oscillator_zero() -> OscillatorState { + return OscillatorState{ .slow_chain = [4]u32{0, 0, 0, 0} }; + } + + // === Single-bit helpers (the original's `~` and `^` on one-bit wires) === + + // ~bit + fn bit_not(a: u32) -> u32 { + if (a == 0) { + return 1; + } + return 0; + } + + // bit ^ bit + fn bit_xor(a: u32, b: u32) -> u32 { + if (a != b) { + return 1; + } + return 0; + } + + // === The decision: the combinational cascade === + + // The four `assign next_chain[i] = ...` lines, selected by bit index. + fn next_chain_bit(state: OscillatorState, i: u32) -> u32 { + if (i == 0) { + return bit_not(state.slow_chain[0]); + } + if (i == 1) { + return bit_xor(state.slow_chain[0], state.slow_chain[1]); + } + if (i == 2) { + return bit_xor(state.slow_chain[1], state.slow_chain[2]); + } + if (i == 3) { + return bit_xor(state.slow_chain[2], state.slow_chain[3]); + } + return 0; // i >= CHAIN_WIDTH: outside the 4-bit chain. + } + + // wire [3:0] next_chain; -- the whole cascade vector. + fn next_chain(state: OscillatorState) -> [4]u32 { + var out : [4]u32 = [0, 0, 0, 0]; + var i : u32 = 0; + while (i < CHAIN_WIDTH) { + out[i] = next_chain_bit(state, i); + i = i + 1; + } + return out; + } + + // assign led = next_chain[0]; -- the module's only output. + fn on_comb(state: OscillatorState) -> bool { + return next_chain_bit(state, 0) == 1; + } + + // === Tests: values the original produces for inputs chosen here === + + test bit_not_truth_table { + // assign next_chain[0] = ~slow_chain[0]; + assert(bit_not(0) == 1); + assert(bit_not(1) == 0); + } + + test bit_xor_truth_table { + // assign next_chain[1] = slow_chain[0] ^ slow_chain[1]; (and friends) + assert(bit_xor(0, 0) == 0); + assert(bit_xor(0, 1) == 1); + assert(bit_xor(1, 0) == 1); + assert(bit_xor(1, 1) == 0); + } + + test zero_chain_led_on { + // slow_chain = 4'b0000 -> next_chain[0] = ~0 = 1 -> led is on. + const state = oscillator_zero(); + assert(on_comb(state)); + const nc = next_chain(state); + assert(nc[0] == 1); + assert(nc[1] == 0); + assert(nc[2] == 0); + assert(nc[3] == 0); + } + + test one_chain_led_off { + // slow_chain = 4'b0001 -> next_chain[0] = ~1 = 0 -> led is off, + // and next_chain[1] = 1 ^ 0 = 1. + const state = OscillatorState{ .slow_chain = [4]u32{1, 0, 0, 0} }; + assert(!on_comb(state)); + const nc = next_chain(state); + assert(nc[0] == 0); + assert(nc[1] == 1); + assert(nc[2] == 0); + assert(nc[3] == 0); + } + + test cascade_vector_0101 { + // slow_chain = 4'b0101 -> next_chain = 4'b1110 -> led is off. + const state = OscillatorState{ .slow_chain = [4]u32{1, 0, 1, 0} }; + const nc = next_chain(state); + assert(nc[0] == 0); + assert(nc[1] == 1); + assert(nc[2] == 1); + assert(nc[3] == 1); + assert(!on_comb(state)); + } + + test cascade_vector_1010 { + // slow_chain = 4'b1010 -> next_chain = 4'b1111 -> led is on. + const state = OscillatorState{ .slow_chain = [4]u32{0, 1, 0, 1} }; + const nc = next_chain(state); + assert(nc[0] == 1); + assert(nc[1] == 1); + assert(nc[2] == 1); + assert(nc[3] == 1); + assert(on_comb(state)); + } + + test cascade_all_ones_collapses_to_zero { + // slow_chain = 4'b1111 -> every XOR pair cancels -> next_chain = 0. + const state = OscillatorState{ .slow_chain = [4]u32{1, 1, 1, 1} }; + const nc = next_chain(state); + assert(nc[0] == 0); + assert(nc[1] == 0); + assert(nc[2] == 0); + assert(nc[3] == 0); + assert(!on_comb(state)); + } + + test next_chain_bit_by_index { + // slow_chain = 4'b0011 -> next[0] = ~1 = 0, next[1] = 1 ^ 1 = 0, + // next[2] = 1 ^ 0 = 1, next[3] = 0 ^ 0 = 0; i = 4 is outside the chain. + const state = OscillatorState{ .slow_chain = [4]u32{1, 1, 0, 0} }; + assert(next_chain_bit(state, 0) == 0); + assert(next_chain_bit(state, 1) == 0); + assert(next_chain_bit(state, 2) == 1); + assert(next_chain_bit(state, 3) == 0); + assert(next_chain_bit(state, 4) == 0); + } + + test led_follows_inverted_bit0 { + // assign led = next_chain[0] = ~slow_chain[0]: bits 1..3 never + // reach the LED. Two chains with the same bit 0 give the same led. + const hi0_a = OscillatorState{ .slow_chain = [4]u32{1, 0, 0, 0} }; + const hi0_b = OscillatorState{ .slow_chain = [4]u32{1, 1, 1, 1} }; + assert(!on_comb(hi0_a)); + assert(!on_comb(hi0_b)); + const lo0_a = oscillator_zero(); + const lo0_b = OscillatorState{ .slow_chain = [4]u32{0, 1, 1, 1} }; + assert(on_comb(lo0_a)); + assert(on_comb(lo0_b)); + } + + test io_structs_carry_the_interface { + // input wire clk is declared but "Not used!"; output wire led + // carries the value the cascade computes for slow_chain = 4'b0000. + const io = inputs(false); + assert(!io.clk); + const state = oscillator_zero(); + const out = outputs(on_comb(state)); + assert(out.led); + } +}