Can a tool prove a rule holds for every possible input, not just the ones you tried?
Simulation walks chosen paths through your design. You write the stimulus, the simulator runs it, and the checks compare. Every green run adds one more path that works.
But the paths you did not write stay unknown, and random stimulus only samples. This lesson explains a method that reasons about every input sequence at once, without running them.
One fact before the idea: this course does not run a formal tool. SymbiYosys is not part of the tested toolchain, so this lesson ships no listing and quotes no transcript. What follows is the concept, so you can recognise what formal asks that simulation cannot.
An input sequence is the list of input values cycle by cycle: reset high, event high, event high, idle, and so on. A simulation picks some sequences and runs them. Formal verification checks a property against every possible sequence.
A property is a rule the design must obey on every cycle, written in the style of the assertions of Assertions. Four rules from the course counter show the shape: reset forces the count to 0, clear beats a simultaneous event, the count wraps from 15 to 0, and an idle cycle holds the count.
Two engines answer the question. A bounded check explores every sequence up to a bound, say the first 20 cycles after reset (illustrative). A proof by induction shows the rule holds at reset and that, if it holds in any reachable state, it still holds after the next clock edge; chained together, the two steps cover every length.
Every formal run ends in one of three ways. The table lists them with what each one asks of you.
Outcome | What it means | What you do next |
|---|---|---|
proven | no input sequence within the stated assumptions breaks the property (and, for a bounded check, none within the bound does) | keep the property; it now guards the rule |
counterexample | one concrete failing input sequence, cycle by cycle | replay it in simulation and fix the design or the property |
inconclusive | the tool ran out of time or memory before deciding | shrink the design under proof, add helper assumptions, or cover the rule with simulation |
Read the middle row twice. A counterexample is a concrete failing input sequence, cycle by cycle: the failing test you did not have to write. Replay it in simulation and it breaks there too.
The figure below draws the difference for one property over the reachable states. On the left, three simulated paths wander from reset and leave most of the region untouched. On the right, the whole region carries check marks: every reachable state obeys the rule.
Take the rule reset always forces the count to 0 and aim it at the reset_last mutant of Tests That Can Fail, which counts before checking reset. The tool answers with a counterexample, and it reads like a simulation trace.
Cycle | rst_n | clear | valid | Count | What the rule needs |
|---|---|---|---|---|---|
0 | 1 | 0 | 1 | 0 to 1 | event counted |
1 | 0 | 0 | 1 | 1 to 2 | rule needs 0; design gives 2 |
Cycle 1 is the whole story: reset asserted with an event present, and the rule needs 0. The mutant counts to 2 instead. Drive this two-cycle sequence in simulation and the strong testbench reports the same mismatch, which is the failure lesson 5.1 traces to broken reset priority.
A proof rests on what you assume about the inputs. Assumptions say which sequences count: reset is asserted on the first cycle, for example. Assume too much and the proof speaks about inputs that never occur; the exact corner you feared, reset together with an event, is easy to assume away by accident.
The bound matters the same way. A bounded pass covers only its depth, like a simulation that stops early. And the property itself must be right: proving the wrong rule proves nothing, which is the moral of lesson 5.1 wearing new clothes.
Formal shines on small control logic and on rules of the form never in an illegal state. It finds corners nobody thought to simulate, such as the reset-and-clear corner of Coverage. It stalls on large designs, because each added state bit multiplies the space to explore, and it never replaces simulation: throughput on real software is measured by running it, not by proving a rule.
No. The proof covers only the first 5 cycles after reset; cycle 16 was never examined. A bounded pass is a statement about its depth, like a simulation that stops early. Extend the bound, switch to induction, or cover the deep case with directed simulation.
Over-constraining the inputs until the proof says nothing. Each assumption removes sequences from the check. Assume reset never arrives together with an event and the proof passes over the very corner that broke lesson 5.1. Review every assumption as sceptically as the design.
Treating proven as the design is correct. A proof covers one property under its assumptions. Unwritten properties, wrong properties and cycles past the bound stay open, so a proven rule joins the evidence instead of ending the argument.
Skipping simulation. Formal says nothing about throughput, about long realistic software runs, or about whether the cycle-by-cycle behavior looks sane in a waveform. Run the loop; prove the rules that guard it.
Rule: a proof guarantees the property you wrote, under the assumptions you stated, and nothing more.
Formal for the count never exceeding 15: it is a rule about every cycle on tiny control state, which a tool checks for all sequences. Simulation for the 3 MB image decode: a huge data path over long realistic traffic is exactly what running beats proving. Formal for reset always forcing 0: a control rule over every sequence, including corners nobody writes stimulus for. Simulation for throughput on real software: a performance number over long realistic runs is measured by running it.
Replay it in simulation: drive those exact inputs, watch the rule break, then decide whether the design or the property is wrong. A counterexample is a failing test you did not have to write, and it points at the exact spec row the design breaks.
The first is a rule about every cycle over a small state space, which the tool decides for all sequences at once. The second is a number over long realistic behavior that depends on software and traffic; no property states it crisply, and the honest evidence is a measured run.
Simulation samples input sequences; formal checks every sequence against a property, up to a bound or by induction.
A proof ends proven, with a counterexample, or inconclusive; each outcome tells you what to do next.
A proof rests on its assumptions, its bound and the property itself; get any of those wrong and the proof says nothing.