RISC-V Becoming Less Risky with the Right Verification
By: Rob van Blommestein
RISC-V continues to make headlines across the electronic design industry. You may have seen the recent news that the OpenHW Group is delivering their first RISC-V core, the CV32E40P.
If you attended last month’s RISC-V Summit, perhaps you attended “CORE-V: Industrial Grade Open-Source RISC-V Cores” by Rick O’Connor, president of the OpenHW Group. In this session, Rick discussed how the organization teamed with OneSpin and several other verification partners to develop the CORE-V-VERIF silicon-proven, industrial-grade functional verification platform. This platform was used to execute the complete verification of the CORE-V CV32E40P and is currently being used to verify the CV32A6 and CV64A6 cores.
The CV32E40P core will be used for high-volume, commercial chip projects with strict integrity criteria. The OpenHW Group recognized that the use of simulation alone would leave the core vulnerable to undetected critical bugs, incomplete coverage, and/or unnoticed hidden instructions—and they fully recognized that any of these verification shortcomings could result in functional errors, safety issues, and security holes. To remedy this, the CORE-V-VERIF platform goes beyond simulation to include OneSpin’s unique formal verification technology, which has proven vital to achieving speedy, successful, and bug-free delivery of the CV32E40P core.
Rick O’Connor understands the impact that formal has on achieving complete verification: “OneSpin’s unique technology was an ideal contribution to the OpenHW Verification Task Group helping to identify bugs that simulation alone would have missed. The OneSpin solution allowed the task group to achieve the coverage necessary to reach the functional RTL freeze signoff goals both in terms of speed and quality.” High praise—thanks, Rick!—but how exactly did OneSpin work with the OpenHW Group to verify their CORE-V core? Collaboration took place from the ground up and continued throughout the verification process.
OneSpin first partnered closely with the OpenHW Verification Task Group to develop a formal verification plan. OneSpin then augmented the SystemVerilog / UVM based CORE-V Verification Test Bench simulation efforts. Assertions were used to prove that the core implementation/RTL model conformed to the ISA; these assertions were either automatically generated or manually written to cover all items of the plan. Code coverage, mutation coverage, and assertion coverage metrics were reviewed to increase confidence that all items in the plan had been addressed. Once the test bench was implemented, runtime was completed in a matter of days and debugging was finished in just minutes. OneSpin detected many critical bugs: eight related to regular and exception instructions and others related to the privileged specification. OneSpin’s agile approach allowed for adjustments to the formal verification schedule to meet the OpenHW Verification Task Group’s verification priorities for maximizing the code freeze outcome. The ultimate result was exhaustive and complete verification in a very short period of time.
Silicon Labs had a front row seat during the verification efforts, as they helped to lead the OpenHW Verification Task Group. Steve Richmond, verification manager at Silicon Labs and co-chair of the task group, stated: “The CV32E40P core is the first open-source core for high-volume chips verified with the state-of-the-art process required for high-integrity, commercial SoCs. OneSpin is a key contributor. The OneSpin RISC-V integrity formal verification solution has systematically detected corner-case bugs in the exception logic and pipeline. These issues would only be triggered under rare conditions in the instruction sequence, memory stalls, and Control and Status Register programming. Constrained-random simulation tests to find these issues would require large investments in development and simulation time.”
Arjan Bink, principal architect at Silicon Labs and chair of the OpenHW Cores Task Group, went on to say: “The pinpointing of the issues’ root cause was impressive and a massive time-saver in debug. The solution also showed almost zero noise in detecting real RTL bugs, as opposed to other approaches where the issues reported often lead to fixes in the verification environment.”
Check out the OpenHW TV episode titled “Deep Dive into Formal Verification for the CORE-V CVE4” featuring our very own Sven Beyer, RISC-V product manager, to learn more about how OneSpin contributed to the verification effort.
Anyone considering using RISC-V as part of their next design understands the customization and flexibility that the open-source architecture offers. However, processor verification is a new requirement that adopters will have to undertake. It is important to note that any user optimizations or additions of custom instructions require a complete re-verification to prevent the same potential problems that the previously mentioned malicious insertions could cause. The complex microarchitectures for achieving power, performance, and area targets, combined with the vast number of instruction combinations, cache, interrupts, exceptions, and myriad custom extensions, all need to be fully verified. Further complicating verification is the need to ensure that the core is correct with respect to the instruction set architecture (ISA), as well as that the RTL matches the ISA.
The OpenHW CV32E40P core is fully verified and ready for use, but there are still some verification challenges that designers will need to overcome when integrating the core: especially in cases where the core is customized. This core, and other RISC-V cores like it, should be re-verified after integration or customization to ensure that any changes do not introduce new bugs or produce unwanted behavior—and formal verification is the way to eliminate risk and exhaustively prove that everything is as it should be.
To learn more about how OneSpin can assure the integrity of your RISC-V design, download our white paper, “Assuring the Integrity of RISC-V Cores and SoCs,” at https://www.onespin.com/resources/white-papers.
