The ABC of Formal Verification

Formal verification constructs a mathematical proof to verify a design-under-test (DUT) against a requirement. The requirement itself can be expressed in multiple ways. Traditional formal verification tools compare the DUT to a second model and determine through Equivalence Checking (EC) if the two models agree on all legal inputs. The best-known method is Assertion-Based Verification (ABV), aka property checking. Assertions are commonly used in simulation-based verification, however, their adoption in formal verification is limited. One of the main reasons for limited formal adoption is a lack of formal methodology that is scalable.

This tutorial webinar covers formal methodology in detail focusing on the ABCs of formal: (A) abstraction, (B) bug hunting & building proofs, and (C) coverage in the context of property checking. Through an example, we show how end-to-end formal testbench models are constructed to build proofs of bug absence and find bugs using abstraction techniques. We discuss in detail how coverage can be used to find missing checkers, and over-constraints establishing sign-off quality verification using the six dimensions of coverage.