Axiomise Presents a Unique Coverage-Driven RISC-v Formal Verification Solution

LONDON, December 8, 2020 (Newswire.com) - ​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.

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.

Contact

Please contact [email protected] for more information and a product demo.

About Axiomise

Axiomise offers cutting-edge, formal verification training, consulting, and services. Axiomise is dedicated to enabling formal through its unique combination of training, consulting, services, and specialized verification solutions for RISC-V. Axiomise was founded by Dr. Ashish Darbari, who has been passionately driving the adoption of formal methods in the last two decades. An active user of all formal technologies, including theorem proving, model checking, and equivalence checking, Dr. Darbari has trained more than 200 engineers across the industry and has 35 US, UK, and EU patents in the field of formal verification.

Axiomise: Predictable Formal Verification.

Engage with Axiomise at:

Website: www.axiomise.com

Twitter: @axiomise

LinkedIn: https://www.linkedin.com/company/axiomise/

Facebook: https://www.facebook.com/axiomise

Axiomise and the Axiomise logo are trademarks of Axiomise Limited, UK. formalISA is a registered trademark of Axiomise Limited. RISC-V is the registered trademark of RISC-V international.

Source: Axiomise