Module gpu_simt_rtl 

gpu_simt_rtl — the GPU processor edge: a tuneable SIMT data-parallel engine in silicon.

The NPU (fabric_rtl::LoopFabric) is a REDUCTION — one body streamed by a loop counter, many→one. A GPU is the opposite: N independent spatial lanes, each running the SAME compiled straight-line kernel (the “shader”) on its OWN data, producing N INDEPENDENT outputs (a MAP), each lane gated by its own predicate bit (SIMT divergence). The lanes are WIRED (spatial) and all compute in ONE cycle — no warp scheduler, no fetch/decode/dispatch — exactly the deterministic Futamura primitive the other edges use, applied across lanes.

One parametrized engine specializes to every mode (the “best of all worlds”):

• SIMT — predicated = true: a per-lane mask; a masked lane contributes 0 (inert).
• SIMD — the special case where every lane is unmasked (mask all-ones).
• map-then-reduce — reduce = Some(op): the N lane outputs feed a cross-lane warp-reduce, which is exactly the NPU’s accumulator (an AluOp fold) placed spatially.
• uniform vs varying — each kernel input is either a broadcast scalar shared by every lane (a GPU “uniform”) or a per-lane vector element (a “varying”).

Physical interface. Exposing every lane’s I/O as top-level ports would be thousands of pins (unroutable on an FPGA, an absurd pad ring on an ASIC). Like the other accelerators (dram_executor, infinichip), the tile has a NARROW streaming interface — a 64-bit din loaded slot-by-slot into an internal lane register file, a go pulse that runs all lanes in parallel (the spatial SIMT step), and a din-width dout read back by raddr. The parallel COMPUTE is the GPU essence; the streaming I/O is how a real accelerator talks to memory.

A lane IS the existing certified straight-line fabric residual (fabric_rtl::FabricOp), so lane arithmetic is not reinvented: the kernel is compiled from English by the REAL compiler (residual_from_source), each lane is a verbatim spatial copy, and the map is proven ≡ the VM lane-by-lane — by direct model comparison and, on a narrow width, EXHAUSTIVELY by our own certified SAT (fabric_to_bounded + prove_unsat). 64-bit signed wrapping, bit-identical to the VM’s Int (its fixed-width projection), matching fabric_rtl.

Structs

SimtEngine

A tuneable SIMT data-parallel engine — the GPU tile.

Enums

LaneArith

The datapath multiply strategy for the lane’s a·x + b arithmetic — a first-class, tuneable, SAT-certified knob. Every strategy is functionally identical (a·x + b, 64-bit wrapping); they trade cycle count against physical (routing / antenna) friendliness.

Slot

One streamed load slot: a broadcast uniform input, the packed mask word, or a per-lane varying input. The load order (uniforms, then mask, then per-lane varyings) is the single source of truth shared by the RTL load FSM, the testbench, and the golden hex writer.

Functions

emit_gpu_simt_testbench

A self-checking iverilog testbench: for each of n_vectors vectors, reset the load counter, stream the load slots from gpu_{name}_in.hex, pulse go (all lanes compute in one cycle), then read back every lane output + the reduced scalar via raddr and compare against the VM oracle in gpu_{name}_out.hex. Prints PASS/FAIL. Layout matches write_gpu_hex.

emit_gpu_simt_verilog

Emit the SIMT engine as synthesizable RTL: a narrow streaming interface (a 64-bit din loaded slot-by-slot into an internal lane register file, a go pulse that runs ALL lanes in one cycle — the spatial SIMT step — and a dout read back by raddr) wrapped around N verbatim copies of the certified kernel, with per-lane predication and an optional warp-reduce. Module name gpu_{name}. Readback: raddr in 0..N selects a lane output; raddr == N selects the reduced scalar (when a reduce is present).

eval_gpu_simt

Evaluate the SIMT engine (the pure-Rust reference the silicon is checked against — N calls to the already-proven eval_fabric, one per lane). lane_inputs[j] are lane j’s n_in kernel inputs (uniform inputs are set equal across lanes by the caller); mask[j] gates lane j when predicated (masked → 0). Returns the per-lane outputs and the optional warp-reduced scalar.

load_slots

The canonical load-slot sequence for an engine.

signoff_advisory

A SOFT signoff advisory (NEVER a lock, NEVER blocks emission): the wide combinational strategies (Combinational, DecomposedFma) at datapath widths >= 32 are met1-antenna-dense on Sky130 — even after fan-out splitting and low utilization, a handful of met1 area-ratio violations remain (empirically ~10 on the N=4 flagship). SequentialFma (one reused adder per lane, bounded fan-out) is antenna-trivial. Returns Some(warning) for the dense envelope, None otherwise.

simt_masked_lane_to_bounded

The BoundedExpr of ONE lane’s predicated output: mask ? kernel : 0 — the SIMT divergence atom (a certified select over the compiled kernel). Uses the single-lane input names in{k} (all lanes are byte-identical modulo the lane suffix, so one lane’s proof covers the array).

simt_reduce_to_bounded

The BoundedExpr of the warp-reduce tail — a left fold of op over the lane-output variables out0..out{N-1}. Lowers the reduce so our SAT can certify it equals an independent fold (that every lane is summed, none dropped or duplicated).

simt_sequential_fma_to_bounded

The BoundedExpr of the SEQUENTIAL shift-add multiply a·x, UNROLLED over width bits, for single-lane inputs a = in0, x = in1. This is the exact combinational image of the SequentialFma FSM’s width-step recurrence: acc += (x[i] ? a<<i : 0) for i in 0..width. Our own certified SAT proves this shift-add equals the hardware a*x for ALL inputs — so the strategy switch is FREE (no divergence). b and the predicate are the same tail the other strategies share, already certified by gpu_kernel_is_certified_equal_to_the_vm_element_op / gpu_predication_is_certified.

simt_sliced_pp_to_bounded

The BoundedExpr of ONE emitted sliced partial product pp — the fan-out-bounded image of the single-select mux mp[0] ? mc : 0. It models the emitted Verilog exactly: pp = { {G{s}} & mc[hi:lo] , ... } over select_slice groups of G = width / select_slice bits, where every msel copy equals the ONE select bit s = mp0. Group g occupies bits [g*G .. g*G+G-1], and its value is s==1 ? mc[hi:lo] : 0 (a G-wide select). Building pp from these per-group selects and proving pp == (s==1 ? mc : 0) CERTIFIES the byte-slicing drops or misaligns no bit — closing the gap where the slice was previously only iverilog-checked.

write_gpu_hex

Build the golden input/output hex, computing the outputs with eval_gpu_simt — the reference the silicon lock separately certifies bit-identical to the VM (so these goldens ARE the VM oracle). The input hex is one word per load slot per vector (uniforms, mask, then per-lane varyings — the load_slots order); the output hex is each lane output then the reduced scalar. vectors[t] provides (lane_inputs, mask) for vector t. Returns (in_hex, out_hex).