11. Mesh and Router
Every chapter so far concerns one cell. This chapter lifts that cell into a 2-D mesh. Above the single-cell proof there are two obligations: transport must deliver the right payload to the right coordinate, and composition must clock the same proved cell at every coordinate. If those obligations hold, the mesh adds communication without adding a second compute semantics.
The RTL for the router and the mesh is future work; what is proved here is the transport-and-composition model the RTL will render.
11.1. The metric
A cell has a position in the mesh. Distance between two positions is Manhattan distance — and it is measured in hops, so it is the transport cost. Cost is zero exactly at the destination.
namespace Honeycomb
#check Coord
#check manhattan
#check manhattan_eq_zero_iff
end Honeycomb
11.2. Deterministic routing and monotone progress
Routing is dimension-order: resolve the horizontal offset first, then the
vertical, then deliver to the local cell. Dimension-order routing is the classic
deadlock-free policy, and here it is what makes progress exact. A hop is one
nearest-neighbour step in the chosen direction.
The first transport theorem is that a hop pays down the remaining cost by exactly one whenever the packet is not already home. Not at most one, not at least one — exactly one. So hop count equals Manhattan distance on the nose, and arrival is neither early nor late. Strict monotone progress — deadlock-freedom — is the immediate corollary.
namespace Honeycomb
#check routeDir
#check hop
#check hop_progress_exact
#check hop_progress
end Honeycomb
11.3. Delivery timing
Iterating the hop gives hops, the position after n cycles. The exact-progress
law lifts to a two-sided timing guarantee: a packet injected at here bound for
dst is at its destination exactly at cycle manhattan here dst, and is
strictly in transit before then.
namespace Honeycomb
#check hops
#check hops_arrives
#check hops_not_before
end Honeycomb
11.4. Packets and faithful transport
A packet carries an opaque payload to a destination. Advancing it changes only its position; the payload is copied verbatim. Payload-independence is the no-corruption guarantee made structural, and because advancing is a function there is no duplication and no drop.
namespace Honeycomb
#check InFlight
#check InFlight.advanceN_pos
#check InFlight.advanceN_payload
end Honeycomb
11.5. Uniform composition
The mesh is the same cell type at every coordinate, each clocked by the single
proved cellClock. The composition operator is pointwise — clocking the mesh at
a coordinate is definitionally the single-cell clock there — so it introduces
no cross-cell coupling in the compute path. Every single-cell theorem lifts
unchanged; in particular the execute-path refinement against the ISA step
function holds at every executing coordinate with a one-line proof. This is "one
proved element, one uniform composition, no special cases" stated as equations.
namespace Honeycomb
#check Mesh
#check meshClock
#check meshClock_pointwise
#check meshClock_execute_refines_step
end Honeycomb
11.6. End to end: transport into a cell
The two layers meet in the delivery theorem. A value produced at cell src and
addressed to dst, carried as a host-write and run for manhattan src dst
network cycles, arrives as that host-write at cell dst — on time, payload
intact — and leaves every other cell of the mesh exactly as it was. The write
delivered is the same applyHostWrites the single-cell lifecycle proofs already
reason about, so the mesh inherits their guarantees without restating them.
namespace Honeycomb
#check deliver
#check injected_packet_delivered
end Honeycomb
Composed with the pointwise refinement, this closes the loop: the mesh is the proved cell, repeated, plus a transport layer that provably delivers on time and touches nothing it should not.
11.7. Generated RTL
The router and a single in-flight packet are rendered to SystemVerilog from the
same Lean RTL DSL as the cell. The combinational honeycomb_router is the
dimension-order decision — routeDir and neighbour — with its dir output
encoded by the shared Dir.code, so the DSL and the emitted Verilog agree on
one numbering by construction. The sequential honeycomb_flit holds one packet
and advances it a hop per clock, pulsing deliver the cycle its position
reaches the destination: exactly hop manhattan src dst, payload carried
verbatim. An Icarus golden test drives it and checks that timing and that
payload against the model.
namespace Honeycomb
#check honeycombRouterModule
#check honeycombFlitModule
#check honeycombRouterSv_from_dsl
end Honeycomb
11.8. A first multi-cell mesh
honeycomb_mesh puts two proved honeycomb_cell instances at (0,0) and
(1,0) with one router-driven transport channel between them. A host-write
injected at the mesh boundary — a data-memory address and value bound for a
destination cell — is advanced one hop per clock and, on arrival, drives that
cell's host-write ports, so the value lands in exactly the destination cell's
data memory and no other cell is touched. It is the RTL image of
injected_packet_delivered, and an Icarus golden test drives it: a write
delivered across the fabric to the right cell, on time, with the other cell's
memory left untouched.
For this first fabric, packet injection is host-driven at the mesh boundary —
a cell-to-network interface, an st to a memory-mapped network port, is future
work — and the single channel carries one packet at a time. What it establishes
is two real cells wired at coordinates with a router between them, and delivery
across the fabric that matches the proved model.
namespace Honeycomb
#check honeycombMeshModule
#check honeycombMeshSv_from_dsl
end Honeycomb
11.9. Cell-to-network interface
The first fabric injected packets at the mesh boundary. This layer lets a
program inject its own: a store (st) to a memory-mapped network aperture
address emits a packet instead of writing local memory. The whole descriptor
fits in the low 15 bits of the store address — bit 14 the network flag, then the
destination coordinate and the remote address — so a program builds it with a
single li and sends with one st; the stored value is the payload.
The addressing convention is proved self-consistent (encode/decode roundtrip),
and a net-store is proved to produce exactly the packet the transport model's
inject builds. Composed with injected_packet_delivered, that closes the loop
in the model: a program's store lands its value in the destination cell's data
memory, on time, and nowhere else.
namespace Honeycomb
#check isNet_encode
#check netStoreEffect_encode
#check netStore_delivered
end Honeycomb
The RTL implements the convention. honeycomb_cell_net is the cell with the
aperture: an st whose address has bit 14 set suppresses the local write and
pulses the net-out ports instead. honeycomb_mesh_net wires that into the
transport — cell0 runs a program and injects, cell1 receives — with no host send
port. An Icarus golden test loads a four-instruction program (li, li, st,
halt) into cell0, starts it, and checks the stored value arrives in cell1's
data memory.
namespace Honeycomb
#check honeycombCellNetModule
#check honeycombMeshNetModule
#check honeycombMeshNetSv_from_dsl
end Honeycomb
The send is not only golden-tested; it has a proved semantic model. execNet
layers the aperture over the base execDecoded, returning the architectural
state and an optional emitted packet. On any ordinary instruction — including a
store to a non-aperture address — it is execDecoded and emits nothing, so the
existing execute-path refinement holds unchanged (execNet_ordinary_refines_step):
the network extension is conservative, with no regression. On an aperture store
it emits the transport inject (execNet_send_inject) and only advances the
program counter, leaving local memory untouched (execNet_send_preserves_data) —
exactly what the RTL does by suppressing the local write. Composed with delivery,
a program's store lands in the destination cell's data memory
(execNet_send_delivered).
namespace Honeycomb
#check execNet_ordinary_refines_step
#check execNet_send_inject
#check execNet_send_delivered
end Honeycomb
Lifted to the busy/halt-gated cell cycle, netCellExecCycle is the model the
generated honeycomb_cell_net corresponds to — the analogue of the base cell's
wordCellExecCycle. On an ordinary cycle it commits the same architectural state
as the ISA step (netCellExecCycle_refines_step), and on a net-store cycle it
emits the transport packet and leaves data memory untouched
(netCellExecCycle_send). So the network cell now stands exactly where the base
cell does: a proved cycle model, generated RTL, and golden tests.
namespace Honeycomb
#check netCellExecCycle_refines_step
#check netCellExecCycle_send
end Honeycomb
11.10. Link contention and deadlock freedom
The transport so far moved one packet at a time. With many in flight, several may want the same outgoing link in one cycle; a router arbitrates, and a blocked packet waits while holding the link it is on. The danger is deadlock: a ring of packets each holding a link the next one needs, forever. Dimension-order routing rules this out, and here is why.
Give every directed link — a channel, a position and an outgoing direction — a global rank, independent of any packet's destination: east/west channels rank below all north/south ones (X is resolved before Y), and within a dimension the rank rises in the direction of travel. The one fact that carries the argument is that the rank strictly increases at every route step — the channel a packet uses next always outranks the one it is on.
namespace Honeycomb
#check routeRank_strictMono
#check chanDep_rank
end Honeycomb
A deadlock is a cycle in the channel-dependency relation (ChanDep): each
packet on one channel needs the next, closing back on itself. But every
dependency edge strictly raises the rank, so a cycle would force a rank to be
strictly less than itself. There is none — contention can delay a packet, never
deadlock the fabric.
namespace Honeycomb
#check chanDep_irrefl
#check no_dep_cycle
end Honeycomb
11.11. Multi-hop: per-cell routers
The meshes above move a packet with one shared router. honeycomb_station gives
each cell its own router and a one-packet inbox: it holds a packet, asks its
router which way to go, and forwards it to that neighbour — or delivers locally
on arrival. honeycomb_line3 wires three stations in a line, so a packet
injected at station 0 for column 2 physically hops 0→1→2 through the middle
station's own routing hardware, one hop per clock, delivered only at the
destination column. Each station reuses the router whose decision mirrors the
proved routeDir; an Icarus golden test injects a packet, checks it arrives at
the far station in exactly two hops with its payload intact, and that the
intermediate stations forward rather than deliver it.
namespace Honeycomb
#check honeycombStationModule
#check honeycombLine3Module
#check honeycombLine3Sv_from_dsl
end Honeycomb
This is real multi-hop over per-cell routers, with one packet in flight; the deadlock-free arbitration proved above is what lets many packets share the links without the fabric locking up.
11.12. Turning routes: a 2-D grid
honeycomb_station2 is the station with all four nearest-neighbour ports, and
honeycomb_grid2 wires four of them into a 2×2 mesh. A packet injected at
(0,0) for (1,1) turns a corner under dimension-order routing — east to
(1,0), then north to (1,1) — two hops through two different per-cell routers,
delivered only at the destination cell. This is the first rendered mesh where a
route actually turns rather than running straight. A golden test drives the
corner route and the two one-hop neighbours, checking hop counts and payloads.
namespace Honeycomb
#check honeycombStation2Module
#check honeycombGrid2Module
#check honeycombGrid2Sv_from_dsl
end Honeycomb
11.13. Link arbitration: flow-controlled contention
The grids so far assume one packet in flight. honeycomb_fstation adds flow
control so many packets can share the links: it accepts a new packet only when
its single buffer is free, grants exactly one offering neighbour by a fixed
priority, and forwards its own packet only when the downstream grants. A blocked
packet waits in place — never dropped — and by the proved dimension-order
deadlock-freedom the waiting can never close into a cycle. honeycomb_fgrid2
wires four of these into a 2×2 with two injection points, so two packets bound
for the same corner contend for its inputs. A golden test injects both the same
cycle and checks that the arbiter serialises them: both are delivered, neither is
lost, and the fabric keeps making progress. This is the hardware payoff of
no_dep_cycle.
namespace Honeycomb
#check honeycombFstationModule
#check honeycombFgrid2Module
#check honeycombFgrid2Sv_from_dsl
end Honeycomb
11.14. A general N×M mesh
honeycombGridModule n m generates the whole fabric: a honeycomb_fstation at
every coordinate, bidirectional nearest-neighbour links between every adjacent
pair — each edge carries a packet lane and a grant in both directions — and a
delivery port per cell, so any coordinate can be a destination. Injection is at
(0,0), and a packet routes there by dimension order over as many hops as the
grid is wide. It is emitted as a concrete 3×3 (honeycomb_grid3), where
(0,0)→(2,2) is a four-hop route that turns; a golden test drives it and the two
straight two-hop edges. Nothing below the generator is new — the same proved
routers, arbitration, and deadlock-freedom, now composed at scale from one Lean
function.
namespace Honeycomb
#check honeycombGridModule
#check honeycombGrid3Sv_from_dsl
end Honeycomb
11.15. A program driving the fabric
honeycomb_progline puts a real program on the mesh. Cell 0 is a
honeycomb_cell_net: it runs a loaded program, and when it executes an st to
the network aperture its net-out ports pulse — those drive station 0's injection
directly, with no host send port. The packet then routes through a line of
flow-controlled honeycomb_fstations to cell 2, a plain honeycomb_cell, where
it lands as a data-memory write. This composes the three proved pieces — the
cell-to-network send, the arbitrated deadlock-free fabric, and a receiving cell —
so a program running on the mesh drives real multi-hop traffic. A golden test
loads the send program, starts cell 0, and checks the value arrives two hops away
in cell 2's memory.
namespace Honeycomb
#check honeycombProglineModule
#check honeycombProglineSv_from_dsl
end Honeycomb
11.16. Backpressure
The line above lets the one packet fit an idle fabric. honeycomb_cell_net_bp
removes that assumption: it is honeycomb_cell_net plus a net_ready input from
the network, and when a net-store is executing but the network cannot accept it
(!net_ready) the cell stalls — it holds the program counter, keeps offering
net_send, and retires nothing — completing the store only once accepted. So a
program can send while the mesh is busy without dropping a packet. Only the
execute step is re-gated; everything else, including the proved net-out logic, is
the net cell verbatim. A golden test drives net_ready low across the store and
checks the cell freezes in place, then releases it and checks the store retires.
namespace Honeycomb
#check honeycombCellNetBpModule
#check honeycombCellNetBpSv_from_dsl
end Honeycomb
What remains is the boot/load/schedule control flow that turns this fabric into a self-hosting machine — checked against the same transport and composition model.