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

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.

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);
+    }
+}