Module fabric_grid 

fabric_grid — a TRUE reconfigurable CGRA: place a fabric’s dataflow onto a 2-D array of identical tiles and route it through a LOCAL switchbox interconnect. The same silicon runs any fabric by reconfiguration — not a bespoke circuit per program.

Interconnect: each tile drives two INDEPENDENT channels — a vertical vs (to its south neighbor) and a horizontal he (to its east neighbor) — so a value flowing down and a value routed across CROSS without conflict (the standard CGRA switchbox). Dataflow is feed-forward (south/east only), so the array is a combinational DAG. A tile reads its north neighbor’s vs and its west neighbor’s he; it may pass either through, TURN one into the other, source a global input / constant, or COMPUTE (an Alu/Select tapping those inputs) and drive the result onto a channel.

The point (proven in fabric_grid’s S3 tests): whatever the placer/router did, the placed + routed array computes EXACTLY the abstract datapath — certified exhaustively by our own SAT. That is the property a trustworthy CGRA compiler needs: place-and-route is semantics-preserving.

Structs

BoundedBuild

The BoundedExpr instance of Datapath — the tree form.

GateBuild

The shared-gate-DAG instance of Datapath — the form the certifier refutes, linear in the circuit instead of in its unfolding.

Grid

A placed-and-routed CGRA: a rows × cols array of tiles plus the tile/channel that carries the result. Feed-forward (dataflow goes south/east), so it is a combinational DAG.

Tile

One configured CGRA tile.

Enums

CellKind

A tile’s optional compute: an arithmetic op or a predicated select over its visible sources.

Chan

Which output channel of a tile carries the fabric’s result.

Drive

What drives one of a tile’s output channels: a routed source, or the tile’s compute result.

MemOp

The three state-plane operations a Mem tile performs against the shared heap (see CellKind::Mem).

Src2

A value source visible to a tile: its north/west channel inputs, a global input, a constant, or zero (an unused channel).

Constants

TILE_OPERAND_CHANNELS

A mux tile’s operand channels: its north and its west. The interconnect gives each tile two.

Traits

Datapath

The datapath vocabulary a placed grid — or a straight-line cell body — is lowered through.

Functions

cells_datapath

Lower a straight-line LoopCell body through the datapath vocabulary b — the placer’s own lowering vocabulary, and the SPECIFICATION side of the placement obligation. None for a cell with no propositional lowering (a functional unit, a memory tile, a packed-SIMD tile).

cells_to_gates

An ALU/select cell body lowered STRAIGHT INTO THE SHARED GATE DAG at width. Linear in the CELLS: a cell read by three later cells is built once and shared by pointer, where the tree form copies it three times (and their readers copy those, and so on — fib.lg’s 75-cell body unfolds to 1 657 763 tree nodes from a few hundred).

certify_reconfig

Certify the reconfigurable array END TO END (Phase 5): build one grid per source function (they must be same-shape residuals so they place identically), then for EACH config value k prove via our certified SAT that config == k reconfigures the ONE array to be EXACTLY the bespoke island grids[k], for ALL inputs. Returns the per-config verdicts — all true ⇒ the config word (streamed per block from the bytecode frame) losslessly selects any block’s datapath on one physical array: “the fabric IS the interpreter”. Each source is (program, fn_name) with a straight-line residual body.

emit_config_grid_verilog

Emit the N-CONFIG reconfigurable array as combinational RTL — the synthesizable twin of time_mux_n_bounded. ONE rows×cols tile grid runs ANY of grids selected by a cfg-bit config word: every tile computes all N fabrics’ drives over the SHARED (config-muxed) neighbour channels and selects by cfg; the result muxes the N output taps. grids must share dimensions (pad with pad_grid first). This is what a fabric_soc flashes: send cfg (the block index from the bytecode frame) + the inputs and the ONE array becomes that block’s datapath — proven semantics-preserving by certify_config_table.

emit_grid_testbench

