logicaffeine_compile/codegen_sva/
cdc.rs

1//! Clock Domain Crossing (CDC) Formal Verification
2//!
3//! CDC bugs are among the hardest to find in simulation. Metastability,
4//! data coherence, and synchronizer correctness require formal analysis.
5
6use super::{SvaProperty, SvaAssertionKind};
7use super::rtl_extract::RtlModule;
8
9/// A clock domain for CDC analysis.
10#[derive(Debug, Clone)]
11pub struct CdcClockDomain {
12    pub name: String,
13    pub clock_signal: String,
14}
15
16/// CDC synchronization pattern.
17#[derive(Debug, Clone, PartialEq)]
18pub enum CdcPattern {
19    TwoFlopSync { source_domain: String, dest_domain: String },
20    ThreeFlopSync { source_domain: String, dest_domain: String },
21    GrayCode { width: u32 },
22    HandshakeCdc { req: String, ack: String },
23    PulseSynchronizer,
24    AsyncFifo,
25}
26
27/// A signal crossing between clock domains.
28#[derive(Debug, Clone)]
29pub struct CdcCrossing {
30    pub signal: String,
31    pub source_domain: String,
32    pub dest_domain: String,
33    pub pattern: Option<CdcPattern>,
34    pub safe: bool,
35}
36
37/// CDC violation type.
38#[derive(Debug, Clone, PartialEq, Eq)]
39pub enum CdcViolationType {
40    MissingSynchronizer,
41    Reconvergence,
42    GlitchRisk,
43    BusWithoutEncoding,
44}
45
46/// A CDC violation.
47#[derive(Debug, Clone)]
48pub struct CdcViolation {
49    pub signal: String,
50    pub source_domain: String,
51    pub dest_domain: String,
52    pub violation_type: CdcViolationType,
53    pub message: String,
54}
55
56/// CDC analysis report.
57#[derive(Debug, Clone)]
58pub struct CdcReport {
59    pub crossings: Vec<CdcCrossing>,
60    pub violations: Vec<CdcViolation>,
61    pub patterns: Vec<CdcPattern>,
62}
63
64/// Analyze an RTL module for clock domain crossing issues.
65pub fn analyze_cdc(
66    rtl: &RtlModule,
67    domains: &[CdcClockDomain],
68) -> CdcReport {
69    let mut crossings = Vec::new();
70    let mut violations = Vec::new();
71    let mut patterns = Vec::new();
72
73    if domains.len() < 2 {
74        return CdcReport { crossings, violations, patterns };
75    }
76
77    // For each signal, determine which domain it belongs to
78    for signal in &rtl.signals {
79        // Check if this signal is used across domains
80        for i in 0..domains.len() {
81            for j in (i + 1)..domains.len() {
82                let src = &domains[i];
83                let dst = &domains[j];
84
85                // Heuristic: signal name contains domain reference
86                let in_src = signal.name.contains(&src.name) || is_in_domain(&signal.name, src);
87                let in_dst = signal.name.contains(&dst.name) || is_in_domain(&signal.name, dst);
88
89                if in_src || in_dst {
90                    // Check for synchronizer pattern
91                    let pattern = detect_pattern(&signal.name, rtl, src, dst);
92                    let safe = pattern.is_some();
93
94                    if let Some(ref pat) = pattern {
95                        patterns.push(pat.clone());
96                    }
97
98                    crossings.push(CdcCrossing {
99                        signal: signal.name.clone(),
100                        source_domain: src.name.clone(),
101                        dest_domain: dst.name.clone(),
102                        pattern: pattern.clone(),
103                        safe,
104                    });
105
106                    if !safe {
107                        violations.push(CdcViolation {
108                            signal: signal.name.clone(),
109                            source_domain: src.name.clone(),
110                            dest_domain: dst.name.clone(),
111                            violation_type: CdcViolationType::MissingSynchronizer,
112                            message: format!(
113                                "Signal '{}' crosses from '{}' to '{}' without synchronizer",
114                                signal.name, src.name, dst.name
115                            ),
116                        });
117                    }
118                }
119            }
120        }
121    }
122
123    // Check for multi-bit crossings without gray code
124    for crossing in &crossings {
125        let sig = rtl.signals.iter().find(|s| s.name == crossing.signal);
126        if let Some(s) = sig {
127            if s.width > 1 && crossing.safe {
128                if let Some(CdcPattern::TwoFlopSync { .. }) = &crossing.pattern {
129                    violations.push(CdcViolation {
130                        signal: crossing.signal.clone(),
131                        source_domain: crossing.source_domain.clone(),
132                        dest_domain: crossing.dest_domain.clone(),
133                        violation_type: CdcViolationType::BusWithoutEncoding,
134                        message: format!(
135                            "Multi-bit signal '{}' (width {}) uses 2-flop sync without gray code",
136                            crossing.signal, s.width
137                        ),
138                    });
139                }
140            }
141        }
142    }
143
144    CdcReport { crossings, violations, patterns }
145}
146
147/// Generate SVA properties for CDC verification.
148pub fn cdc_sva_properties(report: &CdcReport) -> Vec<SvaProperty> {
149    let mut props = Vec::new();
150
151    for crossing in &report.crossings {
152        if let Some(CdcPattern::TwoFlopSync { ref dest_domain, .. }) = crossing.pattern {
153            props.push(SvaProperty {
154                name: format!("cdc_2flop_{}", crossing.signal),
155                clock: format!("clk_{}", dest_domain),
156                body: format!(
157                    "{sig}_sync1 |=> {sig}_sync2",
158                    sig = crossing.signal
159                ),
160                kind: SvaAssertionKind::Assert,
161            });
162        }
163
164        if let Some(CdcPattern::HandshakeCdc { ref req, ref ack }) = crossing.pattern {
165            props.push(SvaProperty {
166                name: format!("cdc_handshake_{}", crossing.signal),
167                clock: "clk".into(),
168                body: format!("{} |-> s_eventually({})", req, ack),
169                kind: SvaAssertionKind::Assert,
170            });
171        }
172    }
173
174    props
175}
176
177fn is_in_domain(signal_name: &str, domain: &CdcClockDomain) -> bool {
178    signal_name.starts_with(&format!("{}_", domain.name))
179}
180
181fn detect_pattern(
182    signal_name: &str,
183    rtl: &RtlModule,
184    src: &CdcClockDomain,
185    dst: &CdcClockDomain,
186) -> Option<CdcPattern> {
187    // Check for 3-flop sync FIRST (before 2-flop, since 3-flop implies sync1+sync2+sync3)
188    let sync1 = format!("{}_sync1", signal_name);
189    let sync2 = format!("{}_sync2", signal_name);
190    let sync3 = format!("{}_sync3", signal_name);
191    if rtl.signals.iter().any(|s| s.name == sync1)
192        && rtl.signals.iter().any(|s| s.name == sync2)
193        && rtl.signals.iter().any(|s| s.name == sync3)
194    {
195        return Some(CdcPattern::ThreeFlopSync {
196            source_domain: src.name.clone(),
197            dest_domain: dst.name.clone(),
198        });
199    }
200
201    // Check for 2-flop sync pattern: signal_sync1, signal_sync2
202    if rtl.signals.iter().any(|s| s.name == sync1) && rtl.signals.iter().any(|s| s.name == sync2) {
203        return Some(CdcPattern::TwoFlopSync {
204            source_domain: src.name.clone(),
205            dest_domain: dst.name.clone(),
206        });
207    }
208
209    // Check for handshake pattern
210    if signal_name.contains("req") {
211        let ack_name = signal_name.replace("req", "ack");
212        if rtl.signals.iter().any(|s| s.name == ack_name) {
213            return Some(CdcPattern::HandshakeCdc {
214                req: signal_name.into(),
215                ack: ack_name,
216            });
217        }
218    }
219
220    // Check for gray code
221    if signal_name.contains("gray") || signal_name.contains("grey") {
222        let sig = rtl.signals.iter().find(|s| s.name == signal_name)?;
223        return Some(CdcPattern::GrayCode { width: sig.width });
224    }
225
226    // Check for FIFO
227    if signal_name.contains("fifo") || signal_name.contains("async_fifo") {
228        return Some(CdcPattern::AsyncFifo);
229    }
230
231    None
232}
logicaffeine_compile/codegen_sva/cdc.rs

logicaffeine_compile/codegen_sva/
cdc.rs
