Module sva_vacuity 

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.

Enums

VacuityStatus

Result of vacuity analysis for a property.

Functions

analyze_vacuity

Analyze whether an SVA property evaluation can be nonvacuous.

is_dead_assertion

Check if ALL evaluation attempts of a property are vacuous. If so, the assertion is dead and provides no verification value.