Formal-based RISC-V processor verification gets deeper than simulation

The flexibility of RISC-V processor IP allows much freedom to meet specific requirements – but it also opens the potential for many bugs created during the design process. Advanced processor features are especially prone to errors, increasing the difficulty and time needed for thorough verification. Born out of necessity, Codasip has pioneered a formal-based RISC-V processor verification process, bringing higher-level simulation and formal verification methods to efficiently verify core modifications, as shared in their latest technical paper.

Digital logic simulation in complexity only scratches the surface

Simulation seems like an ideal solution for digital logic, and it does shake out many bugs in a first pass that runs quickly. It’s logical to think that by simulating functional blocks individually, combining them into a complete design, and simulating it again, coverage would be pretty good.

As it turns out, pretty good is not nearly good enough. Simulation is only as good as the models and conditions applied – and in a complex RISC-V setting, uncertainty prevails. What software is running, which asynchronous events occur, and how the processor transitions from state to state in every possible scenario can be extremely time-consuming to model for simulation. If a simulator stumbles on a problematic corner case, it may only be sheer luck.

L31 block diagram. Source: Codasip

A good example is a branch predictor, such as the block shown in the Codasip L31 RISC-V processor IP. A myriad of states need to be set up to simulate completely how the branch predictor behaves in all cases of caching and pipeline execution.

Codasip uses the word “impossible,” but covering all state space in simulation is impractical, given finite engineering resources and time limits. They see simulation as an essential but not a standalone tool in the formal-based RISC-V processor verification process.

Combining techniques for better coverage in less time

Codasip outlines several advantages of applying formal verification as a complement to simulation.

• Design behaviors are specified using assertions. Assertions are used both in simulation and in formal. In formal, however, a mathematical analysis can sometimes uncover corner cases that the random walk of simulation has a low probability of hitting.
• Formal can also tackle non-functional verification such as clock-gating, X-propagation, and clock domain crossing.
• Formal verification handles investigations where debugging information is limited, providing a way to classify and identify bugs for detailed analysis.

Manually writing assertions remains a problem, especially if one has to go back to write all the assertions for a complex design from scratch. The nice thing about RISC-V being an open architecture is many people are looking at the challenges, including verification. If a team could build on existing assertions from the RISC-V community and incrementally define new ones for their adjustments and additions, it would speed up formal verification.

Codasip has gone one step further, grabbing a golden RISC-V instance. The Siemens OneSpin Processor Verification App consists of a single-cycle execution model of the RISC-V ISA and a set of template assertions to check a design against this model. Codasip has instantiated this model together with the design and specialized the assertions to “connect” both, taking care of the pipeline and other specificities.

End-to-end verification flow for the 3-stage L31 core (when the verified instruction I is neither stalled nor flushed). Source: Codasip.

Automatically is the operative word. In this approach, users can specify RISC-V parameters and extensions, extract design data, add customizations like new instructions, and move to verification without spending time writing assertions manually or trying to split the design into smaller chunks. Codasip has demonstrated verification of the full L31 at once in this approach.

Cutting formal-based RISC-V processor verification down to two hours

The punchline of this technical paper is Codasip reduced the time to verify the L31 core from thousands of simulation hours – assuming that a simulation scenario could even be generated, what could be person-years of effort – to full proof in two hours of run time after setup.

And they didn’t skip steps. They outline three complex corner cases where the approach spotted bugs they didn’t anticipate from the simulation. A branch predictor corruption arose when an undefined instruction generated an exception. Delays and pipeline stalls in the right combination caused multiple executions of the same instruction. A legal FENCE.I instruction got incorrectly marked as illegal.

Codasip uncovered 15 bugs in the formal-based RISC-V processor verification effort for the L31 that their simulations and other steps missed. Design quality increased, and the process laid the path to faster verification of future customizations for their customers.

To get the whole story, download the Codasip technical paper (registration access for full text):

A formal-based approach for efficient RISC-V processor verification