# `cv_x1_pro_subsystem` — Hardware IP Specification & Step 1 Verification Dossier

- **Module Name**: `cv_x1_pro_subsystem` ([`dut.v`](dut.v))
- **IP Scope**: 8-Lane Signed Asymmetric `INT4 × INT8` Group-Dequantized GEMV / KV-Cache Dot-Product Subsystem IP with 4-Bank Interleaved Register-File SRAM and Elastic AXI4-Stream Pipeline
- **Verification Harness**:
  - Directed Self-Checking Testbench (`Icarus Verilog 13.0`): `tb.v`
  - Independent Python Golden Model + `Verilator 5.052` Cycle-Accurate Co-Simulator (`2,560` vectors / `20,480` MAC ops): `cosim_golden_verilator.py`
  - Generated Co-Simulation Artifact: `cosim_report.json`

---

## 1. Input / Output Bit-Level Data Formats

### 1.1 4-Bank Interleaved Weight / KV Port (`sram_we`, `sram_waddr[5:0]`, `sram_wdata[31:0]`)
- **Address Mapping (`sram_waddr[5:0]`)**:
  - `sram_waddr[1:0]` (`bank_sel`): Selects 1 of 4 independent banks (`Bank 0..3`). Low-order bank interleaving ensures sequential tile addresses `0, 1, 2, 3` map across distinct banks `0, 1, 2, 3`.
  - `sram_waddr[5:2]` (`row_addr`): Selects 1 of 16 rows (`Row 0..15`) within the selected bank.
  - Total storage capacity: $4\text{ banks} \times 16\text{ rows} \times 32\text{ bits} = 2{,}048\text{ bits}$ ($512\text{ signed INT4 elements}$).
- **32-Bit Packed `INT4x8` Word (`sram_wdata[31:0]`)**:
  - Packs 8 signed two's-complement 4-bit integers (`kv0..kv7`), each in range $[-8, +7]$:
    $$\text{kv}_i = \text{sram\_wdata}[4i+3 : 4i], \quad i \in \{0, \dots, 7\}$$

### 1.2 AXI4-Stream Slave Query & Control Port (`s_axis_*`)
- **`s_axis_tdata[63:0]` (Packed `INT8x8` Activation / Query Vector)**:
  - Packs 8 signed two's-complement 8-bit integers (`q0..q7`), each in range $[-128, +127]$:
    $$q_i = \text{s\_axis\_tdata}[8i+7 : 8i], \quad i \in \{0, \dots, 7\}$$
- **`s_axis_tuser[19:0]` (Per-Tile Dequantization & Accumulator Control Descriptor)**:
  | Bits | Field | Type | Description |
  |---|---|---|---|
  | `[1:0]` | `bank` | `uint2` | Target SRAM bank (`0..3`) |
  | `[5:2]` | `row` | `uint4` | Target SRAM row (`0..15`) |
  | `[13:6]` | `scale` | `uint8` | Unsigned 8-bit per-group dequantization scale factor ($0 \dots 255$) |
  | `[17:14]` | `zp` | `sint4` | Signed 2's-complement 4-bit asymmetric zero-point ($-8 \dots +7$) |
  | `[18]` | `clr_acc` | `bool` | `1`: Start new accumulation (`acc_base = 0`); `0`: Accumulate onto `m_axis_tdata` |
  | `[19]` | `sat_mode` | `bool` | `1`: Saturate to `INT32_MIN..INT32_MAX`; `0`: Modulo-$2^{32}$ wrap-around |
- **`s_axis_tlast`**: Framing bit propagated identically through the 3-stage pipeline to `m_axis_tlast`.

### 1.3 AXI4-Stream Master Accumulated Output Port (`m_axis_*`)
- **`m_axis_tdata[31:0]`**: Signed two's-complement 32-bit accumulated result (`[-2,147,483,648 .. +2,147,483,647]`).
- **`m_axis_tlast`**: Asserted on the final tile of a reduction packet.
- **`m_axis_tbank[1:0]`**: Echoes the source SRAM bank (`0..3`) of the completed tile for bank-trace verification.

---

## 2. Exact Arithmetic, Rounding & Overflow Rules

