Honeycomb

A small, memory-rich processor cell, verified in Lean and tiled into a mesh. The RTL that goes to silicon is generated from the same proof that specifies it.

Honeycomb is one cell, repeated. There are no special cores, no memory tiers, and no boot master. The only thing that tells one place in the mesh apart from another is distance. Because every cell is the same proved element, verifying the machine means verifying one cell and one way of composing it — and the specification, the proofs, and the generated RTL are all checked together by a single build.

proved cell, repeated across the mesh

40,994 → 802

flip-flops, once the hot memories bind as SRAM macros

22 ns

clock the first routed cell meets at every sky130 corner

uses of sorry; the execute path is proved against the ISA

One cell, repeated

A flat mesh. A 2-D grid of identical cells with nearest-neighbour links. “Compute”, “memory”, “boot”, and “I/O” nodes are programs placed on the same hardware, not different chips.
Distance is the only cost. The one thing that varies is how far a packet travels. Routing pays that distance down one hop per cycle, so a message arrives exactly when its distance says it will. That timing is proved, not estimated.
Memory sits next to compute. Each cell keeps its working set in local SRAM and reads it into the datapath. Binding those memories as real SRAM macros is what took the cell from 40,994 flip-flops down to 802.

One ISA, two kinds of work

The same cell runs two very different workloads. Branch-free dataflow kernels — the fused multiply-accumulate that dominates machine-learning math — run on a short, fixed schedule with exact timing. General control code, including the tools the machine needs to eventually host itself, runs on the same eleven-instruction ISA with bounded worst-case timing. It is a difference of program, not of silicon.

How it’s built

Lean spec→RTL DSL→SystemVerilog→golden sim→sky130 P&R

rtl/honeycomb_cell.sv is not a template. It is rendered from a value in a Lean RTL DSL, and the execute path of that DSL is proved to refine the ISA’s step function. Golden simulations check the emitted Verilog against the model, and OpenLane takes it through synthesis, placement, routing, and timing on the open sky130 process. If any generated file drifts from its source, the build fails.

There is no Honeycomb silicon yet. The current state — how it compares to a GPU, and what is proved versus intended — is on the status page.

Read the book Where it stands Licensing & evaluation