rhdl_dsig_scalable_core/verify/

engine.rs

//! The verifier card kernel: `VERIFY_UNITS` verify units, HBM, registers.
//!
//! **Status:** interface only. The ports, the register map and the HBM layout
//! below are fixed so the host tools can be written against them; the kernel
//! body is being built (see [`super`]).
//!
//! # Ports
//!
//! | Port | Direction | Carries |
//! |---|---|---|
//! | `s_axi_control` | AXI4-Lite slave | the registers below |
//! | `m_axi_records{u}` | AXI4 read master | unit `u`'s records |
//! | `m_axi_verdicts{u}` | AXI4 write master | unit `u`'s verdict bytes |
//!
//! Both of unit `u`'s ports reach the same 1 GiB HBM group, `HBM[4u:4u+3]`.
//!
//! # HBM layout per unit
//!
//! * `records{u}`: `count` records of [`RECORD_BYTES`](super::RECORD_BYTES),
//!   back to back, from a 4 KiB-aligned address.
//! * `verdicts{u}`: `count` verdict bytes in record order, from a 64-byte
//!   aligned address, padded to whole 64-byte beats. The host zero-fills it;
//!   a written verdict always has bit 7 set.
//!
//! Every unit verifies the same `count` records. The host gives each unit
//! whole batches (all 128 records of a batch in a row), so a unit asks the
//! Ed25519 core for at most one certificate check per 128 records.
//!
//! # Register map (32-bit words)
//!
//! | Offset | Name | Access |
//! |---|---|---|
//! | `0x000` | `AP_CTRL`: bit 0 `ap_start`, 1 `ap_done` (clear on read), 2 `ap_idle`, 3 `ap_ready` | RW |
//! | `0x004` | `GIE` | RW |
//! | `0x008` | `IER` bit 0 | RW |
//! | `0x00c` | `ISR` bit 0 (write 1 to toggle) | RW |
//! | `0x010 + 0x10·u` | arg `records{u}` (u64) | W |
//! | `0x018 + 0x10·u` | arg `verdicts{u}` (u64) | W |
//! | `0x090` | arg `count`: records per unit (u32) | W |
//! | `0x098 + 4w` | args `key0`..`key7`: trusted Ed25519 public key, bytes `4w..4w+4` little endian | W |
//! | `0x200` | `MAGIC` = [`MAGIC`] ("DSV1") | R |
//! | `0x204` | `ABI` = [`ABI_VERSION`] | R |
//! | `0x208` | `SHAPE`: units bits 0..8, lanes 8..12, log2 contexts 12..16, table mask 16..28 | R |
//! | `0x20c` | `FAULT`: bit 0 read error, 1 write error, 2 Ed25519 core error, 3 key rejected | R |
//! | `0x210`/`0x214` | `TICKS` lo (snapshots hi) / hi | R |
//! | `0x218`/`0x21c` | `START_TICK` lo/hi | R |
//! | `0x220`/`0x224` | `DONE_TICK` lo/hi: the last verdict write acknowledged | R |
//! | `0x228`/`0x22c` | `KEY_TICK` lo/hi: the trusted key finished loading | R |
//! | `0x230` | `VALID`: records verified valid, all units | R |
//! | `0x234` | `CERT_CHECKS`: Ed25519 verifications issued | R |
//! | `0x238` | `CERT_FAILS`: Ed25519 verifications that failed | R |
//! | `0x240 + 4u` | `RETIRED[u]`: verdicts produced by unit `u` | R |
//!
//! Arguments are accepted only while idle; a finished kernel stays done until
//! reset (one run per reset), exactly as in [`crate::engine`]. The run is
//! timed from `START_TICK` to `DONE_TICK`, which includes loading the trusted
//! key into the Ed25519 core.

use crate::VERIFY_UNITS;
use crate::axi4::{AxiLiteIn, AxiLiteOut, ReadRequest, ReadResponse, WriteRequest, WriteResponse};
use rhdl::prelude::*;

/// `MAGIC` register value ("DSV1" in little-endian ASCII).
pub const MAGIC: b32 = b32(0x3156_5344);
/// Register-map version of the verifier kernel.
pub const ABI_VERSION: b32 = b32(0x0001_0001);

