As processor architecture and design development becomes completely liberated with open-source RISC-V instruction set architecture (ISA), the race to get RISC-V silicon in our hands has increased massively. We have no doubt that in next 5 years, we will see RISC-V based laptops and desktops in the market. But would these processors be of high quality? Would any one of them have a glitch like the famous Intel FDIV bug from the era of mid 90s? Have we learnt what it takes to robustly verify these processors for safety-critical domains, security and functionality?
In this article, we would like to explore these questions from the perspective of open-source RISC-V architecture and will take a look at verification trends and what makes processor verification hard and how it can be made easier with the use of formal methods in particular using the fully automated vendor-neutral formal formalISA® app from Axiomise in combination with the JasperGold® Formal Verification Platform from Cadence. We also discuss a new automated debug, analysis and reporting solution (i-RADARTM) from Axiomise that allows accelerated debug and reporting.