diff --git a/hw/dv/common/models/npu.py b/hw/dv/common/models/npu.py
new file mode 100644
index 0000000..ddc94f0
--- /dev/null
+++ b/hw/dv/common/models/npu.py
@@ -0,0 +1,700 @@
+"""Golden reference model for the `npu` module.
+
+Spec: docs/spec/npu.md (requirements NPU-01 through NPU-23), read against
+docs/spec/soc_1.md for system context (memory map, IRQ map, bus). Pure
+Python, no cocotb / simulator dependency — importable and runnable
+standalone (see `__main__` below), and the single source of "expected
+value" for the npu DV suite (hw/dv/npu/). Per the verif-architect
+clean-room rule (/CLAUDE.md Iron Rule 2), this model was written from the
+spec TEXT only, never from hw/rtl/.
+
+Two API layers, per the issue's ask:
+
+1. Descriptor-level / CSR-mirroring: `write_csr(offset, value)` /
+   `read_csr(offset)`, register offsets and reset values exactly per
+   spec §3 — what a cocotb Wishbone driver calls after translating a WB
+   write/read transaction.
+2. Per-step, lock-step interface for the weight-stream ingress port:
+   `ws_ready` (mirrors `o_ws_ready`) and `step(ws_valid, ws_data)` (mirrors
+   one rising `clk` edge with `i_ws_valid`/`i_ws_data` sampled) — a cocotb
+   bench drives this once per clock edge alongside the DUT.
+
+Bit-exactness core (§4.1, NPU-09..12): `to_s32`, `requantize` — these are
+the functions RTL bit-exactness is ultimately judged against.
+
+Spec ambiguities found while implementing (filed here per the
+verif-architect method — not resolved by picking an interpretation):
+
+  A1. §3.6 does not define an argmax tie-break rule (two channels with an
+      equal winning requantised value). This model keeps the
+      lowest-index winner (strict `>` compare, first-seen wins).
+  A2. §3.1 does not define CTRL.GO and CTRL.ABORT written as 1 in the same
+      write. This model applies ABORT first (forcing IDLE/BUSY=0), then
+      evaluates GO's NPU-21 checks against the resulting state — i.e. an
+      abort-then-dispatch-in-the-same-cycle reading. An equally defensible
+      reading exists (GO ignored whenever ABORT is also set); RTL intake
+      should confirm which one hardware implements.
+  A3. §4.3's `TAIL` state is documented only as "fixed latency, a few
+      cycles" with no exact count. This model does not claim a specific
+      cycle count: `step()` treats `TAIL` as taking exactly one extra
+      step() call before `DONE`. DV must not assert an exact TAIL cycle
+      count against this model — only NPU-18's ordering guarantee
+      (`DONE` never before the last weight byte is consumed) is
+      spec-backed.
+  A4. Neither npu.md nor soc_1.md defines how the *first* activation
+      vector (e.g. a token embedding, before any normal-mode NPU op has
+      run to populate the SRAM via NPU-13 writeback) gets into the 2 kB
+      activation SRAM in the first place. The CSR window is
+      "CSR/descriptor access only" (§1) with no data-write register, and
+      there is no third bus/port into this SRAM in §2. This model exposes
+      `act_sram` as a directly-writable bytearray for test setup, but that
+      is a test-harness convenience, not a modeled hardware interface —
+      flagged for chief-architect / npu.md revision.
+"""
+
+from __future__ import annotations
+
+from collections import deque
+from typing import Iterable, Sequence
+
+
+# --------------------------------------------------------------------------
+# Bit-exact arithmetic core (§4.1, NPU-09 through NPU-12)
+# --------------------------------------------------------------------------
+
+def s8(byte: int) -> int:
+    """Interpret an unsigned byte (0..255) as signed int8 (-128..127)."""
+    byte &= 0xFF
+    return byte - 256 if byte >= 128 else byte
+
+
+def to_s32(value: int) -> int:
+    """Two's-complement-wrap an arbitrary Python int into signed 32 bits.
+
+    Models the physical 32-bit accumulator register (NPU-09): every add
+    wraps like ordinary two's-complement hardware, regardless of whether
+    the workload-legal `K <= 4096` bound (which this spec guarantees never
+    actually overflows) holds — the wrap behavior is a property of the
+    register, not a special case gated on K.
+    """
+    value &= 0xFFFF_FFFF
+    return value - 0x1_0000_0000 if value >= 0x8000_0000 else value
+
+
+def _round_half_away_from_zero(t: int, s: int) -> int:
+    """NPU-11's rounding rule, symbol-for-symbol from the spec pseudocode."""
+    if s == 0:
+        return t
+    half = 1 << (s - 1)
+    if t >= 0:
+        return (t + half) >> s
+    return -((-t + half) >> s)
+
+
+def sat8(value: int) -> int:
+    """NPU-12: clamp to the signed int8 range."""
+    if value > 127:
+        return 127
+    if value < -128:
+        return -128
+    return value
+
+
+def requantize(acc: int, scale_m: int, scale_shift: int) -> int:
+    """NPU-11/NPU-12: `sat8(round_half_away_from_zero(acc * M, s))`.
+
+    `acc` is the lane's final 32-bit signed accumulator; `scale_m` is the
+    unsigned 16-bit `SCALE_M`; `scale_shift` is the unsigned 5-bit
+    `SCALE_SHIFT`. `t = acc * scale_m` is exact Python-integer arithmetic
+    (fits the spec's 48-bit-signed intermediate with no truncation — 48
+    bits is sized to hold the exact 32-bit-signed x 16-bit-unsigned
+    product, not a narrowing point).
+    """
+    acc = to_s32(acc)
+    scale_m &= 0xFFFF
+    scale_shift &= 0x1F
+    t = acc * scale_m
+    rounded = _round_half_away_from_zero(t, scale_shift)
+    return sat8(rounded)
+
+
+# --------------------------------------------------------------------------
+# Weight-stream byte ordering (§2.3 NPU-08, §4.2 NPU-14/NPU-15/NPU-16)
+# --------------------------------------------------------------------------
+
+def pack_weight_stream(
+    weights: Sequence[Sequence[int]], n_len: int, c: int = 8, ws_width: int = 32
+) -> list[int]:
+    """Serialize a K x N weight matrix into the ingress-port word stream.
+
+    `weights[k][n]` is the raw byte (0..255, interpreted signed per s8) for
+    reduction index `k`, output channel `n`. Produces the flattened,
+    k-major/channel-minor, low-byte-first-packed word list NPU-08/NPU-14
+    define: for each output-channel group `g = 0..n_len/c-1`, for each `k`,
+    the `c` bytes `w[k][g*c .. g*c+c-1]` consecutively, before any byte for
+    `k+1`; then packed `ws_width/8` bytes per word, byte `i` at bits
+    `[8i+7:8i]`.
+
+    This is the inverse of what `NpuModel.step()` consumes — used both to
+    drive a DUT's ingress port and, in this file's self-check, to drive
+    `NpuModel` itself so both act on the identical stream.
+    """
+    if n_len % c != 0:
+        raise ValueError(f"n_len={n_len} must be a multiple of c={c} (NPU-21 N_NOT_MULTIPLE_OF_C)")
+    k_len = len(weights)
+    bytes_per_word = ws_width // 8
+    flat: list[int] = []
+    for g in range(n_len // c):
+        for k in range(k_len):
+            row = weights[k]
+            for ch in range(c):
+                flat.append(row[g * c + ch] & 0xFF)
+    if len(flat) % bytes_per_word != 0:
+        raise ValueError(
+            f"K*N ({len(flat)}) must be a multiple of ws_width/8 ({bytes_per_word}) "
+            "for this helper's simple word packing"
+        )
+    words = []
+    for i in range(0, len(flat), bytes_per_word):
+        word = 0
+        for j in range(bytes_per_word):
+            word |= flat[i + j] << (8 * j)
+        words.append(word)
+    return words
+
+
+# --------------------------------------------------------------------------
+# CSR-level descriptor model (§3)
+# --------------------------------------------------------------------------
+
+class NpuModel:
+    """Register- and cycle-level golden model of `npu` (docs/spec/npu.md).
+
+    Construction implements the reset state (NPU-01, §3's reset column):
+    every CSR resets to 0, the sequencer resets to `IDLE`; the activation
+    SRAM's *contents* are explicitly NOT reset (NPU-01: a hard macro, data
+    survives reset) — only `act_sram_bytes`-sized storage is allocated once
+    at construction and left untouched by `reset()`.
+    """
+
+    C = 8
+    ACT_SRAM_BYTES = 2048
+    FIFO_DEPTH = 2
+
+    REG_CTRL = 0x00
+    REG_STATUS = 0x04
+    REG_ERR_CODE = 0x08
+    REG_K_LEN = 0x0C
+    REG_N_LEN = 0x10
+    REG_ACT_BASE = 0x14
+    REG_OUT_BASE = 0x18
+    REG_SCALE_M = 0x1C
+    REG_SCALE_SHIFT = 0x20
+    REG_RESULT_IDX = 0x24
+    REG_RESULT_VAL = 0x28
+
+    _WRITABLE = {
+        REG_CTRL, REG_K_LEN, REG_N_LEN, REG_ACT_BASE, REG_OUT_BASE,
+        REG_SCALE_M, REG_SCALE_SHIFT,
+    }
+    _KNOWN = _WRITABLE | {REG_STATUS, REG_ERR_CODE, REG_RESULT_IDX, REG_RESULT_VAL}
+
+    ERR_NONE = 0
+    ERR_K_ZERO = 1
+    ERR_N_ZERO = 2
+    ERR_N_NOT_MULTIPLE_OF_C = 3
+    ERR_ACT_RANGE = 4
+    ERR_OUT_RANGE = 5
+    ERR_BUSY_REJECT = 6
+
+    def __init__(self, ws_width: int = 32):
+        if ws_width <= 0 or ws_width % 8 != 0 or (self.C * 8) % ws_width != 0:
+            raise ValueError(
+                f"ws_width={ws_width!r} must be a positive multiple of 8 dividing "
+                f"C*8={self.C * 8} bits (§2.4)"
+            )
+        self.ws_width = ws_width
+        self.act_sram = bytearray(self.ACT_SRAM_BYTES)
+        self.reset()
+
+    def reset(self) -> None:
+        """Apply `rst_n` (NPU-01): every CSR/sequencer flop -> its §3 reset
+        value / IDLE. Activation SRAM contents are untouched (see class
+        docstring).
+        """
+        self.mode = 0
+        self.busy = 0
+        self.done = 0
+        self.err = 0
+        self.err_code = self.ERR_NONE
+        self.k_len = 0
+        self.n_len = 0
+        self.act_base = 0
+        self.out_base = 0
+        self.scale_m = 0
+        self.scale_shift = 0
+        self.result_idx = 0
+        self.result_val = 0
+        self._reset_sequencer()
+
+    def _reset_sequencer(self) -> None:
+        self.state = "IDLE"
+        self._fifo: deque[int] = deque()
+        self._group_idx = 0
+        self._group_pos = 0
+        self._accs = [0] * self.C
+
+    # -- IRQ mirrors (§2.5) --------------------------------------------
+    @property
+    def irq_done(self) -> int:
+        return self.done
+
+    @property
+    def irq_err(self) -> int:
+        return self.err
+
+    # -- CSR access (§3, NPU-02..05) ------------------------------------
+    def read_csr(self, offset: int) -> int:
+        """NPU-05: unmapped offsets read 0x0000_0000."""
+        if offset == self.REG_CTRL:
+            return (self.mode & 1) << 1  # GO/ABORT always read back 0 (§3.1)
+        if offset == self.REG_STATUS:
+            return (self.busy & 1) | ((self.done & 1) << 1) | ((self.err & 1) << 2)
+        if offset == self.REG_ERR_CODE:
+            return self.err_code & 0xFFFF_FFFF
+        if offset == self.REG_K_LEN:
+            return self.k_len & 0xFFFF
+        if offset == self.REG_N_LEN:
+            return self.n_len & 0xFFFF
+        if offset == self.REG_ACT_BASE:
+            return self.act_base & 0x7FF
+        if offset == self.REG_OUT_BASE:
+            return self.out_base & 0x7FF
+        if offset == self.REG_SCALE_M:
+            return self.scale_m & 0xFFFF
+        if offset == self.REG_SCALE_SHIFT:
+            return self.scale_shift & 0x1F
+        if offset == self.REG_RESULT_IDX:
+            return self.result_idx & 0xFFFF
+        if offset == self.REG_RESULT_VAL:
+            return self.result_val & 0xFFFF_FFFF
+        return 0x0000_0000
+
+    def write_csr(self, offset: int, value: int) -> None:
+        """NPU-04: full-word write regardless of byte-select. NPU-05:
+        writes to unmapped offsets are silently ignored.
+        """
+        value &= 0xFFFF_FFFF
+        if offset == self.REG_K_LEN:
+            self.k_len = value & 0xFFFF
+        elif offset == self.REG_N_LEN:
+            self.n_len = value & 0xFFFF
+        elif offset == self.REG_ACT_BASE:
+            self.act_base = value & 0x7FF
+        elif offset == self.REG_OUT_BASE:
+            self.out_base = value & 0x7FF
+        elif offset == self.REG_SCALE_M:
+            self.scale_m = value & 0xFFFF
+        elif offset == self.REG_SCALE_SHIFT:
+            self.scale_shift = value & 0x1F
+        elif offset == self.REG_CTRL:
+            self._write_ctrl(value)
+        # else: unmapped/RO offset, silently ignored (NPU-05)
+
+    def _write_ctrl(self, value: int) -> None:
+        go = value & 0x1
+        self.mode = (value >> 1) & 0x1
+        abort = (value >> 2) & 0x1
+
+        if abort:
+            # A2: ABORT applied first; NPU-19's "regardless of current
+            # state" — no-op if already IDLE falls out naturally.
+            self._reset_sequencer()
+            self.busy = 0
+
+        if not go:
+            return
+
+        # NPU-21: priority-ordered malformed-descriptor checks, evaluated
+        # against the register state as it stands after this same write
+        # (including this write's own MODE/ABORT bits) — first match wins.
+        checks = [
+            (self.k_len == 0, self.ERR_K_ZERO),
+            (self.n_len == 0, self.ERR_N_ZERO),
+            (self.n_len % self.C != 0, self.ERR_N_NOT_MULTIPLE_OF_C),
+            (self.act_base + self.k_len > self.ACT_SRAM_BYTES, self.ERR_ACT_RANGE),
+            (self.mode == 0 and self.out_base + self.n_len > self.ACT_SRAM_BYTES, self.ERR_OUT_RANGE),
+            (self.busy == 1, self.ERR_BUSY_REJECT),
+        ]
+        for bad, code in checks:
+            if bad:
+                self.err = 1
+                self.err_code = code
+                return
+
+        # Dispatch (NPU-21 "NONE": IDLE -> RUN, §4.3).
+        self.err = 0
+        self.err_code = self.ERR_NONE
+        self.done = 0
+        self.busy = 1
+        self._group_idx = 0
+        self._group_pos = 0
+        self._accs = [0] * self.C
+        self.state = "RUN"
+
+    # -- Weight-stream ingress + sequencer (§2.3, §4.2, §4.3) -----------
+    @property
+    def ws_ready(self) -> int:
+        """NPU-07: low whenever the 2-entry FIFO holds 2 unconsumed
+        entries, high otherwise.
+        """
+        return int(len(self._fifo) < self.FIFO_DEPTH)
+
+    def step(self, ws_valid: int, ws_data: int) -> dict:
+        """Advance the model by exactly one rising `clk` edge.
+
+        Mirrors what a cocotb bench samples/drives at the DUT boundary
+        each edge: `ws_valid`/`ws_data` are `i_ws_valid`/`i_ws_data` as
+        sampled at this edge; the returned dict mirrors `o_ws_ready`
+        (sampled *before* this edge's push, matching a synchronous FIFO:
+        a word pushed this cycle is not poppable until a later step) plus
+        `busy`/`done`/`err` for convenience.
+
+        One `step()` call: pops and fully unpacks at most one
+        `ws_width`-bit FIFO word (NPU-14/NPU-15 — the sequencer advances
+        lane accumulators as bytes are unpacked from the FIFO), then (if
+        `ws_ready` was high and `ws_valid` is set) pushes the new word.
+        Pop-before-push, as in a real synchronous FIFO.
+        """
+        ready_before = self.ws_ready
+
+        if self.state == "RUN" and self._fifo:
+            word = self._fifo.popleft()
+            self._consume_word(word)
+        elif self.state == "TAIL":
+            # A3: TAIL's exact latency is spec-unspecified ("a few
+            # cycles"); this model takes exactly one extra step().
+            self.state = "DONE"
+        elif self.state == "DONE":
+            self.done = 1
+            self.busy = 0
+            self.state = "IDLE"
+
+        if ready_before and ws_valid:
+            self._fifo.append(ws_data & ((1 << self.ws_width) - 1))
+
+        return {
+            "ws_ready": ready_before,
+            "busy": self.busy,
+            "done": self.done,
+            "err": self.err,
+        }
+
+    def _consume_word(self, word: int) -> None:
+        nbytes = self.ws_width // 8
+        group_size = self.k_len * self.C
+        for i in range(nbytes):
+            byte = (word >> (8 * i)) & 0xFF
+            k = self._group_pos // self.C
+            c = self._group_pos % self.C
+            x = s8(self.act_sram[self.act_base + k])
+            w = s8(byte)
+            self._accs[c] = to_s32(self._accs[c] + x * w)
+            self._group_pos += 1
+            if self._group_pos == group_size:
+                self._finish_group()
+
+    def _finish_group(self) -> None:
+        g = self._group_idx
+        for c in range(self.C):
+            n = g * self.C + c
+            out = requantize(self._accs[c], self.scale_m, self.scale_shift)
+            if self.mode == 0:
+                self.act_sram[self.out_base + n] = out & 0xFF
+            else:
+                # A1: strict '>' -> first (lowest-index) max wins on ties.
+                if n == 0 or out > self.result_val_signed:
+                    self.result_idx = n
+                    self.result_val = out & 0xFFFF_FFFF
+        self._group_pos = 0
+        self._accs = [0] * self.C
+        self._group_idx += 1
+        if self._group_idx * self.C >= self.n_len:
+            self.state = "TAIL"
+
+    @property
+    def result_val_signed(self) -> int:
+        v = self.result_val & 0xFF
+        return s8(v)
+
+    # -- Convenience: one-shot descriptor dispatch -----------------------
+    def dispatch_and_run(
+        self,
+        k_len: int,
+        n_len: int,
+        act_base: int,
+        out_base: int,
+        scale_m: int,
+        scale_shift: int,
+        mode: int,
+        weights: Sequence[Sequence[int]],
+        max_cycles: int = 10_000_000,
+    ) -> None:
+        """Test-harness convenience built entirely from `write_csr`/`step`
+        (no separate arithmetic path): programs the descriptor, dispatches
+        it, and clocks `step()` with an always-ready weight source until
+        the sequencer returns to `IDLE`. Raises if a malformed-descriptor
+        error is raised on dispatch, or if `max_cycles` is exhausted.
+        """
+        self.write_csr(self.REG_K_LEN, k_len)
+        self.write_csr(self.REG_N_LEN, n_len)
+        self.write_csr(self.REG_ACT_BASE, act_base)
+        self.write_csr(self.REG_OUT_BASE, out_base)
+        self.write_csr(self.REG_SCALE_M, scale_m)
+        self.write_csr(self.REG_SCALE_SHIFT, scale_shift)
+        self.write_csr(self.REG_CTRL, (mode & 1) << 1 | 0x1)
+        if self.err:
+            raise RuntimeError(f"dispatch rejected, ERR_CODE={self.err_code}")
+
+        words = iter(pack_weight_stream(weights, n_len, self.C, self.ws_width))
+        pending = None
+        for _ in range(max_cycles):
+            if pending is None:
+                pending = next(words, None)
+            valid = pending is not None
+            data = pending if pending is not None else 0
+            info = self.step(valid, data)
+            if valid and info["ws_ready"]:
+                pending = None
+            if self.state == "IDLE" and self.done:
+                return
+        raise RuntimeError("dispatch_and_run: max_cycles exhausted without DONE")
+
+
+# --------------------------------------------------------------------------
+# Self-check
+# --------------------------------------------------------------------------
+
+def _self_check() -> bool:
+    ok = True
+
+    def check(label: str, got, want) -> None:
+        nonlocal ok
+        status = "PASS" if got == want else "FAIL"
+        if got != want:
+            ok = False
+        print(f"[{status}] {label}: got={got!r} want={want!r}")
+
+    # --- NPU-11 rounding, hand-computed edge cases ---
+    # s=0: no shift/rounding at all.
+    check("round s=0 passthrough", _round_half_away_from_zero(1234, 0), 1234)
+    # s=1, t=5 -> half=1 -> (5+1)>>1 = 3 (away from zero, ties round up).
+    check("round half-up, t=5,s=1", _round_half_away_from_zero(5, 1), 3)
+    # s=1, t=4 -> half=1 -> (4+1)>>1 = 2 (exact tie: 4/2=2.0, +0.5 rounds to 2 via floor(2.5)=2... check by hand)
+    check("round half tie, t=4,s=1", _round_half_away_from_zero(4, 1), 2)
+    # s=1, t=-5 -> -((5+1)>>1) = -3 (away from zero on the negative side too).
+    check("round half-away-negative, t=-5,s=1", _round_half_away_from_zero(-5, 1), -3)
+    # s=3, t=12 -> half=4 -> (12+4)>>3 = 2
+    check("round s=3, t=12", _round_half_away_from_zero(12, 3), 2)
+
+    # --- NPU-12 saturation boundaries ---
+    check("sat8 in-range top", sat8(127), 127)
+    check("sat8 in-range bottom", sat8(-128), -128)
+    check("sat8 clamps above", sat8(128), 127)
+    check("sat8 clamps below", sat8(-129), -128)
+    check("sat8 clamps far above", sat8(999999), 127)
+
+    # --- requantize: worked example combining rounding + saturation ---
+    # acc=100, M=200, s=4: t=20000, half=8, (20000+8)>>4=1250 -> saturate to 127.
+    check("requantize saturates positive", requantize(100, 200, 4), 127)
+    # acc=-100, M=200, s=4: t=-20000 -> -((20000+8)>>4) = -1250 -> saturate -128.
+    check("requantize saturates negative", requantize(-100, 200, 4), -128)
+    # acc=10, M=13, s=2: t=130, half=2, (130+2)>>2=33 -> saturate to 33 (in range).
+    check("requantize in-range", requantize(10, 13, 2), 33)
+    # M=0: forced-zero output regardless of acc (still exercises round/sat trivially).
+    check("requantize M=0 -> 0", requantize(999, 0, 5), 0)
+    # s=0 passthrough then saturate.
+    check("requantize s=0 passthrough+saturate", requantize(200, 1, 0), 127)
+
+    # --- to_s32 two's-complement wrap ---
+    check("to_s32 max positive", to_s32(0x7FFF_FFFF), 2147483647)
+    check("to_s32 wraps at boundary", to_s32(0x8000_0000), -2147483648)
+    check("to_s32 wraps negative-to-positive", to_s32(-0x8000_0001), 2147483647)
+
+    # --- pack_weight_stream: small hand-traced example, K=2,N=8 (C=8, one group) ---
+    W = [[i for i in range(8)], [10 + i for i in range(8)]]  # k=0 row, k=1 row
+    words = pack_weight_stream(W, n_len=8, c=8, ws_width=32)
+    # flat byte order: k=0 c=0..7 (0..7), k=1 c=0..7 (10..17); 4 bytes/word.
+    want_flat = [0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 14, 15, 16, 17]
+    want_words = [
+        want_flat[0] | want_flat[1] << 8 | want_flat[2] << 16 | want_flat[3] << 24,
+        want_flat[4] | want_flat[5] << 8 | want_flat[6] << 16 | want_flat[7] << 24,
+        want_flat[8] | want_flat[9] << 8 | want_flat[10] << 16 | want_flat[11] << 24,
+        want_flat[12] | want_flat[13] << 8 | want_flat[14] << 16 | want_flat[15] << 24,
+    ]
+    check("pack_weight_stream K=2,N=8 word count", len(words), 4)
+    check("pack_weight_stream K=2,N=8 words", words, want_words)
+
+    # --- End-to-end small GEMV, normal mode, hand-computed ---
+    # K=2, N=8 (one group of C=8), activations x = [3, -1] (s8), weights as
+    # above (all positive, small). acc[c] = x0*W[0][c] + x1*W[1][c].
+    # M=1, s=0 (identity passthrough of the raw sum, still through sat8).
+    m = NpuModel(ws_width=32)
+    m.act_sram[0] = 3 & 0xFF   # x[0] = 3
+    m.act_sram[1] = (-1) & 0xFF  # x[1] = -1 (as s8 byte 0xFF)
+    m.dispatch_and_run(
+        k_len=2, n_len=8, act_base=0, out_base=100,
+        scale_m=1, scale_shift=0, mode=0, weights=W,
+    )
+    expected_out = []
+    for c in range(8):
+        acc = 3 * W[0][c] + (-1) * W[1][c]
+        expected_out.append(sat8(acc) & 0xFF)
+    got_out = list(m.act_sram[100:108])
+    check("end-to-end GEMV normal-mode output bytes", got_out, expected_out)
+    check("end-to-end GEMV STATUS.DONE set", m.done, 1)
+    check("end-to-end GEMV STATUS.BUSY clear", m.busy, 0)
+    check("end-to-end GEMV STATUS.ERR clear", m.err, 0)
+
+    # --- Argmax mode, same shape, verify RESULT_IDX/RESULT_VAL ---
+    m2 = NpuModel(ws_width=32)
+    m2.act_sram[0] = 3 & 0xFF
+    m2.act_sram[1] = (-1) & 0xFF
+    m2.dispatch_and_run(
+        k_len=2, n_len=8, act_base=0, out_base=0,
+        scale_m=1, scale_shift=0, mode=1, weights=W,
+    )
+    best_c = max(range(8), key=lambda c: sat8(3 * W[0][c] + (-1) * W[1][c]))
+    best_val = sat8(3 * W[0][best_c] + (-1) * W[1][best_c])
+    check("argmax RESULT_IDX", m2.result_idx, best_c)
+    check("argmax RESULT_VAL (signed)", m2.result_val_signed, best_val)
+
+    # --- Accumulator at workload-maximum magnitude (K=768, all bytes +-127) ---
+    m3 = NpuModel(ws_width=32)
+    K = 768
+    for k in range(K):
+        m3.act_sram[k] = 127  # x[k] = 127 (s8)
+    W3 = [[127] * 8 for _ in range(K)]  # all weight bytes = 127
+    m3.dispatch_and_run(
+        k_len=K, n_len=8, act_base=0, out_base=2000,
+        scale_m=1, scale_shift=0, mode=0, weights=W3,
+    )
+    max_acc = K * 127 * 127
+    check("NPU-09 max-magnitude acc stays in-bounds", max_acc < 2 ** 31, True)
+    check("NPU-09 max-magnitude end-to-end output saturates", list(m3.act_sram[2000:2008]), [127] * 8)
+
+    # --- Accumulator at NPU-09's stated bound (K=4096, all bytes +-127) ---
+    # NPU-09: "the accumulator shall never overflow for any descriptor with
+    # K <= 4096" — a bound this module's ERR_ACT_RANGE check does not itself
+    # enforce (ACT_BASE+K_LEN > 2048 in fact rejects any legal dispatch with
+    # K > 2048, since ACT_SRAM_BYTES=2048 and ACT_BASE >= 0; K=4096 is thus
+    # reachable only via wrap-around reads, an out-of-scope descriptor for
+    # dispatch_and_run). This drives the same lane-accumulate arithmetic
+    # `_consume_word` uses (`to_s32(acc + x*w)`, x=w=127 each MAC, the
+    # magnitude-maximizing case) directly, K=4096 times, to check NPU-09's
+    # overflow claim at its literal stated bound independent of the
+    # separately-spec'd SRAM-sizing check.
+    K4 = 4096
+    acc4 = 0
+    for _ in range(K4):
+        acc4 = to_s32(acc4 + 127 * 127)
+    max_acc4 = K4 * 127 * 127
+    check("NPU-09 K=4096 max-magnitude acc stays in-bounds", max_acc4 < 2 ** 31, True)
+    check("NPU-09 K=4096 accumulator does not wrap (to_s32 matches exact sum)", acc4, max_acc4)
+    check("NPU-09 K=4096 max-magnitude requantised result saturates", requantize(acc4, 1, 0), 127)
+
+    # --- NPU-21 error codes, individually and in priority combination ---
+    def fresh():
+        mm = NpuModel(ws_width=32)
+        return mm
+
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)  # K_LEN still 0
+    check("ERR_CODE K_ZERO", mm.err_code, NpuModel.ERR_K_ZERO)
+    check("STATUS.ERR set on K_ZERO", mm.err, 1)
+
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 2)
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)  # N_LEN still 0
+    check("ERR_CODE N_ZERO", mm.err_code, NpuModel.ERR_N_ZERO)
+
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 2)
+    mm.write_csr(NpuModel.REG_N_LEN, 5)  # not a multiple of C=8
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)
+    check("ERR_CODE N_NOT_MULTIPLE_OF_C", mm.err_code, NpuModel.ERR_N_NOT_MULTIPLE_OF_C)
+
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 2)
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_ACT_BASE, 2047)  # 2047+2 > 2048
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)
+    check("ERR_CODE ACT_RANGE", mm.err_code, NpuModel.ERR_ACT_RANGE)
+
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 2)
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_OUT_BASE, 2047)  # 2047+8 > 2048, mode=0
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)  # MODE=0
+    check("ERR_CODE OUT_RANGE", mm.err_code, NpuModel.ERR_OUT_RANGE)
+
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 2)
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)  # legal dispatch -> BUSY=1
+    check("legal dispatch: BUSY set, no error", (mm.busy, mm.err), (1, 0))
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)  # second GO while BUSY
+    check("ERR_CODE BUSY_REJECT", mm.err_code, NpuModel.ERR_BUSY_REJECT)
+
+    # Priority combination: K_ZERO and ACT_RANGE both true -> K_ZERO wins.
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 0)
+    mm.write_csr(NpuModel.REG_ACT_BASE, 2047)
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)
+    check("NPU-21 priority: K_ZERO beats ACT_RANGE", mm.err_code, NpuModel.ERR_K_ZERO)
+
+    # --- ABORT recovery (NPU-19): forces IDLE/BUSY=0 mid-RUN ---
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 4)
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)
+    mm.step(1, 0x01020304)  # feed one word, still mid-RUN (needs 4 words for K=4,N=8)
+    check("mid-RUN before abort: busy=1", mm.busy, 1)
+    mm.write_csr(NpuModel.REG_CTRL, 0x4)  # ABORT
+    check("NPU-19: ABORT clears BUSY immediately", mm.busy, 0)
+    check("NPU-19: ABORT returns sequencer to IDLE", mm.state, "IDLE")
+
+    # --- ws_ready / FIFO backpressure (NPU-06/07): never drops, stalls instead ---
+    mm = fresh()
+    mm.write_csr(NpuModel.REG_K_LEN, 8)
+    mm.write_csr(NpuModel.REG_N_LEN, 8)
+    mm.write_csr(NpuModel.REG_CTRL, 0x1)
+    r1 = mm.step(1, 0xAAAAAAAA)
+    r2 = mm.step(1, 0xBBBBBBBB)
+    check("ws_ready high with room for 2", (r1["ws_ready"], r2["ws_ready"]), (True, True))
+
+    # --- NPU-15: WS_WIDTH=32 vs WS_WIDTH=64 give identical numerical
+    #     results (only cycle count differs, not RTL, and not this model's
+    #     output values either).
+    W4 = [[(i * 3 + k) % 251 for i in range(8)] for k in range(4)]  # K=4,N=8
+    results = {}
+    for ws_width in (32, 64):
+        mw = NpuModel(ws_width=ws_width)
+        for k in range(4):
+            mw.act_sram[k] = (k * 5 + 1) & 0xFF
+        mw.dispatch_and_run(
+            k_len=4, n_len=8, act_base=0, out_base=50,
+            scale_m=3, scale_shift=2, mode=0, weights=W4,
+        )
+        results[ws_width] = list(mw.act_sram[50:58])
+    check("NPU-15: WS_WIDTH=32 and 64 produce identical results", results[32], results[64])
+
+    print("PASS" if ok else "FAIL")
+    return ok
+
+
+if __name__ == "__main__":
+    result = _self_check()
+    raise SystemExit(0 if result else 1)
diff --git a/hw/dv/npu/vplan.md b/hw/dv/npu/vplan.md
new file mode 100644
index 0000000..507261c
--- /dev/null
+++ b/hw/dv/npu/vplan.md
@@ -0,0 +1,141 @@
+# npu — Verification Plan
+
+Source of truth: `docs/spec/npu.md` §2–§5 (NPU-01..23), read against
+`docs/spec/soc_1.md` for system context (memory map §3.2, IRQ map §4.4,
+bus §2.2). Golden model: `hw/dv/common/models/npu.py` (`NpuModel`,
+`requantize`, `pack_weight_stream`).
+
+Clean room: this plan and the model were written from spec text only; no
+`hw/rtl/` file was read (`/CLAUDE.md` Iron Rule 2).
+
+## Strategy notes
+
+- Every register-level check compares the DUT's `wb_dat_r`/`wb_ack`
+  against `NpuModel.read_csr()` / a directly-computed expected value —
+  never against a previous simulation run.
+- Every weight-stream / compute check drives `NpuModel.step(ws_valid,
+  ws_data)` in lock-step with the DUT's `i_ws_valid`/`i_ws_data` each
+  rising `clk` edge, and compares `o_ws_ready` against the model's
+  returned `ws_ready`, and post-`STATUS.DONE` SRAM contents /
+  `RESULT_IDX`/`RESULT_VAL` against the model's `act_sram` /
+  `result_idx`/`result_val_signed`. `NpuModel.dispatch_and_run()` is the
+  same code path used for directed single-shot descriptors.
+- `C = 8` is fixed by the spec (not a build parameter); `WS_WIDTH` is
+  swept at {32 (committed default, `soc_1.md` SOC1-19), 64 (anticipated
+  upgrade, NPU-15)} wherever a row's behavior could plausibly depend on
+  it. Workload-realistic `(K, N)` pairs come from `profile.md` §2: `K ∈
+  {48, 128, 288, 768}`, `N ∈ {48, 128, 288, 768, 32000}`.
+- "Formal" tag: the requirement is a structural or "never happens"
+  property that a finite set of simulation traces cannot prove
+  exhaustively (register-driven combinational contracts, FSM invariants,
+  absence properties) — handed to the formal-engineer. A sim-side sanity
+  check is still listed since sim runs regardless and catches gross
+  violations early. NPU-09 is a numeric bound over up to 4096 sequential
+  cycles — outside `FORMAL_BMC_DEPTH`'s default reach (`flow/gates.mk`,
+  20) — so it is verified by directed sim at the workload-legal maximum
+  (`K=768`) plus the spec's own closed-form analytic bound, not formal
+  BMC; a k-induction proof is a possible future formal stretch goal, not
+  required for sign-off.
+- Rows below are one per numbered spec "shall" (NPU-01..23). NPU-20 has
+  no independent hardware check beyond NPU-21's `OUT_RANGE` — its row
+  says so explicitly rather than inventing new stimulus.
+
+| Shall ID | What to test | Method | Coverage point | Executable pass criterion |
+|---|---|---|---|---|
+| **NPU-01** (reset values) | While `rst_n` is low and on the first rising edge after deassertion, every CSR reads its §3 reset value (`CTRL`,`STATUS`,`ERR_CODE`,`K_LEN`,`N_LEN`,`ACT_BASE`,`OUT_BASE`,`SCALE_M`,`SCALE_SHIFT`,`RESULT_IDX`,`RESULT_VAL` all 0) and the sequencer is `IDLE`; activation-SRAM *contents* are explicitly not required to reset. | Directed (sim), **formal-tagged** for the "every flop resets" structural claim (exhaustive over reachable pre-reset states). | Cover: reset with SRAM pre-loaded non-zero (from a prior op) vs. freshly-instantiated; reset asserted mid-`RUN`. | Sim: every CSR in `NpuModel.reset()`'s value set matches DUT `wb_dat_r` read-back post-reset; SRAM bytes untouched by reset are excluded from the comparison. Formal: SBY proof `rst_n |-> ##1 (all CSR flops == reset value)` holds at `FORMAL_BMC_DEPTH`, zero counterexamples. |
+| **NPU-02** (WB slave signal set) | Full Wishbone B4 pipelined slave port exists and `wb_stall` is tied low always. | Directed (sim, port-level smoke test) + **formal-tagged** (`wb_stall == 0` is a permanent structural tie, provable exhaustively). | Cover: `wb_stall` sampled every cycle across every other test's traffic (a monitor assertion, not a standalone test). | Sim: a bound monitor flags any cycle where `wb_stall != 0`; zero flags over the full regression. Formal: SBY proof `wb_stall == 0` holds unconditionally, no counterexample. |
+| **NPU-03** (ack timing) | `wb_ack` asserts exactly one cycle after every `wb_cyc && wb_stb`, for reads and writes, at every offset and in every `CTRL`/`STATUS` state. | Directed + constrained-random (randomize offset, r/w, and current `BUSY`/`ERR` state at issue time). | Cross-cover: {offset in {mapped, unmapped}} x {read, write} x {issued while `IDLE`, `RUN`, `TAIL`/`DONE`}. All bins hit. | For every `wb_cyc && wb_stb` cycle, `wb_ack` is 1 exactly one cycle later and 0 on all other cycles for that transaction; zero deviations over the full randomized run. |
+| **NPU-04** (`wb_sel` ignored) | A write with any `wb_sel` pattern (including all-zero or a single byte lane) updates the full 32-bit register from `wb_dat_w`, identically to `wb_sel = 4'hF`. | Directed: repeat one register-write test at each of the 16 `wb_sel` values. | Cover: `wb_sel` ∈ {0x0..0xF} each exercised on at least one writable register. | Post-write read-back equals the written 32-bit value for every `wb_sel` value tested, including `wb_sel = 0x0` (still a full update per NPU-04) — zero mismatches against `NpuModel.write_csr`'s (sel-agnostic) result. |
+| **NPU-05** (unmapped offsets) | An offset in `0x0000`-`0x0FFF` not in §3's table reads `0x0000_0000` and silently ignores writes; `wb_err` never asserts from this module for any offset in-window. | Directed, sweeping representative unmapped offsets (between/after known registers, e.g. `0x2C`, `0x100`, `0x0FFC`) + **formal-tagged** for the "never asserts `wb_err`" absence claim. | Cover: unmapped offsets at a low gap (`0x2C`), a high gap (`0x0FFC`), and just past the last defined register. | Sim: read returns `0x0000_0000`, a preceding value written to that offset never appears on a later read of a *mapped* register (no address aliasing), `wb_err` stays 0 for every offset tested — matches `NpuModel.read_csr()`'s default-0 branch. Formal: SBY proof `wb_err == 0` always, exhaustive over `wb_adr[15:0]`. |
+| **NPU-06** (ingress transfer condition) | A transfer is captured only on a rising edge where `i_ws_valid && o_ws_ready` are both high; the module never samples `i_ws_data` on a cycle where either is low. | Directed: drive `i_ws_valid` high with `o_ws_ready` forced/observed low (FIFO full) and confirm no capture; **formal-tagged** for exhaustive "no capture without both-high" absence property. | Cover: valid-without-ready, ready-without-valid, and both-high, each at least once per `WS_WIDTH` build. | Sim: FIFO occupancy (inferred via subsequent `o_ws_ready` transitions and consumed byte count) changes only on both-high cycles — compare against `NpuModel.step()`'s identical push-gating logic. Formal: SBY proof no FIFO-write-enable-equivalent signal is ever high without both `i_ws_valid && o_ws_ready`. |
+| **NPU-07** (`o_ws_ready` flow control) | `o_ws_ready` is low iff the 2-entry FIFO holds 2 unconsumed entries, high otherwise; no other flow-control mechanism exists. | **Formal-tagged** (combinational contract on internal FIFO occupancy, exhaustive over reachable occupancy states) + sim sanity via back-to-back pushes without a consuming `GO`. | Cover: FIFO occupancy 0, 1, 2 each observed with `o_ws_ready` checked. | Sim: pushing 2 words while `IDLE` (sequencer not consuming) drives `o_ws_ready` low on the 3rd offered word — matches `NpuModel.ws_ready` after two `step()` pushes with `state != "RUN"`. Formal: SBY proof `o_ws_ready == (fifo_count < 2)` holds for all reachable states. |
+| **NPU-08** (byte ordering, bit-exactness-critical) | For output-channel group `g`, weight bytes for a fixed `k` arrive for all `C=8` channels of that group consecutively (k-major, channel-minor), packed low-byte-first per word, before any byte of `k+1`. | Directed: feed a marked/identifiable byte stream (each byte encodes its own intended `(k,n)`) via `NpuModel.pack_weight_stream()` word-for-word into the DUT and confirm the *result* (which requires correct (k,n) attribution to produce the right sum) matches. Constrained-random: random weight matrices, `WS_WIDTH` ∈ {32,64}. | Cross-cover: `WS_WIDTH` ∈ {32,64} x `N/C` ∈ {1, multiple groups} x `K` ∈ {small, `profile.md`-realistic}. | Post-`DONE`, DUT normal-mode SRAM writeback (or argmax `RESULT_IDX`/`RESULT_VAL`) matches `NpuModel.dispatch_and_run()`'s output bit-for-bit for every trial — a byte-order bug produces a wrong sum, which this end-to-end check catches without needing a whitebox probe. Zero mismatches. |
+| **NPU-09** (accumulator never overflows, `K<=4096`) | The 32-bit signed accumulator never overflows for any legal descriptor (`K <= 768` per `profile.md`, spec's own bound extends the guarantee to `K<=4096`). | Directed: `K=768` (workload max), all activation and weight bytes at `±127` (the `|Σ product|`-maximizing pattern) — the spec's own cited worst case. | Cover: accumulator magnitude within one order of magnitude of `2^31` is *not* reachable at `K<=768`; this is the floor, not a ceiling — also run `K=4096` (spec's stated absolute bound) with the same all-`±127` pattern. | `NpuModel.to_s32()` never wraps for either `K` value (assert accumulator, computed independently in the test via plain Python `sum()`, stays within `[-2^31, 2^31-1]` before any `to_s32` call) and the DUT's final requantised output matches `NpuModel`'s bit-for-bit. Zero overflow, zero mismatches. |
+| **NPU-10** (accumulator never software-visible) | No CSR, at any offset, ever exposes the raw 32-bit accumulator value — only `RESULT_VAL` (the *requantised* int8, sign-extended) is readable, and only in argmax mode. | **Formal-tagged** (absence property: no register's next-state or output expression is ever driven directly by an accumulator bit) + sim sanity sweeping every readable offset post-compute. | Cover: every defined register offset read once per completed op (normal and argmax mode), plus every unmapped offset in range. | Sim: no read from any offset, in any state, ever returns a value equal to a lane's live accumulator (checked by comparing every CSR read against `NpuModel`'s tracked internal `_accs`, which must never appear verbatim in any `read_csr` result other than via the defined `requantize()` path). Formal: SBY proof no register output port has a direct (unrequantised) fan-in from any accumulator bit. |
+| **NPU-11** (rounding, round-half-away-from-zero) | `t = acc*M` rounds per the spec's exact pseudocode: ties (and only ties) round away from zero; `s=0` is a passthrough. | Directed: hand-computed corner cases — `s=0`; positive tie (`t` an exact multiple of `2^(s-1)` but not `2^s`); negative tie; non-tie positive/negative. Constrained-random: random `(acc, M, s)` triples compared against `NpuModel.requantize()`. | Cover: `s=0`; `s=31` (max); tie exactly at the rounding boundary, both signs; non-tie both signs. | DUT's post-`DONE` output byte matches `requantize(acc, M, s)` bit-for-bit for every directed and random trial (acc independently reconstructed from the test's own weight/activation stimulus, not read back from RTL). Zero mismatches. |
+| **NPU-12** (saturation) | `out = clamp(rounded, -128, 127)`, unconditional, full signed-int8 clamp. | Directed: `(acc, M, s)` chosen so `rounded` lands just inside, just above, and just below each of `+127`/`-128`; **formal-tagged** for the clamp's unconditional/exhaustive nature. | Cover: `rounded` ∈ {126, 127, 128, -128, -129, -127} (boundary-adjacent set) each hit at least once. | Sim: output equals `sat8(rounded)` for every boundary case, matching `NpuModel.sat8()`. Formal: SBY proof output is always within `[-128,127]` regardless of internal `rounded` magnitude, exhaustive. |
+| **NPU-13** (result-path routing) | Normal mode (`MODE=0`): each requantised output byte for channel `n` is written to activation SRAM at `OUT_BASE+n`. Argmax mode (`MODE=1`): no SRAM write occurs; the value instead updates the running max. | Directed: same descriptor run once in each mode, confirming SRAM at the normal-mode `OUT_BASE` region is untouched after an argmax-mode run (pre-poison the region with a sentinel before the argmax run). | Cover: both modes each run at least once per `(K,N)` shape tested elsewhere in this plan (piggybacks on those rows' stimulus, not separate). | Normal mode: SRAM bytes `[OUT_BASE, OUT_BASE+N)` match `NpuModel.act_sram` post-`DONE`. Argmax mode: SRAM bytes at the sentinel region are bit-identical to their pre-run sentinel value (zero writes leaked). |
+| **NPU-14** (FIFO byte unpacking) | Within a `WS_WIDTH`-bit FIFO word, byte `i` (bits `[8i+7:8i]`) is consumed in ascending `i` order. | Directed: a single word with each byte set to a distinct marker value (e.g. `0x10,0x11,0x12,0x13` at `WS_WIDTH=32`), `K,N` sized so this word's 4 bytes map to 4 distinct, individually observable output channels. | Cover: `WS_WIDTH` ∈ {32,64}, marker word at the start, middle, and end of a group's byte stream. | Each marker byte's contribution appears in the correct output channel per `NpuModel._consume_word()`'s byte-index-to-`(k,c)` mapping — matches DUT output bit-for-bit. |
+| **NPU-15** (bandwidth-following lane feeding, same result at any `WS_WIDTH`) | The sequencer advances a lane as soon as its byte is unpacked, not waiting for all `C` lanes; final numerical result is independent of `WS_WIDTH` (only cycle count differs). | Directed: run the identical `(K,N,weights,activations,M,s)` descriptor at `WS_WIDTH=32` and `WS_WIDTH=64`, compare outputs; separately record cycle counts and confirm the `WS_WIDTH=64` run completes in fewer weight-stream cycles. | Cover: `WS_WIDTH` ∈ {32,64} x at least one multi-group (`N>C`) shape. | Outputs bit-identical between the two `WS_WIDTH` builds (matches `NpuModel`'s own cross-`ws_width` self-check) and `WS_WIDTH=64`'s cycle count to `DONE` is strictly less than `WS_WIDTH=32`'s for the same descriptor. |
+| **NPU-16** (activation broadcast, per-group re-read) | For `N>C`, the sequencer repeats the full `K`-step pass once per group, re-reading the same `K` activation bytes from SRAM each pass against fresh weight bytes. | Directed: `N = 2C` or `3C` (two/three groups), activation vector with distinct per-index values, confirm each group's output depends correctly on the *same* activation vector paired with *that group's* weight columns. | Cover: `N/C` ∈ {1, 2, 3, `768/8=96`, `32000/8=4000`}. | Every group's output bytes match `NpuModel`'s (which re-reads `act_sram[ACT_BASE:ACT_BASE+K]` fresh per group by construction) — a stale-activation bug (e.g. only re-reading group 0's values) is caught since later groups would diverge. |
+| **NPU-17** (BUSY/DONE FSM) | `BUSY=1` throughout `RUN` and `TAIL`, `0` in `IDLE`; `DONE`'s status/IRQ update is latched the same cycle the FSM would otherwise re-enter `IDLE` (no separate one-cycle `DONE`-and-still-busy state). | **Formal-tagged** (FSM invariant, exhaustive over reachable states) + sim sanity recording `BUSY`/`DONE` every cycle of a directed run. | Cover: at least one full `IDLE->RUN->TAIL->DONE->IDLE` cycle sampled every cycle. | Sim: `BUSY` sampled every cycle exactly matches `RUN`/`TAIL` membership per `NpuModel.state`; the cycle `DONE` first reads 1 is the same cycle `BUSY` first reads 0. Formal: SBY proof `DONE && next(!DONE_write) -> !BUSY` (no state where `DONE` is set and `BUSY` is still 1), exhaustive. |
+| **NPU-18** (compute-done never precedes stream-done) | `o_irq_done`/`STATUS.DONE` never assert before all `K*N` weight bytes have been consumed from the FIFO. | **Formal-tagged** (safety property: `DONE` implies consumed-byte-count `== K*N`) + directed sim withholding the final byte and confirming `DONE` stays 0 indefinitely. | Cover: withhold the last 1 byte of a descriptor (stall `i_ws_valid` forever after `K*N-1` bytes) — `DONE` must never assert in the observed window. | Sim: with the final byte withheld, `STATUS.DONE`/`o_irq_done` remain 0 for the entire (long, e.g. 10,000-cycle) observation window; once the byte is supplied, `DONE` asserts within the model's `TAIL`-then-`DONE` window. Formal: SBY proof `DONE -> (bytes_consumed == K_LEN*N_LEN)`, no counterexample. |
+| **NPU-19** (`ABORT` recovery) | Writing `CTRL.ABORT=1` forces `IDLE` immediately, clears `BUSY` and any in-flight accumulation, regardless of current state; no-op if already `IDLE`. | Directed: assert `ABORT` mid-`RUN` (after a partial byte count), mid-`TAIL`, and while already `IDLE`; then dispatch a fresh, different descriptor and confirm no residual state (partial accumulator) leaks into it. | Cover: `ABORT` at {mid-`RUN` early, mid-`RUN` late, mid-`TAIL`, `IDLE`} each exercised. | `BUSY`, `STATUS.DONE`-unaffected-ness, and sequencer state match `NpuModel`'s post-`ABORT` state (`state=="IDLE"`, `busy==0`) in every case, including the `IDLE`-already no-op case (no spurious state change); the subsequent fresh descriptor's result matches a from-reset `NpuModel` run with zero contamination from the aborted op. |
+| **NPU-20** (`lm_head`/large-`N` commits to argmax-only) | No separate hardware check exists for this — it is a consequence of NPU-21's `OUT_RANGE` check: any `MODE=0` descriptor with `OUT_BASE+N_LEN > 2048` (true for any `N` this large) is already rejected. | Not a separate test — see **NPU-21**'s `OUT_RANGE` row, exercised there at `lm_head`-scale (`N=32000`) explicitly. | (covered by NPU-21's `OUT_RANGE` cross-cover at `N=32000`) | (see NPU-21) — this row exists only to record that NPU-20 has no independent stimulus, per the vplan's one-row-per-shall rule. |
+| **NPU-21** (malformed-descriptor priority) | On `CTRL.GO`, the six checks (`K_ZERO,N_ZERO,N_NOT_MULTIPLE_OF_C,ACT_RANGE,OUT_RANGE,BUSY_REJECT`) are evaluated in that priority order; first match sets `ERR_CODE`/`STATUS.ERR`, no dispatch. | Directed: each `ERR_CODE` individually, plus at least one multi-true combination per adjacent pair in the priority list (e.g. `K_ZERO` & `ACT_RANGE` both true) to confirm priority order, not just individual detection. | Cover: all 6 `ERR_CODE` values individually; cross-cover at least 3 combinations spanning non-adjacent priority pairs (e.g. `K_ZERO`+`OUT_RANGE`, `N_ZERO`+`BUSY_REJECT`, `ACT_RANGE`+`OUT_RANGE`). Includes `N=32000` (`lm_head`-scale) `OUT_RANGE` case (closes NPU-20's cross-reference). | `ERR_CODE`/`STATUS.ERR` match `NpuModel._write_ctrl()`'s priority-ordered result for every individual and combined case; `STATUS.BUSY` stays 0 (no dispatch) for every error case. Zero mismatches. |
+| **NPU-22** (`SCALE_M`/`SCALE_SHIFT` full range legal) | Every representable value of both fields (`M` full 16-bit, `s` full 5-bit) is legal — no `ERR_CODE` is ever raised due to their value. | Directed/constrained-random: dispatch legal descriptors at `M` ∈ {0, 1, 0x7FFF, 0xFFFF} and `s` ∈ {0..31}, confirm no `ERR_CODE` results from these fields alone. | Cover: `M` boundary values {0, 0xFFFF}; `s` ∈ {0, 1, 15, 31} (full range represented, not exhaustively enumerated — 32 values is cheap enough to run all of, so do). | For every `(M,s)` combination tested, dispatch succeeds (`ERR_CODE==NONE`) when no *other* field is malformed, and the requantised output matches `NpuModel.requantize()` at that `(M,s)`. |
+| **NPU-23** (weight-stream underrun not self-observable) | This module raises no interrupt of its own for a stream underrun/error — `o_irq_err` is driven only by this module's own `ERR_CODE` table (§5), never by ingress-port starvation. | **Formal-tagged** (absence property: `o_irq_err`'s only sensitivity list is the NPU-21 error-detection logic, not `i_ws_valid`/FIFO-empty conditions) + sim sanity: starve the FIFO indefinitely mid-`RUN` and confirm `o_irq_err` stays 0. | Cover: FIFO starved (no `i_ws_valid`) for a long window (e.g. 10,000 cycles) mid-`RUN`, both with and without a concurrent unrelated CSR read/write. | Sim: `o_irq_err`/`STATUS.ERR` remain 0 throughout the starved window (the module is simply stuck in `RUN`, per spec — matches `NpuModel`, which likewise never sets `err` from FIFO starvation, only from `_write_ctrl`'s NPU-21 checks). Formal: SBY proof `o_irq_err`'s driving expression has no term referencing `i_ws_valid`/FIFO-empty. |
+
+## Row count
+23 rows (NPU-01 through NPU-23), one per spec "shall". NPU-20 is a
+covered-elsewhere row (no independent stimulus), noted above rather than
+silently omitted.
+
+## Notes for dv-engineer
+
+- Golden model API (`hw/dv/common/models/npu.py`):
+  - CSR/descriptor layer: `NpuModel.write_csr(offset, value)` /
+    `read_csr(offset)`, register-offset constants `NpuModel.REG_*`,
+    `ERR_*` code constants — call these after translating a WB
+    write/read transaction, exactly mirroring §3's register map.
+  - Cycle/weight-stream layer: `NpuModel.ws_ready` (compare to DUT
+    `o_ws_ready` before deciding whether to assert `i_ws_valid` that
+    cycle) and `NpuModel.step(ws_valid, ws_data)` (call once per rising
+    `clk` edge, in lock-step with the DUT, exactly as `BlinkModel.step()`
+    is driven per `hw/dv/blink/vplan.md`).
+  - `NpuModel.dispatch_and_run(...)` is a convenience built from the same
+    two calls above (no separate arithmetic path) for directed
+    single-descriptor tests that don't need cycle-by-cycle control (e.g.
+    backpressure injection) — most rows above can use it directly.
+  - `pack_weight_stream(weights, n_len, c, ws_width)` turns a `K x N`
+    weight matrix into the exact ingress-port word sequence (NPU-08
+    order) to drive the DUT's `i_ws_data`.
+- `NpuModel.act_sram` is a directly-writable `bytearray` for test setup
+  (seeding the initial activation vector before a descriptor runs). This
+  is a test-harness convenience only, not a modeled hardware interface —
+  see spec-ambiguity **A4** below; real firmware has no defined path to
+  do this, which is itself a spec gap, not a DV concern to route around
+  silently.
+- `result_val_signed` (a model-only convenience property, not a spec
+  register) returns `RESULT_VAL` decoded back to a signed Python int
+  ([-128,127]) for easier test assertions than sign-extended-in-32-bits
+  comparisons.
+
+## Spec ambiguities filed (not resolved by picking an interpretation)
+
+Also recorded as docstring comments in `hw/dv/common/models/npu.py`, per
+the verif-architect method (file immediately, do not resolve silently):
+
+- **A1 — argmax tie-break undefined.** §3.6 defines `RESULT_IDX` as "the
+  winning output-channel index" but never states what happens when two
+  channels' requantised values tie. The golden model keeps the
+  lowest-index winner; DV should treat this as the model's stance, not a
+  confirmed hardware behavior, until RTL intake / chief-architect rules
+  on it. **Row NPU-21's argmax coverage should include at least one
+  engineered tie** once this is resolved, to confirm RTL matches whatever
+  the ruling is (currently: matches the model's lowest-index-wins choice,
+  informally).
+- **A2 — simultaneous `GO`+`ABORT` in one write undefined.** §3.1
+  describes `ABORT` as an override "regardless of current state" but
+  never addresses a single write setting both `GO=1` and `ABORT=1`. The
+  model applies `ABORT` first, then evaluates `GO`'s checks against the
+  post-abort state (so an abort-then-immediate-redispatch reading is
+  possible). This is a low-priority firmware-shouldn't-do-this case but
+  is a genuine spec gap — flagged, not resolved.
+- **A3 — `TAIL` state's exact cycle count undefined.** §4.3 says only
+  "fixed latency, a few cycles." The model does not claim a specific
+  number and DV must not assert a specific `TAIL` cycle count against
+  it — only NPU-18's ordering guarantee is spec-backed. If RTL intake
+  fixes a specific number, that number is an RTL implementation fact, not
+  something to retrofit into this golden model as if the spec required
+  it.
+- **A4 — no defined path to load the *first* activation vector.** Neither
+  `npu.md` nor `soc_1.md` describes how the initial activation vector
+  (e.g. a token embedding, before any normal-mode NPU op has populated
+  the SRAM via NPU-13 writeback) gets into the 2 kB activation SRAM. The
+  CSR window is described as "CSR/descriptor access only" with no
+  data-write register, and no other port into this SRAM exists in §2.
+  This blocks writing a *fully* end-to-end (cold-boot, first-token)
+  system-level test without an undocumented assumption. Flagged for
+  chief-architect / a future `npu.md` revision, same disposition as the
+  spec's own open-questions section (§7).