Formal Verification in VLSI Design Automation: From Theoretical Foundations to Practical Applications

Date: 2025/03/04 - 2025/03/04

Academic Seminar: Formal Verification in VLSI Design Automation: From Theoretical Foundations to Practical Applications

Speaker: Dr. You Li, Postdoctoral Scholar at Northwestern University

Time: 9:00-10 a.m., March 4th, 2025(Beijing Time)

Online: https://vc.feishu.cn/j/431063434

Abstract

Generative AI has achieved remarkable success in electronic design automation, hardware security and related fields. However, it has an Achilles Heel, which is its tendency to hallucinate. It can generate content that seems plausible but contains subtle factual or logical errors. Formal methods refer to a variety of mathematical rigorous and explainable techniques such as symbolic model checking, theorem proving, and constraint solving. They can produce a proof of correctness if the verified system satisfies the desired properties, or a counterexample otherwise. As such, they can help eliminate hallucinations in AI-generated content and enhance the security of AI-related systems.

In this seminar, I will showcase how to improve the scalability and usability of formal methods by exploiting the underlying problem structures of the corresponding applications. First, I will explain how to derive efficient equivalence checking algorithms for integrated circuits to ensure the correctness of chip designs. Afterward, I will illustrate how to achieve real-time verification for critical network protocols and systems. Next, I will demonstrate how to leverage logic locking, an emerging hardware root-of-trust paradigm to safeguard integrated circuits and AI systems with provable guarantees. Finally, I will present my research perspective in the era of generative AI. For one, I plan to bring together the creativity of generative models and the rigor of formal methods to develop a correct-by-construction design flow for integrated circuits. For another, I plan to integrate logic locking with AI accelerators to protect the security and privacy of AI applications at inference time.

Biography

You Li is currently a postdoctoral scholar at Northwestern University. He obtained his Ph.D. degree in computer engineering from Northwestern University, advised by Prof. Hai Zhou. He received his Bachelors's degree from the University of Michigan - Shanghai Jiao Tong University Joint Institute. His research interests include the theoretical foundations of formal verification and its applications in electronic design automation, hardware security, and AI systems.