A self-checking testbench for the (combinational) tile array: drive each input vector, compare result to the VM oracle from grid_{name}_{in,out}.hex.

emit_grid_verilog

Emit the tile array as combinational RTL: two channel wires (vs/he) per tile, each tile wired only to its north/west neighbours — a genuine nearest-neighbour spatial fabric.

emit_time_multiplexed

Emit the time-multiplexed array as combinational RTL: every tile computes BOTH fabrics’ drives and muxes each channel on ctx; the result muxes the two fabrics’ output taps. One silicon array, two programs — selected by a configuration bit.

eval_grid

Simulate the grid (feed-forward, row-major) and return the PRIMARY output value.

eval_grid_all

Simulate the grid and return ALL output values in all_outs order (for multi-output loop bodies).

eval_grid_all_with_heap

Like eval_grid_all but threads a SHARED heap (for a whole-program block walk with a state plane): every Mem tile touches heap (persisting across blocks), and ALL outputs are returned in all_outs() order so the block-sequencing controller can commit the block’s register writes + read its terminator operand. For a heap-free grid this equals eval_grid_all (the heap stays empty).

eval_grid_with_heap

Simulate a STATE-PLANE grid — one that carries Mem (heap read/write/alloc) tiles — threading ONE shared heap through the tiles in row-major (= placement = program) order, exactly as the model’s eval_cells threads its heap. Non-Mem tiles evaluate combinationally (eval_cell); a Mem tile touches the heap and drives its result onto its output channel. Returns the primary output. This is how Stage X2 proves collections/structs/text run on the grid: eval_grid_with_heap ≡ the whole-program model ≡ the VM.

grid_area

The grid’s area footprint: (rows, cols, used_tiles) — a tile is USED if it computes or drives a non-zero channel. Used to compare placements.

grid_is_combinational

True iff every placed tile is Arith/Select (or pure routing) — i.e. the grid is fully COMBINATIONAL and SAT-lowerable. A Func (division/float) tile has no bitblast lowering, so such a grid is proven by eval ≡ VM + iverilog, not by certify_reconfig/certify_config_table; those refuse a non-combinational grid rather than panic opaquely inside the SAT lowering.

grid_output_datapath

Lower output which (in all_outs order) through the datapath vocabulary b, resolving the array row-major so every tile’s north/west inputs are already lowered (the feed-forward invariant). None when any live tile has no propositional lowering.

grid_output_to_bounded

Lower output which (in all_outs order) to a BoundedExpr at width, naming global inputs via name_in — so the placed+routed array can be proven EQUAL to a reference expressed in the SAME variable namespace (e.g. a loop body’s s0/iv/inv0), exhaustively.

grid_output_to_gates

Lower output which STRAIGHT INTO THE SHARED GATE DAG at width — the certifier’s path. Same walk, same tiles, same circuit as grid_output_to_bounded; it just never materialises the tree, which for a reconvergent datapath is exponentially larger than the array that computes it. None when a tile has no propositional lowering.

grid_to_bounded

The PRIMARY output’s BoundedExpr (output 0) with the default in{k} input names.

pad_grid

Pad a placed grid to a larger target_rows × target_cols array: copy its tiles into the TOP-LEFT corner and leave the rest IDLE. This RESOLVES the same-shape constraint the reconfigurable-array proof needs (time_mux_n_bounded requires equal dimensions) — grids of DIFFERENT shapes co-reside on ONE array without touching any datapath. The output taps keep their positions (valid since the array only GREW), and the added IDLE tiles drive zero; because dataflow is feed-forward (south/east only), no downstream idle tile ever feeds an upstream one, so the padded grid computes EXACTLY the original (eval_grid(pad_grid(g, R, C)) == eval_grid(g)). Panics if asked to shrink.

route_leveled

