RISC-V Summit Buzz – Axiomise Accelerates RISC-V Designs with Next Generation formalISA®

If the recent RISC-V Summit proved one thing it’s that open-source hardware design, and particularly the RISC-V instruction set architecture (ISA) has entered the mainstream. It is a design methodology and architecture to watch closely. Across a broad range of applications from data center, to automotive, to IoT, RISC-V processors are finding a fit to address the huge processing demands of embedded AI. As is the case with any complex system design, a primary care-about is a robust design that is bug-free. Given the complexity of these designs, getting a new RISC-V implementation to that fully verified state can be a daunting task. An effective approach to this problem is by deploying formal verification. Using this approach can be challenging due to the expertise needed but this is where Axiomise can help. The company’s mission to “make formal normal” and its approach, along with RISC-V specific enhancements was on display at the Summit. Read on to see how Axiomise accelerates RISC-V designs with next generation formalISA®.

About Axiomise and formalISA

Axiomise was founded in 2017 by Dr. Ashish Darbari, after spending over two decades in the industry and top research labs increasing formal verification adoption. The company enables formal verification adoption by simplifying jargon and showing design teams how complex problems are easily solved through Axiomise’s abstraction-driven methodologies. These methodologies are vendor neutral. Training and consulting services are also available to enable formal in any corporate setting. You can learn more about Axiomise and its technology on SemiWiki here.

Earlier this year, the company announced its next-generation app specifically targeted at RISC-V processors. This unique push-button solution simplifies everything necessary to make verification efficient and effective. From avoiding test generation (like simulation) by using architectural-specification-precise formal properties to exhaustive testing (via formal) to then saving debug time (70% of verification time spent here) using i-RADAR® to sign-off via scenario coverage and reporting via SURF.  Its debug tool is powered by an intelligent debugger called     i-RADAR and a reporting and coverage solution called SURF.

It was reported in this announcement that the formalISA App has been in use for more than four years to formally verify numerous open-source and commercial RISC-V processors, proving the absence of bugs in out-of-order and in-order cores and exposing bugs in previously verified processors.

The Buzz at RISC-V Summit

At the RISC-V Summit, I was able to speak with Adeel Liaquat, engineering manager at Axiomise. I began by asking Adeel if there was one consistent care-about being expressed at the show. His answer was “time to market.”

He went on to explain that everyone wants an efficient, bug-free RISC-V processor to power new designs. Getting to that goal can be quite time consuming, however. Conventional UVM and simulation technology approaches can fall short of attaining the required level of robustness. Stimulus must be developed to cover all cases, and that is an open-ended, huge undertaking.

Formal verification offers a faster path by verifying the design across all possible states without the need for exhaustive input vectors. Adeel pointed out that handling deadlock conditions is a good example of the benefits of formal verification. These conditions may manifest after years of deployment in the field. It is virtually impossible to run enough vectors to uncover these situations up-front. The exhaustive nature of formal verification will ensure these conditions do not occur.

With all these benefits, why isn’t formal more popular? Adeel explained it’s a combination of awareness of the approach and expertise to implement it. He added that without the right methodology one could wind up in a verification “loop,” using up all licenses and all available time without a concrete result. Axiomise is a company dedicated to address this problem for design teams of all sizes.

From a technology perspective, the formalISA App makes RISC-V ISA specific formal technology available. The i-RADAR debugger simplifies the unique requirements associated with formal verification debugging. And SURF makes it easier to coordinate all the verification runs and consolidate results. Adeel explained that Axiomise can also develop custom capabilities that may be needed as well. Beyond the technology layer, the company offers training and consulting to bring design teams to the required level of proficiency. If internal resources are scarce, Axiomise can create and implement the full formal verification strategy and process for the customer.

This was an insightful discussion – I began to see how the mission of making formal normal was within reach. And that’s how Axiomise accelerates RISC-V designs with next-generation formalISA.