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
201 changes: 201 additions & 0 deletions bootstrap/src/bitnet_irq.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,201 @@
//! BitNet HLS interrupt-controller emitter (Wave 36f, R-BN-6).
//!
//! Exposes a single emitter:
//!
//! * `interrupt_controller` -- async completion signalling for the
//! host CPU. Three interrupt sources (inference_done, dma_done,
//! error) latch into a 3-bit sticky `irq_status` register. The
//! final `irq_out` is the logical OR of `irq_status & irq_enable`.
//! `status_read` clears the latch (read-to-clear semantics) so the
//! host can acknowledge the IRQ from inside the ISR.
//!
//! Port summary:
//!
//! | Group | Signals |
//! |--------------------|---------------------------------------------|
//! | Clock / reset | clk, rst_n |
//! | Interrupt sources | inference_done, dma_done, error |
//! | Mask | irq_enable[2:0] |
//! | Status (RW1C-ish) | irq_status[2:0], status_read |
//! | Output | irq_out |
//!
//! Algorithm ported from `gHashTag/vibee-lang`
//! `src/vibeec/verilog_codegen.zig` lines 1550-1590
//! (`writeInterruptController`). Original author: Dmitrii Vasilev.
//!
//! Constitutional notes:
//! L2: lives only under `bootstrap/`; emitter is a pure additive
//! string builder; no edits under `gen/`, `coq/`, `trios-coq/`,
//! `proofs/`, `specs/`, `conformance/`, `architecture/`,
//! `rings/`, or root `Cargo.toml`.
//! L3: ASCII source, English doc-comments only.
//! L5: numeric kernel untouched -- this emitter is a control-plane
//! signal aggregator; it does not redefine any constant inside
//! the trinity invariant `phi^2 + 1/phi^2 = 3`.
//! L7: no `*.sh` invoked.

/// Default identifier for the interrupt-controller module.
pub const DEFAULT_INTERRUPT_CONTROLLER_NAME: &str = "interrupt_controller";

fn is_valid_verilog_ident(s: &str) -> bool {
let mut chars = s.chars();
let first = match chars.next() {
Some(c) => c,
None => return false,
};
if !(first.is_ascii_alphabetic() || first == '_') {
return false;
}
chars.all(|c| c.is_ascii_alphanumeric() || c == '_')
}

fn resolve_ident<'a>(candidate: &'a str, default: &'a str) -> &'a str {
if is_valid_verilog_ident(candidate) {
candidate
} else {
default
}
}

/// Build the `interrupt_controller` SystemVerilog module text.
///
/// Parameters:
/// * `module_name` -- Verilog identifier; falls back to
/// `interrupt_controller` if the candidate is not a valid Verilog
/// identifier (must start with `[A-Za-z_]` and contain only
/// `[A-Za-z0-9_]`).
pub fn build_interrupt_controller(module_name: &str) -> String {
let name = resolve_ident(module_name, DEFAULT_INTERRUPT_CONTROLLER_NAME);
let mut s = String::new();

s.push_str("// ===========================================================================\n");
s.push_str("// INTERRUPT CONTROLLER - Async completion signaling\n");
s.push_str("// ===========================================================================\n");
s.push_str("// Generated by t27c gen-interrupt-controller (Wave 36f, R-BN-6).\n");
s.push_str("// Three sticky IRQ sources (inference_done, dma_done, error)\n");
s.push_str("// gated by a 3-bit irq_enable mask. status_read clears latches.\n");
s.push_str("\n");

s.push_str(&format!("module {} (\n", name));
s.push_str(" input wire clk,\n");
s.push_str(" input wire rst_n,\n");
s.push_str(" // Interrupt sources\n");
s.push_str(" input wire inference_done,\n");
s.push_str(" input wire dma_done,\n");
s.push_str(" input wire error,\n");
s.push_str(" // Interrupt enable\n");
s.push_str(" input wire [2:0] irq_enable,\n");
s.push_str(" // Status (active-high, clear on read)\n");
s.push_str(" output reg [2:0] irq_status,\n");
s.push_str(" input wire status_read,\n");
s.push_str(" // Interrupt output\n");
s.push_str(" output wire irq_out\n");
s.push_str(");\n");
s.push_str("\n");

s.push_str(" // Capture interrupt events\n");
s.push_str(" always @(posedge clk or negedge rst_n) begin\n");
s.push_str(" if (!rst_n) irq_status <= 3'b000;\n");
s.push_str(" else begin\n");
s.push_str(" if (inference_done) irq_status[0] <= 1'b1;\n");
s.push_str(" if (dma_done) irq_status[1] <= 1'b1;\n");
s.push_str(" if (error) irq_status[2] <= 1'b1;\n");
s.push_str(" if (status_read) irq_status <= 3'b000; // Clear on read\n");
s.push_str(" end\n");
s.push_str(" end\n");
s.push_str("\n");

s.push_str(" // Generate interrupt if any enabled source is active\n");
s.push_str(" assign irq_out = |(irq_status & irq_enable);\n");
s.push_str("\n");

s.push_str("endmodule\n");

s
}

#[cfg(test)]
mod tests {
use super::*;

#[test]
fn ident_validator_basics() {
assert!(is_valid_verilog_ident("interrupt_controller"));
assert!(is_valid_verilog_ident("a"));
assert!(is_valid_verilog_ident("_x"));
assert!(is_valid_verilog_ident("Foo123"));
assert!(!is_valid_verilog_ident(""));
assert!(!is_valid_verilog_ident("9foo"));
assert!(!is_valid_verilog_ident("has space"));
assert!(!is_valid_verilog_ident("dash-name"));
assert!(!is_valid_verilog_ident("uni\u{00e9}"));
}

#[test]
fn default_name_used_when_invalid() {
let v = build_interrupt_controller("");
assert!(v.contains("module interrupt_controller ("));
let v2 = build_interrupt_controller("9bad");
assert!(v2.contains("module interrupt_controller ("));
}

#[test]
fn custom_name_propagates() {
let v = build_interrupt_controller("irq_ctrl");
assert!(v.contains("module irq_ctrl ("));
assert!(!v.contains("module interrupt_controller ("));
}

#[test]
fn all_three_irq_sources_present() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.contains("input wire inference_done,"));
assert!(v.contains("input wire dma_done,"));
assert!(v.contains("input wire error,"));
}

#[test]
fn three_bit_enable_and_status() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.contains("input wire [2:0] irq_enable,"));
assert!(v.contains("output reg [2:0] irq_status,"));
}

#[test]
fn each_source_latches_its_bit() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.contains("if (inference_done) irq_status[0] <= 1'b1;"));
assert!(v.contains("if (dma_done) irq_status[1] <= 1'b1;"));
assert!(v.contains("if (error) irq_status[2] <= 1'b1;"));
}

#[test]
fn status_read_clears_latch() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.contains("if (status_read) irq_status <= 3'b000;"));
}

#[test]
fn reset_zeroes_status() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.contains("if (!rst_n) irq_status <= 3'b000;"));
}

#[test]
fn irq_out_is_or_of_masked_status() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.contains("assign irq_out = |(irq_status & irq_enable);"));
}

#[test]
fn module_ends_with_endmodule() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.trim_end().ends_with("endmodule"));
}

#[test]
fn emitted_text_is_pure_ascii() {
let v = build_interrupt_controller(DEFAULT_INTERRUPT_CONTROLLER_NAME);
assert!(v.is_ascii(), "emitted Verilog must be ASCII");
}
}
Loading
Loading