Technical White Paper: Using Advanced Formal Verification Tools to Efficiently Complete RISC-V Processor Verification

Technical White Paper

Using advanced formal verification tools to efficiently complete RISC-V processor verification

In our previous technical white paper , "Efficient RISC-V Processor Verification Method Based on Formal Verification" , we introduced a formal verification-based, easy-to-mobile RISC-V processor verification program using Codasip L31, a 32-bit mid-range embedded RISC-V processor core for microcontroller applications. Together with the RISC-V ISA golden model and the automatically generated checks for RISC-V compliance, it shows how to effectively locate vulnerabilities that cannot be simulated.

The openness of RISC-V allows the architecture and microarchitecture based on the RISC-V core to be customized and extended to meet specific needs. This desire for design freedom is also shifting the responsibility of the verification part to the growing developer community. However, as more and more companies and developers transform to RISC-V, everyone finds that processor verification is not an easy task. The new features brought by the new standard due to its novelty and flexibility can inadvertently create specification and design loopholes, so processor verification is a very important part of the processor development process.

During the development of a RISC-V processor core of moderate complexity, hundreds or even thousands of bugs are discovered. As more advanced features are introduced, new bugs of varying complexity are introduced. Some types of bugs are so complex that they cannot be found even in simulation. Therefore, RTL verification methods must be enabled by adding formal verification. From extreme bugs to hidden bugs, formal verification allows you to exhaustively explore all states within a reasonable processing time.

In this article, we will take the Siemens EDA processor verification application as an example, combined with the features provided by Codasip L31, a popular RISC-V processor IP, to introduce a specific method of using advanced EDA tools to verify the processor in actual design work. This verification method achieves a high degree of automation by providing a set of dedicated assertion templates for each instruction, eliminating the need for manual design, thereby improving the work efficiency of the formal verification team.

How to use Siemens EDA processors to verify your application

Before we use the tool, we need to set up formal verification for the Codasip L31 RISC-V core. This setup is similar to the setup used to formally verify standard assertions using assertion-based verification (ABV) methods with abstractions, constraints, etc.

The tool allows to verify specific categories of directives and enable or disable certain resource checks. With this tool, our verification can start from a simplified space, which includes:

• Only the simplest instructions, such as only integer operations and logical instructions.

• Only the simplest (but most important) checks are included. For example, updates of general purpose registers. Other checks that can be added later refer to updates of system registers (CSR) or program counter (PC) and memory accesses.

• Main-only mode: no interrupts, aborts, exceptions, or debug access.

These three orthogonal constraints can be relaxed one by one depending on the criticality of the microarchitectural features. Classical formal verification techniques can be used to help obtain the results asserted by the checker: abstraction, design reduction, case splitting, invariant generation, semi-formal bug hunting, etc.

result

This formal-based approach allowed us to find corner cases and provide insights to improve our simulation and testbench. This verification work was done near the end of the project after other simulation-based verification flows had run without finding new vulnerabilities, allowing us to find real and important vulnerabilities.

We can focus on three vulnerabilities in particular, which were found in the Siemens EDA processor verification application for L31. Here is how to find and fix these three vulnerabilities:

1. The branch predictor is broken

With this vulnerability, returning to a PC address that previously held a jump/branch instruction causes the branch predictor to incorrectly predict a jump to another address. This edge case is found when the following conditions are met:

Self-modifying code

An extremely rare version of this vulnerability also occurs when an undefined instruction is added (a new instruction exception):

The vulnerability was discovered by an assertion checking the PC value, which resulted in a branch instruction being incorrectly executed, leading to incorrect code execution. This vulnerability was fixed by properly clearing the buffered data for branch prediction and pipeline.

Finding this vulnerability using the Siemens EDA Processor Verification Application takes 8 cycles and 15 minutes of runtime. Reproducing the vulnerability in simulation requires a random generator that supports self-modifying code that can return exactly the same address and modify that address from a branch to another type of instruction. In other words, a random generator cannot do this. Only a directed sequence that knows the details of the vulnerability can do it.

