Everything you ever wanted to know about RISC-V architectural formal verification
Ashish Darbari is CEO of formal verification consultancy and training provider Axiomise. During the RISC-V Global Forum on September 3, I delivered a talk on the use of formal verification methods to vaccinate designs against catastrophic bugs. Its focus was on the use of formal to establish RISC-V architectural compliance using the formalISA app from Axiomise. Many interesting questions were asked during the talk and also after it. I received numerous emails asking for more information. In this article, I would like to address the most frequently asked of those and discuss the benefits available from formalISA.
- What is architectural verification for processors?
This is the verification of a design entity implemented against architectural requirements or specifications. It is not limited only to microprocessors but can be used for GPUs and networking designs as well.
- What is RISC-V architectural formal verification?
It can be defined as the verification of RISC-V processor implementations against requirements obtained from the published RISC-V standard and formalized in a formal tool that can be run to check if the processor violates the behaviour of the instructions specified in the ISA.
- Is this a kind of compliance testing?
The short answer is, “Yes.” The compliance testing that people in the RISC-V ecosystem commonly refer to is a simulation-based testing of the implementation as opposed to one based on formal methods. In our understanding, this type of test is very popular as most people understand simulation much better than formal methods.
- If it is the same as standard compliance testing, why do it again with formal methods?
Simulation-based testing is inherently limited in its scope as it depends on an input stimulus. In the case of architectural compliance testing, the scope of the work is to check the existence of a simulation trace to validate if a given test based on an instruction can pass or fail on a given implementation. The scope is not to test all combinations of instruction interleaving and register operands. Formal methods-based testing does not rely on any input stimulus; formal tools automatically blast in all possible combinations of input stimulus exercising all combinations by default, provided the formal test bench environment is not over-constrained.
- I heard formal verification can find corner-case bugs but often cannot provide a conclusive outcome due to massive state-space explosion problem.
Yes, in general both observations are true. One reason why formal methods have not seen wider adoption is that when formal checks do not converge, it is often not easy to know why, and certainly not easy to force a convergence. Writing properties in formal languages is often easier than you think; getting them to converge in a formal tool is often harder than you imagine.
- What, in this context, does formalISA do?
formalISA is an APP to carry out automatic, architectural compliance testing in an agile manner using formal verification. Every time, a design change is made, the app can be run push-button to carry out exhaustive testing. formalISA tests exhaustively if a given RTL implementation of a RISC-V core violates the architectural specification of RISC-V, using formal properties coded by Axiomise using the published RISC-V ISA standard. If the property does not fail because there is no bug in the design, we can mathematically prove that there is no bug, using off-the-shelf high-end commercial formal verification tools.
Figure 1. Agile RISC-V formal verification for end-to-end signoff with FormalISA (Axiomise)
- So, what exactly is proven?
formalISA works by modelling at least one check (formal property) for every instruction in the ISA and, through model checking, it examines if that instruction will always work as expected regardless of any micro-architectural optimizations such as pipelining, forwarding, low-power, etc.
- How is this different from simulation-based testing?
The key difference is that all instruction combinations, operands and, inter-leavings are examined at the time of verification for each instruction for which we have a property. During the formal verification run, an instruction being verified will be issued at any time and any number of times. It will be preceded and followed by any number of instructions until the instruction being verified is committed or written back. The check done in formalISA also examines all register operands for all instructions. For LOAD/STORE checks, it even examines all possible variants of these, such as byte, half-word, and word and aligned and misaligned cases for all addressable memory locations. Yes, all addressable memory locations.
- Sounds too good to be true, why should we believe this?
We have several quality markers that reveal the true extent of the verification.
- We carry out design mutation to assess if bugs artificially introduced in the design trigger failures of properties in formalISA.
- We use hooks from different formal tools to assess if there are any over-constraints in the property set.
- We carry out an extensive human review and test multiple RISC-V core implementations to obtain coverage from the field.
- We provide you with coverage metrics to indicate quality. You can visualize these and link them back to the overall verification plan.
- We enable you to reproduce the coverage results across different formal tools, as well as simulators and emulators.
- What is the new coverage solution you are describing today?
Well, if I said to you that formalISA verified all instructions against all combinations, you might ask, “Show me.” You may more specifically ask, “Did we verify the case of an AND instruction being sent ahead of an OR instruction, followed by an ADDI instruction.” We turn such questions into requirements in formalISA that are then verified with a formal verification tool to produce a mathematical proof of correctness for these specific cases. Additionally, the app shows visualizations showing that they can happen. If some of these scenarios cannot happen, we prove mathematically that they are unreachable. The process of going from these questions to results is automated, and all you do is to press the ‘Cover’” button in formalISA.
Figure 2. The formalISA app feature set and context (Axiomise – click to enlarge)
- You say you formally test architectural compliance, build proofs of bug absence, and then demonstrate why these proofs may be real proofs? How long are the runtimes?
That summary is correct. In terms of runtime, once the app is configured to work with your core, it usually takes a few seconds or minutes before the first bugs start to appear. For smaller RISC-V cores such as Ibex and Zero-riscy we were able to prove exhaustive correctness in 24 hours, with 50 per cent of proofs completed in 30 minutes. We found bugs in seconds of wall-clock time. For bigger cores, such as the cv32e40p, the exhaustive proof runtimes are between 24 to 48 hours depending upon the formal verification tool used and the compute cluster on which runs are performed. Bug hunting for bigger cores is also of the order of few seconds to minutes.
- Do we need to be formal verification experts to use formalISA?
No. You do not have to learn anything about formal to take benefit from the app. In fact, you do not write a single line of testbench code, or any code at all. You can, if you want to, add more checks for custom instructions, or we can help you with that. By the way, Axiomise also provides extensive training options to train people in formal verification, so you can learn formal in addition to using the app.
- Does formalISA cover custom instructions?
Not out-of-the-box, as we cannot know which custom instruction a user is going to be interested in. If you do tell us what they are, we can provide you with extensions in our app. One thing we do, of course, is to prove that custom extensions do not break the desired ISA behavior. In the case of Zeroriscy, we showed that they were indeed breaking regular ISA behavior. In the case of OpenHW’s cv32e40p, a project in flight, we can prove exhaustively with higher than 98% proof convergence that the PULP extensions have not broken the regular ISA for a version of that design from July 2020.
- What do we need to use your app?
All you need, is a decent formal verification tool, your RISC-V RTL (in Verilog/VHDL/SystemVerilog) and a coverage specification if you are interested in our coverage analysis. Currently, we support tools from Cadence Design Systems, Mentor, and Synopsys. Our app has also been tested to work with tools from OneSpin Solutions and we are always working on integrating new tools.
- You can find exhaustive proofs, but what about bugs?
When formalISA cannot find proofs, it usually finds failures indicating actual design bugs causing the violation of the ISA. These can be functional bugs, security trojans, deadlocks, livelocks, low-power issues, X-propagation, and functional safety. We have found tons of bugs in different CPU cores, and results are well-documented in several talks, and conference papers.
