Honeycomb
A proof-first processor for memory-bound machine learning.
Honeycomb is built from one memory-rich cell, repeated across a mesh. The cell keeps weights close to the datapath, exposes movement explicitly, and is specified in Lean alongside the RTL generator and refinement proofs.
The problem
Interactive inference is often limited by movement, not arithmetic. On a GPU, batch-1 decode — one request, one token at a time — delivers well under 1% of the chip’s compute-bound rate because each step rereads weights through a distant memory system. Honeycomb changes the unit of computation: each cell owns local SRAM and reads resident weights directly into the datapath.
The second problem is trust. Accelerator specifications, compiler schedules, RTL, and physical implementations usually live as separate artifacts checked against each other by testing. Honeycomb is organized so the architecture contract, executable model, proofs, and generated RTL stay tied together.
The design
Honeycomb keeps the machine deliberately uniform:
- one repeated cell with local SRAM, scalar/control state, a MAC datapath, and network ports;
- one ISA used for both static kernel programs and general control code;
- one explicit movement model over a nearest-neighbour mesh;
- one proof boundary connecting executable semantics to generated RTL.
That is the architecture in one sentence: keep hot data near the compute path, make movement visible, and keep the hardware small enough to prove.
Performance target
The comparison below is same-node: it factors out process generation so the question is architecture rather than fabrication. GPU figures are measured on an RTX 2000 Ada running GPT-2. Honeycomb figures are model targets generated from the book’s recorded constants, not measured silicon results.
| Workload | GPU (measured) | Honeycomb (target) | Evidence |
|---|---|---|---|
| LLM prefill (compute-bound) | 76,206 tok/s (100.0% of peak) | about 0.9×, comparable; MAC utilization ~89–91% | modeled |
| Decode, batch-1 (latency-bound) | 430 tok/s (0.6% of peak) | about 200× faster; weights stay resident, no memory wall | measured / modeled |
| Decode, batch-32 (throughput) | 8,523 tok/s (11.2% of peak) | about 9× faster; batching recovers some GPU throughput | measured / modeled |
GPU: RTX 2000 Ada, GPT-2, same-node. Percentages are computed from the book’s recorded constants.
The intended win is latency-bound inference and long-context work where resident data and explicit movement matter. Compute-bound prefill is expected to be comparable at the same node; raw floating-point density is not the goal. There is no Honeycomb silicon yet.
Current status
The strongest physical result so far is a generated, macro-backed cell taken through sky130 placement, routing, and static timing: honeycomb_cell_mac reaches a powered routed close with 0 DRC violations and timing met across all nine corners at a 29 ns clock. Binding the hot memories as SRAM macros cut mapped flip-flops from 40,994 to 802.
The book is the detailed evidence record. The site pages give the shorter path: