The ABC of formal verification

When: 11 Feb 2021, 16.00 GMT/08.00 PST

Presenter: Dr Ashish Darbari & Joe Hupcey III, Siemens EDA

The art & science of verifying multi-million flip-flop designs

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.

Who should attend?

Verification Engineers
Verification Managers
Architects (CPU/GPU/System)
Practising verification professionals
Undergraduate students
Postgraduate students in CS, and EEE

What do you learn?

Overview of formal methods

How to get started with abstraction in formal property checking?

Bug hunting and building proofs of bug absence

What is formal coverage?

How to use coverage formal sign-off?

Sign-off with bounded proofs

Using equivalence checking to validate design changes

Use coverage techniques to compute logic & area optimizations