The ABC of formal verification

Add to your list(s) Download to your calendar using vCal

• Ashish Darbari (Axiomise)
• Monday 24 April 2023, 13:00-14:00
• Department of Electrical and Electronic Engineering, Room 909B.

If you have a question about this talk, please contact George A Constantinides.

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. 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 scalable formal verification methodology.

This tutorial seminar introduces a formal verification methodology, focusing on the ABCs of formal: (A) abstraction, (B) bug hunting & building proofs, and© 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 how coverage can be used to find missing checkers and over-constraints, establishing sign-off quality verification using the six-dimensions of coverage. At Axiomise, we have been using our scalable verification methods for end-to-end sign-off for semiconductor chips with billions of gates. The methodology we will present in this seminar will give you a taste of what these methods look like for production-grade verification.

Bio

Dr Ashish Darbari is the founder & CEO of Axiomise – a formal verification training, consulting, services, and IP company. Ashish has trained close to 200 engineers in formal verification across some of the best-known names in the industry. He is the developer of the formalISA® app. Ashish has 60 patents in formal verification and over 70 publications. He holds a DPhil in formal verification from the University of Oxford and is a Fellow of the British Computing Society and IETE .

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Department of Electrical and Electronic Engineering, Room 909B

Note that ex-directory lists are not shown.