RISC-V Processor Verification: Challenges And Opportunities For Formal

Talk by Ashish Darbari, (Founder and CEO of Axiomise)

Few processor architectures have evolved as fast as RISC-V. Open-source nature of RISC-V has empowered hundreds of designers to build processor implementations for RISC-V and processors seem to work – well most of the time. Going beyond the hobby projects, moving into commercial production-grade implementations numerous challenges are being seen by designers from software integration to verification. Verification consumes 70% of the overall design cycle with 68% of ASICS going through respins and an equal number late to market.

In this talk, I’ll describe how at Axiomise, we have been overcoming the verification challenge for RISC-V with automated end-to-end formal verification solutions providing excellent opportunities for everyone to build the RISC-V silicon – right first time. Our solutions have been finding bugs in cores, and memory subsystems and are able to build exhaustive proofs of bug absence on not just 32-bit/64-bit in-order cores but also 64-bit out-of-order cores.