RISC-V ISA Formal Proof Kit™

Verifying RISC-V designs with high assurance

ISA Formal Proof Kit™

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.

Why ISA Formal Proof Kit™?

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.

Key Differentiators

Vendor neutral
Axiomise Abstraction Models
Support all major formal tools
A high rate of proof convergence
Get running within minutes of setup
No modification to the design needed

Who should use this?

RISC-V Designers
RISC-V Verification Engineers
RISC-V Architects

How will this kit help?

Find low-power bugs
Catch X-propagation
Catch safety violations
Find deadlocks/livelocks
Expose security vulnerabilities
Catch bugs in design and specification
Check if your CPU design complies with the RISC-V ISA
Check that no micro-architectural bugs break ISA compliance
RISC-V is the trademark of the RISC-V foundation.
ISA Formal Proof Kit is a trademark of Axiomise Limited.
Formal Proof Kit is a trademark of Axiomise Limited.