As processor architecture and design development becomes completely liberated with open-source RISC-V instruction set architecture (ISA), the race to get RISC-V silicon in our hands has increased massively. We have no doubt that in next 5 years, we will see RISC-V based laptops and desktops in the market. But would these processors be of high quality? Would any one of them have a glitch like the famous Intel FDIV bug from the era of mid 90s? Have we learnt what it takes to robustly verify these processors for safety-critical domains, security and functionality?
In this article, we would like to explore these questions from the perspective of open-source RISC-V architecture and will take a look at verification trends and what makes processor verification hard and how it can be made easier with the use of formal methods in particular using the fully automated vendor-neutral formal formalISA® app from Axiomise in combination with the JasperGold® Formal Verification Platform from Cadence. We also discuss a new automated debug, analysis and reporting solution (i-RADARTM) from Axiomise that allows accelerated debug and reporting.
Why is processor verification hard?
Designers are turning to the RISC-V ISA to create many different power/performance-optimized processor architectures for a wide range of devices, from mobile and IoT-Edge all the way to high-end servers. However, each different implementation must execute every single instruction in the ISA with complete functional consistency. This consistent functionality must be fully verified for the wide range of unknown datasets the devices could encounter, which is challenging for traditional verification methods to achieve.
Additionally, pipelined architectures with complex multi-threading and out-of-order execution pose significant challenges for verification. Common verification bugs not easily caught in simulation are due to concurrency, stalling, interrupts, race-conditions, arbitration, and memory ordering. Debug introduces a significant additional challenge and ensuring it is not creating any security leaks poses another headache for designers.
What is the industry doing about it?
Simulation-based verification using UVM relies heavily on stimulus randomization to kick-off verification and uses functional coverage to sign-off. With the complexity and size of the processors, it is not easy to model stimulus that can reach the deep wilderness of micro-architectural state-machine interactions that would be capable of exposing all the bugs in the processor. Functional coverage relies heavily on the very same stimulus and randomization that means your sign-off capabilities are limited – never mind that none of this is exhaustive. Bringing up the UVM infrastructure in terms of human effort to the point that it can yield acceptable functional coverage yield is legendary. Harry Foster’s Wilson research report points out that processor design houses hire 5 verification engineers for every designer, and yet in the very same report where simulation is clearly shown to be the king, points out that 68% of ASICs and 83% of FPGAs fail in their first spin.
So, while it is totally understandable that most of the industry understands simulation-based verification and it is always easy to plod along with what you know best, the complexity of verification challenges and inadequacies of UVM-based verification has forced the industry to adopt formal – and the owners of the established ISAs like Arm and Intel have led the way. These industry leaders knew that consistent behavior of the ISA, across myriad implementation architectures, was vital for a software ecosystem to develop around the ISA. With no single entity responsible for its integrity, ISA verification is even more important for companies investing their resources in RISC-V. Furthermore, if history is anything to learn from, then the Intel FDIV and the more recent family of security flaws – offspring of meltdown and spectre should be an eye opener. Your silicon must work the very first time you bring it up and must always work – many years later – as expected without locking up, and without getting exposed to hackers.
Formal verification: The only gateway for providing exhaustive guarantees
For industry to achieve high-quality verification at reduced cost – formal verification is the only way forward. Writing formal properties takes a fraction of time compared to instrumenting UVM testbenches. Running these formal properties takes even less time. In the last two years, it has repeatedly been shown how Axiomise formal verification solutions prove 27,000+ properties exhaustively on processors such as cv32e40p, ibex, 0riscy and now more recently WARP-V family of processors with six stage in-order pipelines within a few hours.
Yes, there is a human effort needed to code formal properties and it does need experience to know what to code, and how to code the properties efficiently. This is exactly why Axiomise teach formal verification courses – both online self-paced as well as instructor-led.
Axiomise partners with Cadence to offer these courses for customers using the industry-leading JasperGold formal verification platform. However, when there aren’t the resources to learn formal, and deliver high-quality formally verified designs to customers in the time required, then one can buy Axiomise off-the-shelf formal verification solution for RISC-V.
WARP-V Case Study
WARP-V is a brilliant design from Steve Hoover CEO, of RedWood EDA to promote TL-Verilog – a new transactional flavour of Verilog designed to make designers efficient in bringing up designs with fewer bugs and ultimately build RTL correct-by-construction. The beauty of this infrastructure is the ease with which you can design multi-stage pipelined designs with the same canonical high-level TL Verilog model. In fact, we can also extract Verilog out of it and the extracted Verilog is still very much readable.
Formal verification of WARP-V
When Steve designed the WARP-V processor, there were numerous articles written to demonstrate these concepts including many on how Steve and Ákos Hadnagy formally verified the processor. Steve had used the open-source solution. When Steve announced that it was used to verify WARP-V everyone including me trusted that it would be bug-free.
WARP-V formal verification using formalISA®
So, when Shivani Shah started the work with Axiomise on formally verifying the WARP-V processors using the Axiomise’s formalISA solution, we didn’t think at the time we will find any bugs. Why would we find bugs when they already used formal verification? Right?
So, it came to us as real surprise when we started to see property failures within a few minutes of integrating the WARP-V core in our app. The initial instinct was that our verification solution may have an issue, or in fact that the integration was not correct, and mapping files used to configure the app had discrepancy.
When Shivani dug deeper and opened tickets and started to inquire with Steve, it turned out that the issues we found were indeed true design bugs. The initial set of these bugs were all down to how the semantics of branch instructions were interpreted by us in formalISA (in accordance with the RISC-V ISA spec) and how Steve’s design model and the open-source RISC-V formal test bench that happen to agree with each other were not in compliance with the architectural spec. It meant that the WARP-V processors would work as processors but will break the requirements posed by the RISC-V ISA. You can most certainly not expect the software to work as the compiler would behave one way and the hardware another. We scheduled face-to-face meetings with Steve and Akos and both confirmed that these were design bugs.
When we asked Steve as to why they had these bugs in the first place, Steve remarked that at the time of the design he was not clear about some aspects of the specifications, and he relied on using the interpretation of the formal semantics of the open-source RISC-V formal. It is not surprising that Steve didn’t find the bugs himself, but what was surprising was that the formal model used by them had this bug especially as that model is also used by other designers building RISC-V processors.
So, a note of caution: If you’ve been using the same semantics of branch instructions in your core that the open-source formal solution does, chances are you have the same bug in your core!
When Shivani expanded her work and started adding M-extensions to our app, even more bugs were picked up. The full list can be found from our Github page.
Previous verification work carried out with formalISA®
We used our app before to verify other processors. In the RISC-V summit 2019, we outlined our verification methodology providing details of how we start the verification and how checks are modelled in formal. We provided results on verifying 0riscy, and ibex. Although both were small, embedded designs with 2-stage pipelines and 0riscy was already verified before and was in silicon when we started the verification, we found over 65 bugs including deadlocks. Ibex was a near clone of 0riscy. When its development forked out, we looked at it in the early stages and caught several corner-case bugs affecting numerous instructions.
In 2020, we worked with the OpenHW group to formally verify the cv32e40p core. We were able to verify nearly 27,000 properties including extensive coverage in a matter of hours. These results have been presented in the RISC-V summit, 2020 as well as in the webinar in March 2021. We caught several bugs including an inconsistency issue in the published RISC-V ISA specification.
Example of a specification bug caught by formalISA
Fig 1. Inconsistency bug caught by formalISA app.
In the published RISC-V ISA specification v2.2, on page 30 it requires the generation of illegal instruction exception for the shift instructions SLLI, SRLI and SRAI if imm[5] is not equal to 0. However, it is not possible for imm[5] to be non-zero if the instruction decoded is one of the SLLI, SRLI and SRAI as the specification provides the opcodes for these on page 104.
Scenario coverage
Conventional verification of microprocessors relies heavily on architectural testing using simulation. Functional coverage with simulation would test the interactions of different instruction inter-leaving however, the quality of results is limited to specific stimulus patterns. With our scenario coverage we auto-generate assertions and covers to examine a range of interesting scenarios targeting optimizations such as forwarding, pipelined instruction interleaving and the inter-play of stalls, interrupts, and debug.
How does it work?
By reading a user-defined specification from an Excel spreadsheet, the formalISA app will generate proofs of assertions and coverage properties along with waveforms to establish beyond doubt that those specification entries always hold in all reachable states. The figure below shows a user entry specifying that 4 cycles after reset a SUB instruction was issued twice followed by 1-cycle later an OR instruction followed by 1-cycle later an AND instruction. This entry triggers a range of coverage targets (asserts and covers) that are proven in the formal tool. The waveform below shows a scenario satisfying this entry showing forwarding.
Fig 2. Scenario coverage example
Architectural verification planning and status dashboard
The beauty of our solution using the formalISA app is that users can find bugs in RTL or specifications, build proofs and auto-generate the entire verification plan, status and coverage results with a single push-button. The plan and status is linked directly to the RISC-V specification published by the RISC-V international.
Fig 3. Snippet of an example verification plan and status dashboard for WARP-V generated automatically from formalISA®
When using a tool such as Cadence JasperGold® we are also able to generate a rich coverage dashboard exploiting the capabilities of JasperGold.
Fig 4. Coverage metrics obtained within minutes from JasperGold® on cv32e40p
Intelligent Rapid Analysis Debug and Reporting i-RADARTM
When Shivani was finding bugs and we were root-causing them together, it was a significant effort even though we were using formal methods and one of the best formal verification debuggers JasperGold® Visualize. The challenge is that although JasperGold® is already quite cool in how it identifies a precise set of signals linked to the failure of the property in many cases the signal identified are too precise as they are linked to the proof core.
What we mean here is that if a certain bit of a signal for example bit [1:0] of the branch address was responsible for the failure it will show just that, and the user then has to follow the trace systematically which is all good but it takes time for anyone debugging to pull together a narrative of why something failed and understand why it is a bug before it can be sent to a designer.
Without the narrative just with the trace, the designers would often complain about not knowing what is being debugged. To overcome this problem, we designed a new intelligent debug solution in Axiomise called i-RADARTM. It stands for intelligent rapid analysis, debug and reporting which is now offered by Axiomise as a plugin-solution for JasperGold when you purchase the formalISA app.
If you use JasperGold and formalISA app, you will see a GUI button in JasperGold. When you click this button, the Axiomise intelligent analysis is performed on a failing property and a debug report along with VCD is generated for debug handoff to the designers. It means that no human effort needs to be made to debug, troubleshoot, build a report.
i-RADAR in action
Fig 5. i-RADARTM solution showing the failure of the BEQ instruction on WARP-V.
The waveform image that appears when the i-RADARTM is used with Cadence JasperGold®. The trace shows the failing property on BEQ instruction in WARP-V. The precise chain of causality is annotated in the debugger. The report explaining why it is a design bug is also printed in a file shown below.
——————————————————————————————-
formalISA generated cover report for the instruction beq
Generated on 2021-08-22 17:07:44 %
beq.fsdb, beq.vcd, and beq.shm written on disk
——————————————————————————————-
The waveform is for the RISC-V instruction: BEQ
BEQ was triggered for execution and commit (u_isa.beq_instr_trigger) in cycle: 23
Design computes the branch target address in cycle 23 = 32’h00000034
Formal model computes the branch target address in cycle 23 = 32’h00000030
The formal model computes target address in cycle 23 using the PC (32’h00000001) and the offset (32’h00000030)
The value computed by the design 32’h00000034 does not match with the value computed by the formal model 32’h00000030
——————————————————————————————-
Why Axiomise formal verification solution matters?
Axiomise has invested in building an architectural model of the RISC-V ISA with support for privileged instructions as well as regular ones. Having spent years verifying processors, the Axiomise team has distilled down key abstraction techniques in the formalISA® app and ensured that we get them reviewed independently as well as against different processors. Our partnership with Cadence enables us to validate and optimize the formalISA® app for JasperGold® users. Axiomise built the industry’s first scenario-coverage based solution as part of the six-dimensional coverage solution. Our solution is the only solution in the market that works with all the formal verification tools, is push-button and has smart automation from running the first proofs to intelligent debug, to obtaining a comprehensive coverage using the six-dimensions.
For more information, please check out the links:
- Whitepaper
- RISC-V summit 2019
- RISC-V summit 2020
- OpenHW TV talk
- Automatic end-to-end formal verification of RISC-V processors
Conclusion
Designing a processor is one thing, bringing it up in FPGA and demonstrating example program runs is another; but ensuring that this processor is able to run in silicon correctly as expected without having any functional, safety and security flaws is a completely different challenge.
Building silicon with zero defects is not easy and it requires a concerted focussed effort in combining the best verification technologies together to focus on verification concerns not on the political milestones of individuals driving verification. Let’s not kid ourselves anymore – simulation-based verification using UVM will not enable you to verify the processors with high quality never mind nowhere close to being exhaustive. Well known processor design houses such as Intel, IBM, Arm, and AMD have published numerous papers over the last three decades showing how they have complemented and supplemented their verification efforts with formal methods. Formal methods are the only way of obtaining exhaustive verification results, and sign-off your silicon so everyone can sleep better. Using formal methods, we can prove the absence of bugs, bring up corner-case (one in a million chance) bugs in a few seconds, and use different coverage techniques to convince through proofs that when formal says it’s done you are truly done.
Axiomise RISC-V formal verification app formalISA® when used in conjunction with top-end formal verification tools such as JasperGold® from Cadence provide a complete solution reducing human costs in bringing up bespoke testbenches and provides an accelerated path to exhaustive sign-off. With the combined new debug solution, we can perform automated intelligent analysis for a debug handoff to designers shrinking debug time and costs.
Authors:
Ashish Darbari, Axiomise
Pete Hardee, Cadence Design Systems
Also Read
CEO Interview: Dr. Ashish Darbari of Axiomise
Life in a Formal Verification Lane
Why I made the world’s first on-demand formal verification course
Share this post via:
Next Generation of Systems Design at Siemens