Skip to main content

analyze_vacuity

logicaffeine_compile::codegen_sva::sva_vacuity

Function analyze_vacuity 

Source 
pub fn analyze_vacuity(expr: &SvaExpr) -> VacuityStatus
Expand description

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.