By Laurent Arditi, Codasip
During the development of a mid-range complexity RISC-V processor, you can discover hundreds or even thousands of bugs. As you introduce more advanced features, you inadvertently introduce new bugs that vary in complexity. Certain types of bugs are just too complex for simulation to find them. You must therefore augment your RTL verification methods. How do you do that? By adding formal verification. From corner cases to hidden bugs, it allows you to exhaustively explore all states within a reasonable amount of processing time. Let’s have a look in this blog post at how we can raise the quality of RISC-V processors with formal verification.
Why use formal verification for RISC-V?
RISC-V is a modular instruction set architecture for which an architectural test suite can be developed. It is used in simulation-based verification to verify a processor implementation. Similarly, formal methods can be used to verify the architectural compliance of a processor. Why? Because RISC-V is an open standard that everyone can use as a reference model to formally verify an implementation.
Knowing when and how to use formal verification
For all hardware designs, there are good and bad candidates for formal, as well as good and bad times to apply it. RISC-V processors are not different.
Using formal early in a project development, sometimes even before a simulation testbench is ready, is a good approach to flush out obvious bugs. It ensures that the simulation steps we will perform later will not be blocked by these bugs. On the other hand, formal verification is very valuable late in a project to find very nasty corner-case bugs that all other verification methods missed.
Different variants of formal verification can be considered:
- Assertion Based Verification (ABV) using low-level assertions
- End-to-end verification using high-level assertions and often requiring an abstract model of the design.
- Formal flows based on auto-generated assertions are also very useful, such as sequential equivalence checking to verify clock-gating, or X-propagation verification.
- More advanced techniques are also applicable, depending on the block features. For example, for security and functional safety.
But in addition to these, RISC-V processors can be end-to-end verified with an architectural model of the RISC-V ISA. This brings a very high-level of confidence, because all aspects of the processor are implicitly verified, as confirmed with the example bugs we describe in the technical paper we reference and link to at the end of this blog. Applying such a technique cannot be done too early though, because most of the blocks must be ready and connected to each other: instruction fetch, decoder, execution units, load-store interface. Blocks which may not be present, or black-boxed because not mature enough, could include the Memory Management Unit (MMU) and caches.
Formal verification is an essential ‘slice’ of a Swiss cheese model approach
Our processor verification methodology relies on the Swiss cheese model. With this approach, some redundancy is accepted, and even targeted.
Formal is an essential slice of a Swiss cheese model approach for verification
Redundancy is needed
Applying an end-to-end formal approach, as we’ve just described it and as we detail it in our technical paper on efficient verification of RISC-V processors, may seem redundant with a simulation testbench running on the core. And it is! But there are cases where one approach may miss a bug because of missing checkers or input constraints that are too strong (for example if it does not verify in the context of interrupts, or debug commands). And one approach may not be able to find a bug, even if the appropriate checkers and input generators are in place. For simulation, this could be due to a lack of tests. For formal verification, because the state explosion causes the analysis to stop at a bound that is too low.
Targeting corner cases
Formal verification can find most types of bugs, providing that the right assertions are in place, that the input constraints are not too strong, and that appropriate techniques are used to deal with the state explosion (e.g. abstractions). But formal verification is also excellent at finding corner cases because, unlike simulation, it considers them in the same way as basic cases. Bugs that depend on precise timing conditions are usually much easier to find with formal verification than with simulation.
The good and the bad about simulation and formal verification
Formal verification suffers from a bad image when it provides “false failures”. This happens because it works on an “infinity-minus” basis. Indeed, by default, it will reach all states (“infinity”). Some states are not realistic and are discarded by adding “(minus)” constraints. If these constraints are not restrictive enough, they will let false failures appear. If they are too restrictive, they will hide bugs. But there are methods to ensure this is not the case.
Formal verification vs. simulation state exploration – Source: Codasip
On the other hand, simulation works on a “zero-plus” basis. No (“zero”) behaviors except the ones permitted by the testbench will happen (“plus”). “False failures” also appear with simulation (if the testbench permits incorrect input sequences). The problem of hiding bugs also appears with simulation and is more important. If the testbench does not permit a specific valid input sequence, a bug may be missed.
Applying formal verification to Codasip RISC-V cores
Using formal techniques on embedded cores has proven to be successful and efficient. Different types of bugs, from corner cases to hidden bugs, are found when checking ISA compliance.
We detailed our approach to efficiently verify the Codasip L31 embedded core in a dedicated technical paper.
L31 and all other Codasip processors are customizable. Formal verification can play an important role in this field:
- Verify “no-harm”: a customized design must behave the same as the original one when custom extensions are not used.
- Verify customization: enhance the reference model used for ISA compliance to cover the added instructions and registers.
In a future blog post, we will discuss how we have applied the same methodology to application-class processors which are much larger and complex than L31, looking at the challenges we faced and how we overcame them. Stay tuned.