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