Vacuity and unreachable covers
Lesson 3.5 introduced vacuous success. Vacuity is also the mechanism behind most over-constraint false positives, so
it deserves a closer look. An assertion A |-> B is vacuous in an environment if A can never match.
Typical causes:
| Cause | Example |
|---|---|
| Typo or wrong polarity | valid && !valid |-> …, !rst_n vs rst_n |
| Wrong signal | Using req_q (registered, unused) instead of req |
| Impossible timing | start ##1 start |-> … when start is guaranteed to be a single-cycle pulse |
| Over-constraint | An assumption forbids the antecedent (previous lesson) |
| Width / constant mismatch | state == 3'd5 when state is 2 bits wide |
Defences
- Turn on the tool's vacuity check and treat vacuous assertions as failures.
- For key assertions, write explicit antecedent covers — they double as documentation.
- Review trace lengths of covers: if a behaviour you expected to take 5 cycles needs 60, something is off.