logicaffeine_compile/codegen_sva/
dae.rs

1//! dae — Decoupled Access-Execute for the spatial fabric (`FabricTarget::agu`).
2//!
3//! HiVec keeps its PE array fed by splitting address generation out of the compute path. Our fabric's analog:
4//! a straight-line body's ADDRESS-generation cells — the untainted arithmetic that feeds a memory tile's
5//! address, whose dependency cone never crosses a load — are hoisted into a parallel **AGU lane**, while the
6//! compute + memory tiles stay in the **exec lane** in program order. The AGU runs concurrently (a decoupling
7//! queue hides the load), so the exec lane's critical path no longer includes the address arithmetic:
8//! `decoupled_critical_depth = max(agu_lane_depth, exec_lane_depth) ≤ coupled_critical_depth`, strictly less
9//! whenever an address chain fed the compute path. The transform is a pure topological re-layout of the SAME
10//! cells (memory ops keep their relative order), so it is semantics-preserving by construction — proven by
11//! `dae_equiv_lock` (eval ≡ the coupled body) and measured by `dae_perf_lock` (the depth ratchet).
12
13use super::fabric_rtl::{
14    emit_state_plane_verilog, eval_decision_fabric_heap, DecisionFabric, LoopCell, Src,
15};
16use super::fabric_target::FabricTarget;
17
18/// A decoupled schedule: the SAME cells re-laid-out as `[agu lane .. | exec lane ..]` (AGU cells first), with
19/// every `Src::Val` remapped to the new positions. `agu_len` cells form the address-generation lane; the rest
20/// are the exec lane (compute + memory tiles, memory ops preserving program order).
21#[derive(Clone, Debug)]
22pub struct DaeSchedule {
23    pub n_in: usize,
24    pub layout: Vec<LoopCell>,
25    pub result: Src,
26    /// The number of leading `layout` cells that form the AGU lane (`0` ⇒ nothing decoupled).
27    pub agu_len: usize,
28    /// For each `layout` cell, whether it belongs to the AGU lane (`true`) or the exec lane (`false`).
29    pub is_agu: Vec<bool>,
30}
31
32impl DaeSchedule {
33    /// Every AGU-lane cell must be a PURE address computation — never a heap tile. The structural heart of the
34    /// decoupling: the address lane has no side effects, so hoisting it cannot reorder memory.
35    pub fn agu_is_pure(&self) -> bool {
36        self.layout
37            .iter()
38            .zip(&self.is_agu)
39            .filter(|(_, a)| **a)
40            .all(|(c, _)| !is_heap_cell(c))
41    }
42
43    /// The exec lane's critical-path depth, treating every AGU-lane output as depth 0 (supplied by the parallel
44    /// lane through the decoupling queue). This is the compute path the clock actually sees.
45    pub fn exec_lane_depth(&self) -> usize {
46        let mut depth = vec![0usize; self.layout.len()];
47        let mut ans = 0usize;
48        for i in 0..self.layout.len() {
49            if self.is_agu[i] {
50                continue; // AGU cells contribute through the parallel lane, not the exec path
51            }
52            let d = 1 + self.operand_exec_depth(&self.layout[i], &depth);
53            depth[i] = d;
54            ans = ans.max(d);
55        }
56        ans
57    }
58
59    /// The AGU lane's own critical-path depth (runs concurrently with the exec lane).
60    pub fn agu_lane_depth(&self) -> usize {
61        let mut depth = vec![0usize; self.layout.len()];
62        let mut ans = 0usize;
63        for i in 0..self.layout.len() {
64            if !self.is_agu[i] {
65                continue;
66            }
67            let d = 1 + cell_operands(&self.layout[i])
68                .iter()
69                .map(|s| match s {
70                    Src::Val(k) => depth[*k],
71                    _ => 0,
72                })
73                .max()
74                .unwrap_or(0);
75            depth[i] = d;
76            ans = ans.max(d);
77        }
78        ans
79    }
80
81    /// The throughput-limiting depth of the decoupled schedule: the two lanes run concurrently, so the clock
82    /// sees the DEEPER of them — not their sum.
83    pub fn decoupled_critical_depth(&self) -> usize {
84        self.agu_lane_depth().max(self.exec_lane_depth())
85    }
86
87    fn operand_exec_depth(&self, cell: &LoopCell, depth: &[usize]) -> usize {
88        cell_operands(cell)
89            .iter()
90            .map(|s| match s {
91                // An AGU output is precomputed in the parallel lane ⇒ free to the exec path.
92                Src::Val(k) if self.is_agu[*k] => 0,
93                Src::Val(k) => depth[*k],
94                _ => 0,
95            })
96            .max()
97            .unwrap_or(0)
98    }
99}
100
101/// True iff the cell touches the state plane (a load/store/alloc) — the side-effecting tiles the exec lane
102/// must keep in program order.
103pub fn is_heap_cell(cell: &LoopCell) -> bool {
104    matches!(
105        cell,
106        LoopCell::HeapRead { .. }
107            | LoopCell::HeapWrite { .. }
108            | LoopCell::HeapAlloc { .. }
109            | LoopCell::MemRead { .. }
110    )
111}
112
113/// Every `Src` operand a cell reads (compute + address + value, in a stable order).
114fn cell_operands(cell: &LoopCell) -> Vec<Src> {
115    match cell {
116        LoopCell::Arith { a, b, .. }
117        | LoopCell::Func { a, b, .. }
118        | LoopCell::VectorArith { a, b, .. } => vec![*a, *b],
119        LoopCell::Select { ca, cb, t, e, .. } => vec![*ca, *cb, *t, *e],
120        LoopCell::HeapRead { addr } | LoopCell::MemRead { addr } => vec![*addr],
121        LoopCell::HeapWrite { addr, val } => vec![*addr, *val],
122        LoopCell::HeapAlloc { size } => vec![*size],
123    }
124}
125
126/// The ADDRESS-class operands of a cell (what an AGU would precompute): a memory tile's address / alloc size.
127/// Non-memory cells have none.
128fn address_operands(cell: &LoopCell) -> Vec<Src> {
129    match cell {
130        LoopCell::HeapRead { addr } | LoopCell::MemRead { addr } => vec![*addr],
131        LoopCell::HeapWrite { addr, .. } => vec![*addr],
132        LoopCell::HeapAlloc { size } => vec![*size],
133        _ => vec![],
134    }
135}
136
137/// The coupled body's critical-path depth: the longest dependency chain feeding `result` (every operand
138/// counts — address arithmetic sits on the compute path).
139pub fn coupled_critical_depth(cells: &[LoopCell], result: Src) -> usize {
140    let mut depth = vec![0usize; cells.len()];
141    for i in 0..cells.len() {
142        depth[i] = 1 + cell_operands(&cells[i])
143            .iter()
144            .map(|s| match s {
145                Src::Val(k) => depth[*k],
146                _ => 0,
147            })
148            .max()
149            .unwrap_or(0);
150    }
151    match result {
152        Src::Val(k) => depth[k],
153        _ => depth.iter().copied().max().unwrap_or(0),
154    }
155}
156
157/// Remap a `Src` through the old→new cell-index table (leaves `In`/`Const` untouched).
158fn remap(src: Src, newpos: &[usize]) -> Src {
159    match src {
160        Src::Val(k) => Src::Val(newpos[k]),
161        other => other,
162    }
163}
164
165/// Rewrite a cell's operand `Src`s through `newpos`.
166fn remap_cell(cell: &LoopCell, newpos: &[usize]) -> LoopCell {
167    match *cell {
168        LoopCell::Arith { op, a, b } => LoopCell::Arith {
169            op,
170            a: remap(a, newpos),
171            b: remap(b, newpos),
172        },
173        LoopCell::Func { unit, a, b } => LoopCell::Func {
174            unit,
175            a: remap(a, newpos),
176            b: remap(b, newpos),
177        },
178        LoopCell::VectorArith { op, ty, a, b } => LoopCell::VectorArith {
179            op,
180            ty,
181            a: remap(a, newpos),
182            b: remap(b, newpos),
183        },
184        LoopCell::Select { cmp, ca, cb, t, e } => LoopCell::Select {
185            cmp,
186            ca: remap(ca, newpos),
187            cb: remap(cb, newpos),
188            t: remap(t, newpos),
189            e: remap(e, newpos),
190        },
191        LoopCell::HeapRead { addr } => LoopCell::HeapRead {
192            addr: remap(addr, newpos),
193        },
194        LoopCell::MemRead { addr } => LoopCell::MemRead {
195            addr: remap(addr, newpos),
196        },
197        LoopCell::HeapWrite { addr, val } => LoopCell::HeapWrite {
198            addr: remap(addr, newpos),
199            val: remap(val, newpos),
200        },
201        LoopCell::HeapAlloc { size } => LoopCell::HeapAlloc {
202            size: remap(size, newpos),
203        },
204    }
205}
206
207/// Decouple a straight-line body into an AGU lane + exec lane. The AGU lane is the set of cells that
208/// transitively feed a memory tile's address AND whose dependency cone never crosses a load (untainted) — the
209/// address arithmetic that can be precomputed off the compute path. Everything else (compute + the memory
210/// tiles + any pointer-chase address whose cone reads memory) stays in the exec lane, in program order. The
211/// two are concatenated AGU-first with every `Src::Val` remapped, so the layout is a valid topological
212/// reordering of the SAME cells — semantics-preserving by construction.
213pub fn decouple_access(cells: &[LoopCell], result: Src, n_in: usize) -> DaeSchedule {
214    let n = cells.len();
215
216    // taint[i]: cell i's cone contains a load/store/alloc (so it cannot be hoisted onto a pure address lane).
217    let mut taint = vec![false; n];
218    for i in 0..n {
219        taint[i] = is_heap_cell(&cells[i])
220            || cell_operands(&cells[i])
221                .iter()
222                .any(|s| matches!(s, Src::Val(k) if taint[*k]));
223    }
224
225    // feeds_addr[i]: cell i transitively feeds some memory tile's address operand. Seed from address operands,
226    // then close under predecessors (operand indices are strictly smaller, so one reverse sweep suffices).
227    let mut feeds_addr = vec![false; n];
228    for cell in cells {
229        for s in address_operands(cell) {
230            if let Src::Val(k) = s {
231                feeds_addr[k] = true;
232            }
233        }
234    }
235    for i in (0..n).rev() {
236        if feeds_addr[i] {
237            for s in cell_operands(&cells[i]) {
238                if let Src::Val(k) = s {
239                    feeds_addr[k] = true;
240                }
241            }
242        }
243    }
244
245    // The AGU lane: untainted address-feeding cells (pure by construction, and predecessor-closed).
246    let is_agu_orig: Vec<bool> = (0..n).map(|i| feeds_addr[i] && !taint[i]).collect();
247
248    // Concatenate AGU-first (ascending original order preserves dependencies within each lane), remapping Vals.
249    let order: Vec<usize> = (0..n)
250        .filter(|&i| is_agu_orig[i])
251        .chain((0..n).filter(|&i| !is_agu_orig[i]))
252        .collect();
253    let mut newpos = vec![0usize; n];
254    for (new_idx, &old) in order.iter().enumerate() {
255        newpos[old] = new_idx;
256    }
257    let layout: Vec<LoopCell> = order
258        .iter()
259        .map(|&old| remap_cell(&cells[old], &newpos))
260        .collect();
261    let is_agu: Vec<bool> = order.iter().map(|&old| is_agu_orig[old]).collect();
262    let agu_len = is_agu_orig.iter().filter(|&&a| a).count();
263
264    DaeSchedule {
265        n_in,
266        layout,
267        result: remap(result, &newpos),
268        agu_len,
269        is_agu,
270    }
271}
272
273/// Schedule a body FOR a described target: decouple its address lane iff the target carries an AGU
274/// (`target.agu`), else leave it coupled (identity). This is the descriptor knob — a fabric without an AGU
275/// cannot exploit decoupling, so the transform only fires when the target can realize it. Either way the
276/// schedule is semantics-preserving (a proven reordering, or the identity).
277pub fn schedule_for_target(
278    cells: &[LoopCell],
279    result: Src,
280    n_in: usize,
281    target: &FabricTarget,
282) -> DaeSchedule {
283    if target.agu {
284        decouple_access(cells, result, n_in)
285    } else {
286        DaeSchedule {
287            n_in,
288            layout: cells.to_vec(),
289            result,
290            agu_len: 0,
291            is_agu: vec![false; cells.len()],
292        }
293    }
294}
295
296/// Evaluate a decoupled schedule against `inputs` + a shared `heap`, exactly as the coupled body would. Reuses
297/// the decision-fabric heap reduction over the re-laid-out cells — so agreement with the coupled eval is the
298/// semantics-preservation certificate.
299pub fn eval_dae(sched: &DaeSchedule, inputs: &[i64], heap: &mut Vec<i64>) -> i64 {
300    let df = DecisionFabric {
301        n_in: sched.n_in,
302        cells: sched.layout.clone(),
303        result: sched.result,
304        escaped_first_return: false,
305    };
306    eval_decision_fabric_heap(&df, inputs, heap)
307}
308
309/// Render a `Src` as a Verilog operand (`in{k}` / `v{k}` / a signed constant).
310fn src_v(s: &Src) -> String {
311    match s {
312        Src::In(k) => format!("in{k}"),
313        Src::Val(k) => format!("v{k}"),
314        Src::Const(c) if *c < 0 => format!("-64'sd{}", (*c as i128).unsigned_abs()),
315        Src::Const(c) => format!("64'sd{c}"),
316    }
317}
318
319/// Emit a decoupled schedule as COMBINATIONAL Verilog: the AGU lane (address arithmetic) and the exec lane
320/// (compute + loads) are emitted as two labelled regions, the loads reading a `depth`-word heap. Bit-identical
321/// to [`eval_dae`] (out-of-range loads read 0, matching the model) — proven under iverilog by `dae_rtl_lock`.
322/// LOAD-ONLY: `HeapWrite`/`HeapAlloc`/`Func` are the sequenced-state follow-on and panic here (the honest
323/// boundary), so the corpus is streaming reads with computed addresses — the canonical DAE case.
324pub fn emit_dae_verilog(name: &str, sched: &DaeSchedule, depth: usize) -> String {
325    let idxbits = (usize::BITS - (depth - 1).leading_zeros()) as usize; // clog2(depth)
326    let inputs = (0..sched.n_in)
327        .map(|k| format!("input [63:0] in{k}"))
328        .collect::<Vec<_>>()
329        .join(", ");
330    let mut body = String::new();
331    for (i, cell) in sched.layout.iter().enumerate() {
332        if i == 0 && sched.agu_len > 0 {
333            body.push_str("  // --- AGU lane (address generation, runs in parallel) ---\n");
334        }
335        if i == sched.agu_len {
336            body.push_str("  // --- exec lane (compute + loads) ---\n");
337        }
338        match cell {
339            LoopCell::Arith { op, a, b } => {
340                body.push_str(&format!(
341                    "  wire [63:0] v{i} = {};\n",
342                    op.verilog(&src_v(a), &src_v(b))
343                ));
344            }
345            LoopCell::Select { cmp, ca, cb, t, e } => {
346                body.push_str(&format!(
347                    "  wire [63:0] v{i} = ($signed({}) {} $signed({})) ? {} : {};\n",
348                    src_v(ca),
349                    cmp.verilog(),
350                    src_v(cb),
351                    src_v(t),
352                    src_v(e),
353                ));
354            }
355            LoopCell::HeapRead { addr } => {
356                body.push_str(&format!(
357                    "  wire signed [63:0] addr{i} = {};\n",
358                    src_v(addr)
359                ));
360                body.push_str(&format!(
361                    "  wire [63:0] v{i} = (addr{i} >= 0 && addr{i} < {depth}) ? heap[addr{i}[{hi}:0]] : 64'd0;\n",
362                    hi = idxbits - 1,
363                ));
364            }
365            other => panic!(
366                "emit_dae_verilog: {other:?} is the sequenced-state follow-on (load-only today)"
367            ),
368        }
369    }
370    format!(
371        "// dae_{name} — a decoupled ACCESS/EXECUTE datapath: the AGU lane computes addresses in parallel with\n\
372         // the exec lane; loads read a {depth}-word heap. Combinational, ≡ eval_dae under iverilog.\n\
373         module dae_{name}({inputs}, output [63:0] result);\n\
374         \x20 reg [63:0] heap [0:{maxd}];\n\
375         \x20 initial $readmemh(\"dae_{name}_heap.hex\", heap);\n\
376         {body}  assign result = {res};\n\
377         endmodule\n",
378        maxd = depth - 1,
379        res = src_v(&sched.result),
380    )
381}
382
383/// Emit a decoupled schedule that MUTATES the heap (`HeapWrite`/`HeapAlloc`, not just loads) as a SEQUENCED
384/// synthesizable datapath: the decoupled layout (AGU cells hoisted first) is run on the proven state-plane
385/// micro-sequencer (`emit_state_plane_verilog`), which commits heap writes in program order over one shared
386/// heap + a bump allocator. Module `state_{name}` (clk/rst/inN/result/done). Bit-identical to [`eval_dae`]
387/// (≡ the coupled body ≡ the VM); proven under iverilog by `dae_rtl_lock`. Distinct from the combinational
388/// load-only [`emit_dae_verilog`], which realizes the parallel AGU lane for streaming reads.
389pub fn emit_dae_stateful_verilog(name: &str, sched: &DaeSchedule, heap_words: usize) -> String {
390    let df = DecisionFabric {
391        n_in: sched.n_in,
392        cells: sched.layout.clone(),
393        result: sched.result,
394        escaped_first_return: false,
395    };
396    emit_state_plane_verilog(name, &df, heap_words)
397}
398
399/// A self-checking combinational testbench for `dae_{name}`: drive `n` input vectors (each `n_in` words) from
400/// `dae_{name}_in.hex`, compare the settled `result` against the `eval_dae` oracle in `dae_{name}_out.hex`.
401pub fn emit_dae_testbench(name: &str, n_in: usize, n: usize) -> String {
402    let decls = (0..n_in)
403        .map(|k| format!("  reg [63:0] in{k};\n"))
404        .collect::<String>();
405    let ports = (0..n_in)
406        .map(|k| format!(".in{k}(in{k}), "))
407        .collect::<String>();
408    let drive = (0..n_in)
409        .map(|k| format!("      in{k} = oin[i * {n_in} + {k}];\n"))
410        .collect::<String>();
411    format!(
412        r#"`timescale 1ns/1ps
413module tb_dae_{name};
414{decls}  reg [63:0] oin  [0:{in_last}];
415  reg [63:0] oout [0:{last}];
416  wire [63:0] result;
417  integer i, errors = 0;
418  dae_{name} dut({ports}.result(result));
419  initial begin
420    $readmemh("dae_{name}_in.hex", oin);
421    $readmemh("dae_{name}_out.hex", oout);
422    for (i = 0; i < {n}; i = i + 1) begin
423{drive}      #1;
424      if (result !== oout[i]) begin errors = errors + 1; $display("FAIL vec %0d: got %0d", i, $signed(result)); end
425    end
426    if (errors == 0) $display("PASS: {n} decoupled-datapath evals match eval_dae (≡ the coupled body ≡ VM)");
427    else $display("FAIL: %0d decoupled-datapath mismatches", errors);
428    $finish;
429  end
430endmodule
431"#,
432        in_last = n_in * n - 1,
433        last = n - 1,
434    )
435}
logicaffeine_compile/codegen_sva/dae.rs

logicaffeine_compile/codegen_sva/
dae.rs
