Answer each question out loud before opening it. If you miss more than three in the checkpoint, revisit the lessons linked at the end.
It checks a property against every input sequence the assumptions allow and returns a proof or a minimal counterexample; simulation samples one sequence per run.
No violation within N cycles of reset, under the assumptions; nothing about deeper states.
The step can start from unreachable states; helper invariants, asserted and proved, rule them out.
Assumptions stricter than the real environment, which silently exclude legal traces and the bugs in them; covers and planted bugs expose it.
For control logic with short reach: arbiters, FIFOs, counters, credit loops, handshakes, decoders, deadlock, rules that must always hold.
Deep state, wide data, accumulated results, whole systems with software, statistics, and rules nobody wrote as properties.
Proving two implementations behave identically (RTL and netlist, before and after an ECO); it does not check either against the specification.
By rule, in one evidence ledger, with important rules getting both and every assumption of one method verified by the other.
Task. A credit-based link layer has a 16-entry retry buffer, an 8-bit sequence number that wraps, a replay timer of 4,096 cycles and a CRC on every packet. Decide which rules you would prove and which you would simulate, what properties and assumptions the proofs need, and how you would handle the deep state.
Prove: credit conservation (credits plus outstanding packets constant), the retry buffer never overflows or replays a packet it has freed, sequence numbers are assigned consecutively and acknowledged in order, and the replay logic never sends while the link is down. Assumptions: the peer acknowledges only sequence numbers that were sent, within the window; credits are returned only for consumed packets. Deep state: use a parameterised configuration (a 4-entry buffer, 3-bit sequence numbers, a 16-cycle timer) for the proofs, with induction and helper invariants (buffer occupancy equals the distance between head and tail pointers; outstanding count equals the sequence-number distance), and confirm the full-size configuration in simulation. Simulate: the CRC (a reference model in the scoreboard), long error-and-replay scenarios with the real 4,096-cycle timer, throughput and latency under error rates, and interoperability with a real peer model. Use a register app for the control registers and equivalence checking after synthesis.
Five steps: reset, then four pushes; at step 5 the FIFO holds four words and full is still low.
About 3 s at depth 6, 41 s at depth 8, over five minutes at depth 10.
The count equals the distance between the pointers, and is at most 4.
An assumption is never checked; if false, it silently removes real behaviour from the proof.
A cover on "full", written as an assertion of its negation, that passed: full was unreachable.
Accepted and ignored it, so the bound properties were never checked; a deliberately false property passing revealed it.
Register checking against the machine-readable register map.
7 and 9.
BUG_1 and BUG_22: their effects need more cycles than the bound (a full FIFO, a credit returned during sleep).
Their rules (framing, error flags, counters, registers, configuration, sleep and wake) had no formal properties.