Axiomise verifies Bluespec's RISC-V cores using formalISA and footprint tools

Axiomise, a UK-based formal verification company, used its formalISA and footprint tools, both part of its axiomiser platform, to verify the latest RISC-V processor core from Bluespec Inc. Axiomise integrated Bluespec's core into its formalISA application and, within the first few weeks, began identifying bugs and building exhaustive mathematical proofs of the design's correctness.

formalISA is an automated formal verification tool that uses SystemVerilog Assertions to construct formal correctness proofs for RISC-V chip designs, drawing on Axiomise's own advanced abstraction models. Unlike traditional testing, which checks a design against specific scenarios, formal verification mathematically proves a design behaves correctly across all possible cases. The tool has been used to verify more than a dozen processors over the past six years, and comes with an integrated debugger called i-RADAR and an ISA coverage analyzer that works with commercially available formal property-checking tools. footprint, a separate tool from Axiomise, calculates how efficiently a chip design uses silicon area, with accuracy guaranteed through formal mathematical proof, helping optimize a design's power consumption, performance, and physical area, together often referred to as PPA.

Charlie Hauck, CEO of Bluespec, said the company has traditionally relied on a combination of simulation and FPGA testing to validate its designs, and that while it expected formal verification to catch bugs during development, it was pleasantly surprised at how quickly Axiomise was able to find not just early-stage bugs but also deep, hard-to-detect issues around performance, such as livelocks, a type of software failure where a system appears active but makes no actual progress, while also providing mathematical proof of correctness.

Bluespec SystemVerilog (BSV) is a high-level hardware description language with advanced features designed to speed up hardware development. It uses a behavioral model built around "Atomic Rules" and interfaces, providing a high-level way to describe concurrent hardware operations. Its strong support for parameterization enables modular, reusable designs, while a robust, flexible type system with user-defined overloading supports expressive, type-safe design work. Together, these features make BSV particularly well suited to building hardware systems that are correct, scalable, and easy to maintain, and the language has been used in high-profile projects ranging from early architectural research to commercial systems-on-chip over the past two decades.

Dr. Ashish Darbari, founder and CEO of Axiomise, said the company has used formalISA before to verify various RISC-V designs, but that verifying a machine-generated version of a core introduces new verification challenges, particularly around debugging. To address that, Axiomise enhanced its i-RADAR debugging tool. He noted that the core included branch predictors and advanced speculative execution features, meaning the processor tries to predict and execute instructions ahead of time to improve speed, which added complexity to the formal proof process. He said Axiomise always aims for fully exhaustive proofs, since they help surface hard-to-find corner-case bugs, and that the company used its library of advanced proof techniques, developed over several years, to build complete, end-to-end proofs for this particular core.

Hauck added that Bluespec typically focuses on functional testing first before moving on to performance, but that using Axiomise's combined toolset, formalISA for functional verification and footprint for performance and area analysis, let the company gain valuable insight into both functionality and performance simultaneously, something he said the company hadn't previously realized formal verification could offer. He said the tools uncovered functional bugs while also providing performance and area analysis, which helped speed up Bluespec's development cycle and support more informed design decisions.