A credit counter passes months of random simulation. A formal tool, run on the counter alone for twenty minutes, returns a nine-cycle trace: a credit returns in the same cycle a reset is released and a packet is sent, and the count ends one too high. The sequence is legal but so specific that random stimulus would have needed astronomically many cycles to stumble on it. The tool did not get lucky. It looked at every sequence.
What can formal tools prove about a protocol that simulation cannot, and how are they used?
The obvious answer is that more simulation, and better coverage, eventually finds everything. Simulation only checks the sequences it generates. The bugs that survive good simulation are combinations of rare events in specific cycles: a reset and a credit return and a send together, two requests colliding at a wrap-around. Coverage plans name the corners you thought of; the dangerous ones are the corners you did not.
Assertions (assert): the properties to prove, the same ones used in simulation (lesson 15.3).
Assumptions (assume): the rules the environment follows, typically the partner's side of the protocol. Without them, the tool finds "bugs" caused by impossible inputs.
Covers (cover): situations the tool must show are reachable, so you know the assumptions did not rule everything out.
Result: a proof that the assertion holds for every input sequence allowed by the assumptions, or a counterexample trace, usually short (fact T31).
// snippet: formal setup for the receiving side of a credit link
// The sender's side of the protocol is assumed; the receiver's is asserted.
assume property (@(posedge clk) disable iff (!rst_n)
vld |-> credits_at_sender > 0); // the sender never sends without credit
assert property (@(posedge clk) disable iff (!rst_n)
occupancy <= DEPTH); // the buffer never overflows
assert property (@(posedge clk) disable iff (!rst_n)
occupancy + credits_at_sender + credits_in_flight == DEPTH); // credits conserved
cover property (@(posedge clk) occupancy == DEPTH); // the buffer can really fillThe conservation assertion states the credit loop's invariant directly: every buffer slot is either occupied, held as a credit by the sender, or a credit on its way back. Any leak or double count breaks it.
Property | Why formal suits it |
|---|---|
Handshake rules (hold, stable) | Small, local; proved quickly for every stall pattern |
Credit and counter conservation | Invariants over all interleavings of sends, returns and resets |
FIFO and buffer overflow or underflow | Corner cases at full and empty with simultaneous push and pop |
Deadlock and liveness | Can prove "eventually" or produce a looping trace (Part 9) |
Arbiter fairness | Bounded-wait properties for every request pattern |
Ordering rules | No illegal overtaking, for every arrival order |
State-space size: whole subsystems are too large; formal works best on blocks and interfaces, with the rest abstracted.
Bounded results: a bounded proof to depth N says nothing beyond N; induction-based proofs cover all depths but may need helper invariants.
Over-constraining: a wrong assumption can hide real bugs; covers guard against it.
Data-heavy behaviour: long arithmetic pipelines and end-to-end data transformations are better checked by simulation against a model.
Practice | Use |
|---|---|
Protocol assertion IP in formal | The same AXI protocol assertions used in simulation drive formal proofs on an interface (fact A29) |
Assume-guarantee | Each side's rules are assumptions when verifying the other side, assertions when verifying itself |
Formal for deadlock | Proving credit loops and arbiters free of deadlock and starvation |
The opening counter (illustrative) had a priority bug: on the cycle reset was released, its update logic applied both the reset value and the credit return. The formal counterexample was nine cycles long and pointed at the line. A regression of the corrected counter proved the conservation invariant unbounded in a few minutes, and the same setup was reused for every credit counter in the chip.
An over-constraining assumption can make the design's interesting states unreachable, so every assertion passes vacuously; covers show those states are still reachable.
Occupancy plus credits held by the sender plus credits in flight equals D, at every cycle.
Formal checks every input sequence the assumptions allow, finding rare combinations simulation misses.
Assume the partner's rules, assert your own, and use covers to catch over-constraint.
Best for handshakes, counters, credit loops, FIFOs, arbiters, ordering and deadlock; simulation keeps data paths.