Goals
Honeycomb is trying to be a general, checkable processor architecture for machine-learning workloads whose bottleneck is data movement. It is not a claim that every workload gets faster. It is a narrower claim: if weights and streams can live near the datapath, and if movement is explicit enough to schedule, then latency-bound inference should improve while the machine remains small enough to verify.
There is no Honeycomb silicon. The current evidence is a mix of Lean theorems, generated RTL, golden simulations, analytical models, and recorded open-source physical-design runs.
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 approach page explains the architecture choice behind those goals: one repeated cell, explicit movement, and distance treated as cost.
Evidence standard
Public claims use the book’s evidence categories:
- [proved] means a Lean theorem in the book.
- [modeled] means a checked analytical model using stated constants.
- [recorded] means a measured or externally observed result copied into the book.
- [target] means intended behavior, not completed evidence.
The book is deliberately conservative about boundaries. It proves the model and several RTL-generation paths; it does not yet prove parser-level SystemVerilog equivalence, signoff-clean GDS, power, or fabricated silicon.
Current state
The repository already contains:
- fixed-width processor semantics, instruction encoding, and fetch refinement. [proved]
- kernel dot correctness, block-float identity, scheduling invariants, and overflow bounds. [proved]
- a Lean RTL DSL with generated cell, router, and small mesh RTL. [proved / recorded]
- golden simulation tests for generated SystemVerilog. [recorded]
- a macro-backed sky130 cell that routes with powered SRAM macros, zero DRC violations, and timing met across nine corners at a 29 ns clock. [recorded]
Binding the cell memories as SRAM macros is a central result. The inferred-memory version mapped to 40,994 flip-flops; the macro-backed version maps to 802 flip-flops plus five SRAM macros. That is the difference between a proof/simulation boundary and a plausible physical cell.
Performance envelope
The public performance stance is same-node and workload-specific. Honeycomb targets latency- and memory-bound regimes first, not peak FLOP leadership.
The prefill and batch-1 / batch-32 decode table on the home page is generated from the book’s recorded constants. The longer-horizon rows are:
| Workload | GPU baseline | Honeycomb target | Tag |
|---|---|---|---|
| Long-context decode | KV movement dominates above long contexts | win target: resident KV and SRAM bandwidth reduce off-chip traffic | [modeled] |
| Training, per device | dense GEMM remains strong on GPUs | behind target: Honeycomb trades compute density for memory locality | [modeled] |
| Training, at scale | cluster communication limits scaling | parity-to-ahead target if in-fabric reduce replaces off-chip all-reduce | [modeled / target] |
| Any checked workload | testing only | exact semantics and proof-carrying artifacts where the model is closed | [proved] |
The honest summary: Honeycomb is expected to win where memory traffic dominates latency, be comparable on some compute-bound inference at the same node, trail GPUs on raw floating-point density, and offer stronger correctness evidence than conventional accelerator flows.
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 8x the inference footprint [modeled]. That is a sizing rule: more trainable capacity means more cells, not a magic change in per-cell SRAM ratio.
The strongest training argument is communication. A mesh can reduce gradients inside the fabric instead of round-tripping everything through off-chip links. That still leaves open work: low-precision gradient numerics 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 different memory sizes, MAC counts, widths, and numeric options while keeping the same ISA and proof structure.
- Inference build: MAC-rich, block-float 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.
Near-term milestones
- Finish the physical cell: tighten the floorplan, run signoff DRC, and keep the generated/golden/proved flow intact. [target]
- Scale the mesh evidence: move from small generated meshes to larger fabrics with contention and deadlock-freedom carried through the model. [proved in part / target]
- Close the fetch-after-write rule: prove and generate the deterministic path from written instruction memory to executable code. [target]
- Build a placement proof boundary: prove that a scheduled, placed dataflow graph refines its source graph for well-formed placements. [target]
- Keep public numbers generated: site claims should come from checked constants or recorded evidence, not hand-maintained prose. [recorded / target]
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, a full OS, POSIX, or measured-silicon claims before silicon exists. Parser-level SystemVerilog refinement is a documented boundary, not a current proof.