/// Offset of arg `records0`; unit `u`'s is `+ 0x10·u`.
pub const ARG_RECORDS: usize = 0x010;
/// Offset of arg `verdicts0`; unit `u`'s is `+ 0x10·u`.
pub const ARG_VERDICTS: usize = 0x018;
/// Offset of arg `count`.
pub const ARG_COUNT: usize = 0x090;
/// Offset of arg `key0`; word `w`'s is `+ 4w`.
pub const ARG_KEY: usize = 0x098;
/// Offset of `MAGIC`.
pub const REG_MAGIC: usize = 0x200;
/// Offset of `ABI`.
pub const REG_ABI: usize = 0x204;
/// Offset of `SHAPE`.
pub const REG_SHAPE: usize = 0x208;
/// Offset of `FAULT`.
pub const REG_FAULT: usize = 0x20c;
/// Offset of `TICKS` lo.
pub const REG_TICKS: usize = 0x210;
/// Offset of `START_TICK` lo.
pub const REG_START_TICK: usize = 0x218;
/// Offset of `DONE_TICK` lo.
pub const REG_DONE_TICK: usize = 0x220;
/// Offset of `KEY_TICK` lo.
pub const REG_KEY_TICK: usize = 0x228;
/// Offset of `VALID`.
pub const REG_VALID: usize = 0x230;
/// Offset of `CERT_CHECKS`.
pub const REG_CERT_CHECKS: usize = 0x234;
/// Offset of `CERT_FAILS`.
pub const REG_CERT_FAILS: usize = 0x238;
/// Offset of `RETIRED[0]`; unit `u`'s is `+ 4u`.
pub const REG_RETIRED: usize = 0x240;

/// Kernel inputs.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct VerifyEngineInput {
    /// Host control channel.
    pub axi: AxiLiteIn,
    /// Record read channels, one per unit.
    pub records: [ReadResponse; VERIFY_UNITS],
    /// Verdict write channels, one per unit.
    pub verdicts: [WriteResponse; VERIFY_UNITS],
}

/// Kernel outputs.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct VerifyEngineOutput {
    /// Host control channel.
    pub axi: AxiLiteOut,
    /// Record read channels, one per unit.
    pub records: [ReadRequest; VERIFY_UNITS],
    /// Verdict write channels, one per unit.
    pub verdicts: [WriteRequest; VERIFY_UNITS],
}

// ------------------------------------------------------------------ cluster

use crate::engine::set_half_kernel;
use crate::verify::certs::CertResult;
use crate::verify::chains::{CONTEXTS, LANES};
use crate::relay::{Delay, PipeIn, RelayPipe, ToggleLink};
use crate::verify::certs::CertRequest;
use crate::verify::unit::{UnitInput, VerifyUnit};
use rhdl::core::ReplicatedSynchronous;
use rhdl_fpga::core::dff::DFF;

/// What the cluster sees of the Ed25519 verify core.
#[derive(Clone, Copy, Debug, PartialEq, Digital, Default)]
pub struct EdStatus {
    /// The core takes a request this cycle.
    pub ready: bool,
    /// A result pulse.
    pub result_valid: bool,
    /// The result verified.
    pub result_ok: bool,
    /// The result's tag (`unit << 6 | entry`).
    pub result_tag: b16,
    /// A key load may start.
    pub load_key_ready: bool,
    /// Slot 0's state: 0 empty, 1 loading, 2 ready, 3 invalid key.
    pub key_state: b2,
    /// The core's sticky invariant violation.
    pub internal_error: bool,
}

/// What the cluster asks of the Ed25519 verify core.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct EdCommand {
    /// Present a request.
    pub valid: bool,
    /// The 64-byte commitment as eight little-endian words.
    pub message: [b64; 8],
    /// `R ‖ S` as eight little-endian words.
    pub signature: [b64; 8],
    /// The trusted key as four little-endian words.
    pub public_key: [b64; 4],
    /// `unit << 6 | entry`.
    pub tag: b16,
    /// Load the trusted key into slot 0.
    pub load_key_valid: bool,
}

/// Cluster inputs: the kernel's plus the Ed25519 core's outputs.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct ClusterInput {
    /// The kernel's ports.
    pub kernel: VerifyEngineInput,
    /// The Ed25519 core.
    pub ed: EdStatus,
}

/// Cluster outputs: the kernel's plus the Ed25519 core's inputs.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct ClusterOutput {
    /// The kernel's ports.
    pub kernel: VerifyEngineOutput,
    /// The Ed25519 core.
    pub ed: EdCommand,
}

/// Host arguments.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct VerifyArgs {
    /// Record buffer per unit.
    pub records: [b64; VERIFY_UNITS],
    /// Verdict buffer per unit.
    pub verdicts: [b64; VERIFY_UNITS],
    /// Records per unit.
    pub count: b32,
    /// Trusted Ed25519 key, eight 32-bit words.
    pub key: [b32; 8],
}

