Formal Verification, 2nd Edition

Chapter 9: Formal verification's greatest bloopers: the danger of false positives

Abstract

In Chapter 9, we discuss some real-life examples of cases where formal verification (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 SystemVerilog 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 properties, review of reset conditions, and simulation of assumptions. A third cause is implicit or misunderstood assumptions, ...