Reduce Risk with RISC-V Processor Design

Dr Ashish Darbari
Aug 14, 2019 · 5 min read

Use formal verification with a tool you like to exhaustively prove that your design works

Image for post
Image for post
Formally verify your RISC-V designs in a scalable way with predictability

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

Image for post
Image for post

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

Image for post
Image for post
A differentiated solution from Axiomise for RISC-V formal 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

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

Corner-case bugs: bugs that are hard-to-catch using simulation

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.

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch

Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore

Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store