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
What remains for the fabric is a larger generated mesh with per-cell routers, placement, scheduling, and self-hosted control programs all checked against the same transport and composition model.