A Holistic View Of RISC-V Verification

Last month, we discussed the growth of the RISC-V open processor ecosystem, the two main organizations driving it, and the role that OneSpin plays. In addition, we have become very active in the RISC-V community and have more than a dozen technical articles published, conference talks presented, and upcoming talks accepted. We tend to focus on the challenges of verifying RISC-V IP cores and system-on-chip (SoC) designs containing these cores. Since I have been on the front line speaking at many of these conferences, I’d like to share my perspective on how the industry’s view of RISC-V verification is growing and evolving.

In the beginning, the whole idea of verification was focused on demonstrating compliance to the RISC-V Instruction Set Architecture (ISA) documents. The ISA is at the heart of the definition for any type of processor design. It defines the instructions, registers, flags, and the other elements that determine the capability of the design. There’s a lot of talk about compliance test suites to check that a RISC-V core matches the ISA. Such test suites are familiar to users of many types of design standards. They are sometimes provided by organizations supporting the standard as an aid to implementation and interoperability. There is clear value in multiple development teams verifying their designs with the same third-party compliance suite.

From our first involvement with RISC-V, we expanded the view of compliance to include the use of formal verification. No simulation test suite, no matter how extensive, can prove compliance to any specification. Proofs are the exclusive domain of formal engines, which can perform exhaustive analysis and show that there is no possible way for a design to violate the behavior rules captured as assertions. That’s exactly where we started: we translated the rules in the ISA specifications into SystemVerilog Assertions and ran formal verification on existing RISC-V cores. We found some very interesting design bugs that had been missed by extensive simulation with large test suites. The value of formal for compliance is clear.

Compliance is only the first step. The RISC-V ISA has many options in terms of instructions, data widths, protection, and more. The assertions must be adaptable to reflect which optional features should be verified depending the configuration of a particular core design. The ISA is extensible as well, permitting custom instructions to be defined. The assertions and the formal methodology must also be extensible, both verifying the added features and proving that the baseline ISA functionality has not been compromised. I’m starting to hear more recognition of these challenges in the RISC-V community, although still focused more on simulation than formal.

I’m not hearing much discussion (yet) on verification of a processor core’s microarchitecture. The RISC-V ISA was explicitly designed to be flexible enough to support a wide range of implementations. Modern processor design leverages multi-level caches, multi-stage pipelines, out-of-order instruction execution, branch prediction, speculative instruction execution, instruction and data pre-fetching, and other advanced techniques. Formal verification is powerful enough to verify the microarchitectures supporting these techniques. In the end, the entire processor core design must be verified, not just the specific features from the ISA that might be captured in a simple checklist-based compliance test suite.

I’ll go further than that: in the end, the entire SoC containing the RISC-V core (or cores) must be verified. It is quite likely that the SoC integration team will want to re-run formal verification on the core as part of the acceptance criteria. In many cases, configuring the core for the ISA options, extending the ISA, and verifying the microarchitecture will be as much the responsibility of the SoC team as the core provider. Once the team is comfortable with the core itself, the engineers need to verify that it has been integrated correctly. Chip-level formal connectivity checking can prove that this integration is correct, far faster and far more completely than any simulation-based approach.

There’s much more to this story. Many RISC-V cores are used in SoCs that have strict requirements for functional safety, security, and trust. For example, it may be necessary to prove that neither the core nor the rest of the chip contains any design vulnerabilities that could be exploited by malicious agents during production use. It may be critical to ensure that no hardware Trojans have been inserted into the core or the SoC at any stage of the development process. Both of these challenges are also well addressed by formal verification, which can prove not only that the design does what it is supposed to do, but also that it does not do what it is not supposed to do.

Although safety, security, and trust are becoming larger concerns in the overall semiconductor industry, so far I am not hearing much discussion on these topics focused on RISC-V. At OneSpin, we’ve been tackling these challenges for some time, both in general as part of our design integrity solution and specifically in the context of RISC-V. We recently authored a white paper on “Assuring the Integrity of RISC-V Cores and SoCs” that covers the full range of topics that I’ve touched on in this post. You can download it at https://www.onespin.com/resources/white-papers/ and I believe that you will find it both educational and useful for developing your own RISC-V verification plans.