Formal Verification

Chapter 9

Formal verification’s greatest bloopers

The danger of false positives

In Chapter 9, we discuss some real-life examples of cases where FV techniques were applied incorrectly, sometimes resulting in false positives: cases where a “formally proven” design turned out to contain errors. The simplest cases result from misuse or misunderstanding of the System Verilog language, which should be addressed by strong linting and manual reviews. Another class of these problems is vacuity issues, where part of the problem space is ignored; prevent these using tool features, good cover points, review of reset conditions, and simulation of assumptions. A third cause is implicit or misunderstood assumptions, addressable by careful review of assumptions ...