Part 7 answers: When should we prove instead of test?
Formal tools consider every input sequence the environment allows, so they find rare combinations simulation would need years to hit, and can prove that none exist. They struggle with large designs, long sequences and heavy data paths, and every proof depends on assumptions that may hide bugs.
This part covers bounded and full proofs, assumptions and over-constraint, where formal wins and where simulation wins, formal apps such as equivalence checking, and how to split a verification plan between proof and test. Proofs on this course run for real, with Yosys and an SMT solver.
Explain what a bounded proof and an induction proof each guarantee.
Spot an over-constrained proof and guard against it.
Split a verification plan between formal and simulation.
Answer each in your head before opening it. If two or more feel shaky, revisit Part 6: Coverage first.
That every planned situation was exercised, not that the design behaved correctly in them.
The stimulus can no longer reach the remaining bins; change the stimulus, prove them unreachable, or waive them.
Whether the testbench detects deliberately injected bugs: the quality of the checks, not of the design.
# | Lesson | Level | Status |
|---|---|---|---|
7.1 | W · Working | Ready | |
7.2 | S · Senior | Ready | |
7.3 | S · Senior | Ready | |
7.4 | S · Senior | Ready | |
7.5 | S · Senior | Ready | |
7.6 | S · Senior | Ready | |
7.7 | S · Senior | Ready | |
7.8 | P · Principal | Ready | |
7.9 | S · Senior | Ready | |
— | all levels | Ready |
Every lesson in this part is ready. Work through them in order: each one sets up the problem the next one solves.
This course teaches the decisions behind verification. These lessons teach the tools and syntax that carry them out, so this part links to them instead of repeating them.