kvfabric

A decode-phase KV-cache engine for LLM inference, written in SystemVerilog and carried all the way to a sign-off-clean GDSII on SkyWater 130nm — then scaled to sixteen nodes running sequence-parallel decode over a 4x4 torus NoC.

Paged KV-cache allocation, KV quantization, and streaming online softmax are established techniques for long-context decode. All three were designed in software, assuming an idealized interconnect. This project asks what changes when they are built as hardware and run over an interconnect that actually exists.

Results

Physical design (sky130, LibreLane)	0 DRC, 0 LVS, setup WNS = TNS = 0, hold WNS = TNS = 0
Area / power	0.598 mm², 7.93 mW @ 65 ns (~15.4 MHz)
Formal	kv_allocator free-list invariants proved by k-induction (SymbiYosys + z3)
RTL	17 modules, ~3.5K lines
Verification	15 cocotb testbenches, bit-exact against golden NumPy models, under full throughput and randomized backpressure; 10 model-level test suites
Mesh	16 nodes over an unmodified 4x4 torus, bit-exact in RTL

The node

                  ┌────────────────────────────────────────────────────┐
                  │                   kvfabric_node                    │
 host ──cfg bus──▶│  ctrl_regs (RO status: free_count, busy, m)        │
                  │                                                    │
 host ─newblk_req▶│  kv_allocator ──▶ kv_block_table                   │
                  │                        ▲ lookup (cached per block) │
 host ──q vector─▶│  q regfile             │                           │
                  │       │           kv_fetch ◀──▶ mem_port ──────────┼──▶ mem_model
                  │       │          (read-ahead FIFO)                 │    (sim only,
                  │       │                │ K word     │ V word       │    param. latency,
                  │       │                ▼            ▼              │    stands in for
                  │       │         kv_dequantizer (shared)            │    off-chip DRAM/HBM)
                  │       │                │            │              │
                  │       └──────────▶ qk_dot           │              │
                  │                        │ score      │              │
                  │                        ▼            ▼              │
                  │                   online_softmax_unit              │
                  │                        │ (m, l, acc)               │
                  │                        ▼                           │
                  │                   kv_quantizer                     │
                  │                        │ (exp + INT4 codes)        │
                  │                        ▼                           │
                  │                   noc_adapter ─────────────────────┼──▶ torus router
                  └────────────────────────────────────────────────────┘    LOCAL port

Three ideas do the work:

• Paged block allocation — a hardware analog of vLLM's PagedAttention. A physical-block free list (kv_allocator) plus a logical→physical translation layer (kv_block_table). The two are deliberately separate modules: the free list is the piece with invariants crisp enough to prove, and folding a lookup RAM into it muddies both.
• Group-wise power-of-two quantization — INT4/INT8 with one shared scale per group of elements, chosen as a power of two so dequantization is a shift. No dividers anywhere in the datapath.
• Streaming online softmax — the FlashAttention merge rule in hardware, so a node never materializes the full attention matrix and partial results from different nodes can be combined in any order.

Key parameters (all DSE axes): BLOCK_SIZE 16, HEAD_DIM 64, MAX_BLOCKS 64, QUANT_GROUP_SIZE 32, QUANT_BITS 4, PREFETCH_DEPTH 2.

kvfabric-mesh, and the result that came out of it

A sequence's KV cache is sharded by position across N nodes, one per torus router LOCAL port. Each node produces a local partial (m, l, acc); those are reduced across the NoC by the online-softmax merge rule until one node holds the global result. The merge is associative and commutative, so any schedule forming a spanning in-tree computes the same answer — which makes the schedule a pure cost decision.

The central finding is that endpoint ejection bandwidth, not network topology, is the binding constraint. Deriving the schedule from the router's real routing function — transcribed from the NoC's actual xy_route_logic, not from an idealized model — yields single-hop transfers, flat peak link load, and deadlock freedom without virtual channels, structurally rather than by adding buffering.

Two further results, both measured against RTL rather than asserted:

• The gather is unnecessary. A reduce-scatter left sharded measures 565 cycles against 1120 for reduce-scatter + gather.
• Reduction-internal wire precision dominates mesh accuracy — far more than arithmetic precision. INT4 on the wire compounds to 26.6% error across four hops, against the datapath's own 0.3–0.5%. INT8 cuts that to 1.6%.

Layout

rtl/        17 SystemVerilog modules
models/     golden NumPy reference models — the verification oracle
tb/         cocotb testbenches + pytest runners (Icarus Verilog)
tests/      model-level tests (fixed-point vs float oracle, cost models)
formal/     SymbiYosys k-induction proof of the allocator
docs/        architecture.md — the living spec
briefs/     D1–D6 engineering task briefs
progress.md dated, newest-first build and debug log

Method

Two rules that shaped everything here:

1. Golden Python model before RTL, always. For numerically approximate hardware (fixed-point exp(), for one), the fixed-point model is validated against the float oracle first, and only then is RTL written bit-exact to the fixed-point model.
2. Bit-exact, or explicitly tolerance-bounded. Every testbench runs under both full throughput and randomized backpressure, because a design that only works when its consumer is always ready is not finished.

docs/architecture.md marks each module implemented, verified only once its RTL and testbenches actually pass, and progress.md records the bugs and how they were fixed — including the failures, which are usually the more useful half.

Running it

python3 -m venv --system-site-packages .venv
. .venv/bin/activate && pip install -r requirements.txt

pytest tests/                 # model-level suites, fast, no simulator needed
pytest tb/ -m "not slow"      # cocotb RTL testbenches (needs Icarus Verilog)
pytest tb/                    # everything, including the 16-node mesh

Formal proof of the allocator:

cd formal
sby -f kv_allocator_prove4.sby    # k-induction, capacity 4   (~2 s)
sby -f kv_allocator_prove8.sby    # k-induction, capacity 8   (~35 s)

Requires SymbiYosys, Yosys, and z3. See formal/README.md for the strengthening invariants, the one environment assumption the proof rests on, and its scope limits — all three are stated honestly there rather than glossed.

Note on the mesh tests: the 4x4 torus NoC is a separate, pre-existing RTL project and is not vendored here. The mesh testbenches expect it alongside this repo; the node-level tests are self-contained and run without it.

Not built yet

Stated plainly, since a spec that hides its gaps is not useful:

• sram_l2 — an on-chip OpenRAM macro above mem_port. The closed physical design run does not include it.
• The KV write path (quantize and store new tokens).
• mem_port is a parameterized latency model standing in for off-chip DRAM/HBM. There is no real PHY.
• Empty shards: a node holding no tokens never emits a partial, so the reduction hangs. The models handle this; the RTL needs an identity-partial path.
• Overlapping merge with reception, and packing 8 accumulator codes per framed value (145 flits → 89 at HEAD_DIM=64).

Papers

The mesh work is written up for IEEE Embedded Systems Letters and ACM TECS, with an arXiv preprint. Links will be added here once they are live.