Lesson 9.4 · When Proofs Lie: Avoiding False Positives

Reset and clock mistakes

The most spectacular false positive takes one character. A design uses an active-low reset, rst_n. The property file is copied from a block with an active-high reset:

one character, every proof meaningless

default disable iff (rst_n);      // WRONG: should be (!rst_n)

Now every assertion is disabled whenever the design is out of reset, i.e. during all normal operation. The tool proves everything instantly. Variants of the same mistake:

The tool's reset command uses the wrong polarity, so the design is held in reset forever.
An assumption keeps reset asserted (e.g. assume property (!rst_n) intended as "reset at the start").
A clock is declared with the wrong name, so the design never gets a clock edge and nothing changes.
Gated or divided clocks are not modelled, so part of the design is frozen.

With disable iff (rst_n), assertions are only evaluated while rst_n is low (in reset). Normal operation is never checked.