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 new file mode 100644 index 0000000000..b8281dbdf4 --- /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: 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. + +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 981ea6c152..0000000000 --- a/bootstrap/src/host/csr_map.rs +++ /dev/null @@ -1,214 +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() { - for w in CSR_OFFSETS.windows(2) { - assert!(w[0] < w[1], "CSR offsets not strictly increasing"); - } - } - - #[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"); - } - } - - #[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.is_power_of_two()); - assert!(STATUS_DONE_MASK.is_power_of_two()); - assert!(STATUS_ERROR_MASK.is_power_of_two()); - } - - #[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 new file mode 100644 index 0000000000..c9f7d95ac6 --- /dev/null +++ b/specs/host/csr_map.t27 @@ -0,0 +1,315 @@ +// 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). 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 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 + +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); + // 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + // 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]; + 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 { + 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 { + 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; + } +}