Reduce Risk with RISC-V Processor Design
Use formal verification with a tool you like to exhaustively prove that your design works
Designing RISC cores is easier, with the advent of open-source RISC-V ISA and a whole new eco-system being developed around software and tools. What is not discussed as much in the realms of RISC-V is the need and gaps in verification. Although, formal verification has received a lot more attention in the context of RISC-V a lot of this is not a neutral ground where RISC-V designers can simply choose to use whatever formal tool they like and can get a kickstart with using formal verification right away. Our formal verification solution is the only one in the industry offering a complete vendor-neutral formal verification solution for RISC-V processor verification.
Axiomise vision
At Axiomise, we have the vision of enabling all design verification engineers in the use of formal verification regardless of their choice of tool, by providing them powerful methodologies that are guaranteed to power up formal users providing predictability in verification.
Founded by Dr. Ashish Darbari with two decades of formal verification experience in research labs and industry, and over 50 papers and patents in formal verification, he formed Axiomise with the mission to make it easier for everyone to become an expert with formal verification.
Vendor-neutral solution
While we certainly offer bleeding-edge training to enable new and experienced users to get the best our of formal, we have recently launched a first-of-its-kind solution for RISC-V processor verification.
You design, use our formal proof kit and any formal verification tool you like, and within minutes you will be up and running finding bugs in your designs, and building proofs of bug absence. Overall you will obtain a very high verification throughput — and all of this without having to write a single line of verification code.
Our solution is designed using the industry-standard SystemVerilog assertions (supported by all the tools) and our methodology is backed up by two decades of experience in the field is guaranteed to make you happy and productive.
Architectural and micro-architectural verification
Recently, we verified a family of RISC-V processor designs, some of whom have been in silicon for some time and found tons of bugs ranging from catching un-intended code insertions (trojans), functional safety issues (lockstep mismatches), deadlocks, reachable X-issues, and catching wasted dynamic power. We went beyond the usual architectural or micro-architectural verification in a combined flow leveraging the newly designed ISA formal proof kit from Axiomise.
On zeroriscy, we caught over 90 bugs (most of these were deadlocks due to a buggy debug unit), on microriscy, over 60 bugs were caught and on ibex — a processor under development — 65 bugs.
The beauty of our solution is that to get started it takes minutes and the results from verification runs start appearing right away — again all without the user having to write a single line of verification code. While it is understandable that ibex is under development, so one would expect bugs, but given that ibex is a near-clone of zeroriscy which has been around for some time I didn’t expect these many to be there.
Functional bugs within minutes
The nice thing about our formal verification approach is that it took less than 5 minutes to find the first set of issues (57 checks failed on the ibex processor for example) — the time it takes for a quick coffee! Once we have debugged the root-cause we either fix the design or temporarily guard the verification environment by disabling the buggy interface to see if we can get the checks to prove exhaustively. If we do this, then we can get exhaustive proofs on all the key checks of the RV32IC subset of the ISA in about two hours — the time it takes to get a luxury business lunch or a team get-together! Other bugs we caught were on functional safety (lockstep), X-reachability, deadlocks and power issues.
Corner-case bugs: bugs that are hard-to-catch using simulation
What is even more intriguing is that a lot of the bugs we have found on ibex are corner-case bugs extremely difficult to catch with dynamic simulation, architectural simulation tests, or even FPGA/emulation. We demonstrated that these bugs will only ever manifest when the design is in a certain internal state when some input signals change their state. Our ability to find bugs, demonstrate that they are corner-case bugs, and show precise conditions when they will and when they won’t cause problems — and all this within minutes of runtime is unique to formal verification powered up by Axiomise methodology.
On zeroriscy, previously verified and running in silicon (40 nm ASIC and FPGA) we have found deadlocks, un-intended code insertions causing security vulnerabilities and dynamic power and X issues.
We invite and encourage you to use our solution to get started on the fast, track of formal verification, without needing the expertise in formal verification. However, if you fancy being an expert yourself, we can share our experience through our training courses. I’ve over the last decade taught over a hundred engineers in different organizations some of whom have made formal verification a choice of their career. You’re welcome to check the testimonials on our website.
You design, you verify your designs with formal verification using our solution and your choice of formal verification tool. You design, we verify using your choice of formal verification tool.
Unlock the true potential of formal verification and de-risk the risk that comes with easy-design and challenging verification with our RISC-V formal verification proof kit which works with all the formal verification tools.
Download our whitepaper providing more details of our solution and methodology on how we verified a family of RISC-V processors.
