logicaffeine_compile/codegen_sva/
backend.rs

1//! The target-backend seam.
2//!
3//! Everything up to a placed [`Grid`] is target-agnostic (English → `LoopCell` IR → certified placement). Only
4//! the final `Grid → bytes` step is backend-specific. This module names that seam as a [`TargetBackend`] trait
5//! so a new hardware backend (e.g. the SambaNova RDU) is a tested extension point instead of a loose
6//! convention. Emission is target-specific; the proof-carrying [`certify`](TargetBackend::certify) is
7//! backend-agnostic (default impl), so even a backend that can't emit its vendor config yet still proves a
8//! placement ≡ its source.
9
10use super::fabric_grid::{emit_config_grid_verilog, emit_grid_verilog, Grid};
11use super::fabric_rtl::FabricOp;
12use super::fabric_target::FabricTarget;
13use super::pnr_certificate::{certify_external_placement, PlacementCertificate};
14use crate::spatial::lower::rdu::{neutral_envelope, GridBody, NeutralBody, GATED_REASON};
15use crate::spatial::rdu_chip::{RduChip, RduChipFacts};
16
17/// What a backend produces from a placed grid.
18#[derive(Clone, Debug)]
19pub enum BackendArtifact {
20    /// Synthesizable RTL — our own Sky130/FPGA silicon path.
21    Verilog(String),
22    /// Vendor config emission is gated on the SDK. Carries the ready-to-bridge NEUTRAL placement (a
23    /// deterministic dump of the placed grid), so the ONLY remaining work is the vendor's config format. This
24    /// is never a faked config — it is an honest "the placement is ready; the config format is pending the
25    /// SDK." The proof that this placement ≡ the source is available separately via
26    /// [`TargetBackend::certify`], which needs no SDK at all.
27    SdkGated {
28        neutral_placement: String,
29        reason: &'static str,
30    },
31}
32
33impl BackendArtifact {
34    pub fn as_verilog(&self) -> Option<&str> {
35        match self {
36            BackendArtifact::Verilog(s) => Some(s),
37            _ => None,
38        }
39    }
40    pub fn is_sdk_gated(&self) -> bool {
41        matches!(self, BackendArtifact::SdkGated { .. })
42    }
43}
44
45/// A named codegen backend for a described [`FabricTarget`].
46pub trait TargetBackend {
47    fn name(&self) -> &str;
48    fn target(&self) -> &FabricTarget;
49    /// Emit a single placed grid to this backend's artifact.
50    fn emit_grid(&self, name: &str, g: &Grid) -> BackendArtifact;
51    /// Emit an N-way reconfigurable array of placed grids to this backend's artifact.
52    fn emit_config_grid(&self, name: &str, grids: &[&Grid], cfg_width: u32) -> BackendArtifact;
53    /// Prove a placement computes `source` for every bounded input and return a re-checkable certificate (or
54    /// `None`, fail-closed). Backend-agnostic — proof-carrying place-and-route is not tied to the emission
55    /// format, so every backend inherits it. This is what lets an RDU backend add value before its SDK exists.
56    fn certify(
57        &self,
58        g: &Grid,
59        source: &[FabricOp],
60        result: usize,
61        width: u32,
62    ) -> Option<PlacementCertificate> {
63        certify_external_placement(g, source, result, width)
64    }
65}
66
67/// A deterministic, parseable neutral dump of a placed grid — the artifact the vendor-config bridge consumes.
68/// Rows/cols are walked in order and every field is a `Copy` enum's `Debug`, so the output is stable (no
69/// hashmap iteration). It is NOT any vendor's format; it is the ready-to-bridge placement.
70pub fn serialize_grid(g: &Grid) -> String {
71    let mut s = format!(
72        "grid rows={} cols={} n_in={} out={:?} extra_outs={:?}\n",
73        g.rows, g.cols, g.n_in, g.out, g.extra_outs
74    );
75    for (r, row) in g.tiles.iter().enumerate() {
76        for (c, t) in row.iter().enumerate() {
77            s.push_str(&format!(
78                "  [{r},{c}] alu={:?} vs={:?} he={:?}\n",
79                t.alu, t.vs, t.he
80            ));
81        }
82    }
83    s
84}
85
86/// The default backend: our Sky130/FPGA path. A faithful wrapper of the existing free emitters — byte-identical
87/// to calling `emit_grid_verilog` / `emit_config_grid_verilog` directly.
88pub struct SkyVerilogBackend {
89    pub target: FabricTarget,
90}
91
92impl SkyVerilogBackend {
93    pub fn new() -> Self {
94        SkyVerilogBackend {
95            target: FabricTarget::full(64, 64, 64),
96        }
97    }
98}
99
100impl Default for SkyVerilogBackend {
101    fn default() -> Self {
102        Self::new()
103    }
104}
105
106impl TargetBackend for SkyVerilogBackend {
107    fn name(&self) -> &str {
108        "sky130-verilog"
109    }
110    fn target(&self) -> &FabricTarget {
111        &self.target
112    }
113    fn emit_grid(&self, name: &str, g: &Grid) -> BackendArtifact {
114        BackendArtifact::Verilog(emit_grid_verilog(name, g))
115    }
116    fn emit_config_grid(&self, name: &str, grids: &[&Grid], cfg_width: u32) -> BackendArtifact {
117        BackendArtifact::Verilog(emit_config_grid_verilog(name, grids, cfg_width))
118    }
119}
120
121/// The SambaNova **RDU** slot — the placed-grid lane, for either RDU generation ([`RduChip`]). Its target is
122/// the chip's [`FabricTarget`] derived from [`RduChipFacts`]. It cannot emit RDA/SambaFlow config today —
123/// that needs the vendor SDK — so its emission is honestly [`BackendArtifact::SdkGated`]: it hands back the
124/// `logos.spatial.neutral` v2 envelope under `"lane": "grid"`, the same envelope the spatial lane emits,
125/// with the ready-to-bridge deterministic grid dump as its body. Its proof-carrying
126/// [`certify`](TargetBackend::certify) works NOW (no SDK), so an RDU-bound placement already ships with a
127/// machine-checkable proof it ≡ the source. When the SDK lands, only the `envelope → RDA config` translation
128/// is added.
129pub struct RduBackend {
130    pub facts: RduChipFacts,
131    pub target: FabricTarget,
132}
133
134impl RduBackend {
135    /// The SN40L lane.
136    pub fn new() -> Self {
137        Self::for_chip(RduChip::Sn40l)
138    }
139    /// The lane for one RDU generation, its target derived from that chip's facts.
140    pub fn for_chip(chip: RduChip) -> Self {
141        Self::with_facts(chip.facts())
142    }
143    /// The lane for facts with numbers dropped in (an SDK reading, a probe).
144    pub fn with_facts(facts: RduChipFacts) -> Self {
145        RduBackend {
146            target: facts.fabric_target(),
147            facts,
148        }
149    }
150    pub const GATED_REASON: &'static str = GATED_REASON;
151
152    fn envelope(&self, body: GridBody) -> String {
153        neutral_envelope(
154            &self.facts.spatial_target(),
155            &self.facts,
156            NeutralBody::Grid(body),
157            None,
158        )
159    }
160}
161
162impl Default for RduBackend {
163    fn default() -> Self {
164        Self::new()
165    }
166}
167
168impl TargetBackend for RduBackend {
169    fn name(&self) -> &str {
170        self.target.name
171    }
172    fn target(&self) -> &FabricTarget {
173        &self.target
174    }
175    fn emit_grid(&self, name: &str, g: &Grid) -> BackendArtifact {
176        let dump = serialize_grid(g);
177        let body = GridBody {
178            name: name.to_string(),
179            pretty: dump.clone(),
180            grids: vec![dump],
181            cfg_width: None,
182        };
183        BackendArtifact::SdkGated {
184            neutral_placement: self.envelope(body),
185            reason: GATED_REASON,
186        }
187    }
188    fn emit_config_grid(&self, name: &str, grids: &[&Grid], cfg_width: u32) -> BackendArtifact {
189        let dumps: Vec<String> = grids.iter().map(|g| serialize_grid(g)).collect();
190        let body = GridBody {
191            name: name.to_string(),
192            pretty: dumps.join("---\n"),
193            grids: dumps,
194            cfg_width: Some(cfg_width),
195        };
196        BackendArtifact::SdkGated {
197            neutral_placement: self.envelope(body),
198            reason: GATED_REASON,
199        }
200    }
201}
logicaffeine_compile/codegen_sva/backend.rs

logicaffeine_compile/codegen_sva/
backend.rs
