logicaffeine_compile/codegen_sva/
power.rs

1//! Power-Aware Formal Verification
2//!
3//! Power domains introduce isolation, retention, and level shifting requirements.
4//! Missing isolation cells cause functional bugs in power-managed designs.
5
6use super::{SvaProperty, SvaAssertionKind};
7
8/// Power domain state.
9#[derive(Debug, Clone, PartialEq, Eq)]
10pub enum PowerState {
11    On,
12    Off,
13    Retention,
14}
15
16/// A power domain definition.
17#[derive(Debug, Clone)]
18pub struct PowerDomain {
19    pub name: String,
20    pub state: PowerState,
21    pub signals: Vec<String>,
22    pub always_on: bool,
23}
24
25/// A signal crossing between power domains.
26#[derive(Debug, Clone)]
27pub struct PowerCrossing {
28    pub signal: String,
29    pub source_domain: String,
30    pub dest_domain: String,
31    pub has_isolation: bool,
32    pub has_level_shifter: bool,
33}
34
35/// Power violation type.
36#[derive(Debug, Clone, PartialEq, Eq)]
37pub enum PowerViolationType {
38    MissingIsolation,
39    MissingRetention,
40    MissingLevelShifter,
41    IncorrectSequence,
42}
43
44/// A power violation.
45#[derive(Debug, Clone)]
46pub struct PowerViolation {
47    pub signal: String,
48    pub violation_type: PowerViolationType,
49    pub message: String,
50}
51
52/// Power analysis report.
53#[derive(Debug, Clone)]
54pub struct PowerReport {
55    pub domains: Vec<PowerDomain>,
56    pub crossings: Vec<PowerCrossing>,
57    pub violations: Vec<PowerViolation>,
58}
59
60/// Analyze power domains and crossings for violations.
61pub fn analyze_power(
62    domains: &[PowerDomain],
63    crossings: &[PowerCrossing],
64) -> PowerReport {
65    let mut violations = Vec::new();
66
67    for crossing in crossings {
68        // Find source domain
69        let source = domains.iter().find(|d| d.name == crossing.source_domain);
70
71        // Check isolation requirement
72        if let Some(src) = source {
73            if !src.always_on && !crossing.has_isolation {
74                violations.push(PowerViolation {
75                    signal: crossing.signal.clone(),
76                    violation_type: PowerViolationType::MissingIsolation,
77                    message: format!(
78                        "Signal '{}' crosses from '{}' to '{}' without isolation cell",
79                        crossing.signal, crossing.source_domain, crossing.dest_domain
80                    ),
81                });
82            }
83        }
84
85        // Check level shifter
86        if !crossing.has_level_shifter {
87            // Only flag if domains have different implied voltage levels
88            // Simplified: flag if explicitly missing
89            violations.push(PowerViolation {
90                signal: crossing.signal.clone(),
91                violation_type: PowerViolationType::MissingLevelShifter,
92                message: format!(
93                    "Signal '{}' crosses domains without level shifter",
94                    crossing.signal
95                ),
96            });
97        }
98    }
99
100    // Check retention
101    for domain in domains {
102        if domain.state == PowerState::Retention {
103            let has_retention_signals = !domain.signals.is_empty();
104            if !has_retention_signals {
105                violations.push(PowerViolation {
106                    signal: domain.name.clone(),
107                    violation_type: PowerViolationType::MissingRetention,
108                    message: format!("Domain '{}' in retention but has no signals", domain.name),
109                });
110            }
111        }
112    }
113
114    PowerReport {
115        domains: domains.to_vec(),
116        crossings: crossings.to_vec(),
117        violations,
118    }
119}
120
121/// Generate SVA properties for power isolation verification.
122pub fn verify_isolation(domain: &PowerDomain) -> Vec<SvaProperty> {
123    let mut props = Vec::new();
124
125    if !domain.always_on {
126        for sig in &domain.signals {
127            props.push(SvaProperty {
128                name: format!("power_isolation_{}", sig),
129                clock: "clk".into(),
130                body: format!(
131                    "({}_power_off) |-> ({}_iso == 1'b0)",
132                    domain.name, sig
133                ),
134                kind: SvaAssertionKind::Assert,
135            });
136        }
137    }
138
139    props
140}
141
142/// Generate SVA properties for power sequencing.
143pub fn power_sequence_properties(domains: &[PowerDomain]) -> Vec<SvaProperty> {
144    let mut props = Vec::new();
145
146    for domain in domains {
147        if !domain.always_on {
148            props.push(SvaProperty {
149                name: format!("power_seq_{}", domain.name),
150                clock: "clk".into(),
151                body: format!(
152                    "({name}_power_on) |-> ({name}_iso_release)",
153                    name = domain.name
154                ),
155                kind: SvaAssertionKind::Assert,
156            });
157        }
158    }
159
160    props
161}
logicaffeine_compile/codegen_sva/power.rs

logicaffeine_compile/codegen_sva/
power.rs
