Limits, outcomes and the right mindset
Three possible answers
For every assertion, a formal tool ends up in one of three places:
| Result | What it means | What you do |
|---|---|---|
| ✔ Proven | No legal input sequence of any length can violate the assertion. | Check it is not vacuous and that assumptions are not over-constraining (Chapter 9). |
| ✘ Failed (CEX) | The tool found a legal-looking trace that violates it. | Debug: is it a design bug, a wrong assertion, or a missing assumption? |
| ◐ Inconclusive / bounded | No CEX found up to N cycles, but no full proof either. | Decide whether N is deep enough, or reduce complexity (Chapter 10). |
Why not everything can be proven quickly
Checking properties of hardware is, in the worst case, extremely hard: the number of states doubles with every flip-flop, which is called state-space explosion. A design with 300 flip-flops already has more potential states than there are atoms in the observable universe. Engines succeed in practice because real designs are highly structured and properties usually depend on a small part of the logic — but no tool can promise a quick answer for everything.
The practical response is not to give up but to shape the problem:
- Verify smaller pieces — a block instead of a subsystem.
- Write local properties — a property that depends on 40 flops is easier than one that depends on 4,000.
- Abstract — replace a large counter or memory with a simpler model that preserves what the property needs.
- Accept bounded results consciously — when you can argue that N cycles reach every interesting state.
Garbage in, garbage out
A proof is only as meaningful as the properties and assumptions you give the tool. If an assertion checks the wrong thing, proving it is worthless. If an assumption accidentally forbids real behaviour, the tool may "prove" assertions that are actually broken. The habit that separates good formal engineers from beginners is skepticism about passing results: always ask "what could make this proof meaningless?" Covers, sanity checks and reviews are your defences, and you will practise all of them in this course.