Description

Formal verification has a modern history of over 70 years, and yet it is the least understood technology for practical use. Formal methods are used these days to find bugs and sign-off complex hardware designs with over 1.1 billion gates and yet very few people know the secrets of applying it successfully.

This course provides an overview of formal methods covering all essential technologies of formal including theorem proving, property checking, and equivalence checking. The bulk of the course is focused on property checking and how it can be deployed for large-scale verification in the industry. We focus on problem-solving & methodology of problem reduction to tackle the main challenge of formal verification - namely proof convergence and coverage & sign-off. 

Who should attend?


Designers

Architects

Verification engineers

Prerequisites

Passion to learn formal methods

Some knowledge of digital design 

Verilog/VHDL/SystemVerilog

What you will learn?

Why use formal verification?

History of formal methods

Foundations of formal methods

How to deploy agile formal?

Abstractions

Focus on proof convergence

Bug hunting

 Six-dimensional coverage

When to use simulation and when to use formal?



Class Schedule

Representative class agenda

Course Bonus

Live demos

Hands-on experience

Lifetime access to the material

Formative Quizzes 

Graded Quiz Exam

 Certificate

Instructor

Dr. Ashish Darbari

Dr. Ashish Darbari is the founder & CEO of Axiomise. He has been teaching & practising formal in the industry for over a decade. He holds a Doctorate in formal verification from the University of Oxford. He spent several years in advanced research in fault tolerance computing & formal methods, and in the development of certified SAT solvers at the University of Southampton where he was also a Royal Academy of Engineering Visiting Professor between 2015-2018. Before starting Axiomise, he has worked at Intel, Arm, Imagination Technologies and OneSpin Solutions where he headed their product team. He holds 60 US, UK & EU patents in formal verification and is a Fellow of the British Computing Society, and the IETE.