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?
Practising verification professionals
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