2. Multiple executions of the same instruction

With this bug, NPC (Next PC) unit stalls occur, which causes the same address to be fetched multiple times. Each instruction is executed and retired.

This extreme case occurs when the following conditions are met:

• The core is configured with TCM.

• Specific delays can be seen on the extraction bus.

• Specific pauses can be seen within the pipeline.

The vulnerability directly causes a stall in the rest of the pipeline that is not handled correctly, resulting in multiple executions of the same instruction. This vulnerability can be fixed by correctly handling stalls in the rest of the pipeline.

Finding this vulnerability using the Siemens EDA Processor Verification Application takes 5 cycles and 10 minutes of runtime. Reproducing it in simulation requires a random pattern of random delays and pauses, but also requires a fair amount of "luck" to reproduce this particular sequence.

3. Legal FENCE.I instructions are considered illegal

With this vulnerability, memory barriers are handled by the CSR unit. If the instruction bits (bits [31:20]) corresponding to the CSR address bits of a CSR operation match certain CSR registers (e.g., debug, counters), the instruction may be incorrectly marked as illegal.

This extreme case is found when the following conditions are met:

• There are random bits in imm[11:0]/rs1/rd.

• These bits match some other illegal instructions.

The direct consequence of this vulnerability is that an illegal instruction exception is raised incorrectly. This vulnerability can be fixed by correctly decoding the complete instruction in each part of the pipeline.

Finding this vulnerability using the Siemens EDA Processor Verification Application took only 8 cycles and 5 minutes of runtime. Because the compiler only creates the simplest binary encoding implementation, it is difficult to reproduce the vulnerability in simulation. It requires a special compiler to create variants of the legitimate encoding, or special directed testing with various encodings.

Advantages/Conclusions Found

Applying this approach can improve the productivity of the verification team. Increase efficiency during critical phases of the project. While building the right setup takes effort in the beginning, progress accelerates as we add new instruction categories and new checkers. This "sweet spot" is where we find most issues, and things start to slow down as constraints are relaxed to allow the tool to explore more esoteric modes of operation.

Figure 1. The sweet spot for verifying the best efficiency of the L31 RISC-V core (Source: Codasip)

Overall, using the Siemens EDA Processor Verification Application is quite efficient because the overall effort required to verify the entire CPU is much lower than the effort required to achieve similar verification quality manually. Of the total 30 vulnerabilities, 15 were found through formal verification.

Table 1 Simulation vs Formal Verification

When combined together to achieve a high level of quality, simulation and formal verification are extremely powerful and allow us to foster a virtuous cycle of verification improvements.

Figure 2 Achieving first-class quality through continuous improvement (Source: Codasip)

The solution was proven to work on the Codasip L31, a 3-stage pipeline microcontroller, and is now deployed in Codasip's next-generation RISC-V cores, including embedded and application cores. With the knowledge accumulated from verifying applications using Siemens EDA processors on the L31, the effort required to establish a robust environment can be reduced even if the application core is more complex. Next steps for Codasip include further research on how the tool can be applied to superscalar and out-of-order cores, as well as support for new RISC-V extensions.

Additional reading

• Efficient Verification of RISC-V Processors - Technical White Paper:

• Building a Swiss Cheese Model Approach for Processor Verification - Blog Post:

This article is excerpted from the white paper "Form-based Efficient RISC-V Processor Verification Methodology - Formal Verification", published by Codasip, a leading global RISC-V supplier and processor solution leader headquartered in Europe, whose processor IP is currently deployed in billions of chips . Codasip provides customized computing to customers by combining the open RISC-V ISA, Codasip Studio processor design automation tool and high-quality processor IP. This innovative approach enables easy customization and differentiated design, thereby developing high-performance, game-changing products and achieving true transformation. If you want to get the full version of this white paper, you can visit the Codasip Chinese website or follow the company's WeChat official account.