Axiomise designed a formal verification proof kit for checking RISC-V ISA compliance for specific RISC-V micro-architectures. Our proof kit can be used by anyone familiar with Verilog/VHDL and SystemVerilog Assertions. The proof kit comes with a pre-compiled library of SVA properties that match the intent of the RISC-V ISA. Simply bolt this proof kit on top of your design, using a single setup file, and you will be up and running within minutes. You’re not limited to any specific formal verification tool or any specific proprietary assertion languages, and you do not have to modify the design in any way! On several designs that we tested, we have found greater than 99% proof convergence across all major formal verification tools, and in this process discovered numerous bugs.

RISC-V based eco-system is growing at an astronomical speed. What is lacking in this eco-system is the wide use of formal verification. Formal verification relies on building exhaustive proofs of bug absence and in this process discovers bugs in the design. Finding corner-case bugs that establish functional defects in the micro-architecture is one challenge, while at the same time establishing compliance with the architecture is another. Being able to establish with confidence that the CPU implementation actually implements the ISA and only those instructions that are in the ISA is a major challenge for any kind of verification; formal being no exception. We need to ensure that no malicious bugs are in the CPU design regardless of whether they are due to micro-architectural implementation defects, deliberate trojan insertions, or unintended bugs due to the misunderstanding of RISC-V ISA.

Obtaining scalable formal verification is a major challenge. At Axiomise we specialise in bringing predictability and scalability back to formal verification. We have designed a library of abstractions and problem reduction techniques that we have used in building our RISC-V proof kit. This means we are able to guarantee the same end result with any formal verification tool of your choice; the run time does vary but what is proven in one tool gets proved in another, and what remains unresolved in one tool remains in the other tool as well.