u280_shell_rhdl/
frame_store.rs

1//! Canonical frame validation and two-slot synchronous block-RAM storage.
2
3use rhdl::prelude::*;
4use rhdl_fpga::core::ram::synchronous::{In as SyncBramIn, SyncBRAM, Write as SyncBramWrite};
5use wots_rhdl::SignerOutputBeat;
6
7/// Seven address bits encode `{slot, beat}` as `slot * 64 + beat`.
8pub const FRAME_STORE_ADDRESS_BITS: usize = 7;
9
10/// Memory access for the two complete frame slots.
11#[derive(Clone, Copy, Debug, Digital, PartialEq)]
12pub struct FrameStoreInput {
13    /// Synchronous read address.
14    pub read_addr: b7,
15    /// Optional capture write.
16    pub write: SyncBramWrite<[b8; 64], FRAME_STORE_ADDRESS_BITS>,
17}
18
19impl Default for FrameStoreInput {
20    fn default() -> Self {
21        Self {
22            read_addr: b7(0),
23            write: SyncBramWrite::<[b8; 64], FRAME_STORE_ADDRESS_BITS> {
24                addr: b7(0),
25                value: [b8(0); 64],
26                enable: false,
27            },
28        }
29    }
30}
31
32/// BRAM-backed storage; validity and ownership live in the shell controller.
33#[derive(Clone, Debug, Default, Synchronous, SynchronousDQ)]
34pub struct FrameStore {
35    memory: SyncBRAM<[b8; 64], FRAME_STORE_ADDRESS_BITS>,
36}
37
38impl SynchronousIO for FrameStore {
39    type I = FrameStoreInput;
40    type O = [b8; 64];
41    type Kernel = frame_store_kernel;
42}
43
44/// Preserve the RAM as a native synchronous child.
45#[kernel]
46#[allow(clippy::used_underscore_binding)] // The standard clock/reset port is consumed by the synchronous-kernel boundary.
47pub fn frame_store_kernel(
48    _clock_reset: ClockReset,
49    input: FrameStoreInput,
50    q: FrameStoreQ,
51) -> ([b8; 64], FrameStoreD) {
52    (
53        q.memory,
54        FrameStoreD {
55            memory: SyncBramIn::<[b8; 64], FRAME_STORE_ADDRESS_BITS> {
56                read_addr: input.read_addr,
57                write: input.write,
58            },
59        },
60    )
61}
62
63/// Map a slot and beat to the physical BRAM address.
64#[kernel]
65pub fn frame_store_address_kernel(slot: b1, beat: b6) -> b7 {
66    let wide_slot: b7 = slot.resize();
67    let wide_beat: b7 = beat.resize();
68    (wide_slot << 6) | wide_beat
69}
70
71/// Validate every byte-control and identity invariant before a BRAM write.
72#[kernel]
73#[allow(clippy::comparison_chain, clippy::needless_range_loop)] // Keep the three canonical beat classes explicit and aligned with the protocol proof cases.
74pub fn captured_beat_is_canonical_kernel(
75    candidate: SignerOutputBeat,
76    expected_beat: b6,
77    frame_active: bool,
78    expected_job: b32,
79    expected_cluster: b2,
80) -> bool {
81    let mut high_padding_zero = true;
82    for lane in 32..64 {
83        if candidate.beat.data[lane] != b8(0) {
84            high_padding_zero = false;
85        }
86    }
87    let control_ok = if expected_beat < b6(34) {
88        candidate.beat.keep == b64(0xffff_ffff_ffff_ffff) && !candidate.beat.last
89    } else if expected_beat == b6(34) {
90        candidate.beat.keep == b64(0x0000_0000_ffff_ffff)
91            && candidate.beat.last
92            && high_padding_zero
93    } else {
94        false
95    };
96    let identity_ok = !frame_active
97        || (candidate.beat.job_id == expected_job && candidate.cluster == expected_cluster);
98    candidate.cluster < b2(3) && control_ok && identity_ok
99}
u280_shell_rhdl/frame_store.rs

u280_shell_rhdl/
frame_store.rs
