Formal Verification in RISC-V CPU Design Verification Flow

Abstract

In recent years, the popularity of RISC-V cores has continued to rise. The flexibility and scalability of its architecture have brought convenience in applications, but it has also brought huge challenges to design verification. For traditional simulation based verification, proof of correctness and security is hard to achieve. At this moment, formal verification with its advantages in completeness and correctness behavior has become a new choice. It has become improvement for simulation based verification. Even more, when a full proof is done, it can replace simulation, and ensure the correctness of the design. This article introduces the theory and actual implementation of processor formal verification.