logicaffeine_web/ui/pages/
hardware_report.rs

1//! What Hardware mode makes of the editor's text: which kind of design it is, and everything the
2//! Studio shows for it. One pure reading, so the panels, Execute and Compile can never disagree
3//! about what the file is.
4
5use logicaffeine_compile::codegen_sva::hw_pipeline::KgSummary;
6
7/// The kinds of design Hardware mode reads, by what the text names.
8#[derive(Clone, Copy, Debug, PartialEq, Eq)]
9pub enum HardwareKind {
10    /// An English temporal spec ("Always, if request is high, …"), synthesized to an SVA.
11    EnglishSpec,
12    /// Movements and their conflicts, designed into a phase plan and a controller.
13    SignalPlan,
14    /// A Verilog module with an assertion, model-checked.
15    Verilog,
16    /// A `registers:` budget and live ranges, allocated and certified.
17    RegisterAlloc,
18    /// A `pigeons:` count, refuted and certified.
19    Pigeonhole,
20}
21
22impl HardwareKind {
23    /// The title of the panel that holds the result.
24    pub fn result_title(self) -> &'static str {
25        match self {
26            HardwareKind::EnglishSpec => "SVA",
27            HardwareKind::SignalPlan => "Signal Plan",
28            HardwareKind::Verilog => "Model Check",
29            HardwareKind::RegisterAlloc => "Allocation",
30            HardwareKind::Pigeonhole => "Proof",
31        }
32    }
33
34    /// Whether Compile makes something (a Rust runtime monitor), so the result panel offers a
35    /// Rust view.
36    pub fn compiles(self) -> bool {
37        match self {
38            HardwareKind::EnglishSpec => true,
39            HardwareKind::SignalPlan | HardwareKind::Verilog | HardwareKind::RegisterAlloc | HardwareKind::Pigeonhole => false,
40        }
41    }
42}
43
44/// Which kind of design `content` is; `None` for an empty editor. A spec is the kind whose field
45/// it names (`pigeons:`, `registers:`), whatever its values, so a mistake in one is reported as
46/// that spec's mistake.
47pub fn kind_of(content: &str) -> Option<HardwareKind> {
48    use super::hardware_spec::{field_value, PIGEONS, REGISTERS};
49    if content.trim().is_empty() {
50        return None;
51    }
52    let names = |field: &str| content.lines().any(|line| field_value(line, field).is_some());
53    Some(if names(PIGEONS) {
54        HardwareKind::Pigeonhole
55    } else if names(REGISTERS) {
56        HardwareKind::RegisterAlloc
57    } else if content.contains("module") && content.contains("endmodule") {
58        HardwareKind::Verilog
59    } else if content.to_lowercase().contains("conflict") {
60        HardwareKind::SignalPlan
61    } else {
62        HardwareKind::EnglishSpec
63    })
64}
65
66/// Whether the editor holds Verilog: a line that opens a `module`, or an `endmodule` — known from
67/// the first line of a module being written, before [`kind_of`] can call it finished Verilog.
68pub fn is_verilog(content: &str) -> bool {
69    content.contains("endmodule")
70        || content.lines().any(|line| line.trim_start().strip_prefix("module").is_some_and(|rest| rest.starts_with([' ', '(', '#'])))
71}
72
73/// One labelled block of the result panel.
74#[derive(Clone, Debug, PartialEq)]
75pub struct Section {
76    pub label: &'static str,
77    pub body: String,
78}
79
80/// Everything the Studio shows for a Hardware design.
81#[derive(Clone, Debug, Default, PartialEq)]
82pub struct HardwareReport {
83    pub sections: Vec<Section>,
84    /// The verdict line and whether it is a success, a failure, or neither.
85    pub verdict: Option<(String, Option<bool>)>,
86    /// A counterexample when the verdict fails, a witness run when it holds.
87    pub trace: Vec<(String, String)>,
88    pub signals: Vec<String>,
89    pub kg: KgSummary,
90    pub error: Option<String>,
91}
92
93/// Read `content` as its kind of design.
94pub fn analyze(content: &str) -> Option<(HardwareKind, HardwareReport)> {
95    let kind = kind_of(content)?;
96    let report = match kind {
97        HardwareKind::Pigeonhole => pigeonhole(content),
98        HardwareKind::RegisterAlloc => allocation(content),
99        HardwareKind::Verilog => verilog(content),
100        HardwareKind::SignalPlan => signal_plan(content),
101        HardwareKind::EnglishSpec => english_spec(content),
102    };
103    Some((kind, report))
104}
105
106fn failed(error: String) -> HardwareReport {
107    HardwareReport { error: Some(error), ..HardwareReport::default() }
108}
109
110/// The first problem the spec's own service finds, as the report's error.
111fn spec_problem(content: &str) -> Option<String> {
112    super::hardware_spec::problems(content).into_iter().next().map(|p| p.message)
113}
114
115fn pigeonhole(content: &str) -> HardwareReport {
116    use super::pigeonhole_viz::{headline, parse_pigeonhole_spec, report};
117    match parse_pigeonhole_spec(content) {
118        Some(spec) => HardwareReport {
119            sections: vec![Section { label: "Certified pigeonhole refutation", body: report(&spec) }],
120            verdict: Some((headline(&spec), Some(true))),
121            ..HardwareReport::default()
122        },
123        None => failed(spec_problem(content).unwrap_or_else(|| "A pigeonhole spec is one line, `pigeons: N`.".to_string())),
124    }
125}
126
127fn allocation(content: &str) -> HardwareReport {
128    use super::register_alloc_viz::{allocation_report, linear_scan_assignment, parse_register_spec, render};
129    match parse_register_spec(content) {
130        Some(spec) if spec_problem(content).is_none() => {
131            let fits = linear_scan_assignment(&spec).iter().all(Option::is_some);
132            let (_, verdict) = render(&spec);
133            HardwareReport {
134                sections: vec![Section { label: "Certified register allocation", body: allocation_report(&spec) }],
135                verdict: Some((verdict, Some(fits))),
136                ..HardwareReport::default()
137            }
138        }
139        _ => failed(spec_problem(content).unwrap_or_else(|| {
140            "A register allocation needs at least one live range, `name: first-last`, under its `registers:` budget.".to_string()
141        })),
142    }
143}
144
145fn verilog(content: &str) -> HardwareReport {
146    use logicaffeine_compile::codegen_sva::rtl::parse_transition_system;
147    use logicaffeine_proof::bmc::{BmcOutcome, InductionOutcome};
148    let ts = match parse_transition_system(content) {
149        Ok(ts) => ts,
150        Err(e) => return failed(format!("RTL parse error: {}", e.message)),
151    };
152    let names: Vec<String> = ts
153        .registers
154        .iter()
155        .map(|r| if r.width > 1 { format!("{}[{}]", r.name, r.width) } else { r.name.clone() })
156        .collect();
157    let summary = format!(
158        "{} {}: {}.\nChecked in every reachable state by bounded model checking and k-induction, with no Z3.",
159        names.len(),
160        if names.len() == 1 { "register" } else { "registers" },
161        names.join(", ")
162    );
163    let to_trace = |trace: Vec<(String, bool)>| -> Vec<(String, String)> {
164        trace.into_iter().map(|(n, v)| (n, if v { "1" } else { "0" }.to_string())).collect()
165    };
166    let breaks = |k: u32| format!("\u{2717} Can break at step {k}: the waveform shows the run that breaks it");
167    let unexpressible = || ("This property isn't expressible yet. Try a simpler one.".to_string(), None);
168    let (verdict, trace) = match ts.prove_invariant(4) {
169        InductionOutcome::Proven => (
170            ("\u{2713} Always holds: proven for every reachable state (k-induction, no Z3)".to_string(), Some(true)),
171            ts.witness_trace(18).map(to_trace).unwrap_or_default(),
172        ),
173        InductionOutcome::CounterexampleAt { k, trace } => ((breaks(k), Some(false)), to_trace(trace)),
174        InductionOutcome::NotInductive => match ts.bmc(28) {
175            BmcOutcome::CounterexampleAt { k, trace } => ((breaks(k), Some(false)), to_trace(trace)),
176            BmcOutcome::NoneWithin(n) => (
177                (format!("No failure found within {n} steps, but this depth can't prove it always holds"), None),
178                Vec::new(),
179            ),
180            BmcOutcome::Unsupported => (unexpressible(), Vec::new()),
181        },
182        InductionOutcome::Unsupported => (unexpressible(), Vec::new()),
183    };
184    HardwareReport {
185        sections: vec![Section { label: "Transition system", body: summary }],
186        verdict: Some(verdict),
187        trace,
188        ..HardwareReport::default()
189    }
190}
191
192fn signal_plan(content: &str) -> HardwareReport {
193    use logicaffeine_compile::codegen_sva::controller_gen::generate_controller;
194    use logicaffeine_compile::codegen_sva::rtl::parse_transition_system;
195    use logicaffeine_compile::codegen_sva::signal_design::design_from_spec;
196    use logicaffeine_proof::bmc::InductionOutcome;
197    let (intersection, plan) = match design_from_spec(content) {
198        Ok(designed) => designed,
199        Err(e) => return failed(e),
200    };
201    let phases: Vec<String> = plan
202        .groups()
203        .iter()
204        .enumerate()
205        .map(|(p, group)| format!("Phase {}: {}", p + 1, intersection.names(group).join(", ")))
206        .collect();
207    let verilog = generate_controller(&intersection, &plan);
208    let controller_proven = matches!(parse_transition_system(&verilog).map(|ts| ts.prove_invariant(4)), Ok(InductionOutcome::Proven));
209    let minimal = if !plan.minimal_certified {
210        String::new()
211    } else if plan.num_phases <= 1 {
212        " \u{00b7} a single phase suffices".to_string()
213    } else {
214        format!(" \u{00b7} provably minimal ({}-phase impossible)", plan.num_phases - 1)
215    };
216    let controller_note = if controller_proven { " \u{00b7} generated controller PROVEN conflict-free (k-induction)" } else { "" };
217    HardwareReport {
218        sections: vec![
219            Section { label: "Phase plan", body: phases.join("\n") },
220            Section { label: "Generated controller", body: verilog.trim_end().to_string() },
221        ],
222        verdict: Some((
223            format!(
224                "\u{2713} Conflict-free {}-phase plan synthesized{minimal}{controller_note} (certified by our SAT solver, no Z3)",
225                plan.num_phases
226            ),
227            Some(true),
228        )),
229        signals: intersection.movements.clone(),
230        ..HardwareReport::default()
231    }
232}
233
234/// The SVA property a synthesis names, for the PSL and Rust emitters.
235fn property(synth: &logicaffeine_compile::codegen_sva::fol_to_sva::SynthesizedSva) -> logicaffeine_compile::codegen_sva::SvaProperty {
236    use logicaffeine_compile::codegen_sva::{sanitize_property_name, SvaAssertionKind, SvaProperty};
237    let kind = match synth.kind.as_str() {
238        "cover" => SvaAssertionKind::Cover,
239        "assume" => SvaAssertionKind::Assume,
240        _ => SvaAssertionKind::Assert,
241    };
242    let name = if synth.signals.is_empty() { "p_property".to_string() } else { sanitize_property_name(&synth.signals.join("_")) };
243    SvaProperty { name, clock: "clk".to_string(), body: synth.body.clone(), kind }
244}
245
246fn english_spec(content: &str) -> HardwareReport {
247    use logicaffeine_compile::codegen_sva::fol_to_sva::synthesize_sva_from_spec;
248    use logicaffeine_compile::codegen_sva::hw_pipeline::{check_spec_vacuity, kg_summary, prove_spec_sva_equivalence, VacuityReport};
249    let synth = match synthesize_sva_from_spec(content, "clk") {
250        Ok(synth) => synth,
251        Err(e) => return failed(e),
252    };
253    let psl = logicaffeine_compile::codegen_sva::emit_psl_property(&property(&synth));
254    let vacuity = match check_spec_vacuity(content, 8) {
255        Ok(VacuityReport::Vacuous) => " \u{00b7} \u{26A0} never triggers (vacuous)",
256        Ok(VacuityReport::NonVacuous) => " \u{00b7} the trigger can actually fire",
257        _ => "",
258    };
259    let (verdict, trace) = match prove_spec_sva_equivalence(content, &synth.body, 8) {
260        Ok(r) if r.equivalent => ((format!("\u{2713} Matches the spec: certified, kernel-checked, no Z3{vacuity}"), Some(true)), Vec::new()),
261        Ok(r) => {
262            let trace = r.counterexample.unwrap_or_default();
263            let shown = trace.iter().map(|(k, v)| format!("{k}={v}")).collect::<Vec<_>>().join(", ");
264            ((format!("\u{2717} Not equivalent to the spec. Counterexample: {shown}{vacuity}"), Some(false)), trace)
265        }
266        Err(e) => ((format!("Proof unavailable: {e}{vacuity}"), None), Vec::new()),
267    };
268    HardwareReport {
269        sections: vec![
270            Section { label: "SystemVerilog Assertion", body: synth.sva_text.clone() },
271            Section { label: "PSL", body: psl },
272        ],
273        verdict: Some(verdict),
274        trace,
275        signals: synth.signals.clone(),
276        kg: kg_summary(content).unwrap_or_default(),
277        error: None,
278    }
279}
280
281/// What Compile makes of a design.
282#[derive(Clone, Debug, PartialEq)]
283pub enum Compiled {
284    /// A Rust runtime monitor.
285    Rust(String),
286    /// Nothing to compile, and why: the note the Studio shows instead.
287    Nothing(&'static str),
288    /// The design could not be read.
289    Failed(String),
290}
291
292/// Why Compile makes nothing for a design of `kind` — `None` for an English spec, which compiles to
293/// a Rust runtime monitor. The toolbar shows the same words on the disabled button.
294pub fn nothing_to_compile(kind: HardwareKind) -> Option<&'static str> {
295    match kind {
296        HardwareKind::EnglishSpec => None,
297        HardwareKind::SignalPlan => Some(
298            "A signal plan compiles to hardware, not Rust: its generated controller is the Verilog in the Signal Plan panel, proven conflict-free.",
299        ),
300        HardwareKind::Verilog => Some(
301            "Verilog is already hardware, so there is no Rust monitor to generate. Execute model-checks its assertion.",
302        ),
303        HardwareKind::RegisterAlloc => Some("A register allocation has nothing to compile. Execute certifies it."),
304        HardwareKind::Pigeonhole => Some("A pigeonhole instance has nothing to compile. Execute certifies its refutation."),
305    }
306}
307
308/// Compile `content`: an English spec becomes a Rust runtime monitor; every other design says why
309/// there is nothing to compile, instead of blaming the design.
310pub fn compiled(content: &str) -> Compiled {
311    let Some(kind) = kind_of(content) else { return Compiled::Nothing("Write a design to compile.") };
312    if let Some(note) = nothing_to_compile(kind) {
313        return Compiled::Nothing(note);
314    }
315    match logicaffeine_compile::codegen_sva::fol_to_sva::synthesize_sva_from_spec(content, "clk") {
316        Ok(synth) => Compiled::Rust(logicaffeine_compile::codegen_sva::emit_rust_monitor(&property(&synth))),
317        Err(e) => Compiled::Failed(e),
318    }
319}
320
321#[cfg(test)]
322#[path = "../../../../../crates/logicaffeine_tests/unit/logicaffeine_web/ui/pages/hardware_report/tests.rs"]
323mod tests;
logicaffeine_web/ui/pages/hardware_report.rs

logicaffeine_web/ui/pages/
hardware_report.rs