/// Register file, run state, timing and the certificate arbiter.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
#[doc(hidden)]
pub struct ClusterControl {
    /// Host arguments.
    args: VerifyArgs,
    /// Running.
    running: bool,
    /// Finished (sticky until reset).
    done: bool,
    /// `ap_done` not yet read.
    done_unread: bool,
    /// `GIE`.
    gie: bool,
    /// `IER`.
    ier: bool,
    /// `ISR`.
    isr: bool,
    /// Free-running tick counter.
    ticks: b64,
    /// Tick at start.
    start_tick: b64,
    /// Tick when the last verdict was acknowledged.
    done_tick: b64,
    /// Tick when the key settled.
    key_tick: b64,
    /// High half captured with `TICKS` lo.
    ticks_hi: b32,
    /// The key load was requested.
    key_sent: bool,
    /// The key settled (ready or invalid).
    key_settled: bool,
    /// Round-robin pointer of the certificate arbiter.
    next_unit: b3,
    /// AXI-Lite write address latch.
    aw_addr: b12,
    /// Write address latched.
    aw_have: bool,
    /// Write data latch.
    w_data: b32,
    /// Write data latched.
    w_have: bool,
    /// Write response pending.
    b_valid: bool,
    /// Read data pending.
    r_valid: bool,
    /// Read data.
    r_data: b32,
    /// `ed_request` holds a request the Ed25519 core has not taken yet.
    ed_valid: bool,
    /// The request presented to the Ed25519 core (see [`EdHeld`]).
    ed_request: EdHeld,
}

/// The request presented to the Ed25519 core, held in registers: the
/// core's input logic is deep, and fed straight from the arbiter's mux (or
/// the key registers) it was the routed kernel's worst path into the core
/// (verifier build v1, −1.24 ns, 11 levels).
#[derive(Clone, Copy, Debug, PartialEq, Digital, Default)]
#[doc(hidden)]
pub struct EdHeld {
    message: [b64; 8],
    signature: [b64; 8],
    public_key: [b64; 4],
    tag: b16,
}

impl Default for ClusterControl {
    /// IDLE, zero arguments.
    fn default() -> Self {
        Self {
            args: VerifyArgs {
                records: [b64(0); VERIFY_UNITS],
                verdicts: [b64(0); VERIFY_UNITS],
                count: b32(0),
                key: [b32(0); 8],
            },
            running: false,
            done: false,
            done_unread: false,
            gie: false,
            ier: false,
            isr: false,
            ticks: b64(0),
            start_tick: b64(0),
            done_tick: b64(0),
            key_tick: b64(0),
            ticks_hi: b32(0),
            key_sent: false,
            key_settled: false,
            next_unit: b3(0),
            aw_addr: b12(0),
            aw_have: false,
            w_data: b32(0),
            w_have: false,
            b_valid: false,
            r_valid: false,
            r_data: b32(0),
            ed_valid: false,
            ed_request: EdHeld::default(),
        }
    }
}

/// A read address on its way to HBM.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct ArItem {
    /// Burst address.
    pub araddr: b64,
    /// Beats minus one.
    pub arlen: b8,
}

/// A read beat on its way back to a unit.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct RItem {
    /// A beat.
    pub rvalid: bool,
    /// Its data.
    pub rdata: [b8; 64],
    /// Its response code.
    pub rresp: b2,
    /// Last beat of its burst.
    pub rlast: bool,
}

/// A write address on its way to HBM.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct AwItem {
    /// Burst address.
    pub awaddr: b64,
    /// Beats minus one.
    pub awlen: b8,
}

/// A write beat on its way to HBM.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct WItem {
    /// Its data.
    pub wdata: [b8; 64],
    /// Last beat of its burst.
    pub wlast: bool,
}

/// A write response on its way back to a unit.
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct BItem {
    /// A response.
    pub bvalid: bool,
    /// Its code.
    pub bresp: b2,
}

/// What the cluster tells a unit (static during a run, latency tolerant).
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct UnitControl {
    /// The kernel runs.
    pub run: bool,
    /// The unit's record buffer.
    pub records_base: b64,
    /// The unit's verdict buffer.
    pub verdicts_base: b64,
    /// Records per unit.
    pub count: b32,
}

/// What a unit reports (counters, latency tolerant).
#[derive(Clone, Copy, Debug, PartialEq, Digital)]
pub struct UnitStatus {
    /// Records retired.
    pub retired: b32,
    /// Valid records retired.
    pub valid: b32,
    /// Certificate checks issued.
    pub cert_checks: b32,
    /// Certificate checks failed.
    pub cert_fails: b32,
    /// All verdicts written and acknowledged.
    pub done: bool,
    /// Bit 0 read error, bit 1 write error.
    pub error: b2,
}

