Industrial-strength formal verification for production-grade RISC-V SoCs
LONDON, GB / ACCESS Newswire / July 18, 2025 / Axiomise partners with Bluespec to verify its RISC-V cores.
The Axiomise formal verification solution, powered by its formalISA® and footprint® apps, part of the axiomiser® platform, was used to verify the latest RISC-V core from Bluespec Inc®. The UK-based company, Axiomise, integrated the Bluespec core into the formalISA app and, within the first few weeks, started identifying bugs and building exhaustive proofs of correctness.
formalISA is an automated architectural formal verification solution that utilises SystemVerilog Assertions (SVA) to construct formal proofs of correctness for RISC-V designs, leveraging in-house advanced abstraction models. It has been used to verify over a dozen processors over the last six years. formalISA comes with an advanced debugger, i-RADAR®, and an ISA Coverage analyser® that is integrated with all the commercial formal property checking tools. footprint is an advanced PPA solution from Axiomise that computes silicon utilisation with accuracies guaranteed from a formal proof, optimising power, performance and area.
“Traditionally, we have used a combination of simulation and FPGA testing to validate our designs. We were naturally expecting formal verification to pick up bugs as well, as the design was under development. But we were pleasantly surprised at how, in few weeks, Axiomise was able to not only find early stage bugs but also find deep corner cases around performance, such as livelocks, and provide proofs of correctness,” said Charlie Hauck, CEO of Bluespec Inc.
Bluespec SystemVerilog® (BSV) is a high-level hardware description language with advanced features that accelerate hardware development. A superior behavioural model based on Atomic Rules and interfaces provides a high-level abstraction for hardware concurrency. Powerful parameterisation enables highly modular and reusable designs, and a strong, polymorphic type system with user-defined overloading enables expressive, type-safe design. Together, these features make BSV exceptionally well-suited for building correct, scalable, and maintainable hardware systems. Over the last two decades, high-profile projects from architectural exploration to commercial SoCs have used BSV.
“We have used formalISA before to verify several RISC-V designs. Verifying a machine-generated version presents new challenges in verification, especially for debugging. To overcome the debugging challenge of the machine-generated code, we enhanced our i-RADAR solution. The core had branch predictors and advanced speculative features. This added interesting challenges for proof complexity. We always aim for 100% exhaustive proofs, as they allow us to flush out corner-case bugs. We used the formalISA library of advanced proof recipes developed for several years to obtain end-to-end proofs for this core”, said Dr. Ashish Darbari, Founder & CEO of Axiomise.
Hauck added, “Typically, we focus on functional testing first and then performance, however with the combination of tools that Axiomise used – formalISA for functional testing and footprint for performance and area – we were able to obtain valuable insights into both functionality and performance at the same time – something we hadn’t fully appreciated formal verification could offer. The solutions were able to uncover functional bugs while understanding the performance and area analysis. This helped us to accelerate our development cycle and make more informed design decisions”.
Axiomise, formalISA, axiomiser, and footprint are trademarks of Axiomise Limited, UK. Bluespec is a registered trademark of Bluespec Inc., USA.
SOURCE: Axiomise Ltd.
