logicaffeine_compile/codegen_sva/
chan_rtl.rs

1//! chan_rtl — the deterministic channel in silicon: a bounded FIFO.
2//!
3//! The language's `Pipe` is a FIFO, bounded, move-semantics channel
4//! (`logicaffeine_runtime::channel::Chan`): values leave in the order they entered, a full
5//! buffer refuses a sender (`has_room = len < capacity`), an empty buffer refuses a
6//! receiver. This module emits that exact discipline as a synthesizable sync FIFO and proves,
7//! under iverilog, that replaying an arbitrary send/recv trace produces the same pop sequence
8//! as the software channel's bounded `VecDeque` — the channel's determinism, in hardware.
9//!
10//! It is *one channel's* buffer. The multi-node routing/rendezvous (who is connected to whom,
11//! select, blocking hand-off across cores) stays the scheduler/message-passing layer — a
12//! projection, not this block.
13
14const DEPTH: usize = 8;
15
16/// Emit the bounded sync FIFO: combinational front-read (`dout`), combinational `full`/`empty`/
17/// handshake, registered pointers + count. `pushed = push & !full`, `popped = pop & !empty`.
18pub fn emit_chan_fifo_verilog() -> String {
19    r#"// chan_fifo — the language Pipe (bounded FIFO channel) in silicon.
20// FIFO order, bounded (full refuses a sender, empty refuses a receiver) — the discipline of
21// logicaffeine_runtime::channel::Chan. Proven ≡ the software channel by chan_fifo_matches_the_runtime_channel.
22// DEPTH = 8, WIDTH = 32.
23module chan_fifo(
24  input             clk,
25  input             rst,
26  input             push,
27  input  [31:0]     din,
28  input             pop,
29  output [31:0]     dout,     // combinational: the oldest buffered value (FIFO front)
30  output            pushed,   // this cycle's push was accepted (buffer had room)
31  output            popped,   // this cycle's pop was accepted (buffer was non-empty)
32  output            empty,
33  output            full,
34  output [3:0]      count
35);
36  reg [31:0] mem [0:7];
37  reg [3:0]  cnt;             // 0..8
38  reg [2:0]  head, tail;      // wrap mod 8
39  assign empty  = (cnt == 4'd0);
40  assign full   = (cnt == 4'd8);
41  assign popped = pop  && !empty;
42  assign pushed = push && !full;
43  assign dout   = mem[head];
44  assign count  = cnt;
45  always @(posedge clk) begin
46    if (rst) begin
47      cnt <= 4'd0; head <= 3'd0; tail <= 3'd0;
48    end else begin
49      if (popped) head <= head + 3'd1;
50      if (pushed) begin mem[tail] <= din; tail <= tail + 3'd1; end
51      cnt <= cnt - (popped ? 4'd1 : 4'd0) + (pushed ? 4'd1 : 4'd0);
52    end
53  end
54endmodule
55"#
56    .to_string()
57}
58
59/// A self-checking testbench: replay an N-step (push, pop, din) trace and compare the DUT's
60/// pop sequence against the software channel oracle from `chan_{ctrl,din,pops}.hex`.
61pub fn emit_chan_fifo_testbench(n: usize, npops: usize, final_count: usize) -> String {
62    format!(
63        r#"// tb_chan_fifo — HW bounded FIFO vs the software channel (VecDeque) oracle.
64`timescale 1ns/1ps
65module tb_chan_fifo;
66  localparam N = {n};
67  localparam M = {npops};
68  reg clk = 0; always #5 clk = ~clk;
69  reg rst = 1, push = 0, pop = 0;
70  reg [31:0] din;
71  reg [7:0]  ctrl [0:{clast}];
72  reg [31:0] dvec [0:{clast}];
73  reg [31:0] pops [0:{plast}];
74  wire [31:0] dout; wire pushed, popped, empty, full; wire [3:0] count;
75  integer i, k, errors;
76  chan_fifo dut(.clk(clk), .rst(rst), .push(push), .din(din), .pop(pop),
77                .dout(dout), .pushed(pushed), .popped(popped),
78                .empty(empty), .full(full), .count(count));
79  initial begin
80    errors = 0; k = 0;
81    $readmemh("chan_ctrl.hex", ctrl);
82    $readmemh("chan_din.hex", dvec);
83    $readmemh("chan_pops.hex", pops);
84    repeat (3) @(posedge clk); #1 rst = 0;
85    for (i = 0; i < N; i = i + 1) begin
86      push = ctrl[i][0]; pop = ctrl[i][1]; din = dvec[i]; #1;   // settle combinational
87      if (popped) begin
88        if (k >= M || dout !== pops[k]) begin errors = errors + 1; $display("FAIL pop %0d", k); end
89        k = k + 1;
90      end
91      @(posedge clk); #1;                                       // advance FIFO state
92    end
93    push = 0; pop = 0; #1;
94    if (k !== M) begin errors = errors + 1; $display("FAIL: %0d pops, expected %0d", k, M); end
95    if (count !== {final_count}) begin errors = errors + 1; $display("FAIL final count %0d != {final_count}", count); end
96    if (errors == 0) $display("PASS: {n}-step FIFO trace matches the software channel oracle (%0d pops)", k);
97    else $display("FAIL: %0d FIFO mismatches", errors);
98    $finish;
99  end
100endmodule
101"#,
102        n = n,
103        npops = npops,
104        final_count = final_count,
105        clast = n - 1,
106        plast = if npops == 0 { 0 } else { npops - 1 },
107    )
108}
109
110/// Reproducible (push, pop, din) trace + the software-channel oracle (bounded VecDeque, FIFO)
111/// popped-value sequence. Returns (ctrl.hex, din.hex, pops.hex, npops, final_count).
112fn chan_trace(n: usize) -> (String, String, String, usize, usize) {
113    use std::collections::VecDeque;
114    let mut st: u64 = 0x00F1_F0D0_0DBA_5E12;
115    let mut next = || {
116        st = st
117            .wrapping_mul(6364136223846793005)
118            .wrapping_add(1442695040888963407);
119        st >> 32
120    };
121    let (mut ctrl, mut din, mut pops) = (String::new(), String::new(), String::new());
122    let mut q: VecDeque<u32> = VecDeque::new();
123    let mut npops = 0usize;
124    for _ in 0..n {
125        let r = next();
126        // Bias toward keeping the buffer busy: push ~62%, pop ~62% (both can fire).
127        let push = (r % 8) < 5;
128        let pop = ((r >> 3) % 8) < 5;
129        let d = next() as u32;
130        ctrl.push_str(&format!("{:02x}\n", (push as u8) | ((pop as u8) << 1)));
131        din.push_str(&format!("{:08x}\n", d));
132        let do_pop = pop && !q.is_empty();
133        let do_push = push && q.len() < DEPTH;
134        if do_pop {
135            pops.push_str(&format!("{:08x}\n", *q.front().unwrap()));
136            q.pop_front();
137            npops += 1;
138        }
139        if do_push {
140            q.push_back(d);
141        }
142    }
143    (ctrl, din, pops, npops, q.len())
144}
145
146#[cfg(test)]
147#[path = "../../../logicaffeine_tests/unit/logicaffeine_compile/codegen_sva/chan_rtl/tests.rs"]
148mod tests;
logicaffeine_compile/codegen_sva/chan_rtl.rs

logicaffeine_compile/codegen_sva/
chan_rtl.rs