/// Everything of the kernel except the Ed25519 core.
///
/// Kept separate so simulations can answer certificate checks with a fast
/// software model; [`VerifyEngine`] adds the real core.
///
/// Every signal between a unit and the shared logic or the HBM ports passes
/// through registers ([`crate::relay`]), as in the signer: units sit in their
/// own SLRs, and an unregistered crossing cannot meet 205 MHz. Handshaked
/// channels (AR, AW, W) use relay pipes; channels without back-pressure (R,
/// B, results, control, status) use delay lines; the wide, rare certificate
/// requests use toggle links.
#[derive(Clone, Debug, Synchronous, SynchronousDQ)]
pub struct VerifyCluster<const TABLE_MASK: usize> {
    /// Registers, timing, arbiter.
    control: DFF<ClusterControl>,
    /// The verify units (one module, `VERIFY_UNITS` instances).
    units: ReplicatedSynchronous<VerifyUnit<TABLE_MASK>, VERIFY_UNITS>,
    /// Read addresses, unit → HBM.
    ar: [RelayPipe<ArItem>; VERIFY_UNITS],
    /// Read beats, HBM → unit.
    r: [Delay<RItem>; VERIFY_UNITS],
    /// Write addresses, unit → HBM.
    aw: [RelayPipe<AwItem>; VERIFY_UNITS],
    /// Write beats, unit → HBM.
    w: [RelayPipe<WItem>; VERIFY_UNITS],
    /// Write responses, HBM → unit.
    b: [Delay<BItem>; VERIFY_UNITS],
    /// Run configuration, cluster → unit.
    to_unit: [Delay<UnitControl>; VERIFY_UNITS],
    /// Certificate requests, unit → arbiter.
    requests: [ToggleLink<CertRequest>; VERIFY_UNITS],
    /// Certificate answers, arbiter → unit.
    results: [Delay<CertResult>; VERIFY_UNITS],
    /// Counters, unit → cluster.
    status: [Delay<UnitStatus>; VERIFY_UNITS],
}

impl<const TABLE_MASK: usize> Default for VerifyCluster<TABLE_MASK> {
    /// Power-on: IDLE, every unit reset.
    fn default() -> Self {
        Self {
            control: DFF::new(ClusterControl::default()),
            units: ReplicatedSynchronous::new(VerifyUnit::default()),
            ar: core::array::from_fn(|_| RelayPipe::default()),
            r: core::array::from_fn(|_| Delay::default()),
            aw: core::array::from_fn(|_| RelayPipe::default()),
            w: core::array::from_fn(|_| RelayPipe::default()),
            b: core::array::from_fn(|_| Delay::default()),
            to_unit: core::array::from_fn(|_| Delay::default()),
            requests: core::array::from_fn(|_| ToggleLink::default()),
            results: core::array::from_fn(|_| Delay::default()),
            status: core::array::from_fn(|_| Delay::default()),
        }
    }
}

impl<const TABLE_MASK: usize> SynchronousIO for VerifyCluster<TABLE_MASK> {
    type I = ClusterInput;
    type O = ClusterOutput;
    type Kernel = verify_cluster_kernel<TABLE_MASK>;
}

/// Eight little-endian 64-bit words of 64 bytes.
#[allow(clippy::needless_range_loop)]
#[kernel]
pub fn words64_kernel(bytes: [b8; 64]) -> [b64; 8] {
    let mut words = [b64(0); 8];
    for w in 0..8 {
        words[w] = bytes[8 * w].resize::<64>()
            | (bytes[8 * w + 1].resize::<64>() << 8)
            | (bytes[8 * w + 2].resize::<64>() << 16)
            | (bytes[8 * w + 3].resize::<64>() << 24)
            | (bytes[8 * w + 4].resize::<64>() << 32)
            | (bytes[8 * w + 5].resize::<64>() << 40)
            | (bytes[8 * w + 6].resize::<64>() << 48)
            | (bytes[8 * w + 7].resize::<64>() << 56);
    }
    words
}

/// `SHAPE`: units, lanes, log2 contexts, table mask.
const SHAPE: usize = VERIFY_UNITS | (LANES << 8) | ((CONTEXTS.trailing_zeros() as usize) << 12);

