Roadmap

Each rung funds and de-risks the next.

Honeycomb is trying to be a general, checkable processor architecture for machine-learning workloads whose bottleneck is data movement. That is a narrow claim, and this page states what has to become true for it to hold, what the evidence is today, and what is being built next.

There is no Honeycomb silicon. The current evidence is Lean theorems, generated RTL, golden simulations, analytical models, and recorded open-source physical-design runs — every claim tagged on the status board.

What must be true

Honeycomb succeeds only if these statements hold together:

• Correctness: the executable semantics, generated RTL, and hardware-visible interfaces refine a single architecture contract.
• Determinism: static kernels have exact or tightly bounded timing, and general control code has a bounded worst-case model.
• Locality: the compiler can keep hot weights and streams near the datapath often enough to avoid recreating the GPU memory wall.
• Physical viability: a memory-rich cell can route and time against real SRAM macros.
• Scale: a uniform mesh can move values, synchronize work, and tolerate defects without introducing special hardware roles.

The architecture page explains the design choice behind those goals; the verification page explains the construction method and its current boundary.

Where the ladder stands

Done and recorded: a generated, macro-backed cell through sky130 signoff — zero-DRC route, clean KLayout DRC and LVS, nine-corner timing with every memory clock-gated and the reset fully timed, the routed netlist passing its golden suite and a lock-step ISA co-simulation at gate level; a streaming kernel datapath at one MAC per cycle; measured clock-gating levers cutting cell power by 62%; a self-booting, capability-gated tile fabric that scatters, launches, and gathers work with no host; and a tile-resident RV32IMA interpreter that boots Linux to a login prompt on the FPGA rig, at the reference emulator’s speed.

In flight — the data plane. Batch-1 decode reads every active weight byte exactly once per token, so tokens/second is aggregate memory bandwidth divided by active bytes. The milestones that follow from that arithmetic: an 8-wide kernel MAC (one shared-exponent block region folded per cycle), double-buffered weight banks so refill overlaps compute, self-advancing DMA descriptor chains so the control plane leaves the per-token path, and multiple injection points at the mesh perimeter for HBM-class streaming.

In flight — the control plane. The supervisor owns descriptor chains and capability grants; guests request work and never touch the fabric’s grant surface. Bulk storage attaches behind the same external-memory seam that boots the machine. A model compiler shards checkpoints into block-format regions sized to tile SRAM and emits the descriptor chains — on this architecture, most serving-stack machinery (batching, expert prefetch, speculative decode) is a schedule on existing seams, not new hardware.

In flight — the proof boundary. The verification page’s tracked edges are roadmap items, not caveats to live with. Four of them closed in the latest review sweep — the compute cell’s AST-level refinement (execute, read/decode, and store write ports), the run-level trace theorems, buffer-level deadlock-freedom, and the deployed fair arbiter. The frontier now: a whole-grid multi-packet liveness theorem, an ISA-correctness story for the RV32 interpreter, and rendering the proved read-reply return capability into the fabric RTL.

Platform. A larger mesh on the current FPGA rig at realistic bandwidth; an inter-board link layer modelled in Lean as a lossy-wire refinement of the proved channel, then run over real pads between boards; and an energy ledger attaching pJ constants to the existing utilization and transport models, so tokens/joule projections carry the same numbers-from-proofs provenance as everything else.

Then silicon: a 16 nm test chip — a 3×3 mesh, the smallest with a fully-interior node, so first silicon measures the genuinely risky pieces (router, nearest-neighbour flow control, DMA distribution, multi-hop kernels) at real interconnect timing rather than just a lone datapath — the point where the performance page’s anchor switches from sky130 estimates to measured silicon.

Performance envelope

The public performance stance is same-node and workload-specific: win where memory traffic dominates latency, be comparable on some compute-bound inference, trail GPUs on raw floating-point density, and offer stronger correctness evidence than conventional accelerator flows. The longer-horizon rows:

Training

Training is a harder claim. The forward pass benefits from resident weights, but backward passes have less reuse and more state; the current model treats training capacity as roughly 8× the inference footprint — a sizing rule, not a per-cell change. The strongest training argument is communication: a mesh can reduce gradients inside the fabric instead of round-tripping through off-chip links. Low-precision gradient numerics still need their own convergence study and their own arithmetic proofs.

Variants

Honeycomb is a parameterized cell generator, not one fixed point. Different chips can choose memory sizes, MAC counts, widths, and numeric options while keeping the same ISA and proof structure:

• Inference build: MAC-rich, block-format transport, optimized for batch-1 decode and long context.
• Training build: more SRAM and bandwidth, wider accumulation, and proof work for training numerics.
• Dense-FP build: reserved for workloads that need wider floating-point multiply rather than low-precision transport.

Within a chip, the goal remains one uniform cell. Across chips, parameters may change only if the proofs re-close under those parameters. A hand-written RTL fork or separate semantics would break the core claim.

Non-goals

Honeycomb is not pursuing cache coherence, virtual memory, implicit remote loads, in-place JIT, a distinct conductor core, service tiles, analog compute-in-memory, FPGA-reconfigurable cells, POSIX, or measured-silicon claims before silicon exists. Parser-level SystemVerilog equivalence is a documented boundary, not a current proof.