A Scalable Formal Approach for Correctness-Assured Hardware Design

Speaker: Dr. Jin Yang, Intel Labs
Date: March 8, 2023

Correctness must be a first principle in hardware design, especially for security and safety critical applications. We will give an overview of our scalable approach for correctness-assured hardware design at behavioral level, based on formalizing microarchitecture features as program transformations in an incremental compiler design and microprocessor correctness as a refined notation of compiler correctness. We will show how our approach is applied to designing a formally verified FHE (Fully Homo-morphic Encryption) accelerator.

Speaker bio:
Jin Yang is a Senior Principal Engineer in Strategic CAD Lab, Intel Labs. He is responsible for applied formal methods research for system software, hardware and security specification, design and verification. He joined Intel in 1997 after receiving his Ph.D. in CS from University of Texas at Austin, and has led many high-impact research projects and initiatives in Intel. He is active in the CAD and formal methods research communities with over 50 publications.