When: 11 March 2021, 14:00 GMT / 15:00 CET / 16:00 EET and Israel / 9am ET

Presenter: Dr  Ashish Darbari

Exhaustive formal verification of processors

Processor verification has always been a significant challenge. With the open-source RISC-V® ISA, we see an emerging revolution for processor design with lots of new commercial-grade processors for a wide range of applications ranging from embedded, storage, automotive, AI/ML, 5G, to IoT. While power, performance, and area (PPA) remain important, safety and security verification are also gaining prominence.

While formal property checking continues to see growing adoption, only 40% of the ASIC/IC projects use it. Most of the verification is still being dominated by simulation cycles and test cases, and recent industry trends suggest 68% of the projects miss their schedule and an equal number require respin.

How do we change the status quo, well, for processor verification at least? How can we enable a seamless adoption of formal verification (FV) for RISC-V processors?

This webinar will provide answers to these questions. We describe our coverage-driven processor verification methodology using the Axiomise RISC-V processor verification app – formalISA® and the Cadence JasperGold® verification platform. We will show how the coverage and proof-convergence methodology of formalISA® enabled by the Cadence JasperGold® was used to find bugs (even in processors already in silicon) and prove bug absence leading to the sign-off of different RISC-V processors with nearly 100% proof-convergence.