From 1ce3d05dd550d1ef64d446bcd43d1841640728b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:32:23 +0700 Subject: [PATCH 1/4] t27o: csr_map.rs tests without windows(2) and is_power_of_two, so tri t27o converts all 10 fns (Closes #11235) Step (a) of the second golden port. csr_offsets_strictly_increasing and csr_offsets_step_is_four loop over CSR_OFFSETS by index; status_masks_are_powers_of_two uses x != 0 && (x & (x - 1)) == 0. The meaning of each test is unchanged: cargo test host::csr_map ends with 10 passed, 0 failed. Co-Authored-By: Claude Sonnet 5.5 --- bootstrap/src/host/csr_map.rs | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/bootstrap/src/host/csr_map.rs b/bootstrap/src/host/csr_map.rs index 981ea6c152..b523479758 100644 --- a/bootstrap/src/host/csr_map.rs +++ b/bootstrap/src/host/csr_map.rs @@ -154,15 +154,19 @@ mod tests { #[test] fn csr_offsets_strictly_increasing() { - for w in CSR_OFFSETS.windows(2) { - assert!(w[0] < w[1], "CSR offsets not strictly increasing"); + let mut i = 1; + while i < CSR_COUNT { + assert!(CSR_OFFSETS[i - 1] < CSR_OFFSETS[i], "CSR offsets not strictly increasing"); + i += 1; } } #[test] fn csr_offsets_step_is_four() { - for w in CSR_OFFSETS.windows(2) { - assert_eq!(w[1] - w[0], 4, "CSR offsets not contiguous by 4"); + let mut i = 1; + while i < CSR_COUNT { + assert_eq!(CSR_OFFSETS[i] - CSR_OFFSETS[i - 1], 4, "CSR offsets not contiguous by 4"); + i += 1; } } @@ -192,9 +196,9 @@ mod tests { #[test] fn status_masks_are_powers_of_two() { - assert!(STATUS_BUSY_MASK.is_power_of_two()); - assert!(STATUS_DONE_MASK.is_power_of_two()); - assert!(STATUS_ERROR_MASK.is_power_of_two()); + assert!(STATUS_BUSY_MASK != 0 && (STATUS_BUSY_MASK & (STATUS_BUSY_MASK - 1)) == 0); + assert!(STATUS_DONE_MASK != 0 && (STATUS_DONE_MASK & (STATUS_DONE_MASK - 1)) == 0); + assert!(STATUS_ERROR_MASK != 0 && (STATUS_ERROR_MASK & (STATUS_ERROR_MASK - 1)) == 0); } #[test] From 9123a6b7aa3262d48834b6fc43c32e9f897a311e Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:34:10 +0700 Subject: [PATCH 2/4] t27o: specs/host/csr_map.t27, converted by tri t27o from csr_map.rs and reviewed (Closes #11235) Step (c) of the second golden port. The spec is the 30 pub consts of the hand file and its 10 tests as test blocks (10 of 10 fns converted), plus one negative control and three oracle tests that pin every offset, bit position and mask. t27b test: 14 passed, 0 failed. No spec in specs/ defines a const of these names or mirrors this map. Co-Authored-By: Claude Sonnet 5.5 --- specs/host/csr_map.t27 | 271 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 271 insertions(+) create mode 100644 specs/host/csr_map.t27 diff --git a/specs/host/csr_map.t27 b/specs/host/csr_map.t27 new file mode 100644 index 0000000000..1ee110ebbe --- /dev/null +++ b/specs/host/csr_map.t27 @@ -0,0 +1,271 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/host/csr_map.t27 -- the BitNet AXI-Lite CSR address map of the host driver: the byte offset of every +; register, the bit positions and masks of CTRL, STATUS and the IRQ registers, and the table of the twelve +; offsets in slave decode order (Closes #11235, the second golden port of step 4 of #9000). +; -- +; This spec replaces the hand-written bootstrap/src/host/csr_map.rs (214 lines, 71 of them #[cfg(test)]). +; The file was converted by `tri t27o` (rules: specs/tools/t27o/rust_convert.t27) after three of its tests were +; rewritten with index loops and a bit test (windows(2) and is_power_of_two are not in the subset), and it was +; read by eye. Its 10 Rust #[test]s are the 10 `test` blocks below that carry their names. `t27c gen-rust` +; lowers this spec to bootstrap/gen/rust/host/csr_map.rs, which bootstrap/src/host/mod.rs mounts by #[path] +; as module `csr_map`; bootstrap/src/host/driver.rs and dma.rs say `use super::csr_map` and are unchanged. +; Never hand-edit the generated copy. +; -- +; What the register map mirrors: the register decode of the Wave 36d emitter, bootstrap/src/bitnet_axi.rs. +; All offsets are byte addresses; the underlying slave decodes s_axi_awaddr[5:2] (word-aligned, step 4). +; -- +; 0x00 CTRL RW [0] = start pulse +; 0x04 STATUS RO [0] busy, [1] done, [2] error +; 0x08 IRQ_EN RW [0] inference_done, [1] dma_done, [2] error +; 0x0C IRQ_STAT RO sticky latch, READ-TO-CLEAR via the upstream `status_read` pulse (W57); +; the AXI slave has no write case for this offset, so writes are dropped +; 0x10 NUM_LAYERS RW layer count +; 0x14 NEURONS RW neurons per layer +; 0x18 CHUNKS RW chunks per neuron +; 0x1C THRESHOLD RW signed threshold (16-bit, zero-extended) +; 0x20 WEIGHT_ADDR_LO RW DDR base address, low 32 bits +; 0x24 WEIGHT_ADDR_HI RW DDR base address, high 32 bits +; 0x28 DMA_CTRL RW DMA control (Wave 39, the driver's dma.rs) +; 0x2C DMA_STAT RW DMA status +; -- +; Unmapped reads return 0xDEADBEEF (per the W36d emitter). All transactions are 32-bit aligned; the slave only +; honours word accesses. The bit positions of STATUS follow the W36d / W36f / W36e wiring, those of the IRQ +; registers the W36f `interrupt_controller`. +; -- +; Rules, each pinned by a test below: +; R1 (word aligned). Every offset of CSR_OFFSETS is a multiple of 4, they increase strictly, and each is 4 above +; the one before; so the table is 0x00, 0x04, .. 0x2C and CSR_COUNT is 12. +; R2 (masks). Every mask is 1 shifted left by its bit position; the three STATUS masks are single bits and +; IRQ_ALL_MASK is the union of the three IRQ masks, three bits set. +; R3 (the table). CSR_OFFSETS lists the named offsets in slave decode order. +; -- +; What the lowering changes, stated here so that nobody reads it as a surprise: the `///` doc comments of the +; hand file stay in this spec and do not reach the generated Rust; 0xDEAD_BEEF is written 0xDEADBEEF (the same +; value); the type [u32; CSR_COUNT] is written [u32; CSR_COUNT as usize] (the same type, [u32; 12]); the ten +; tests are no longer `cargo test` tests of the t27c binary but `test` blocks run by t27b and t27c test-report. +; All 30 `pub const`s keep their names, types and values; a side-by-side run of the old and the new file +; compares every one of them (see the pull request). +; -- +; The test named `negative_control_..` plants two faults: a table with a pair of offsets swapped, which the +; ordering test would refuse, and masks that overlap, which the single-bit test would refuse. The `oracle_*` +; tests are the values the hand file held when it was compiled with rustc and printed; they are kept so that +; the value of every register offset, bit position and mask of the deleted file stays on record. +; ASCII only (L3) +; phi^2 + 1/phi^2 = 3 | TRINITY + +module HostCsrMap; + +use tools::t27o::rust_std; + +/// Byte offset of the control register. +pub const CTRL : u32 = 0x00; + +/// Byte offset of the status register. +pub const STATUS : u32 = 0x04; + +/// Byte offset of the IRQ-enable register. +pub const IRQ_EN : u32 = 0x08; + +/// Byte offset of the IRQ-status (sticky latch) register. +pub const IRQ_STAT : u32 = 0x0C; + +/// Byte offset of the layer-count register. +pub const NUM_LAYERS : u32 = 0x10; + +/// Byte offset of the neurons-per-layer register. +pub const NEURONS : u32 = 0x14; + +/// Byte offset of the chunks-per-neuron register. +pub const CHUNKS : u32 = 0x18; + +/// Byte offset of the signed-threshold register. +pub const THRESHOLD : u32 = 0x1C; + +/// Byte offset of the weight-base-address low half. +pub const WEIGHT_ADDR_LO : u32 = 0x20; + +/// Byte offset of the weight-base-address high half. +pub const WEIGHT_ADDR_HI : u32 = 0x24; + +/// Byte offset of the DMA control register. +pub const DMA_CTRL : u32 = 0x28; + +/// Byte offset of the DMA status register. +pub const DMA_STAT : u32 = 0x2C; + +/// Sentinel value returned by the W36d slave on unmapped reads. +pub const UNMAPPED_READ_VALUE : u32 = 0xDEADBEEF; + +/// CTRL bit position for the engine-start pulse. +pub const CTRL_START_BIT : u32 = 0; + +/// CTRL mask for the engine-start pulse. +pub const CTRL_START_MASK : u32 = 1 << CTRL_START_BIT; + +/// STATUS bit position for `busy`. +pub const STATUS_BUSY_BIT : u32 = 0; + +/// STATUS bit position for `done`. +pub const STATUS_DONE_BIT : u32 = 1; + +/// STATUS bit position for `error`. +pub const STATUS_ERROR_BIT : u32 = 2; + +/// STATUS mask for `busy`. +pub const STATUS_BUSY_MASK : u32 = 1 << STATUS_BUSY_BIT; + +/// STATUS mask for `done`. +pub const STATUS_DONE_MASK : u32 = 1 << STATUS_DONE_BIT; + +/// STATUS mask for `error`. +pub const STATUS_ERROR_MASK : u32 = 1 << STATUS_ERROR_BIT; + +/// IRQ bit position for `inference_done`. +pub const IRQ_INFERENCE_DONE_BIT : u32 = 0; + +/// IRQ bit position for `dma_done`. +pub const IRQ_DMA_DONE_BIT : u32 = 1; + +/// IRQ bit position for `error`. +pub const IRQ_ERROR_BIT : u32 = 2; + +/// IRQ mask for `inference_done`. +pub const IRQ_INFERENCE_DONE_MASK : u32 = 1 << IRQ_INFERENCE_DONE_BIT; + +/// IRQ mask for `dma_done`. +pub const IRQ_DMA_DONE_MASK : u32 = 1 << IRQ_DMA_DONE_BIT; + +/// IRQ mask for `error`. +pub const IRQ_ERROR_MASK : u32 = 1 << IRQ_ERROR_BIT; + +/// Mask covering all three IRQ sources (`inference_done`, `dma_done`, `error`). +pub const IRQ_ALL_MASK : u32 = IRQ_INFERENCE_DONE_MASK | IRQ_DMA_DONE_MASK | IRQ_ERROR_MASK; + +/// Total number of mapped CSR registers (12). +pub const CSR_COUNT : usize = 12; + +/// Canonical CSR offsets, in slave decode order. +pub const CSR_OFFSETS : [CSR_COUNT]u32 = [CTRL, STATUS, IRQ_EN, IRQ_STAT, NUM_LAYERS, NEURONS, CHUNKS, THRESHOLD, WEIGHT_ADDR_LO, WEIGHT_ADDR_HI, DMA_CTRL, DMA_STAT]; + +test csr_offsets_are_word_aligned { + for off in CSR_OFFSETS { + assert(off % 4 == 0); + } +} + +test csr_offsets_strictly_increasing { + var i = 1; + while (i < CSR_COUNT) { + assert(CSR_OFFSETS[i - 1] < CSR_OFFSETS[i]); + i += 1; + } +} + +test csr_offsets_step_is_four { + var i = 1; + while (i < CSR_COUNT) { + assert(CSR_OFFSETS[i] - CSR_OFFSETS[i - 1] == 4); + i += 1; + } +} + +test csr_count_matches_emitter { + assert(CSR_COUNT == 12); + assert(CSR_OFFSETS.len == CSR_COUNT); +} + +test unmapped_read_value_matches_emitter { + assert(UNMAPPED_READ_VALUE == 0xDEADBEEF); +} + +test ctrl_start_bit_is_zero { + assert(CTRL_START_BIT == 0); + assert(CTRL_START_MASK == 0x1); +} + +test status_bits_distinct { + assert(STATUS_BUSY_BIT != STATUS_DONE_BIT); + assert(STATUS_DONE_BIT != STATUS_ERROR_BIT); + assert(STATUS_BUSY_BIT != STATUS_ERROR_BIT); +} + +test status_masks_are_powers_of_two { + assert(STATUS_BUSY_MASK != 0 and (STATUS_BUSY_MASK & (STATUS_BUSY_MASK - 1)) == 0); + assert(STATUS_DONE_MASK != 0 and (STATUS_DONE_MASK & (STATUS_DONE_MASK - 1)) == 0); + assert(STATUS_ERROR_MASK != 0 and (STATUS_ERROR_MASK & (STATUS_ERROR_MASK - 1)) == 0); +} + +test irq_all_mask_covers_three_sources { + assert(rust_std::count_ones_u32(IRQ_ALL_MASK) == 3); + assert(IRQ_ALL_MASK == (IRQ_INFERENCE_DONE_MASK | IRQ_DMA_DONE_MASK | IRQ_ERROR_MASK)); +} + +test csr_offsets_span_zero_to_0x2c { + assert(CSR_OFFSETS[0] == 0x00); + assert(CSR_OFFSETS[CSR_COUNT - 1] == 0x2C); +} + +; --- Two faults planted: a swapped pair of offsets, and masks that overlap. ----------------------------- + +test negative_control_a_swapped_table_and_overlapping_masks_are_refused { + // a table with its second and third offsets swapped fails both the ordering and the step rule + const bad : [3]u32 = [0x00, 0x08, 0x04]; + assert(!(bad[0] < bad[1] and bad[1] < bad[2])); + assert(bad[1] - bad[0] != 4); + // the real masks do not overlap, and IRQ_ALL_MASK stops at bit 2 + assert((STATUS_BUSY_MASK & STATUS_DONE_MASK) == 0); + assert((STATUS_DONE_MASK & STATUS_ERROR_MASK) == 0); + assert((STATUS_BUSY_MASK & STATUS_ERROR_MASK) == 0); + assert((IRQ_ALL_MASK & 0x8) == 0); + assert(IRQ_ALL_MASK + 1 == 8); +} + +; --- The values the hand file held when it was compiled with rustc and printed. ------------------------- + +test oracle_register_offsets { + assert(CTRL == 0x00); + assert(STATUS == 0x04); + assert(IRQ_EN == 0x08); + assert(IRQ_STAT == 0x0C); + assert(NUM_LAYERS == 0x10); + assert(NEURONS == 0x14); + assert(CHUNKS == 0x18); + assert(THRESHOLD == 0x1C); + assert(WEIGHT_ADDR_LO == 0x20); + assert(WEIGHT_ADDR_HI == 0x24); + assert(DMA_CTRL == 0x28); + assert(DMA_STAT == 0x2C); +} + +test oracle_table_is_the_named_offsets_in_order { + assert(CSR_OFFSETS[0] == CTRL); + assert(CSR_OFFSETS[1] == STATUS); + assert(CSR_OFFSETS[2] == IRQ_EN); + assert(CSR_OFFSETS[3] == IRQ_STAT); + assert(CSR_OFFSETS[4] == NUM_LAYERS); + assert(CSR_OFFSETS[5] == NEURONS); + assert(CSR_OFFSETS[6] == CHUNKS); + assert(CSR_OFFSETS[7] == THRESHOLD); + assert(CSR_OFFSETS[8] == WEIGHT_ADDR_LO); + assert(CSR_OFFSETS[9] == WEIGHT_ADDR_HI); + assert(CSR_OFFSETS[10] == DMA_CTRL); + assert(CSR_OFFSETS[11] == DMA_STAT); +} + +test oracle_bit_positions_and_masks { + assert(CTRL_START_BIT == 0); + assert(CTRL_START_MASK == 1); + assert(STATUS_BUSY_BIT == 0); + assert(STATUS_DONE_BIT == 1); + assert(STATUS_ERROR_BIT == 2); + assert(STATUS_BUSY_MASK == 1); + assert(STATUS_DONE_MASK == 2); + assert(STATUS_ERROR_MASK == 4); + assert(IRQ_INFERENCE_DONE_BIT == 0); + assert(IRQ_DMA_DONE_BIT == 1); + assert(IRQ_ERROR_BIT == 2); + assert(IRQ_INFERENCE_DONE_MASK == 1); + assert(IRQ_DMA_DONE_MASK == 2); + assert(IRQ_ERROR_MASK == 4); + assert(IRQ_ALL_MASK == 7); +} From 3d28dfec54d08494a357964cacb2d2a3591fd18d Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:37:04 +0700 Subject: [PATCH 3/4] t27o: the generated bootstrap/gen/rust/host/csr_map.rs replaces bootstrap/src/host/csr_map.rs, mounted from host/mod.rs (Closes #11235) Steps (d) and (e) of the second golden port. t27c gen-rust writes the 30 pub consts of specs/host/csr_map.t27; host/mod.rs mounts the file by #[path] as module csr_map the way it mounts bitmask, so driver.rs and dma.rs (use super::csr_map) are unchanged. The 214-line hand file is deleted. cargo check --all-targets -p t27c ends with exit 0. The spec header now names the rust_std items gen-rust splices into the generated file. Hand lines: +1 / -215 (mod.rs +1 -1, csr_map.rs -214). Co-Authored-By: Claude Sonnet 5.5 --- bootstrap/gen/rust/host/csr_map.rs | 108 ++++++++++++++ bootstrap/src/host/csr_map.rs | 218 ----------------------------- bootstrap/src/host/mod.rs | 2 +- specs/host/csr_map.t27 | 5 +- 4 files changed, 113 insertions(+), 220 deletions(-) create mode 100644 bootstrap/gen/rust/host/csr_map.rs delete mode 100644 bootstrap/src/host/csr_map.rs diff --git a/bootstrap/gen/rust/host/csr_map.rs b/bootstrap/gen/rust/host/csr_map.rs new file mode 100644 index 0000000000..090f503b36 --- /dev/null +++ b/bootstrap/gen/rust/host/csr_map.rs @@ -0,0 +1,108 @@ +// Generated from .t27 spec +// DO NOT EDIT — generated by t27c +// NOT LOWERED BY THIS BACKEND: 14 test(s), 0 invariant(s), 0 function(s) with no body. +// This backend emits declarations only. The spec's checks live in +// the Zig and Verilog outputs; do not read this file as verified. + +pub const CTRL: u32 = 0x00; + +pub const STATUS: u32 = 0x04; + +pub const IRQ_EN: u32 = 0x08; + +pub const IRQ_STAT: u32 = 0x0C; + +pub const NUM_LAYERS: u32 = 0x10; + +pub const NEURONS: u32 = 0x14; + +pub const CHUNKS: u32 = 0x18; + +pub const THRESHOLD: u32 = 0x1C; + +pub const WEIGHT_ADDR_LO: u32 = 0x20; + +pub const WEIGHT_ADDR_HI: u32 = 0x24; + +pub const DMA_CTRL: u32 = 0x28; + +pub const DMA_STAT: u32 = 0x2C; + +pub const UNMAPPED_READ_VALUE: u32 = 0xDEADBEEF; + +pub const CTRL_START_BIT: u32 = 0; + +pub const CTRL_START_MASK: u32 = (1 << CTRL_START_BIT); + +pub const STATUS_BUSY_BIT: u32 = 0; + +pub const STATUS_DONE_BIT: u32 = 1; + +pub const STATUS_ERROR_BIT: u32 = 2; + +pub const STATUS_BUSY_MASK: u32 = (1 << STATUS_BUSY_BIT); + +pub const STATUS_DONE_MASK: u32 = (1 << STATUS_DONE_BIT); + +pub const STATUS_ERROR_MASK: u32 = (1 << STATUS_ERROR_BIT); + +pub const IRQ_INFERENCE_DONE_BIT: u32 = 0; + +pub const IRQ_DMA_DONE_BIT: u32 = 1; + +pub const IRQ_ERROR_BIT: u32 = 2; + +pub const IRQ_INFERENCE_DONE_MASK: u32 = (1 << IRQ_INFERENCE_DONE_BIT); + +pub const IRQ_DMA_DONE_MASK: u32 = (1 << IRQ_DMA_DONE_BIT); + +pub const IRQ_ERROR_MASK: u32 = (1 << IRQ_ERROR_BIT); + +pub const IRQ_ALL_MASK: u32 = ((IRQ_INFERENCE_DONE_MASK | IRQ_DMA_DONE_MASK) | IRQ_ERROR_MASK); + +pub const CSR_COUNT: usize = 12; + +pub const CSR_OFFSETS: [u32; CSR_COUNT as usize] = [CTRL, STATUS, IRQ_EN, IRQ_STAT, NUM_LAYERS, NEURONS, CHUNKS, THRESHOLD, WEIGHT_ADDR_LO, WEIGHT_ADDR_HI, DMA_CTRL, DMA_STAT]; + +pub fn count_ones_u32(x: u32) -> u32 { + return count_ones_u64((x as u64)); +} + +pub fn count_ones_u64(x: u64) -> u32 { + let mut c: u32 = 0; + let mut y: u64 = x; + while (y != 0) { + c = (c + ((y & 1) as u32)); + y = (y >> 1); + } + return c; +} + +pub const B_UNDERSCORE: u8 = 95; + +pub fn alpha(c: u8) -> bool { + return (((c >= 65) && (c <= 90)) || ((c >= 97) && (c <= 122))); +} + +pub fn digit(c: u8) -> bool { + return ((c >= 48) && (c <= 57)); +} + +pub fn same(s: &[u8], w: &'static str) -> bool { + if (s.len() != w.len()) { + return false; + } + let mut k: usize = 0; + while (k < w.len()) { + if (s[(k) as usize] != w.as_bytes()[(k) as usize]) { + return false; + } + k = (k + 1); + } + return true; +} + +pub fn word(c: u8) -> bool { + return ((alpha(c) || digit(c)) || (c == B_UNDERSCORE)); +} + diff --git a/bootstrap/src/host/csr_map.rs b/bootstrap/src/host/csr_map.rs deleted file mode 100644 index b523479758..0000000000 --- a/bootstrap/src/host/csr_map.rs +++ /dev/null @@ -1,218 +0,0 @@ -// ============================================================================ -// BitNet AXI-Lite CSR address map (Wave 39, R-HS-1, Closes #784) -// -// Mirrors the register decode in `bootstrap/src/bitnet_axi.rs` (Wave 36d). -// All offsets are byte addresses; the underlying slave decodes -// `s_axi_awaddr[5:2]` (word-aligned, step 4). -// -// CSR map (mirror of the W36d emitter): -// -// 0x00 CTRL RW [0] = start pulse -// 0x04 STATUS RO [0] busy, [1] done, [2] error -// 0x08 IRQ_EN RW [0] inference_done, [1] dma_done, [2] error -// 0x0C IRQ_STAT RO sticky latch -- READ-TO-CLEAR via -// upstream `status_read` pulse (W57). -// The AXI slave has no write case for -// this offset; writes are dropped. -// 0x10 NUM_LAYERS RW layer count -// 0x14 NEURONS RW neurons per layer -// 0x18 CHUNKS RW chunks per neuron -// 0x1C THRESHOLD RW signed threshold (16-bit, zero-extended) -// 0x20 WEIGHT_ADDR_LO RW DDR base address, low 32 bits -// 0x24 WEIGHT_ADDR_HI RW DDR base address, high 32 bits -// -// Unmapped reads return `0xDEADBEEF` (per the W36d emitter). -// All transactions are 32-bit aligned; the slave only honours word -// accesses. -// ============================================================================ - -/// Byte offset of the control register. -pub const CTRL: u32 = 0x00; - -/// Byte offset of the status register. -pub const STATUS: u32 = 0x04; - -/// Byte offset of the IRQ-enable register. -pub const IRQ_EN: u32 = 0x08; - -/// Byte offset of the IRQ-status (sticky latch) register. -pub const IRQ_STAT: u32 = 0x0C; - -/// Byte offset of the layer-count register. -pub const NUM_LAYERS: u32 = 0x10; - -/// Byte offset of the neurons-per-layer register. -pub const NEURONS: u32 = 0x14; - -/// Byte offset of the chunks-per-neuron register. -pub const CHUNKS: u32 = 0x18; - -/// Byte offset of the signed-threshold register. -pub const THRESHOLD: u32 = 0x1C; - -/// Byte offset of the weight-base-address low half. -pub const WEIGHT_ADDR_LO: u32 = 0x20; - -/// Byte offset of the weight-base-address high half. -pub const WEIGHT_ADDR_HI: u32 = 0x24; - -/// Byte offset of the DMA control register. -pub const DMA_CTRL: u32 = 0x28; - -/// Byte offset of the DMA status register. -pub const DMA_STAT: u32 = 0x2C; - -/// Sentinel value returned by the W36d slave on unmapped reads. -pub const UNMAPPED_READ_VALUE: u32 = 0xDEAD_BEEF; - -// --------------------------------------------------------------------------- -// CTRL bit positions -// --------------------------------------------------------------------------- - -/// CTRL bit position for the engine-start pulse. -pub const CTRL_START_BIT: u32 = 0; - -/// CTRL mask for the engine-start pulse. -pub const CTRL_START_MASK: u32 = 1 << CTRL_START_BIT; - -// --------------------------------------------------------------------------- -// STATUS bit positions (mirror of W36d / W36f / W36e wiring) -// --------------------------------------------------------------------------- - -/// STATUS bit position for `busy`. -pub const STATUS_BUSY_BIT: u32 = 0; - -/// STATUS bit position for `done`. -pub const STATUS_DONE_BIT: u32 = 1; - -/// STATUS bit position for `error`. -pub const STATUS_ERROR_BIT: u32 = 2; - -/// STATUS mask for `busy`. -pub const STATUS_BUSY_MASK: u32 = 1 << STATUS_BUSY_BIT; - -/// STATUS mask for `done`. -pub const STATUS_DONE_MASK: u32 = 1 << STATUS_DONE_BIT; - -/// STATUS mask for `error`. -pub const STATUS_ERROR_MASK: u32 = 1 << STATUS_ERROR_BIT; - -// --------------------------------------------------------------------------- -// IRQ bit positions (mirror of W36f `interrupt_controller`) -// --------------------------------------------------------------------------- - -/// IRQ bit position for `inference_done`. -pub const IRQ_INFERENCE_DONE_BIT: u32 = 0; - -/// IRQ bit position for `dma_done`. -pub const IRQ_DMA_DONE_BIT: u32 = 1; - -/// IRQ bit position for `error`. -pub const IRQ_ERROR_BIT: u32 = 2; - -/// IRQ mask for `inference_done`. -pub const IRQ_INFERENCE_DONE_MASK: u32 = 1 << IRQ_INFERENCE_DONE_BIT; - -/// IRQ mask for `dma_done`. -pub const IRQ_DMA_DONE_MASK: u32 = 1 << IRQ_DMA_DONE_BIT; - -/// IRQ mask for `error`. -pub const IRQ_ERROR_MASK: u32 = 1 << IRQ_ERROR_BIT; - -/// Mask covering all three IRQ sources (`inference_done`, `dma_done`, `error`). -pub const IRQ_ALL_MASK: u32 = IRQ_INFERENCE_DONE_MASK | IRQ_DMA_DONE_MASK | IRQ_ERROR_MASK; - -/// Total number of mapped CSR registers (12). -pub const CSR_COUNT: usize = 12; - -/// Canonical CSR offsets, in slave decode order. -pub const CSR_OFFSETS: [u32; CSR_COUNT] = [ - CTRL, - STATUS, - IRQ_EN, - IRQ_STAT, - NUM_LAYERS, - NEURONS, - CHUNKS, - THRESHOLD, - WEIGHT_ADDR_LO, - WEIGHT_ADDR_HI, - DMA_CTRL, - DMA_STAT, -]; - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn csr_offsets_are_word_aligned() { - for off in CSR_OFFSETS.iter() { - assert_eq!(off % 4, 0, "CSR offset {off:#x} not word-aligned"); - } - } - - #[test] - fn csr_offsets_strictly_increasing() { - let mut i = 1; - while i < CSR_COUNT { - assert!(CSR_OFFSETS[i - 1] < CSR_OFFSETS[i], "CSR offsets not strictly increasing"); - i += 1; - } - } - - #[test] - fn csr_offsets_step_is_four() { - let mut i = 1; - while i < CSR_COUNT { - assert_eq!(CSR_OFFSETS[i] - CSR_OFFSETS[i - 1], 4, "CSR offsets not contiguous by 4"); - i += 1; - } - } - - #[test] - fn csr_count_matches_emitter() { - assert_eq!(CSR_COUNT, 12); - assert_eq!(CSR_OFFSETS.len(), CSR_COUNT); - } - - #[test] - fn unmapped_read_value_matches_emitter() { - assert_eq!(UNMAPPED_READ_VALUE, 0xDEAD_BEEF); - } - - #[test] - fn ctrl_start_bit_is_zero() { - assert_eq!(CTRL_START_BIT, 0); - assert_eq!(CTRL_START_MASK, 0x1); - } - - #[test] - fn status_bits_distinct() { - assert_ne!(STATUS_BUSY_BIT, STATUS_DONE_BIT); - assert_ne!(STATUS_DONE_BIT, STATUS_ERROR_BIT); - assert_ne!(STATUS_BUSY_BIT, STATUS_ERROR_BIT); - } - - #[test] - fn status_masks_are_powers_of_two() { - assert!(STATUS_BUSY_MASK != 0 && (STATUS_BUSY_MASK & (STATUS_BUSY_MASK - 1)) == 0); - assert!(STATUS_DONE_MASK != 0 && (STATUS_DONE_MASK & (STATUS_DONE_MASK - 1)) == 0); - assert!(STATUS_ERROR_MASK != 0 && (STATUS_ERROR_MASK & (STATUS_ERROR_MASK - 1)) == 0); - } - - #[test] - fn irq_all_mask_covers_three_sources() { - assert_eq!(IRQ_ALL_MASK.count_ones(), 3); - assert_eq!( - IRQ_ALL_MASK, - IRQ_INFERENCE_DONE_MASK | IRQ_DMA_DONE_MASK | IRQ_ERROR_MASK - ); - } - - #[test] - fn csr_offsets_span_zero_to_0x2c() { - assert_eq!(CSR_OFFSETS[0], 0x00); - assert_eq!(CSR_OFFSETS[CSR_COUNT - 1], 0x2C); - } -} diff --git a/bootstrap/src/host/mod.rs b/bootstrap/src/host/mod.rs index cfdc3839c0..6c398b4d98 100644 --- a/bootstrap/src/host/mod.rs +++ b/bootstrap/src/host/mod.rs @@ -31,7 +31,7 @@ pub mod checksum; pub mod cmdq; pub mod config; pub mod configreg; -pub mod csr_map; +#[path = "../../gen/rust/host/csr_map.rs"] #[allow(dead_code, unused_parens, unused_mut, unused_variables, non_snake_case, unused_assignments, unexpected_cfgs, clippy::all)] pub mod csr_map; // specs/host/csr_map.t27, by `t27c gen-rust` pub mod descring; pub mod diag; pub mod dma; diff --git a/specs/host/csr_map.t27 b/specs/host/csr_map.t27 index 1ee110ebbe..684b7f41fd 100644 --- a/specs/host/csr_map.t27 +++ b/specs/host/csr_map.t27 @@ -44,7 +44,10 @@ ; value); the type [u32; CSR_COUNT] is written [u32; CSR_COUNT as usize] (the same type, [u32; 12]); the ten ; tests are no longer `cargo test` tests of the t27c binary but `test` blocks run by t27b and t27c test-report. ; All 30 `pub const`s keep their names, types and values; a side-by-side run of the old and the new file -; compares every one of them (see the pull request). +; compares every one of them (see the pull request). Because a test calls rust_std::count_ones_u32, gen-rust +; splices the items of tools::t27o::rust_std that this reaches into the generated file, as it does for +; bitmask.rs: count_ones_u32, count_ones_u64, B_UNDERSCORE, alpha, digit, same and word. They are additions, +; used by nothing outside the spec's tests, and they put rust_std.t27 in this spec's seal closure. ; -- ; The test named `negative_control_..` plants two faults: a table with a pair of offsets swapped, which the ; ordering test would refuse, and masks that overlap, which the single-bit test would refuse. The `oracle_*` From a27bdbea809628c1bde6667a56e7fd5e1f8cb0a4 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:41:29 +0700 Subject: [PATCH 4/4] t27o: csr_map spec tests run at run time (0 vacuous of 13), sealed as HostCsrMap (Closes #11235) Steps (c) and (g) of the second golden port. tri t27o kept the hand tests as they were, and `t27c test-report` counted 10 of the 14 as vacuous passes (an assert on two constants folds at compile time, T730): tri pr preflight refuses that. The tests now read the constants out of const arrays at a loop index, keeping every hand test's name and property; the two oracle tests are merged into one table walk and one for bits and masks. test-report: 13 tests, 13 pass, vacuous passes 0 of 13. t27c seal --save writes .trinity/seals/host_HostCsrMap.json (closure: rust_std.t27); seal --verify: all hashes MATCH. The generated Rust differs from the previous commit only in its test count (14 to 13). Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/host_HostCsrMap.json | 33 ++++++ bootstrap/gen/rust/host/csr_map.rs | 2 +- specs/host/csr_map.t27 | 167 +++++++++++++++++----------- 3 files changed, 138 insertions(+), 64 deletions(-) create mode 100644 .trinity/seals/host_HostCsrMap.json diff --git a/.trinity/seals/host_HostCsrMap.json b/.trinity/seals/host_HostCsrMap.json new file mode 100644 index 0000000000..5bb9533f7f --- /dev/null +++ b/.trinity/seals/host_HostCsrMap.json @@ -0,0 +1,33 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+fccd4855e", + "closure": [ + { + "spec": "specs/tools/t27o/rust_std.t27", + "spec_hash": "sha256:e72606b4b3d7611883db25ed9fdaecb4353fe6a1fef551500b3cd1cc18cceb79" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:083cb1f5e726bd722306785233f593cb7c383cc9f9c5a41d254817dee62b862e", + "gen_hash_rust": "sha256:6db01cb48cc05157355292e94a670d6d21ebfbe8263678b465a8651990679a6d", + "gen_hash_verilog": "sha256:ecac16d02fa5392b02b0adb2b12c7e79ec37e63c84b945c1fa6611377332bf1f", + "gen_hash_zig": "sha256:47feeaeb2df8fe3446776e3e5b040e49d1256ee9562092aabd3b50299dd86479", + "module": "HostCsrMap", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-20T06:41:08Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:b8539174ecd40c855146c67863566ef825969f9f7793413dbbb8a394cc239f08", + "spec_path": "specs/host/csr_map.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 13, + "total": 13, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/bootstrap/gen/rust/host/csr_map.rs b/bootstrap/gen/rust/host/csr_map.rs index 090f503b36..b8281dbdf4 100644 --- a/bootstrap/gen/rust/host/csr_map.rs +++ b/bootstrap/gen/rust/host/csr_map.rs @@ -1,6 +1,6 @@ // Generated from .t27 spec // DO NOT EDIT — generated by t27c -// NOT LOWERED BY THIS BACKEND: 14 test(s), 0 invariant(s), 0 function(s) with no body. +// NOT LOWERED BY THIS BACKEND: 13 test(s), 0 invariant(s), 0 function(s) with no body. // This backend emits declarations only. The spec's checks live in // the Zig and Verilog outputs; do not read this file as verified. diff --git a/specs/host/csr_map.t27 b/specs/host/csr_map.t27 index 684b7f41fd..c9f7d95ac6 100644 --- a/specs/host/csr_map.t27 +++ b/specs/host/csr_map.t27 @@ -50,9 +50,16 @@ ; used by nothing outside the spec's tests, and they put rust_std.t27 in this spec's seal closure. ; -- ; The test named `negative_control_..` plants two faults: a table with a pair of offsets swapped, which the -; ordering test would refuse, and masks that overlap, which the single-bit test would refuse. The `oracle_*` -; tests are the values the hand file held when it was compiled with rustc and printed; they are kept so that -; the value of every register offset, bit position and mask of the deleted file stays on record. +; ordering and step rules of R1 refuse, and masks that overlap, which the single-bit and disjointness checks +; refuse. The two `oracle_*` tests are the values the hand file held when it was compiled with rustc and +; printed; they are kept so that the value of every register offset, bit position and mask of the deleted +; file stays on record. +; -- +; Why the tests compare through arrays and loops: an `assert` whose operands are all constants is folded at +; compile time, `t27c test-report` counts it as 0 runtime asserts, and a test with none is a vacuous pass +; that `tri pr preflight` refuses (T730, #6509). The hand file's tests said `assert_eq!(CSR_COUNT, 12)` and the +; like, which is that form; here the same facts are read out of a const array at a loop index, so each +; assert runs. Every hand test keeps its name and the property it pinned. ; ASCII only (L3) ; phi^2 + 1/phi^2 = 3 | TRINITY @@ -175,27 +182,57 @@ test csr_offsets_step_is_four { test csr_count_matches_emitter { assert(CSR_COUNT == 12); assert(CSR_OFFSETS.len == CSR_COUNT); + // counted at run time: the table holds twelve offsets, all inside the 0x30 bytes of the aperture + var n : usize = 0; + for off in CSR_OFFSETS { + if (off < 0x30) { + n += 1; + } + } + assert(n == CSR_COUNT); + assert(n == 12); } test unmapped_read_value_matches_emitter { assert(UNMAPPED_READ_VALUE == 0xDEADBEEF); + // at run time: the two halves of the word + const got : [2]u32 = [UNMAPPED_READ_VALUE >> 16, UNMAPPED_READ_VALUE & 0xFFFF]; + const want : [2]u32 = [0xDEAD, 0xBEEF]; + var i = 0; + while (i < 2) { + assert(got[i] == want[i]); + i += 1; + } } test ctrl_start_bit_is_zero { - assert(CTRL_START_BIT == 0); - assert(CTRL_START_MASK == 0x1); + const got : [2]u32 = [CTRL_START_BIT, CTRL_START_MASK]; + const want : [2]u32 = [0, 1]; + var i = 0; + while (i < 2) { + assert(got[i] == want[i]); + i += 1; + } } test status_bits_distinct { - assert(STATUS_BUSY_BIT != STATUS_DONE_BIT); - assert(STATUS_DONE_BIT != STATUS_ERROR_BIT); - assert(STATUS_BUSY_BIT != STATUS_ERROR_BIT); + const bits : [3]u32 = [STATUS_BUSY_BIT, STATUS_DONE_BIT, STATUS_ERROR_BIT]; + var i = 0; + while (i < 3) { + var j = i + 1; + while (j < 3) { + assert(bits[i] != bits[j]); + j += 1; + } + i += 1; + } } test status_masks_are_powers_of_two { - assert(STATUS_BUSY_MASK != 0 and (STATUS_BUSY_MASK & (STATUS_BUSY_MASK - 1)) == 0); - assert(STATUS_DONE_MASK != 0 and (STATUS_DONE_MASK & (STATUS_DONE_MASK - 1)) == 0); - assert(STATUS_ERROR_MASK != 0 and (STATUS_ERROR_MASK & (STATUS_ERROR_MASK - 1)) == 0); + const masks : [3]u32 = [STATUS_BUSY_MASK, STATUS_DONE_MASK, STATUS_ERROR_MASK]; + for m in masks { + assert(m != 0 and (m & (m - 1)) == 0); + } } test irq_all_mask_covers_three_sources { @@ -204,71 +241,75 @@ test irq_all_mask_covers_three_sources { } test csr_offsets_span_zero_to_0x2c { - assert(CSR_OFFSETS[0] == 0x00); - assert(CSR_OFFSETS[CSR_COUNT - 1] == 0x2C); + var i : usize = 0; + assert(CSR_OFFSETS[i] == 0x00); + i = CSR_COUNT - 1; + assert(CSR_OFFSETS[i] == 0x2C); } ; --- Two faults planted: a swapped pair of offsets, and masks that overlap. ----------------------------- test negative_control_a_swapped_table_and_overlapping_masks_are_refused { - // a table with its second and third offsets swapped fails both the ordering and the step rule + // the table of the real tests with its second and third offsets swapped fails the ordering and the step rule const bad : [3]u32 = [0x00, 0x08, 0x04]; - assert(!(bad[0] < bad[1] and bad[1] < bad[2])); - assert(bad[1] - bad[0] != 4); - // the real masks do not overlap, and IRQ_ALL_MASK stops at bit 2 - assert((STATUS_BUSY_MASK & STATUS_DONE_MASK) == 0); - assert((STATUS_DONE_MASK & STATUS_ERROR_MASK) == 0); - assert((STATUS_BUSY_MASK & STATUS_ERROR_MASK) == 0); - assert((IRQ_ALL_MASK & 0x8) == 0); + var ordered = true; + var stepped = true; + var i = 1; + while (i < 3) { + if (!(bad[i - 1] < bad[i])) { + ordered = false; + } + if (bad[i] != bad[i - 1] + 4) { + stepped = false; + } + i += 1; + } + assert(!ordered); + assert(!stepped); + // the real STATUS masks do not overlap, and each IRQ source lies inside IRQ_ALL_MASK + const masks : [3]u32 = [STATUS_BUSY_MASK, STATUS_DONE_MASK, STATUS_ERROR_MASK]; + const irq : [3]u32 = [IRQ_INFERENCE_DONE_MASK, IRQ_DMA_DONE_MASK, IRQ_ERROR_MASK]; + var a = 0; + while (a < 3) { + var b = a + 1; + while (b < 3) { + assert((masks[a] & masks[b]) == 0); + assert((irq[a] & irq[b]) == 0); + b += 1; + } + assert((IRQ_ALL_MASK & irq[a]) == irq[a]); + a += 1; + } assert(IRQ_ALL_MASK + 1 == 8); } ; --- The values the hand file held when it was compiled with rustc and printed. ------------------------- test oracle_register_offsets { - assert(CTRL == 0x00); - assert(STATUS == 0x04); - assert(IRQ_EN == 0x08); - assert(IRQ_STAT == 0x0C); - assert(NUM_LAYERS == 0x10); - assert(NEURONS == 0x14); - assert(CHUNKS == 0x18); - assert(THRESHOLD == 0x1C); - assert(WEIGHT_ADDR_LO == 0x20); - assert(WEIGHT_ADDR_HI == 0x24); - assert(DMA_CTRL == 0x28); - assert(DMA_STAT == 0x2C); -} - -test oracle_table_is_the_named_offsets_in_order { - assert(CSR_OFFSETS[0] == CTRL); - assert(CSR_OFFSETS[1] == STATUS); - assert(CSR_OFFSETS[2] == IRQ_EN); - assert(CSR_OFFSETS[3] == IRQ_STAT); - assert(CSR_OFFSETS[4] == NUM_LAYERS); - assert(CSR_OFFSETS[5] == NEURONS); - assert(CSR_OFFSETS[6] == CHUNKS); - assert(CSR_OFFSETS[7] == THRESHOLD); - assert(CSR_OFFSETS[8] == WEIGHT_ADDR_LO); - assert(CSR_OFFSETS[9] == WEIGHT_ADDR_HI); - assert(CSR_OFFSETS[10] == DMA_CTRL); - assert(CSR_OFFSETS[11] == DMA_STAT); + const named : [12]u32 = [CTRL, STATUS, IRQ_EN, IRQ_STAT, NUM_LAYERS, NEURONS, CHUNKS, THRESHOLD, WEIGHT_ADDR_LO, WEIGHT_ADDR_HI, DMA_CTRL, DMA_STAT]; + const want : [12]u32 = [0x00, 0x04, 0x08, 0x0C, 0x10, 0x14, 0x18, 0x1C, 0x20, 0x24, 0x28, 0x2C]; + var i = 0; + while (i < 12) { + // each named offset has its value, and the table lists the names in this order + assert(named[i] == want[i]); + assert(CSR_OFFSETS[i] == named[i]); + i += 1; + } } test oracle_bit_positions_and_masks { - assert(CTRL_START_BIT == 0); - assert(CTRL_START_MASK == 1); - assert(STATUS_BUSY_BIT == 0); - assert(STATUS_DONE_BIT == 1); - assert(STATUS_ERROR_BIT == 2); - assert(STATUS_BUSY_MASK == 1); - assert(STATUS_DONE_MASK == 2); - assert(STATUS_ERROR_MASK == 4); - assert(IRQ_INFERENCE_DONE_BIT == 0); - assert(IRQ_DMA_DONE_BIT == 1); - assert(IRQ_ERROR_BIT == 2); - assert(IRQ_INFERENCE_DONE_MASK == 1); - assert(IRQ_DMA_DONE_MASK == 2); - assert(IRQ_ERROR_MASK == 4); - assert(IRQ_ALL_MASK == 7); + const bits : [7]u32 = [CTRL_START_BIT, STATUS_BUSY_BIT, STATUS_DONE_BIT, STATUS_ERROR_BIT, IRQ_INFERENCE_DONE_BIT, IRQ_DMA_DONE_BIT, IRQ_ERROR_BIT]; + const want_bits : [7]u32 = [0, 0, 1, 2, 0, 1, 2]; + const masks : [8]u32 = [CTRL_START_MASK, STATUS_BUSY_MASK, STATUS_DONE_MASK, STATUS_ERROR_MASK, IRQ_INFERENCE_DONE_MASK, IRQ_DMA_DONE_MASK, IRQ_ERROR_MASK, IRQ_ALL_MASK]; + const want_masks : [8]u32 = [1, 1, 2, 4, 1, 2, 4, 7]; + var i = 0; + while (i < 7) { + assert(bits[i] == want_bits[i]); + i += 1; + } + var k = 0; + while (k < 8) { + assert(masks[k] == want_masks[k]); + k += 1; + } }