Formally verify your RISC-V designs

Processor verification is a hard and challenging task because of complex architecture, custom instructions, exceptions and interrupts, very complex μ-Architecture, and continuous PPA optimizations. With the unprecedent freedom RISC-V spec offers to users in terms of optional instructions and features, custom instructions and microarchitecture varieties, complete verification of RISC-V cores is quite challenging. The Processor core verification app provides >10x verification runtime and setup speed-up, exhaustive u-Architecture verification, proven 100% coverage and no undocumented RTL, as well as ISA compliance as a side product. It provides a high degree of automation with no need for writing assertions or functional coverage and quickly root causes bugs. Because of the complexity of RISC-V processors, its verification is a high-effort task, and debugging is slow, simulation cannot hit all pipeline corner-cases also writing functional coverage model is difficult and we face functional/structural coverage closure issues. Furthermore, adding a single new instruction introduces bugs in existing functionality and requires complete re-verification.

In this session, you'll learn about formal processor verification approaches, including what they are, how to apply them, and the advantages of advanced formal technologies, which can be utilized by any engineer who wants to speed-up processor verification by >10x and increase quality of code.