Axiomise® will present a unique, coverage-driven verification solution for RISC-V® processors in the RISC-V Summit 2020 being held from 8-10 December.
Axiomise has designed an automated formal verification solution for RISC-V that proves compliance testing through formal proofs rather than simulation. Using the state-of-the-art abstraction techniques, Axiomise has built a push-button, formal verification solution to achieve three goals – catch bugs, prove bug absence, and sign-off designs with metric-driven coverage solution leveraging any formal verification tool in the market. Using their formalISA® app, Axiomise can accomplish ISA compliance and full functional verification against the published ISA from the RISC-V international. As part of building the app, Axiomise tested multiple cores and extensively verified the OpenHW CV32E40P processor.
“Axiomise built a new coverage-driven methodology exploiting six dimensions of coverage to provide a complete map from requirements to verification plan and regressions. We used our app to formally verify CV32E40P. The goal was to ensure that bugs are not missed, and the formal testbench delivers high-quality results that are vendor-neutral and reproducible in dynamic simulation,” says Dr. Ashish Darbari, Founder & CEO of Axiomise.
Read More: Maintaining a Secure Data Culture During and After COVID-19
The formalISA app generates proofs in a few hours, using a push-button flow, and works with any formal verification tool. It provides a much broader spectrum of proof results and coverage beyond what can be achieved with any one tool. Dr. Ashish Darbari will present the key facets of the solution and the results obtained for CV32E40P verification in a paper titled Coverage-driven Formal Verification for RISC-V ISA Compliance in the RISC-V Summit on 9 December at 11.30 a.m. PST.
“We were impressed both by Axiomise’s agility and the quality of results. Using their formalISA® app and the formal verification tools from different EDA vendors, Axiomise was able to find bugs in RTL, provide exhaustive proofs of bug absence for end-to-end proofs, and obtain coverage analysis often within a few hours,” said Rick O’Connor, President & CEO, OpenHW Group.
