logicaffeine_compile/codegen_sva/
mod.rs

1//! SVA/PSL Code Generation for Hardware Verification
2//!
3//! Generates SystemVerilog Assertions (SVA), Property Specification Language (PSL),
4//! and Rust runtime monitors from temporal property specifications.
5
6pub mod sva_model;
7pub mod sva_to_verify;
8pub mod fol_to_verify;
9pub mod sva_to_proof;
10pub mod bitblast;
11pub mod rtl;
12pub mod hw_pipeline;
13pub mod rtl_extract;
14pub mod fol_to_sva;
15pub mod signal_design;
16pub mod controller_gen;
17pub mod traffic_flow;
18pub mod coverage;
19pub mod sufficiency;
20pub mod rtl_kg;
21pub mod synthesis_refine;
22pub mod protocols;
23pub mod verify_to_kernel;
24pub mod ci;
25pub mod power;
26pub mod cdc;
27pub mod verified_compiler;
28pub mod z3_synth;
29pub mod synthesize;
30pub mod sva_vacuity;
31
32#[cfg(feature = "verification")]
33pub mod waveform;
34#[cfg(feature = "verification")]
35pub mod testgen;
36#[cfg(feature = "verification")]
37pub mod decompose;
38#[cfg(feature = "verification")]
39pub mod invariants;
40#[cfg(feature = "verification")]
41pub mod spec_health;
42
43/// Assertion type — determines the SVA wrapper.
44#[derive(Debug, Clone, PartialEq, Eq)]
45pub enum SvaAssertionKind {
46    /// `assert property` — hard safety requirement.
47    Assert,
48    /// `cover property` — liveness / expected behavior.
49    Cover,
50    /// `assume property` — environment constraint.
51    Assume,
52}
53
54/// A single SVA property ready for emission.
55#[derive(Debug, Clone)]
56pub struct SvaProperty {
57    pub name: String,
58    pub clock: String,
59    pub body: String,
60    pub kind: SvaAssertionKind,
61}
62
63/// Sanitize a human-readable property name into a valid SVA identifier.
64/// "Data Integrity" → "p_data_integrity"
65pub fn sanitize_property_name(name: &str) -> String {
66    let sanitized: String = name
67        .chars()
68        .map(|c| if c.is_alphanumeric() { c.to_ascii_lowercase() } else { '_' })
69        .collect();
70    format!("p_{}", sanitized.trim_matches('_'))
71}
72
73/// Emit a single SVA property with its assertion wrapper.
74pub fn emit_sva_property(prop: &SvaProperty) -> String {
75    let wrapper = match prop.kind {
76        SvaAssertionKind::Assert => "assert property",
77        SvaAssertionKind::Cover => "cover property",
78        SvaAssertionKind::Assume => "assume property",
79    };
80
81    let error_action = match prop.kind {
82        SvaAssertionKind::Assert => {
83            format!(" else $error(\"{} violation\")", prop.name)
84        }
85        _ => String::new(),
86    };
87
88    format!(
89        "property {};\n    @(posedge {}) {};\nendproperty\n{} ({}){};",
90        prop.name, prop.clock, prop.body, wrapper, prop.name, error_action
91    )
92}
93
94/// Emit multiple SVA properties as a complete module.
95pub fn emit_sva_module(props: &[SvaProperty]) -> String {
96    props
97        .iter()
98        .map(|p| emit_sva_property(p))
99        .collect::<Vec<_>>()
100        .join("\n\n")
101}
102
103/// Emit a single PSL property.
104pub fn emit_psl_property(prop: &SvaProperty) -> String {
105    let kind = match prop.kind {
106        SvaAssertionKind::Assert => "assert always",
107        SvaAssertionKind::Cover => "cover",
108        SvaAssertionKind::Assume => "assume always",
109    };
110    format!("-- {}\n{} ({});", prop.name, kind, prop.body)
111}
112
113/// Emit a Rust runtime monitor scaffold for a property.
114///
115/// Generates a struct with a `check()` method stub. The generated `check()`
116/// always returns `true` — callers must fill in the signal-dependent logic
117/// for their specific use case. This is a code generation template, not a
118/// complete monitor implementation.
119pub fn emit_rust_monitor(prop: &SvaProperty) -> String {
120    let struct_name = prop
121        .name
122        .replace("p_", "")
123        .split('_')
124        .map(|w| {
125            let mut c = w.chars();
126            match c.next() {
127                None => String::new(),
128                Some(f) => f.to_uppercase().collect::<String>() + c.as_str(),
129            }
130        })
131        .collect::<String>()
132        + "Monitor";
133
134    format!(
135        r#"pub struct {struct_name} {{
136    cycle: u64,
137}}
138
139impl {struct_name} {{
140    pub fn new() -> Self {{
141        Self {{ cycle: 0 }}
142    }}
143
144    /// Check the property for one clock cycle.
145    /// Returns true if the property holds.
146    pub fn check(&mut self) -> bool {{
147        self.cycle += 1;
148        // Property: {body}
149        // Scaffold: fill in signal-dependent check logic for your design
150        true
151    }}
152}}"#,
153        struct_name = struct_name,
154        body = prop.body,
155    )
156}
logicaffeine_compile/codegen_sva/mod.rs

logicaffeine_compile/codegen_sva/
mod.rs