1. **Exact Integer Arithmetic (Zero Rounding / Truncation Loss)**:
   All internal datapath widths are sized to preserve full mathematical precision without intermediate truncation or rounding:
   - **Step 1 (Asymmetric Zero-Point Subtraction — Stage 1)**:
     $$\text{deq\_kv}_i = \text{sext}_5(\text{kv}_i) - \text{sext}_5(\text{zp}) \in [-15, +15] \quad (\text{5-bit signed})$$
   - **Step 2 (8-Lane Parallel Multiplication — Stage 2)**:
     $$\text{prod}_i = \text{deq\_kv}_i \times q_i \in [-1{,}920, +1{,}920] \quad (\text{13-bit signed})$$
     *(Note: $+1{,}920$ is reached when $\text{kv}_i = -8, \text{zp} = +7 \Rightarrow \text{deq\_kv}_i = -15$ and $q_i = -128$; $-1{,}920$ is reached when $\text{kv}_i = +7, \text{zp} = -8 \Rightarrow \text{deq\_kv}_i = +15$ and $q_i = -128$.)*
   - **Step 3 (Balanced Binary Adder Tree Reduction — Stage 2)**:
     $$\text{raw\_dot} = \sum_{i=0}^{7} \text{prod}_i \in [-15{,}360, +15{,}360] \quad (\text{16-bit signed})$$
   - **Step 4 (Group Scale Multiplication — Stage 3)**:
     $$\text{scaled\_dot} = \text{raw\_dot} \times \text{zext}_9(\text{scale}) \in [-3{,}916{,}800, +3{,}916{,}800] \quad (\text{25-bit signed})$$

