ABSTRACT: Formal methods are deeply rooted in the foundational theories of Computer Science. The past decade has seen phenomenal adoption of formal methods in electronic design verification, and semiconductor companies want to solve more fundamentally challenging problems with such methods. In the process, a new roadmap for formal verification seems to be evolving. We will discuss three dimensions of this roadmap. Firstly, we will explore the wide milieu of problems where formal methods are being used. Secondly, we discuss the need for new types of algorithms and proof methodologies to handle verification problems that are fundamentally harder than bit-level digital systems. Thirdly, we explore the role of AI/ML as a key enabler for the new roadmap of formal verification.

ABOUT THE SPEAKER: Dr Pallab Dasgupta currently leads Research and Innovation on Formal Verification at Synopsys, Sunnyvale. He has more than 25 years of experience in formal verification technologies. He had been a professor and former Dean of Sponsored Research at the Indian Institute of Technology Kharagpur for many years, collaborating with many semiconductor and EDA companies, and heading one of the most well-known research groups on formal methods and EDA – one that has produced more than 250 research publications and generations of students who are formal verification practitioners today.