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 ...
Get Formal Verification now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