/// The cluster's logic.
#[allow(clippy::needless_range_loop, clippy::too_many_lines)]
#[kernel]
pub fn verify_cluster_kernel<const TABLE_MASK: usize>(
    clock_reset: ClockReset,
    input: ClusterInput,
    q: VerifyClusterQ<TABLE_MASK>,
) -> (ClusterOutput, VerifyClusterD<TABLE_MASK>) {
    let resetting = clock_reset.reset.any();
    let mut c = q.control;
    let args = q.control.args;
    c.ticks = q.control.ticks + b64(1);
    let ed = input.ed;

    // ------------------------------------------------ progress
    let mut all_done = true;
    let mut read_error = false;
    let mut write_error = false;
    let mut valid = b32(0);
    let mut checks = b32(0);
    let mut fails = b32(0);
    for u in 0..VERIFY_UNITS {
        let s = q.status[u];
        all_done = all_done && s.done;
        read_error = read_error || (s.error & b2(1)) != b2(0);
        write_error = write_error || (s.error & b2(2)) != b2(0);
        valid = valid + s.valid;
        checks = checks + s.cert_checks;
        fails = fails + s.cert_fails;
    }
    let key_bad = q.control.key_settled && ed.key_state == b2(3);
    let fault_bits: b32 = (if read_error { b32(1) } else { b32(0) })
        | (if write_error { b32(2) } else { b32(0) })
        | (if ed.internal_error { b32(4) } else { b32(0) })
        | (if key_bad { b32(8) } else { b32(0) });
    // Unit status arrives through delay lines; only trust `done` after a
    // start has had time to reach the units and come back.
    let settled_start = q.control.ticks - q.control.start_tick > b64(16);
    if q.control.running && all_done && q.control.key_settled && settled_start {
        c.running = false;
        c.done = true;
        c.done_unread = true;
        c.isr = true;
        c.done_tick = q.control.ticks;
    }

    // ------------------------------------------------ trusted key
    let mut key_words = [b64(0); 4];
    for w in 0..4 {
        key_words[w] = args.key[2 * w].resize::<64>() | (args.key[2 * w + 1].resize::<64>() << 32);
    }
    let load_key = q.control.running && !q.control.key_sent && ed.load_key_ready && !resetting;
    if load_key {
        c.key_sent = true;
    }
    if q.control.key_sent && !q.control.key_settled && (ed.key_state == b2(2) || ed.key_state == b2(3)) {
        c.key_settled = true;
        c.key_tick = q.control.ticks;
    }

    // ------------------------------------------------ certificate arbiter
    // Oldest-pointer round robin: the first unit at or after `next_unit`
    // with a request, while the core is ready and the key has settled.
    let mut pick_found = false;
    let mut pick = b3(0);
    for i in 0..VERIFY_UNITS {
        let u = VERIFY_UNITS - 1 - i;
        if q.requests[u].valid && b3(u as u128) >= q.control.next_unit {
            pick_found = true;
            pick = b3(u as u128);
        }
    }
    if !pick_found {
        for i in 0..VERIFY_UNITS {
            let u = VERIFY_UNITS - 1 - i;
            if q.requests[u].valid {
                pick_found = true;
                pick = b3(u as u128);
            }
        }
    }
    // One request register in front of the core: it loads when empty and
    // empties when the core takes it (a check is ~735 cycles, so issuing at
    // most every other clock costs nothing).
    if q.control.ed_valid && ed.ready {
        c.ed_valid = false;
    }
    let issue = pick_found && !q.control.ed_valid && q.control.key_settled && !resetting;
    let mut request = q.requests[0].data;
    for u in 0..VERIFY_UNITS {
        if pick == b3(u as u128) {
            request = q.requests[u].data;
        }
    }
    let mut held = q.control.ed_request;
    held.public_key = key_words;
    if issue {
        c.next_unit = if pick == b3((VERIFY_UNITS - 1) as u128) { b3(0) } else { pick + b3(1) };
        c.ed_valid = true;
        held.message = words64_kernel(request.commitment);
        held.signature = words64_kernel(request.signature);
        held.tag = (pick.resize::<16>() << 6) | request.entry.resize::<16>();
    }
    c.ed_request = held;

    // ------------------------------------------------ AXI-Lite write
    let axi = input.kernel.axi;
    if axi.aw_valid && !q.control.aw_have {
        c.aw_addr = axi.aw_addr;
        c.aw_have = true;
    }
    if axi.w_valid && !q.control.w_have {
        c.w_data = axi.w_data;
        c.w_have = true;
    }
    if q.control.b_valid && axi.b_ready {
        c.b_valid = false;
    }
    if q.control.aw_have && q.control.w_have && !q.control.b_valid {
        let a = q.control.aw_addr;
        let v = q.control.w_data;
        c.aw_have = false;
        c.w_have = false;
        c.b_valid = true;
        if a == b12(0x000) && (v & b32(1)) == b32(1) && !q.control.running && !q.control.done {
            c.running = true;
            c.start_tick = q.control.ticks;
        }
        if a == b12(0x004) {
            c.gie = (v & b32(1)) == b32(1);
        }
        if a == b12(0x008) {
            c.ier = (v & b32(1)) == b32(1);
        }
        if a == b12(0x00c) && (v & b32(1)) == b32(1) {
            c.isr = !q.control.isr;
        }
        if !q.control.running && !q.control.done {
            for u in 0..VERIFY_UNITS {
                if a == b12((ARG_RECORDS + 16 * u) as u128) || a == b12((ARG_RECORDS + 16 * u + 4) as u128) {
                    c.args.records[u] = set_half_kernel(args.records[u], v, a == b12((ARG_RECORDS + 16 * u + 4) as u128));
                }
                if a == b12((ARG_VERDICTS + 16 * u) as u128) || a == b12((ARG_VERDICTS + 16 * u + 4) as u128) {
                    c.args.verdicts[u] = set_half_kernel(args.verdicts[u], v, a == b12((ARG_VERDICTS + 16 * u + 4) as u128));
                }
            }
            if a == b12(ARG_COUNT as u128) {
                c.args.count = v;
            }
            for w in 0..8 {
                if a == b12((ARG_KEY + 4 * w) as u128) {
                    c.args.key[w] = v;
                }
            }
        }
    }

    // ------------------------------------------------ AXI-Lite read
    if q.control.r_valid && axi.r_ready {
        c.r_valid = false;
    }
    let ar_ready = !q.control.r_valid;
    if axi.ar_valid && ar_ready {
        let a = axi.ar_addr;
        let mut value = b32(0);
        if a == b12(0x000) {
            value = (if q.control.running { b32(1) } else { b32(0) })
                | (if q.control.done_unread { b32(2) } else { b32(0) })
                | (if !q.control.running { b32(4) } else { b32(0) })
                | (if q.control.done_unread { b32(8) } else { b32(0) });
            c.done_unread = false;
        }
        if a == b12(0x004) {
            value = if q.control.gie { b32(1) } else { b32(0) };
        }
        if a == b12(0x008) {
            value = if q.control.ier { b32(1) } else { b32(0) };
        }
        if a == b12(0x00c) {
            value = if q.control.isr { b32(1) } else { b32(0) };
        }
        if a == b12(REG_MAGIC as u128) {
            value = MAGIC;
        }
        if a == b12(REG_ABI as u128) {
            value = ABI_VERSION;
        }
        if a == b12(REG_SHAPE as u128) {
            value = b32((SHAPE | (TABLE_MASK << 16)) as u128);
        }
        if a == b12(REG_FAULT as u128) {
            value = fault_bits;
        }
        if a == b12(REG_TICKS as u128) {
            value = q.control.ticks.resize();
            c.ticks_hi = (q.control.ticks >> 32).resize();
        }
        if a == b12((REG_TICKS + 4) as u128) {
            value = q.control.ticks_hi;
        }
        if a == b12(REG_START_TICK as u128) {
            value = q.control.start_tick.resize();
        }
        if a == b12((REG_START_TICK + 4) as u128) {
            value = (q.control.start_tick >> 32).resize();
        }
        if a == b12(REG_DONE_TICK as u128) {
            value = q.control.done_tick.resize();
        }
        if a == b12((REG_DONE_TICK + 4) as u128) {
            value = (q.control.done_tick >> 32).resize();
        }
        if a == b12(REG_KEY_TICK as u128) {
            value = q.control.key_tick.resize();
        }
        if a == b12((REG_KEY_TICK + 4) as u128) {
            value = (q.control.key_tick >> 32).resize();
        }
        if a == b12(REG_VALID as u128) {
            value = valid;
        }
        if a == b12(REG_CERT_CHECKS as u128) {
            value = checks;
        }
        if a == b12(REG_CERT_FAILS as u128) {
            value = fails;
        }
        for u in 0..VERIFY_UNITS {
            if a == b12((REG_RETIRED + 4 * u) as u128) {
                value = q.status[u].retired;
            }
        }
        c.r_valid = true;
        c.r_data = value;
    }

    // ------------------------------------------------ units and their links
    let result_unit: b3 = (ed.result_tag >> 6).resize();
    let mut units = [UnitInput {
        run: false,
        records_base: b64(0),
        verdicts_base: b64(0),
        count: b32(0),
        records: input.kernel.records[0],
        verdicts: input.kernel.verdicts[0],
        cert_taken: false,
        cert_result: CertResult::default(),
    }; VERIFY_UNITS];
    let mut ar = [PipeIn::<ArItem> {
        data: ArItem { araddr: b64(0), arlen: b8(0) },
        valid: false,
        taken: false,
    }; VERIFY_UNITS];
    let mut r = [RItem {
        rvalid: false,
        rdata: [b8(0); 64],
        rresp: b2(0),
        rlast: false,
    }; VERIFY_UNITS];
    let mut aw = [PipeIn::<AwItem> {
        data: AwItem { awaddr: b64(0), awlen: b8(0) },
        valid: false,
        taken: false,
    }; VERIFY_UNITS];
    let mut w = [PipeIn::<WItem> {
        data: WItem { wdata: [b8(0); 64], wlast: false },
        valid: false,
        taken: false,
    }; VERIFY_UNITS];
    let mut b = [BItem { bvalid: false, bresp: b2(0) }; VERIFY_UNITS];
    let mut to_unit = [UnitControl {
        run: q.control.running,
        records_base: args.records[0],
        verdicts_base: args.verdicts[0],
        count: args.count,
    }; VERIFY_UNITS];
    let mut requests = [PipeIn::<CertRequest> {
        data: q.units[0].cert_request,
        valid: false,
        taken: false,
    }; VERIFY_UNITS];
    let mut results = [CertResult::default(); VERIFY_UNITS];
    let mut status = [UnitStatus {
        retired: b32(0),
        valid: b32(0),
        cert_checks: b32(0),
        cert_fails: b32(0),
        done: false,
        error: b2(0),
    }; VERIFY_UNITS];
    let mut records = [input.kernel.records[0]; VERIFY_UNITS];
    let mut verdicts = [input.kernel.verdicts[0]; VERIFY_UNITS];
    let mut records_out = [q.units[0].records; VERIFY_UNITS];
    let mut verdicts_out = [q.units[0].verdicts; VERIFY_UNITS];
    for u in 0..VERIFY_UNITS {
        let unit = q.units[u];
        let port_r = input.kernel.records[u];
        let port_w = input.kernel.verdicts[u];
        // Unit side.
        records[u] = ReadResponse {
            arready: q.ar[u].ready,
            rvalid: q.r[u].rvalid,
            rdata: q.r[u].rdata,
            rresp: q.r[u].rresp,
            rlast: q.r[u].rlast,
        };
        verdicts[u] = WriteResponse {
            awready: q.aw[u].ready,
            wready: q.w[u].ready,
            bvalid: q.b[u].bvalid,
            bresp: q.b[u].bresp,
        };
        let control = q.to_unit[u];
        units[u] = UnitInput {
            run: control.run,
            records_base: control.records_base,
            verdicts_base: control.verdicts_base,
            count: control.count,
            records: records[u],
            verdicts: verdicts[u],
            cert_taken: unit.cert_request.valid && q.requests[u].ready,
            cert_result: q.results[u],
        };
        // Links toward HBM.
        ar[u] = PipeIn::<ArItem> {
            data: ArItem {
                araddr: unit.records.araddr,
                arlen: unit.records.arlen,
            },
            valid: unit.records.arvalid,
            taken: q.ar[u].valid && port_r.arready,
        };
        aw[u] = PipeIn::<AwItem> {
            data: AwItem {
                awaddr: unit.verdicts.awaddr,
                awlen: unit.verdicts.awlen,
            },
            valid: unit.verdicts.awvalid,
            taken: q.aw[u].valid && port_w.awready,
        };
        w[u] = PipeIn::<WItem> {
            data: WItem {
                wdata: unit.verdicts.wdata,
                wlast: unit.verdicts.wlast,
            },
            valid: unit.verdicts.wvalid,
            taken: q.w[u].valid && port_w.wready,
        };
        records_out[u] = ReadRequest {
            arvalid: q.ar[u].valid,
            araddr: q.ar[u].data.araddr,
            arlen: q.ar[u].data.arlen,
            rready: true,
        };
        verdicts_out[u] = WriteRequest {
            awvalid: q.aw[u].valid,
            awaddr: q.aw[u].data.awaddr,
            awlen: q.aw[u].data.awlen,
            wvalid: q.w[u].valid,
            wdata: q.w[u].data.wdata,
            wlast: q.w[u].data.wlast,
            bready: true,
        };
        // Links back from HBM.
        r[u] = RItem {
            rvalid: port_r.rvalid,
            rdata: port_r.rdata,
            rresp: port_r.rresp,
            rlast: port_r.rlast,
        };
        b[u] = BItem {
            bvalid: port_w.bvalid,
            bresp: port_w.bresp,
        };
        // Control, certificates, status.
        to_unit[u] = UnitControl {
            run: q.control.running,
            records_base: args.records[u],
            verdicts_base: args.verdicts[u],
            count: args.count,
        };
        requests[u] = PipeIn::<CertRequest> {
            data: unit.cert_request,
            valid: unit.cert_request.valid,
            taken: issue && pick == b3(u as u128),
        };
        results[u] = CertResult {
            valid: ed.result_valid && result_unit == b3(u as u128),
            entry: ed.result_tag.resize(),
            ok: ed.result_ok,
        };
        status[u] = UnitStatus {
            retired: unit.retired,
            valid: unit.valid,
            cert_checks: unit.cert_checks,
            cert_fails: unit.cert_fails,
            done: unit.done,
            error: unit.error,
        };
    }
    let d = VerifyClusterD::<TABLE_MASK> {
        control: c,
        units,
        ar,
        r,
        aw,
        w,
        b,
        to_unit,
        requests,
        results,
        status,
    };
    (
        ClusterOutput {
            kernel: VerifyEngineOutput {
                axi: AxiLiteOut {
                    aw_ready: !q.control.aw_have,
                    w_ready: !q.control.w_have,
                    b_valid: q.control.b_valid,
                    b_resp: b2(0),
                    ar_ready,
                    r_valid: q.control.r_valid,
                    r_data: q.control.r_data,
                    r_resp: b2(0),
                    interrupt: q.control.gie && q.control.ier && q.control.isr,
                },
                records: records_out,
                verdicts: verdicts_out,
            },
            ed: EdCommand {
                valid: q.control.ed_valid,
                message: q.control.ed_request.message,
                signature: q.control.ed_request.signature,
                public_key: q.control.ed_request.public_key,
                tag: q.control.ed_request.tag,
                load_key_valid: load_key,
            },
        },
        d,
    )
}

