At Axiomise, we’ve been talking about the formal verification of RISC-V processors with the focus largely on architectural compliance of RISC-V implementations against the ISA. Thanks to the RISC-V revolution, the focus on architectural verification has come back. I say come back because architectural formal verification of processors has been discussed and used in the past to many processors, including RISC architectures, AMD, Intel, and IBM. Arm has promoted its use on their designs through model checking approach.

Architectural verification has been considered to be the holy grail of verification. Despite complex micro-architectural verification of modern-day processors, one can never say for sure if the verified implementation ‘does’ or ‘does not’ match the ISA semantics. Whereas instruction-set based directed tests also called architectural-tests can test the conformance of a specific implementation, it is not robust. Constrained-random simulation verification aka UVM, can go quite deep in the micro-architectural verification, but its usage for architectural ISA testing is an overkill, so not used that much for ISA compliance. Given, that UVM is widely considered as the main verification workhorse, in most processor vendors, there is usually a gap between architectural testing and micro-architectural testing leaving the potential for missed bugs.

If a specific processor implementation does not match the architectural semantics of a given ISA, the damage can be big, equally, if we can demonstrate beyond doubt that it does, the return-on-investment (ROI) is big. So, in our view the architectural verification is a big requirement, can be a big liability and can be a big asset – so think big!

If a processor implementation matches its expected ISA semantics but still has bugs that are beyond the scope of architectural verification, then architectural verification is not good enough. Modern-day processors, especially the ones used in low-power devices are heavily optimized for area and power. We all expect our devices to be small and consume less power and have better battery life. Designers dream up of creative optimizations to reduce power and optimize sharing of resources to minimize area – a source of great ROI on design, but a cause of verification concerns that are not all possible to catch purely by architectural ISA verification.

So, diving deep into the nitty-gritty of implementation optimizations as small as they may be, from the verification perspective is micro-architectural verification where we flush out bugs in FSMs, deadlocks, livelocks, X-reachability analysis, unreachable code, redundant code and so on. Due to requirements of automotive functional safety, and avionics the processors have to be tested for lockstep compliance. Breaking down verification requirements into smaller ones, and applying purpose-built verification techniques to verify each of these is the topic of micro-architectural verification.  Breaking down the overall verification scope into smaller ones is better – so think small!

Formal methods are a well-established field dating back to early 1970s in modern times but its roots in philosophy and epistemic logic date back even further. Modern-day formal methods saw a renaissance with the industry focus on property checking aka model checking.  While, theorem proving dominated the space of formal methods for a long period and does not suffer from state-space exploration limitations of its cousin model checking its adoption is limited.  To get the best out of theorem provers we need a strong mathematical background in discrete maths and computational logic, which many design-verification engineers in semi-conductor industry don’t have. Also, theorem provers cannot provide you an explanation about why they could not prove a theorem. If you cannot prove the main theorem, you need to supply all the necessary lemmas and there is usually no obvious explicit hint. So, in that sense theorem provers cannot automatically find bugs in your models, although we can prove theorems establishing bug absence on models of any size.

For the last three decades model checking has been deployed widely across the semiconductor industry mainly because it can provide waveforms when properties (lemmas of theorem provers) do not prove against the design model (RTL). Design verification engineers can debug these waveforms like they do with simulation traces and can easily root-cause the issues. Once the offending issue is fixed, a property can be proven exhaustively against the RTL offering exhaustive proofs of bug absence.

I love formal as we have used it to find functional bugs in designs with 1 billion gates  (338 million flops) without any black-boxing or cut-pointing – widely used techniques for cutting out design logic in the RTL so the formal tools can cope with increasing design sizes. At Axiomise, we can do this as we have been doing formal verification for over two decades, but can someone new to the filed do this? The short answer is yes, and Axiomise is enabling this through their unique training offerings.

One central question that remains unresolved,  is who is going to write the properties/assertions/lemmas – whatever you may want to call it. Now, I’m a big fan of using our brains and encouraging others to think, plan and then execute – meaning the DV engineers should be the ones writing these. This question is not that different from asking who will write test cases, design test benches and write functional coverage in a UVM based verification. For formal verification, the properties are a cornerstone of verification, but so is the underlying formal model. A lot of the challenges arise from understanding ‘what to check’ and this could be different based on micro-architecture specification. However, for architectural verification and a subset of micro-architectural verification tasks, one can provide an automatic suite of properties. This is certainly the case for microprocessors and RISC-V is no exception. 

Open-source RISC-V, and now MIPS and Power architectures are changing the game for everyone. We don’t need to pay anyone a hefty architectural licensing fee for designing processors, but to be honest verification (catching design errors) and not design itself is the biggest cost with some estimates at 70% of the overall DV cost for most of the industry. The cost is in tools, workforce, and time. What is not factored in is methodology and training, but we can come to this sometime later.

We look at the open-source architecture as an opportunity to solve complex verification challenges by offering a set of automated flows, proof kits, and methodology that can be used across the board to address both architectural challenges as well as micro-architectural ones. We need high-quality tools, industry-proven, and vendor-neutral high-quality methodology to address the challenges of ‘big’ and ‘small’ verification.

At Axiomise, we are proud to be partners with four major tool vendors – Cadence®, Mentor – A Siemens Business®, Synopsys®, and Onespin Solutions®. These organizations have invested millions over the last two decades in building high-quality tools and have very strong R&D. What we offer is a range of methodology, flows and proof kits to address the ‘big’ and the ‘small’ verification challenges built on top of the tool stack.

We designed an ISA formal proof kit for architectural verification of RISC-V designs. Our solution is designed using the non-proprietary assertion language – SystemVerilog Assertions (SVA) and works across all the tools. When we couple this with our unique methodology, we get a very powerful proof kit that scales nicely on different processors, provides predictable results and works with a tool of your choice!

Our recently, announced RISC-V ISA formal proof kit® has been deployed in the field on several processors. We described our methodology and results in a whitepaper.

In the DVCon India conference next week, I will talk about how we found over 65 bugs including functional, safety, security and power-related ones in ibex – a RISC-V processor currently being implemented in Cambridge by lowRISC. The processor ibex is a near-clone of zeroriscy from the well-known PULP platform team, and though we found bugs in zeroriscy as well, the ones we find on ibex are new, and different from the ones we found on zeroriscy. I will show how the ‘big’ verification challenges of architectural verification were solved using our proof kit and how we caught security (trojans) and functional issues that were leveraged with the ‘smaller’ but equally important micro-architectural verification challenges exposing functional safety holes, X-issues, power issues, and deadlocks aka lockups.

Our methodology provides greater than 99% proof convergence; it takes minutes to set up and get running finding bugs and establishing exhaustive proofs.

The secret of success with formal verification of RISC-V processors can be summarised as:

• Think big: use the rigor of formal to establish that implementations conform to the ISA semantics. Exhaustive architectural verification is a great asset.
• Think small: do not forget to deploy a full micro-architectural verification plan. Micro-architecture verification will expose bugs that architecture verification won’t.
• Use proof automation: Use a scalable & predictable ISA formal proof kit that can be used with any formal verification tool.
• Methodology: Cannot say this enough times, but a good, vendor-neutral methodology is a must.

We believe in good methodologies that can make a real difference in your projects. What we show you will work not just for the processors but also for other IP and subsystems on SoCs. We do not like lockups – not in hardware designs and not to lock you into a specific tool either!

RISC-V – you design, we verify using the tool of your choice!