AREA-MINIMIZING placer (level scheduling). The naive route_straight_line gives every cell two rows (a routing row + a compute row). But a cell whose operands are all global inputs or constants (topological LEVEL 0) needs NO routing row — its operands are tapped directly — so all level-0 cells share ONE compute row (row 0), packed across columns. Deeper cells still get their own routing+compute rows. For DAGs with input-parallelism this collapses the row count (a chain saves a little; a wide fan-in tree saves a lot). Correctness is unchanged — the S3 SAT proof validates the compact placement exactly as it did the naive one.

route_loop_body

Map a LOOP BODY onto the tile array. Same diagonal placement + Manhattan routing as the straight-line case, but each LoopCell may be a Select (a mux tile — the grid already models it), and the body produces MULTIPLE outputs (one per loop-carried next-state register, in next order). Global-input / constant operands are tapped directly; cell-value operands route (each distinct producer takes one of the tile’s two channels — a computed PREDICATE routes exactly like a computed data arm, and two ports reading one producer share a channel). This grid is the combinational BODY datapath of a loop-on-a-grid — the controller (counter / fabric predicate) latches its outputs, exactly as with the hand-wired body.

route_straight_line

The placer + router. Map a straight-line fabric (FabricOp SSA, from the real compiled residual) onto the tile array. Placement: cell i computes on the diagonal at (2(i+1), i) — its own column i carries its result downward. Routing: an operand that is a global input or constant is TAPPED directly (inputs fan out for free); an operand that is another cell’s value is routed via a Manhattan path — forked EAST off its column (he←N, which coexists with the column’s downward vs←N, so fan-out costs nothing) and turned back into the consumer’s north (vs←W) or read from its west. Correct by construction; the S3 SAT proof catches any slip.

run_program_cfg_on_grid

Run a whole (acyclic-control-flow) function on the reconfigurable GRID (Stage X4 — the whole-program XPU). Each basic block’s straight-line body is PLACED on a fresh tile array (route_loop_body, the block’s live-in registers as inputs) with its downstream Srcs as the grid’s outputs — every register write, then the terminator’s predicate/return operand; eval_grid_all reads them off the placed array, the register file is updated, and a block-sequencing controller walks the terminator graph (Jump/Branch/Return), reconfiguring the array to the next block. So a BRANCHY whole program runs as spatial dataflow on ONE array (each block a reconfiguration), proven ≡ eval_program_cfg_fabric ≡ the VM. A block may carry Mem (heap read/write/alloc) tiles: ONE heap is threaded across every reconfiguration (eval_grid_all_with_heap), so collections/structs persist across blocks — the state plane. (Loops are the separate loop fabric.)

tile_channel_demand

How many operand channels the switchbox must route into ONE tile for cell.

time_mux_bounded

The combined output of a TIME-MULTIPLEXED array: one physical grid whose every tile is muxed by a ctx selector between fabric a’s config (ctx=1) and fabric b’s config (ctx=0). Because the neighbour channels are themselves ctx-muxed, when ctx=1 the whole array carries a’s dataflow and when ctx=0 it carries b’s — proven in the P3 test. a and b must share dims.

time_mux_n_bounded

The RECONFIGURABLE array (Phase 5): ONE tile grid runs ANY of grids selected by a CONFIG WORD — the generalization of time_mux_bounded from a 1-bit ctx (2 fabrics) to a cfg_width-bit word (N fabrics). Every tile computes all N fabrics’ drives over the SHARED muxed neighbour channels, then selects by config; the output tap muxes likewise. This is “the fabric IS the interpreter”: the config word (streamed per block from the LGB1 frame) reconfigures the SAME silicon to be any block’s datapath. config is fixed to a concrete value here so the lock proves, per value k, that the reconfigured array is EXACTLY the bespoke island grids[k] (config == k ⇒ array ≡ grids[k]). All grids must share dimensions (same-shape fabrics place identically).

unroutable_cell

The first cell of cells the router cannot place, as (cell index, channels it demands). None when every cell fits the interconnect. The gate a certifier consults BEFORE calling route_loop_body, so an unplaceable body is declined by name instead of panicking inside the placer.