const _: () = assert!(VERIFY_UNITS <= 8, "unit numbers are 3 bits");

// ------------------------------------------------------------------- kernel

use rhdl_ed25519_live::sha_ring::{ShaDone, ShaRingOut};
use rhdl_ed25519_live::verify_core::{KnownKeyVerifyCore, VerifyIn};
use rhdl_ed25519_live::wire::{ScalarWords, VerifyRequest, Words512};

/// The Ed25519 verify core of the kernel: one verify machine, its own
/// SHA-512 ring, one scalar ring (`1,1,1,0`), sized for one certificate
/// check per 128 DSig verifications.
pub type CertCore = KnownKeyVerifyCore<1, 1, 1, 0>;

/// The verifier card kernel: [`VerifyCluster`] plus the Ed25519 verify core.
#[derive(Clone, Debug, Synchronous, SynchronousDQ)]
pub struct VerifyEngine<const TABLE_MASK: usize> {
    /// Registers, units and the certificate arbiter.
    cluster: VerifyCluster<TABLE_MASK>,
    /// Strict Ed25519 verification of batch certificates.
    ed: CertCore,
}

impl<const TABLE_MASK: usize> Default for VerifyEngine<TABLE_MASK> {
    /// Power-on: IDLE, no key loaded.
    fn default() -> Self {
        Self {
            cluster: VerifyCluster::default(),
            ed: CertCore::default(),
        }
    }
}

