The verification of modern-day processors is a non-trivial exercise, and RISC-V® is no exception. In this article, we present a formal verification methodology for verifying a family of RISC-V® “low-power” processors. Our methodology is both new and unique in the way we address the challenges of verification going beyond just functional verification. We focus on architectural verification, lockstep verification (part of functional safety), X-issues due to low-power design, and security. Our approach finds bugs in previously verified and taped-out cores as well as establish bug absence through exhaustive proofs of correctness for end-to-end checks.
At Axiomise, we have designed a new RISC-V® ISA Formal Proof Kit® covering the RV32IC subset of the RISC-V® ISA (so far) to address the problem of architectural verification. We find architectural bugs – ISA instructions not executed in the micro architecture but also prove bug absence exhaustively when an ISA has been implemented correctly. Using Questa® PropCheck, so far, we found several bugs covering architectural violations, X-propagation, and potential security vulnerability on zeroriscy besides seeing multiple failures with deadlock checks. On ibex, a new 32-bit core under development, so far, we have discovered several failures on architectural checks and eight violations of lockstep verification, and X-issues. Our work defines a new milestone in exhaustive formal verification of microprocessors as it proposes a new way of addressing several verification challenges by combining our new formal tool vendor-neutral ISA Formal Proof Kit® along with lockstep verification, deadlock checking, X-checking, and security analysis.
Our proof kit can be used by any designer or verification engineer using any formal verification tool of their choice. Within minutes of setup, they will be up and running finding bugs as well as having proofs of bug absence as well as establishing ISA compliance. All results reported in this article have been communicated to the PULP platform team and the DV engineers at lowRISC, Cambridge who are designing ibex.
Functional verification of processors has been a known challenge, but with the advent of open-source RISC-V® a new wave of computing has ushered. Not only universities, but several big corporations have accelerated the design of new RISC-V® cores. The range of applications is varied from the smallest 2-stage, pipelined low-power CPUs to bigger out-of-order superscalar designs. One thing, however, is common – verification remains a challenge. Despite all the excitement on new micro-architectural variations from chip vendors, one still needs to demonstrate that the design works as intended. Because the ISA itself is free and open-sourced and in many cases, the design implementations are also open-source, it has become easier for formal verification evangelists to investigate whether these designs do as they say on the tin.
The RISC-V® design eco-system is also spanning a new verification eco-system, especially for formal verification with several players now exercising formal verification ranging from theorem proving to property checking based solutions. Whereas, theorem proving based verification doesn’t suffer from the state-space explosion challenge that formal property checking based verification has, the learning curve with theorem proving is significant and is not something widely adopted in the industry at large. Another major weakness of theorem proving is that while one can construct proofs of correctness by the safe and systematic application of inference rules in a theorem prover, one cannot ever obtain a counter-example when there is a bug in the implementation or specification. You almost need a mathematical wizard to discover the problems as part of the proof building process!
Formal property checking aka model checking is an automated formal verification technology suited for finding bugs as well as building proofs with several established commercial vendors offering formal tools with a very wide base of users in the industry. The main challenge is in understanding how to develop formal properties that can generate predictable & scalable results across all the formal tools.
In this article, we present a formal verification methodology that provides a tool vendor-agnostic solution for the formal verification of RISC-V® processors requiring the user to have no formal verification expertise. With a simple set up, the user can orchestrate a range of verification checks on their RISC-V® designs without having to write a single line of the verification code. As our solution is designed using the non-proprietary SystemVerilog Assertions (SVA) supported by all the tool vendors, it makes it easier for designers and verification engineers in the industry to understand our solution, review it, and expand on it if they choose to. Using our kit, users get the results verifying beyond doubt that their design will work as intended against the architectural requirements of the RISC-V® ISA. Our methodology also provides checks for finding deadlocks in the design as well as probing the design for any X-related issues typical of low-power designs, while at the same time finding dynamic power issues and discovering any potential security holes as well as establishing baseline compliance for lockstep verification — a requirement for automotive processors.
THE AXIOMISE METHODOLOGY
Our formal verification methodology is built around addressing the architectural verification problem for RISC-V® as well as all the necessary micro-architectural challenges. The Axiomise ISA Formal Proof Kit® is designed using the RISC-V® ISA specification and is customized for every new implementation within minutes. The customized kit contains SVA properties that are then used to verify the specific RISC-V® implementation using the best-in-class formal verification tools such as Questa® PropCheck as shown in Figure 1.
Figure 1 - Our architectural proof kit finds bugs and proofs using Questa® PropCheck within minutes!
We designed several automated formal verification techniques that were used to address the many challenges of (1) architectural verification, (2) X-propagation, (3) deadlock verification, (4) lock-step verification, (5) security, and (6) dynamic power. The key aspects of our methodology are outlined here.
We considered each instruction as a dynamic transaction in hardware with a defined starting point (when it is issued) and an endpoint (when it completes). Mostly, we had one assertion per instruction check (with some exceptions such as JAL and JALR, and LOAD/STORES). The basic methodology relied on capturing the start, and the endpoint of each instruction by sampling expected values and actual value in testbench registers and controlling the sampling through the start point and endpoint. This way we allowed complete freedom to the CPU to issue whatever instruction it wanted to and when it wanted to, but our modeling code will sample in the start point, endpoint, expected value, and actual value whenever an instruction was detected to have been issued and completed. This approach allowed a whole stream of instructions to be in flight at any time during our checking, allowing all kinds of permutations of instructions to be in flight before and after the one we are checking at any point of time. The basic code for each check states that “when this instruction is issued, then sometime later we expect to see the results of its execution” having a cause-effect relationship captured in the assertion.
Consider the following example of checking a BEQ instruction in the RISC-V® ISA. The BEQ instruction specification states that if the values in register rs1 and rs2 are equal when a branch-if-equal (BEQ) is detected then the next state of the program counter (PC) will be the branch address. It is modeled in our proof kit through the following SVA.
assert property ($rose(is_a_beq) && (axiomise_REG_rs1==axiomise_REG_rs2)
|-> ## `REG_DELAY axiomise_n_pc==branch_addr);
Note the use of
$rose. It allows for efficient simulation runs for the same assertion and the use of the macro `REG_DELAY, which specifies for a given implementation how long will it before the PC will be updated. Also, note the use of axiomise* prefix, which is used to distinguish the namespace of testbench signals from design signals. The following expressions in Verilog define the signals used in the property.
assign branch_addr = axiomise_decoded_pc +
assign is_a_branch = axiomise_instr[6:0] == AXIOMISE_OPCODE_BRANCH;
assign is_a_beq = is_a_branch && axiomise_instr[14:12]==3'b000;
We ensured that we didn’t make comparisons directly with the branch address signal in the design, but instead had an expected model of it in the testbench derived from the ISA.
We wrote checks to verify that none of the design signals were unknown. Rather than writing these checks for all design signals, we wrote them only for signals on the interfaces of the design units. Our view was that if an X cannot reach the interface of a module, it cannot reach the output either, though we did have checks on the output pins as well. One important point on methodology – in formal tools, the checking on a 3-valued domain is not turned on by default, so one must explicitly turn-on the X-checking. The treatment of Xs on primary inputs is also different between different tools. So extra care is needed to enforce constraints on primary inputs to force non-X values on them, or else we get spurious failure. If we drive X on inputs, we see X-propagating on the outputs.
For checking deadlocks, we created a library of assertion checks for each single-bit signal in the design (including wires, registers and control states in FSM) and asked the question if they would toggle infinitely often.
For security, we didn’t have detailed specifications, so in the absence of such detailed requirements, we explored potential security vulnerabilities by asking questions on design-build quality and architectural compliance. If the design-build quality is robust, it means it is immune to certain malicious code insertions (trojans), and additionally, if the design can provably demonstrate the compliance against the ISA, then it is secure with respect to the ISA. These two analyses do not mean that the design is 100% secure – it only means it is secure against a subset of vulnerabilities.
For formally verifying lockstep behavior we created two copies of the cores and tied their inputs together. We then instrumented checks to verify if the outputs of the cores always remain equal. This approach is enough to catch all lockstep bugs.
We investigated a class of failures related to the stability of signals on the interface of the core. We wanted to check if the payload remained stable when it should and doesn’t cause any unnecessary toggle of flops resulting in dynamic power consumption.
In the first instance, we started verifying the well-known 32-bit processor zeroriscy from the PULP platform group, which had been previously verified and taped-out at 40nm in ASIC and FPGA. Within the first six weeks, we found several deadlock bugs as well as exhaustively proved end-to-end functional properties on ISA. A lot of the time spent in this initial phase was spent in building our ISA Formal Proof Kit® and understanding/debugging failures. The actual run-time for the checks was a matter of hours but debugging each failure and classifying it as a genuine design bug took time.
Deadlock: Most of the bugs were down to a buggy debug unit. The debug unit caused 77 deadlock properties to fail out of the 134 checks suggesting a problem. We reported these to the designers, but as the designers already know that there are problems with the debug, they haven’t investigated any of these failures. We have done an initial investigation on a few of these and found that if the incoming debug request arrived more than once or if there was a debug resume event after the first debug request was initiated, it causes several design signals to lockup.
Architectural & Security: We found an interesting bug through an architectural check on the LOAD instruction. This bug not only causes problems with functional correctness of the LOAD execution but also exposes a potential security vulnerability.
Dynamic Power: Another class of bugs we found were on the instruction and data memory side where stability checks had failed. The core sends out a valid request (*req_o) and when an incoming grant (*gnt_i) arrives the address and other related payloads such as write data, and byte-enable is transferred across the memory interface. What we noted was that if there is no incoming grant, but there is a valid outgoing request (req_o==1’b1), the address, write data and byte-enable was not stable. Our initial response was that these are functional bugs. Designers, however, believed that this is not a real design issue and to save the area for a low-power processor, not using registers is a small sacrifice to make. We found that the stability problem does not affect the actual execution of any instruction, so yes, it may not be a functional issue. However, we believe that as addresses, write data, and byte-enable toggle, they burn dynamic power. If for example, the incoming grant is delayed for several cycles on the interface, these signals will continue to toggle burning power – not ideal for a low-power processor. When we conveyed this to the designers, they seem more persuaded to fix this issue.
X-Propagation: Other bugs that we found were about redundant undriven logic (causing X issues), redundant, unused signals with constant values, and a potential security vulnerability found due to a failing check on the execution of the LOAD instruction.
Lockstep: We didn’t find any bugs with lockstep verification (provided we turn-off the incoming debug_req_i pin) and were able to exhaustively prove that two copies of the zeroriscy core would run in lockstep.
Deadlock: For deadlock checking, we found 28 properties that failed the deadlock check, while 40 were proven exhaustively. We didn’t investigate all the 28 failures but certainly investigated a few. The tools show us a scenario where it is possible to drive an X on the instruction bus infinitely often causing some of the signals to be stuck at 1 or 0. For example, a 32-bit X value can be assigned a combination of 0s and 1s so that it causes the opcode to remain a STORE (or LOAD) forever, causing a data write signal to remain high or low forever. Although we could call this scenario somewhat pathological, it is certainly possible.
Architectural: For ibex, the results are different from zeroriscy, and that is to be expected as the core is still under development, although ibex has been cloned from zeroriscy. We wanted to test our ISA Formal Proof Kit® initially on ibex, so we started initially with just architectural testing in mind. It took 30 minutes to set up our proof kit. Our initial set up was to turn off the debug completely (disable the incoming debug_req_i pin) as we thought ibex was a clone of zeroriscy with now a known debug issue it would be wise to constrain the debug interface off. Once the debug was disabled, we started getting exhaustive proofs of correctness for all the ISA checks in our proof kit. 47% of these were proven in about 25 minutes of wall clock time, further 33% in 2 hours, and the last 20% in about 24 hours.
However, once we enable the debug_req_i pin to go high by disabling our constraints on the debug interface, we noticed that almost all the ISA checks (about 57 of our ISA properties) failed. It turned out that almost all of them are down to one major bug in the design related to a controller state machine. When the state machine was in the DECODE state and an input debug request was made in that cycle; it will end up failing the execution of the instruction that was in flight (being decoded and executed), as shown in Figure 2.
Figure 2 - BEQ failure on ibex, with a bug that affects nearly every instruction in ibex
X-Propagation: We tested ibex for X-propagation and found eight bugs, regardless of whether the debug interface is enabled or not. It means that the processor will exhibit correct functionality for all instructions we tested when debug is disabled, but it will show reachable X issue for some of the outputs of the core. When a design runs in silicon, there is no X, only 0s and 1s. The X that cause differences in lockstep behavior does not cause any problems during the ISA execution. It is because an X is treated like a Boolean during a normal formal verification run, allowing for the X to be replaced by 0 and 1.
Lockstep: We found eight violations for lockstep. The root cause of this is X-assignments. If two cores are configured to run in lockstep, they exhibit different I/O behavior, as the X in the design takes on the Boolean value 0 in one copy of the design and 1 in the other copy.
Security: It is well-known that if an X is reachable at the outputs, it can cause information leakage if an attacker can observe the primary inputs. What we see with the X-failures and lockstep analysis – visible Xs and lockstep differences on outputs exposes potential security vulnerabilities with ibex. Our deadlock analysis revealed that due to the X-problem, some of the outputs and internal state could be deadlocked; this happened due to the Xs on the instruction bus. Though it seems pathological at first, we believe an attacker can make use of these input scenarios to cause the core to lockup.
Dynamic Power: The dynamic power issue we noted on zeroriscy exists on ibex as well at the time of testing it.
Our reusable methodology provides unique insights on verifying a family of RISC-V® processors, some of whom have been previously verified and taped-out. We found bugs (including corner case ones) and proved conclusive bug absence when we fixed bugs. Although we used Questa® Formal for most of our work, our solution is completely vendor agnostic, can be run with any formal tool. We have used the well-known general-purpose languages – Verilog and SVA supported by all the formal tool vendors. We believe this is a significant milestone – industry’s first vendor-neutral solution that is able to prove end-to-end functional correctness and finding bugs in 32-bit processors using vendor-neutral formal tools, using our automated architectural (ISA) Formal Proof Kit® augmented with other important verification tasks such as deadlock and lockstep verification and X-propagation. More details are available from the RISC-V® YouTube® channel. All results reported in this article have been communicated to the PULP platform team and the DV engineers at lowRISC, Cambridge who are designing ibex.
Back to Top