- Designed using standard SVA;
- Complies with the latest RISC-V ISA;
- Completely formal tool vendor agnostic;
- Works with all major formal verification tool;
- Requires no modifications to the design;
- Minimal setup;
- Requires no formal expertise to use;
- Fully expansive;
- Results appear within minutes;
- Corner case bugs;
- Greater than 99% proof convergence.
We developed a new formal proof kit using the industry standard, non-proprietary SystemVerilog assertions (SVA) for establishing ISA compliance based on the published RISC-V ISA and used this to determine if a given processor implementation conforms to the ISA semantics. Our solution is completely formal tool vendor agnostic, requires no modification of the design, and only requires the end user to be familiar with Verilog/VHDL. Moreover, our methodology is reusable for other RISC-V processors. Our “axiomising” methodology is built using the open standard of SystemVerilog assertions (SVA) and is enhanced for performance with our abstractions and problem reduction tool kit. We have deployed our methodology in practice to ensure that we can establish that all functional/safety/security/power requirements of a processor are turned into provably valid axioms (properties) of the design implementation.
All our proof checks converge – meaning they either produce a Pass or a Fail outcome. When the outcome is a Pass, it means a given check is valid for the implementation under all possible combinations of inputs and states. In case of a failure, it indicates there is a mismatch between the design model and our checker model, which is then debugged to root-cause the issue. We were able to exhaustively prove conformance of the design implementation against our proof kit checks for RV32IC subset of RISC-V ISA for a family of RISC-V processors from the PULP platform group using any of the available off-the-shelf formal verification tools from Cadence Design Systems, Synopsys Inc, Mentor – a Siemens Business and OneSpin Solutions. Some tools were able to produce results within a few hours, and a few others took about 72 hours, but the result is the same with all the tools – what proves in one is proven in another, what fails in one remains failed in another. Within an hour, we can get proofs to converge on all the checks other than LOAD/STORES, with over 75% of the non-LOAD/STORE checks done in 7 minutes of wall clock time.
Bugs and Proofs
Coverage and Completeness
We used a range of coverage techniques harnessing mechanisms in the tools that we used and complemented it with our techniques to ensure we built a complete solution. Being able to use different coverage solutions from different vendors offers the benefit of finding any discrepancies that you may miss if you were using only one specific tool. We introduced hand mutations (bugs) in the design to check if our properties were sensitive to them. This way, we established that our checks were indeed doing the right thing. It is a very effective, efficient and economical method in terms of run time performance to find problems with testbench. We exploited this technique heavily. We then reviewed whether we have mapped all the instructions to checks in our test environment, so we can determine if we are complete with respect to the ISA. Structural and functional coverage metrics indicated if there were any blind spots in our verification models with over-constraints.
In the context of processor verification, the use of formal verification has been around for at least three decades. The earliest applications made use of theorem provers, and the emphasis has largely been on establishing functional correctness of processor models designed in the language of the underlying proof tool. Ken McMillan devised advanced problem reduction techniques and showed how out-of-order processor implementations could be verified with formal when the processor design was coded in the formal tool SMV. However, widespread applications of formal verification at the commercial level have largely been limited with notable exceptions being the pioneering work done by Boyer Moore to verify the floating point unit of AMD processor using ACL2 theorem prover, Intel using their proprietary tool Forte, IBM using its proprietary tool Rulebase Sixth Sense, and more recently Arm who reported developing a tool to verify ISA compliance of their implementations. Alglave et al.’s work on relaxed memory models and our work on using Event-B for formal modelling, testing and verification of HSA memory models are other important pieces of work in the context of formal methods and processor verification.
In the context of RISC processors, S. Tahar’s work on formal verification of the first generation of RISC processors is important. He devised a framework of correctness and formalised it inside the HOL 4 theorem prover. For RISC-V, a lot of effort has kicked-off in applying formal verification. On the one hand, formal tools such as Coq and Bluespec are used to model the ISA of RISC-V with the intent of finding consistency issues; and on the other hand property checking based solutions have been used for finding micro-architectural bugs as well as establish conformance to the ISA . Whereas the work done by Chilipala in is indeed valuable, it is not clear how many users not familiar with Coq and BlueSpec can make use of it. A lot of hardware design is done using standard VHDL/Verilog, and it is not clear how the work done in  can be of direct use in verifying such designs without a substantial investment in enabling people in writing processor designs in BlueSpec, and at least having a basic understanding of Coq formalisms.
We believe that the work done by Hummenberger et al. in and the OneSpin Solutions appears to be directly useful however both of these solutions requires the end user to be locked into the respective proprietary tools. Although Hummenberger et al., do have an open source version of their tool in the public domain, this requires a somewhat intrusive setup requiring the instrumentation of the RISC-V design with testbench interface signals and also in some cases requires modifications to suit the tool limitations as evidenced by some of their users.
As regards to the solution from OneSpin Solutions, it is developed around a OneSpin proprietary assertion language (called operational assertions), and the vendor claims that by using this they can guarantee a gap-free formal verification solution. However, to exploit this gap-free aspect, the user has to use the formal tools (DV-Verify and DV-Certify) from OneSpin. There is no support for operational assertions inside any other formal tool. OneSpin Solutions does mention the usage of SVA and that there is a translator for operational assertions into SVA; however it has been made clear through their publications that to obtain gap-free solution one has to use operational assertions not standard SVA to model requirements.
We aimed to carry out an end-to-end formal verification with the limitations (a) that our work was carried out away from designers with limited access (b) we had no prior knowledge of design microarchitecture and (c) we had no comprehensive, detailed specification describing interfaces and internal state-machines.
In many ways, our work represents the reality of modern-day design verification where busy designers do not often document a detailed micro-architectural specification, and the first lot of verification is often carried out locally by the designers themselves using simulation or the knowledge about the specification is passed through word-of-mouth to the verification engineers who verify the design independently.
To the best of our knowledge, this is the first formal verification solution that is independent of a specific formal verification tool vendor, uses the open standard of SVA that all tools support and requires minimal setup guaranteeing greater than 99% proof convergence.
You can take our proof kit today and use the formal verification tool of your choice and start finding bugs in your RISC-V designs and build proofs of bug absence. Contact us to request a demo.