logicaffeine_compile/codegen_sva/
coverage.rs

1//! Specification Coverage Metrics
2//!
3//! Computes how well a set of SVA properties covers the specification KG.
4
5use logicaffeine_language::semantics::knowledge_graph::HwKnowledgeGraph;
6use serde::{Serialize, Deserialize};
7
8/// Coverage metrics for a specification.
9#[derive(Debug, Clone, Serialize, Deserialize)]
10pub struct SpecCoverage {
11    pub signal_coverage: f64,
12    pub property_coverage: f64,
13    pub edge_coverage: f64,
14    pub temporal_coverage: f64,
15    pub uncovered_signals: Vec<String>,
16    pub uncovered_properties: Vec<String>,
17}
18
19/// Compute specification coverage given a KG and a set of covered signal names.
20pub fn compute_coverage(kg: &HwKnowledgeGraph, covered_signals: &[String]) -> SpecCoverage {
21    let total_signals = kg.signals.len();
22    let total_properties = kg.properties.len();
23    let total_edges = kg.edges.len();
24
25    let covered_count = kg.signals.iter()
26        .filter(|s| covered_signals.iter().any(|c| c == &s.name))
27        .count();
28
29    let uncovered_signals: Vec<String> = kg.signals.iter()
30        .filter(|s| !covered_signals.iter().any(|c| c == &s.name))
31        .map(|s| s.name.clone())
32        .collect();
33
34    let signal_coverage = if total_signals > 0 {
35        covered_count as f64 / total_signals as f64
36    } else {
37        0.0
38    };
39
40    // Edge coverage: fraction of edges where BOTH endpoints are covered
41    let covered_edges = kg.edges.iter()
42        .filter(|e| covered_signals.iter().any(|c| c == &e.from)
43            && covered_signals.iter().any(|c| c == &e.to))
44        .count();
45    let edge_coverage = if total_edges > 0 {
46        covered_edges as f64 / total_edges as f64
47    } else {
48        0.0
49    };
50
51    // Property coverage: fraction of properties whose associated edge signals are covered
52    let covered_props = kg.properties.iter()
53        .filter(|p| {
54            // A property is covered if its associated edge has both endpoints covered
55            kg.edges.iter().any(|e| {
56                e.property.as_deref() == Some(&p.name)
57                    && covered_signals.iter().any(|c| c == &e.from)
58                    && covered_signals.iter().any(|c| c == &e.to)
59            })
60        })
61        .count();
62    let property_coverage = if total_properties > 0 {
63        covered_props as f64 / total_properties as f64
64    } else {
65        0.0
66    };
67
68    // Temporal coverage: temporal properties (safety/liveness) that are covered
69    let temporal_props = kg.properties.iter()
70        .filter(|p| p.property_type == "safety" || p.property_type == "liveness")
71        .count();
72    let covered_temporal = kg.properties.iter()
73        .filter(|p| {
74            (p.property_type == "safety" || p.property_type == "liveness")
75                && kg.edges.iter().any(|e| {
76                    e.property.as_deref() == Some(&p.name)
77                        && covered_signals.iter().any(|c| c == &e.from)
78                        && covered_signals.iter().any(|c| c == &e.to)
79                })
80        })
81        .count();
82    let temporal_coverage = if temporal_props > 0 {
83        covered_temporal as f64 / temporal_props as f64
84    } else {
85        0.0
86    };
87
88    // Uncovered properties: only those NOT covered
89    let uncovered_properties: Vec<String> = kg.properties.iter()
90        .filter(|p| {
91            !kg.edges.iter().any(|e| {
92                e.property.as_deref() == Some(&p.name)
93                    && covered_signals.iter().any(|c| c == &e.from)
94                    && covered_signals.iter().any(|c| c == &e.to)
95            })
96        })
97        .map(|p| p.name.clone())
98        .collect();
99
100    SpecCoverage {
101        signal_coverage,
102        property_coverage,
103        edge_coverage,
104        temporal_coverage,
105        uncovered_signals,
106        uncovered_properties,
107    }
108}
logicaffeine_compile/codegen_sva/coverage.rs

logicaffeine_compile/codegen_sva/
coverage.rs
