Skip to main content

Module dae

Module dae 

Source
Expand description

dae — Decoupled Access-Execute for the spatial fabric (FabricTarget::agu).

HiVec keeps its PE array fed by splitting address generation out of the compute path. Our fabric’s analog: a straight-line body’s ADDRESS-generation cells — the untainted arithmetic that feeds a memory tile’s address, whose dependency cone never crosses a load — are hoisted into a parallel AGU lane, while the compute + memory tiles stay in the exec lane in program order. The AGU runs concurrently (a decoupling queue hides the load), so the exec lane’s critical path no longer includes the address arithmetic: decoupled_critical_depth = max(agu_lane_depth, exec_lane_depth) ≤ coupled_critical_depth, strictly less whenever an address chain fed the compute path. The transform is a pure topological re-layout of the SAME cells (memory ops keep their relative order), so it is semantics-preserving by construction — proven by dae_equiv_lock (eval ≡ the coupled body) and measured by dae_perf_lock (the depth ratchet).

Structs§

DaeSchedule
A decoupled schedule: the SAME cells re-laid-out as [agu lane .. | exec lane ..] (AGU cells first), with every Src::Val remapped to the new positions. agu_len cells form the address-generation lane; the rest are the exec lane (compute + memory tiles, memory ops preserving program order).

Functions§

coupled_critical_depth
The coupled body’s critical-path depth: the longest dependency chain feeding result (every operand counts — address arithmetic sits on the compute path).
decouple_access
Decouple a straight-line body into an AGU lane + exec lane. The AGU lane is the set of cells that transitively feed a memory tile’s address AND whose dependency cone never crosses a load (untainted) — the address arithmetic that can be precomputed off the compute path. Everything else (compute + the memory tiles + any pointer-chase address whose cone reads memory) stays in the exec lane, in program order. The two are concatenated AGU-first with every Src::Val remapped, so the layout is a valid topological reordering of the SAME cells — semantics-preserving by construction.
emit_dae_stateful_verilog
Emit a decoupled schedule that MUTATES the heap (HeapWrite/HeapAlloc, not just loads) as a SEQUENCED synthesizable datapath: the decoupled layout (AGU cells hoisted first) is run on the proven state-plane micro-sequencer (emit_state_plane_verilog), which commits heap writes in program order over one shared heap + a bump allocator. Module state_{name} (clk/rst/inN/result/done). Bit-identical to eval_dae (≡ the coupled body ≡ the VM); proven under iverilog by dae_rtl_lock. Distinct from the combinational load-only emit_dae_verilog, which realizes the parallel AGU lane for streaming reads.
emit_dae_testbench
A self-checking combinational testbench for dae_{name}: drive n input vectors (each n_in words) from dae_{name}_in.hex, compare the settled result against the eval_dae oracle in dae_{name}_out.hex.
emit_dae_verilog
Emit a decoupled schedule as COMBINATIONAL Verilog: the AGU lane (address arithmetic) and the exec lane (compute + loads) are emitted as two labelled regions, the loads reading a depth-word heap. Bit-identical to eval_dae (out-of-range loads read 0, matching the model) — proven under iverilog by dae_rtl_lock. LOAD-ONLY: HeapWrite/HeapAlloc/Func are the sequenced-state follow-on and panic here (the honest boundary), so the corpus is streaming reads with computed addresses — the canonical DAE case.
eval_dae
Evaluate a decoupled schedule against inputs + a shared heap, exactly as the coupled body would. Reuses the decision-fabric heap reduction over the re-laid-out cells — so agreement with the coupled eval is the semantics-preservation certificate.
is_heap_cell
True iff the cell touches the state plane (a load/store/alloc) — the side-effecting tiles the exec lane must keep in program order.
schedule_for_target
Schedule a body FOR a described target: decouple its address lane iff the target carries an AGU (target.agu), else leave it coupled (identity). This is the descriptor knob — a fabric without an AGU cannot exploit decoupling, so the transform only fires when the target can realize it. Either way the schedule is semantics-preserving (a proven reordering, or the identity).