impl<const TABLE_MASK: usize> SynchronousIO for VerifyEngine<TABLE_MASK> {
    type I = VerifyEngineInput;
    type O = VerifyEngineOutput;
    type Kernel = verify_engine_kernel<TABLE_MASK>;
}

/// Wires the cluster to the Ed25519 core.
#[kernel]
pub fn verify_engine_kernel<const TABLE_MASK: usize>(
    _clock_reset: ClockReset,
    input: VerifyEngineInput,
    q: VerifyEngineQ<TABLE_MASK>,
) -> (VerifyEngineOutput, VerifyEngineD<TABLE_MASK>) {
    let ed = q.ed;
    let command = q.cluster.ed;
    let d = VerifyEngineD::<TABLE_MASK> {
        cluster: ClusterInput {
            kernel: input,
            ed: EdStatus {
                ready: ed.ready,
                result_valid: ed.valid,
                result_ok: ed.ok,
                result_tag: ed.tag,
                load_key_ready: ed.load_key_ready,
                key_state: ed.key_state[0],
                internal_error: ed.internal_error,
            },
        },
        ed: VerifyIn {
            valid: command.valid,
            request: VerifyRequest {
                message: Words512 { words: command.message },
                public_key: ScalarWords { words: command.public_key },
                signature: Words512 { words: command.signature },
                tag: command.tag,
            },
            load_key_valid: command.load_key_valid,
            load_key: ScalarWords { words: command.public_key },
            load_slot: b3(0).resize(),
            sha_ext: ShaRingOut {
                ready: false,
                done: ShaDone {
                    valid: false,
                    tag: b16(0),
                    state: [b64(0); 8],
                },
            },
        },
    };
    (q.cluster.kernel, d)
}