2. **33-Bit Extended Accumulation & Overflow / Underflow Rules (Stage 3)**:
   Let $\text{acc\_base} = 0$ if $\text{clr\_acc} = 1$, else $\text{m\_axis\_tdata}$.
   The 33-bit extended signed sum is computed as:
   $$\text{acc\_ext\_sum}[32:0] = \text{sext}_{33}(\text{acc\_base}) + \text{sext}_{33}(\text{scaled\_dot})$$
   - **Positive Overflow Condition (`pos_ovf`)**: `(!acc_ext_sum[32] && acc_ext_sum[31])` ($\text{acc\_ext\_sum} > +2{,}147{,}483{,}647$).
   - **Negative Underflow Condition (`neg_udf`)**: `(acc_ext_sum[32] && !acc_ext_sum[31])` ($\text{acc\_ext\_sum} < -2{,}147{,}483{,}648$).
   - **When `sat_mode == 1` (Saturating Mode)**:
     - If `pos_ovf`: `m_axis_tdata <= 32'sh7FFF_FFFF` (`+2,147,483,647`) and `sat_overflow_sticky <= 1'b1`.
     - If `neg_udf`: `m_axis_tdata <= -32'sh8000_0000` (`-2,147,483,648`) and `sat_overflow_sticky <= 1'b1`.
   - **When `sat_mode == 0` (Modulo-$2^{32}$ Wrap-Around Mode)**:
     - `m_axis_tdata <= acc_ext_sum[31:0]` (standard two's-complement 32-bit wrap-around; `sat_overflow_sticky` is not asserted).

---

## 3. Reset & Backpressure Semantics

1. **Reset Behavior (`rst_n`)**:
   - Active-low asynchronous reset (`always @(posedge clk or negedge rst_n)`).
   - Asserting `rst_n == 0` deterministically zeroes all 4 SRAM banks (`sram_bank0..3`), the 4-entry FIFO (`fifo_mem`, `fifo_wr_ptr`, `fifo_rd_ptr`, `fifo_count`), all 3 pipeline stages (`s1_*`, `s2_*`, `m_axis_*`), `sat_overflow_sticky`, and all telemetry counters (`perf_mac_tiles`, `perf_stall_cycles`, `perf_bank_conflicts`).
2. **Upstream Backpressure (`s_axis_tvalid` / `s_axis_tready`)**:
   - A 4-entry elastic ingress FIFO decouples upstream bursts from pipeline stalls.
   - `s_axis_tready = (fifo_count < 3'd4)`.
   - Push occurs on `posedge clk` iff `s_axis_tvalid && s_axis_tready`. Simultaneous push and pop (`2'b11`) keeps `fifo_count` constant with zero bubble penalty.
3. **Downstream Backpressure (`m_axis_tvalid` / `m_axis_tready` & `pipe_stall`)**:
   - Global stall signal: `pipe_stall = m_axis_tvalid && !m_axis_tready`.
   - When `pipe_stall == 1`:
     - `fifo_pop` is deasserted (`0`), halting FIFO reads while still allowing `fifo_push` until `fifo_count == 4`.
     - Stage 1 (`s1_*`), Stage 2 (`s2_*`), and Stage 3 (`m_axis_*`) registers are completely frozen.
     - `m_axis_tvalid`, `m_axis_tdata`, `m_axis_tlast`, and `m_axis_tbank` remain strictly invariant until `m_axis_tready == 1`.

---

## 4. SRAM Synthesis Form & Interface Standard Compliance Scope

1. **Physical Synthesis Form of On-Chip SRAM (`sram_bank0..3`)**:
   - In [`dut.v`](dut.v), `sram_bank0..3` are written as behavioral Verilog register arrays with asynchronous reset initialization (`reg [31:0] sram_bank0 [0:15]`).
   - **Honest Synthesis Disclosure**: Standard-cell synthesis (`Yosys`) maps these 4 banks (`2,048` bits) to **standard-cell flip-flop register files (`2,048 × DFFR_X1` + read multiplexer trees)**, **not** a foundry 6T/8T compiled SRAM hard macro (`lef/lib` memory compiler). For larger capacities (e.g., $\ge 4\text{ KB}$ per bank), a production ASIC replaces `sram_bank0..3` with vendor single-port/pseudo-dual-port SRAM macros adding a 1-cycle synchronous read latency.
2. **Interface Standard Compliance Scope**:
   - **AXI4-Stream (`s_axis_*`, `m_axis_*`)**: Complies with the **ARM AMBA 4 AXI4-Stream Protocol Specification (ARM IHI 0051A)** core transfer subset (`TVALID`, `TREADY`, `TDATA`, `TUSER`, `TLAST`), including Section 2.2.1 handshake invariance rules. Optional sideband signals (`TSTRB`, `TKEEP`, `TID`, `TDEST`, `TWAKEUP`) are omitted.
   - **SRAM Write Interface (`sram_we`, `sram_waddr`, `sram_wdata`)**: Synchronous single-cycle local write port (not an AXI4-Lite/AXI4 slave). If `sram_we` writes to `(bank, row)` on the exact clock cycle `fifo_pop` reads the same `(bank, row)`, the combinational read port observes the pre-write register value (read-old-data semantics).

---

## 5. Formal Verification Scope & Boundaries (`formal_verify.py`)

- **Solver & Engine**: `Yosys 0.70 (yosys-smtbmc)` + `Z3 5.3.1` (Bounded Model Checking `14` steps + Temporal $k$-Induction `12` steps).
- **Initial Reset Assumption**: Step 0 assumes `rst_n == 0`, and Steps $\ge 1$ assume `rst_n == 1`.
- **Proven Safety & Forward-Progress Properties (`P1..P7`)**:
  - `P1_FIFO_BOUNDS`: `fifo_count <= 4`, no push when full (`fifo_count == 4 && !fifo_pop`), no pop when empty (`fifo_count == 0`).
  - `P2_FIFO_PTR_INVARIANT`: Modular pointer distance `(fifo_wr_ptr - fifo_rd_ptr) mod 4 == fifo_count[1:0]`, and `fifo_wr_ptr == fifo_rd_ptr` when `fifo_count in {0, 4}`.
  - `P3_AXI4_STREAM_MASTER_HOLD`: When `m_axis_tvalid && !m_axis_tready`, on the next cycle `m_axis_tvalid == 1` and `m_axis_tdata`, `m_axis_tlast`, `m_axis_tbank` remain invariant.
  - `P4_COMPLETE_PIPELINE_STALL_CONSERVATION`: When `m_axis_tvalid && !m_axis_tready`, all Stage 1 (`s1_valid`, `s1_deq_kv_packed`, `s1_q_packed`, `s1_scale`, `s1_clr_acc`, `s1_sat_mode`, `s1_tlast`, `s1_bank`), Stage 2 (`s2_valid`, `s2_raw_dot`, `s2_scale`, `s2_clr_acc`, `s2_sat_mode`, `s2_tlast`, `s2_bank`), and `fifo_rd_ptr` registers remain strictly unchanged.
  - `P5_SATURATION_CLAMP_AND_STICKY`: Combinational clamp output equals `INT32_MAX`/`INT32_MIN` when `s2_sat_mode && (pos_ovf || neg_udf)` (else `acc_ext_sum[31:0]`), and `sat_overflow_sticky` asserts on the cycle following any un-stalled saturating overflow and remains `1` thereafter.
  - `P6_DEQUANT_ARITH_BOUNDS`: Stage 1 dequantized values `deq_kv` remain within `[-15, +15]`.
  - `P7_NON_STALLED_FORWARD_PROGRESS`: Whenever `!(m_axis_tvalid && !m_axis_tready)`, `fifo_pop` advances to `s1_valid` in 1 cycle, `s1_valid` advances to `s2_valid` in 1 cycle, and `s2_valid` advances to `m_axis_tvalid` in 1 cycle.
- **Explicit Boundary of Formal Proof**: The SMT proof establishes the above safety and 1-cycle stage-transfer properties under post-reset operation; full end-to-end multi-cycle arithmetic equivalence across all 2,560 tensor reductions is verified by the independent Python Golden Model + Verilator co-simulation (`cosim_golden_verilator.py`), and fault detection is verified by deterministic fault injection (`make_buggy_dut()`), not automated AI patch synthesis.