logicaffeine_compile/codegen_sva/
sufficiency.rs

1//! Property Sufficiency Analysis
2//!
3//! Before running verification, check if your properties are sufficient
4//! to cover the spec.
5
6use logicaffeine_language::semantics::knowledge_graph::HwKnowledgeGraph;
7use serde::{Serialize, Deserialize};
8
9/// Sufficiency analysis report.
10#[derive(Debug, Clone, Serialize, Deserialize)]
11pub struct SufficiencyReport {
12    pub lonely_signals: Vec<String>,
13    pub unconstrained_outputs: Vec<String>,
14    pub missing_handshakes: Vec<(String, String)>,
15    pub coverage_ratio: f64,
16    pub recommendations: Vec<String>,
17}
18
19/// Known handshake pairing patterns: (trigger_pattern, response_patterns)
20const HANDSHAKE_PAIRS: &[(&str, &[&str])] = &[
21    ("req", &["ack", "gnt", "grant"]),
22    ("request", &["acknowledge", "acknowledgment", "response", "grant"]),
23    ("valid", &["ready", "rdy"]),
24    ("cmd", &["resp", "response"]),
25    ("start", &["done", "complete"]),
26];
27
28/// Analyze property sufficiency from a KG.
29pub fn analyze_sufficiency(kg: &HwKnowledgeGraph) -> SufficiencyReport {
30    use logicaffeine_language::semantics::knowledge_graph::SignalRole;
31
32    let signal_names: std::collections::HashSet<String> = kg.signals.iter().map(|s| s.name.clone()).collect();
33    let edge_signals: std::collections::HashSet<String> = kg.edges.iter()
34        .flat_map(|e| vec![e.from.clone(), e.to.clone()])
35        .collect();
36
37    // Lonely signals: not mentioned in any edge
38    let lonely_signals: Vec<String> = signal_names.iter()
39        .filter(|s| !edge_signals.contains(*s))
40        .cloned()
41        .collect();
42
43    // Unconstrained outputs: output signals with no driving edge
44    let unconstrained_outputs: Vec<String> = kg.signals.iter()
45        .filter(|s| s.role == SignalRole::Output)
46        .filter(|s| !kg.edges.iter().any(|e| e.to == s.name))
47        .map(|s| s.name.clone())
48        .collect();
49
50    // Missing handshake pairs: detect common naming patterns without edges
51    let mut missing_handshakes: Vec<(String, String)> = Vec::new();
52    for (trigger_pattern, response_patterns) in HANDSHAKE_PAIRS {
53        let trigger_match = kg.signals.iter().find(|s| {
54            s.name.to_lowercase().contains(trigger_pattern)
55        });
56        if let Some(trigger_sig) = trigger_match {
57            for resp_pattern in *response_patterns {
58                let resp_match = kg.signals.iter().find(|s| {
59                    let lower = s.name.to_lowercase();
60                    lower.contains(resp_pattern) && s.name != trigger_sig.name
61                });
62                if let Some(resp_sig) = resp_match {
63                    // Check if there's already a direct edge between them
64                    let has_edge = kg.edges.iter().any(|e| {
65                        (e.from == trigger_sig.name && e.to == resp_sig.name)
66                        || (e.from == resp_sig.name && e.to == trigger_sig.name)
67                    });
68                    if !has_edge {
69                        missing_handshakes.push((trigger_sig.name.clone(), resp_sig.name.clone()));
70                    }
71                    break; // Only match first response pattern
72                }
73            }
74        }
75    }
76
77    // Coverage ratio
78    let total = signal_names.len() + kg.edges.len();
79    let covered = edge_signals.len();
80    let coverage_ratio = if total > 0 { covered as f64 / total as f64 } else { 0.0 };
81
82    // Recommendations
83    let mut recommendations = Vec::new();
84    for sig in &lonely_signals {
85        recommendations.push(format!("Signal '{}' is not constrained by any property", sig));
86    }
87    for sig in &unconstrained_outputs {
88        recommendations.push(format!("Output '{}' has no driving property", sig));
89    }
90    for (trigger, response) in &missing_handshakes {
91        recommendations.push(format!("Missing handshake: '{}' has no edge to '{}'", trigger, response));
92    }
93
94    SufficiencyReport {
95        lonely_signals,
96        unconstrained_outputs,
97        missing_handshakes,
98        coverage_ratio,
99        recommendations,
100    }
101}
logicaffeine_compile/codegen_sva/sufficiency.rs

logicaffeine_compile/codegen_sva/
sufficiency.rs
