Formal Verification Of RISC-V Cores

RISC-V is hot and stands at the beginning of what may be a major shift in the industry. Even a cursory review of upcoming conferences programs and recent technical articles makes that clear. While it is still early in the evolution of the processor architecture, there is certainly the potential that RISC-V will be a game-changer in the IP and semiconductor industry. As “a free and open ISA enabling a new era of processor innovation through open standard collaboration,” it directly challenges several well-established processor families. This definition comes from the RISC-V Foundation, which assumed support and evolution of RISC-V after the original development in the EECS Department at the University of California, Berkeley.

The RISC-V instruction set architecture (ISA) was designed with a large amount of configurability in terms of optional extensions such as IEEE 754-2008 floating-point support. It is not architected towards specific technologies or microarchitecture styles, thus allowing for a wide variety of implementations currently available as open-source cores. Anyone can design a core or use one in a system-on-chip (SoC) project. It is precisely this openness and wide appeal that makes thorough verification of a RISC-V core essential. With traditional processor families, there are only one or two suppliers who have been providing core and chips for many years. The suppliers are expected to verify their products, and it is unusual for SoC designers to feel that they must re-verify the cores they license.

In contrast, there are already multiple parties offering RISC-V cores and this number will grow significantly over the next few years. There is no one central team designing and verifying these cores. For the RISC-V ecosystem to thrive, core suppliers need an independent verification solution to ensure that their designs are compatible with one another and compliant with the ISA specification. Thorough verification is essential to compete successfully against the established processor families with their years of extensive validation and silicon implementation. Similarly, SoC developers must ensure that the cores they license are fully verified and ISA-compliant.

Beyond functional correctness, both core vendors and users face challenges of safety, security, and trust. Many RISC-V cores will be designed into products with strict functional safety requirements. The designs must include safety logic to handle random errors in the field, such as alpha particle hits. Standards such as ISO 26262 for automotive electronics require verification of the safety logic and calculation of the probability of failure.

In addition, many RISC-V cores will be used in applications that must be secure from adversary attacks. Core (and SoC) designs must be analyzed for security vulnerabilities that could be exploited by someone wishing to take control of the system. The consequences for such applications as autonomous vehicles, nuclear power plants, and military/aerospace could be dire indeed. Adversary attacks may be aided by hardware Trojans or other malicious logic inserted into the core (or SoC) by rogue individuals or tools in the design chain. The verification process must include detection of any such breaches of trust.

All these challenges lead to one inescapable conclusion: RISC-V cores must be formally verified. Formal tools can guarantee that a core design implements the ISA exactly, missing no required functionality while not inserting any deliberate or unintended behavior that violates the ISA. This includes screening the design for security vulnerabilities and detecting any hardware Trojans. Only formal tools 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. Formal applications (apps) can also analyze the core design for functional safety and calculate the fault and failure metrics required by safety standards.

For the growth of the RISC-V ecosystem, it is best if formal verification can be performed by third-party tools and IP. This allows multiple core vendors to verify with the same solution, establishing it as a de facto standard. SoC providers licensing open-source cores can use the same tools and IP to screen potential cores and double-check compliance as well as adherence to safety, security, and trust requirements. With these goals in mind, OneSpin recently introduced our RISC-V Integrity Verification Solution.

Our solution formalizes the RISC-V ISA in a set of SystemVerilog Assertions (SVA). These assertions define the results for each instruction and cover execution from instruction decode to completion. A finite number of assertions can cover any arbitrarily long instruction sequence in any RISC-V implementation. This approach enables 100% formal proof for implementation of all instructions against the ISA specification and guarantees that a core is fully compliant. It also detects any extra functionality beyond the ISA specification, formally verifying trust that the core contains no hardware Trojans or other unintended functionality. The solution is being delivered as a series of apps to make use as pushbutton as possible. It is flexible enough to verify user-added custom extensions while ensuring that compliance is not compromised.

We have already used this solution to verify existing RISC-V implementations and have found some interesting design bugs. We will present papers at several upcoming events, including the Government Microcircuit Applications & Critical Technology Conference (GOMACTech) and the RISC-V Workshop in Taiwan, and will share presentations, papers, and results when we can. In the meantime, contact us if you are developing or considering licensing a RISC-V core. We look forward to helping to create a rich ecosystem.