Automatic end-to-end formal verification of RISC-V processors
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.
Who should attend?
Practising verification professionals
What do you learn?
Why is processor verification hard?
Why simulation-based verification is not enough?
Challenges with formal property checking
Architectural formal verification
Why should you trust formal verification?
How to sign-off formal verification of processors?