What formal verification really is

Imagine you are handed a padlock and asked: "Can this lock ever be opened without the right key?" One way to answer is to try every key in a big bucket and see whether any of them works. That is simulation: you pick inputs, run them, and look at the results. If none of your keys opens the lock, you feel better — but you have only tested the keys you had.

The other way is to take the lock apart and reason about the pins and springs until you can say, with certainty, which keys can turn the cylinder. That is formal verification (FV): instead of trying values, a tool builds a mathematical model of the design and proves whether a statement about it holds for every possible input sequence.

Why "trying more tests" does not scale

Consider a humble 32-bit adder with two inputs. It has 2⁶⁴ ≈ 1.8 × 10¹⁹ input combinations. Even at a billion simulations per second, checking them all would take roughly 585 years — for a block with no state at all. Add a few registers and the number of sequences of inputs explodes far beyond that. Real designs have thousands of flip-flops. Simulation can never be exhaustive; it can only be clever about where it looks.

Formal tools avoid enumerating values one by one. They manipulate sets of values symbolically (using techniques you will meet in Chapter 2), so a single run can say "for all 2⁶⁴ input pairs, the sum is correct" or "here is the one input pair where it is wrong".

The three ingredients

Every formal run, whatever the tool, combines three things:

1. The design — your RTL, usually SystemVerilog or VHDL.
2. Assertions — statements that must always be true, e.g. grant is never given to two requesters at once.
3. Assumptions (constraints) — what the outside world is allowed to do, e.g. a request stays high until it is granted.

The tool then answers one question per assertion: "Is there any sequence of legal inputs, starting from reset, that makes this assertion false?"

The vocabulary you will use daily