logicaffeine_compile/codegen_sva/
sva_vacuity.rs

1//! SVA Nonvacuous Evaluation Tracking (IEEE 16.14.8)
2//!
3//! Implements the 33 rules (a-ag) for determining when an assertion
4//! evaluation is nonvacuous. A vacuous success means the antecedent
5//! was never triggered — the property never actually tested the design.
6//! If ALL evaluation attempts are vacuous, the assertion is dead.
7
8use super::sva_model::SvaExpr;
9
10/// Result of vacuity analysis for a property.
11#[derive(Debug, Clone, PartialEq)]
12pub enum VacuityStatus {
13    /// The evaluation is definitely nonvacuous
14    Nonvacuous,
15    /// The evaluation is vacuous (property never tested)
16    Vacuous,
17    /// Cannot determine statically — depends on runtime values
18    Unknown,
19}
20
21/// Analyze whether an SVA property evaluation can be nonvacuous.
22///
23/// Returns `Nonvacuous` if there exists at least one evaluation attempt
24/// where the property is exercised (antecedent triggered, etc.).
25/// Returns `Vacuous` if the property can NEVER be exercised.
26/// Returns `Unknown` for runtime-dependent cases.
27///
28/// IEEE 16.14.8 rules a-ag.
29pub fn analyze_vacuity(expr: &SvaExpr) -> VacuityStatus {
30    match expr {
31        // Rule (a): A sequence is always nonvacuous
32        SvaExpr::Delay { .. } | SvaExpr::Repetition { .. } |
33        SvaExpr::GotoRepetition { .. } | SvaExpr::NonConsecRepetition { .. } => {
34            VacuityStatus::Nonvacuous
35        }
36
37        // Rule (b): strong(seq) is always nonvacuous
38        SvaExpr::Strong(_) => VacuityStatus::Nonvacuous,
39
40        // Rule (c): weak(seq) is always nonvacuous
41        SvaExpr::Weak(_) => VacuityStatus::Nonvacuous,
42
43        // Rule (d): not p is nonvacuous iff p is nonvacuous
44        SvaExpr::PropertyNot(inner) => analyze_vacuity(inner),
45
46        // Rule (e): p or q is nonvacuous if either is
47        SvaExpr::Or(l, r) | SvaExpr::SequenceOr(l, r) | SvaExpr::PropertyIff(l, r) => {
48            match (analyze_vacuity(l), analyze_vacuity(r)) {
49                (VacuityStatus::Nonvacuous, _) | (_, VacuityStatus::Nonvacuous) => {
50                    VacuityStatus::Nonvacuous
51                }
52                (VacuityStatus::Vacuous, VacuityStatus::Vacuous) => VacuityStatus::Vacuous,
53                _ => VacuityStatus::Unknown,
54            }
55        }
56
57        // Rule (f): p and q is nonvacuous if either is
58        SvaExpr::And(l, r) | SvaExpr::SequenceAnd(l, r) => {
59            match (analyze_vacuity(l), analyze_vacuity(r)) {
60                (VacuityStatus::Nonvacuous, _) | (_, VacuityStatus::Nonvacuous) => {
61                    VacuityStatus::Nonvacuous
62                }
63                (VacuityStatus::Vacuous, VacuityStatus::Vacuous) => VacuityStatus::Vacuous,
64                _ => VacuityStatus::Unknown,
65            }
66        }
67
68        // Rule (g): if(cond) p else q — nonvacuous if either branch can be
69        SvaExpr::IfElse { then_expr, else_expr, .. } => {
70            match (analyze_vacuity(then_expr), analyze_vacuity(else_expr)) {
71                (VacuityStatus::Nonvacuous, _) | (_, VacuityStatus::Nonvacuous) => {
72                    VacuityStatus::Nonvacuous
73                }
74                _ => VacuityStatus::Unknown,
75            }
76        }
77
78        // Rule (h): seq |-> prop is nonvacuous when seq has an endpoint match
79        // Rule (i): seq |=> prop is nonvacuous when seq has a match point
80        SvaExpr::Implication { antecedent, .. } => {
81            // The antecedent must be able to match for the property to be nonvacuous
82            match analyze_vacuity(antecedent) {
83                VacuityStatus::Nonvacuous => VacuityStatus::Unknown, // depends on runtime
84                VacuityStatus::Vacuous => VacuityStatus::Vacuous,
85                VacuityStatus::Unknown => VacuityStatus::Unknown,
86            }
87        }
88
89        // Rule (j-k): followed-by operators
90        SvaExpr::FollowedBy { antecedent, .. } => {
91            match analyze_vacuity(antecedent) {
92                VacuityStatus::Nonvacuous => VacuityStatus::Unknown,
93                VacuityStatus::Vacuous => VacuityStatus::Vacuous,
94                VacuityStatus::Unknown => VacuityStatus::Unknown,
95            }
96        }
97
98        // Rule (l-n): nexttime/s_nexttime — nonvacuous if next tick exists and body nonvacuous
99        SvaExpr::Nexttime(inner, _) | SvaExpr::SNexttime(inner, _) => {
100            analyze_vacuity(inner)
101        }
102
103        // Rule (p): always p — nonvacuous when p is nonvacuous at some tick
104        SvaExpr::Always(inner) | SvaExpr::SAlways(inner) => {
105            analyze_vacuity(inner)
106        }
107
108        // Rule (q-r): always [m:n] p — nonvacuous at some tick in range
109        SvaExpr::AlwaysBounded { body, .. } | SvaExpr::SAlwaysBounded { body, .. } => {
110            analyze_vacuity(body)
111        }
112
113        // Rule (s): s_eventually p — nonvacuous if p holds at some tick
114        SvaExpr::SEventually(inner) => analyze_vacuity(inner),
115
116        // Rule (u): eventually [m:n] p — nonvacuous
117        SvaExpr::EventuallyBounded { body, .. } | SvaExpr::SEventuallyBounded { body, .. } => {
118            analyze_vacuity(body)
119        }
120
121        // Rule (v): p until q — nonvacuous
122        SvaExpr::Until { .. } => VacuityStatus::Nonvacuous,
123
124        // Rule (z): p implies q — nonvacuous when p is true
125        SvaExpr::PropertyImplies(lhs, _) => {
126            match analyze_vacuity(lhs) {
127                VacuityStatus::Nonvacuous => VacuityStatus::Unknown, // depends on p being true
128                VacuityStatus::Vacuous => VacuityStatus::Vacuous,
129                VacuityStatus::Unknown => VacuityStatus::Unknown,
130            }
131        }
132
133        // Rule (ag): disable iff (rst) p — nonvacuous when rst is not always active
134        SvaExpr::DisableIff { body, .. } => {
135            analyze_vacuity(body)
136        }
137
138        // PropertyCase: vacuity depends on whether the case expression matches
139        // any item at runtime. Without a default, unmatched cases are vacuously true.
140        // This is runtime-dependent, so return Unknown.
141        SvaExpr::PropertyCase { default, .. } => {
142            if default.is_some() {
143                // With a default, some branch always fires
144                VacuityStatus::Nonvacuous
145            } else {
146                // Without a default, whether any case matches is runtime-dependent
147                VacuityStatus::Unknown
148            }
149        }
150
151        // Atomic signals, constants, system functions — nonvacuous (they always evaluate)
152        SvaExpr::Signal(_) | SvaExpr::Const(_, _) |
153        SvaExpr::Rose(_) | SvaExpr::Fell(_) | SvaExpr::Past(_, _) |
154        SvaExpr::Stable(_) | SvaExpr::Changed(_) |
155        SvaExpr::Not(_) | SvaExpr::Eq(_, _) | SvaExpr::NotEq(_, _) |
156        SvaExpr::LessThan(_, _) | SvaExpr::GreaterThan(_, _) |
157        SvaExpr::LessEqual(_, _) | SvaExpr::GreaterEqual(_, _) |
158        SvaExpr::Ternary { .. } |
159        SvaExpr::OneHot0(_) | SvaExpr::OneHot(_) | SvaExpr::CountOnes(_) |
160        SvaExpr::IsUnknown(_) | SvaExpr::Sampled(_) | SvaExpr::Bits(_) | SvaExpr::Clog2(_) |
161        SvaExpr::CountBits(_, _) | SvaExpr::IsUnbounded(_) |
162        SvaExpr::AcceptOn { .. } | SvaExpr::RejectOn { .. } |
163        SvaExpr::SyncAcceptOn { .. } | SvaExpr::SyncRejectOn { .. } |
164        SvaExpr::FirstMatch(_) | SvaExpr::Throughout { .. } | SvaExpr::Within { .. } |
165        SvaExpr::Intersect { .. } |
166        SvaExpr::BitAnd(_, _) | SvaExpr::BitOr(_, _) | SvaExpr::BitXor(_, _) |
167        SvaExpr::BitNot(_) | SvaExpr::ReductionAnd(_) | SvaExpr::ReductionOr(_) |
168        SvaExpr::ReductionXor(_) | SvaExpr::BitSelect { .. } | SvaExpr::PartSelect { .. } |
169        SvaExpr::Concat(_) | SvaExpr::ConstCast(_) |
170        SvaExpr::FieldAccess { .. } | SvaExpr::EnumLiteral { .. } |
171        SvaExpr::Triggered(_) | SvaExpr::Matched(_) |
172        SvaExpr::ImmediateAssert { .. } |
173        SvaExpr::SequenceAction { .. } |
174        SvaExpr::Clocked { .. } |
175        SvaExpr::LocalVar(_) |
176        SvaExpr::ArrayMap { .. } |
177        SvaExpr::TypeThis |
178        SvaExpr::RealConst(_) => {
179            VacuityStatus::Nonvacuous
180        }
181    }
182}
183
184/// Check if ALL evaluation attempts of a property are vacuous.
185/// If so, the assertion is dead and provides no verification value.
186pub fn is_dead_assertion(expr: &SvaExpr) -> bool {
187    matches!(analyze_vacuity(expr), VacuityStatus::Vacuous)
188}
logicaffeine_compile/codegen_sva/sva_vacuity.rs

logicaffeine_compile/codegen_sva/
sva_vacuity.rs
