Invited: A Scalable Formal Approach for Correctness-Assured Hardware Design
Jin Seok Yang, Jeremy Casas, Zhenkun Yang · 2023
Correctness must be a first principle in hardware/-software co-design, especially for security and safety critical applications. We will give an overview of our scalable approach for correctness-assured hardware/software 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 Homomorphic Encryption) accelerator.