Every proof in this course is a question about an assertion: can its failure state be reached? This section teaches SVA only as the proof engine reads it. The language itself lives in the SystemVerilog course; here each textbook operator is translated into the Boolean history form the proof front end accepts, and every rule is shown passing on a correct design and failing on a mutant.
Topic | What it covers | After it you can... |
|---|---|---|
Monitors, sampling, delay pipelines and the translation table | Turn any textbook rule into a runnable Boolean history check. | |
Overlapped versus non-overlapped, level versus edge, stability, history windows | Place every check in the right cycle and window. | |
Safety versus liveness, weak and strong, bounded response, fairness | Classify a rule and say what result a proof can honestly give. | |
Reading failures, vacuity, mutation checks, the review checklist | Prove that a property can fail before trusting its pass. |
Suggested order: top to bottom. The first topic builds the monitor picture and the translation table everything else relies on; the second fixes the one-cycle errors reviewers find most often; the third draws the line between what is provable and what needs a bound; the fourth turns that scepticism into a review routine. Readers chasing one failure can start at its topic and follow the links back.