Axiomise: Formal, Especially for RISC-V

I recently talked to Ashish Darbari, the CEO of Axiomise. They are based in London, where Ashish ended up having bounced around the world. But more of that later. I also discovered that he would be presenting at CadenceLIVE In Munich the following week, so I planned to attend that presentation and discuss that in this post too.

If you've never heard of Axiomise, let me tell you what they do. They have a four-pronged approach to the market. Ashish explained it to me:

• Consulting where we can work with companies where employees, including me, can give advice on a limited-time contract.
• Services angle, we take on the projects in a turnkey manner and code testbenches, etc. These are long-term six months to a year or more.
• Training: enable people to do it themselves. We have lots of courses, instructor-led, online, video
• For certain domains like RISC-V companies that don’t have enough talent or budget and want to verify their designs using an automatic solution we have FormalISA. See below in the CadenceLIVE section.

Ashish

So how did Ashish get to start Axiomise just over five years ago?

The first half of his life and education was in India, and he studied to be an electrical engineer. Then he switched to computer science and went to Germany to pursue a master's in computational logic (aka formal methods, in effect). He wanted to find a common ground between electronics and formal. so it seemed hardware model checking would be a perfect topic for a PhD. So he moved to the UK to do a PhD at Oxford (actually, a DPhil. which is Oxford-speak for PhD). Then he went to Intel for six months in Oregon. At the time, 2004, Intel probably had the best formal team in the world, put together after the infamous floating point bug FDIV. If you are interested, see my Semiwiki blog post, Jasper User Group Keynotes, where Bob Bentley tells the story (that was before Cadence had acquired Jasper). After his PhD, which took over five years, he focused more on combining test and formal methods, years before this became a hot topic due to functional safety, at Southampton University for about four years.

There were no jobs in the industry in 2010 in formal. But he interviewed with Arm in Cambridge and talked about formal methods. He stayed at Arm for 1.5 years, where, among other things, he created the roadmap for formal verification deployment. He then decided to go "home" to India and worked in a General Motors R&D lab specializing in formal methods applied to control software. But GM had its problems and laid off all the PhDs in Bangalore. So he came back to Britain, got a job at Imagination Technologies, and set up a verification methodology group with three people. They serviced 50 projects in three years, and also trained 90 engineers. But Imagination fell on hard times around then and started to lay people off. His team didn't get laid off, but people left anyway, and he was eventually alone.

So he joined OneSpin. But before he moved back to Germany, where they were based, he realized EDA was not his thing, and he was more interested in how the tools were used

So he created Axiomise with the goal to "make formal normal".

Today they are ten people from across the world based just outside London in Hemel Hempstead. 

We got to talking about machine learning in Jasper, and he is impressed:

I can tell you for the projects we are executing with Jasper, we can see the improvements from machine learning.

 

CadenceLIVE Europe

Ashish presented at CadenceLIVE Europe. The first part of his presentation was an introduction to Axiomise, very similar to what I covered in the early part of this post, so I'll skip that. I'll focus on FormalISA (pronounced "formalizer"). This is an automated tool for formal verification of RISC-V processors. It already knows the semantics of all the RISC-V instructions, and so all you need to do is use the GUI to load the processor into the tool and within minutes, hours, or days Jasper will get your proofs of bugs coming out. Sometimes, it is faster than that. One time Ashish set it up, went to boil some water for a cup of tea, and when he got back, it had found many corner-case bugs.

There is a GUI to load the processor into the tool, pick a tool, then the design and testbench go inside the formal tool, and within hours or days, you get proofs or bugs coming out. Many processors have been tested in the last few years, and Axiomise found bugs in almost all of them. See the table above for a few.

So in the context of RISC-V, Axiomise has a fully-automatic solution. It is actually vendor-neutral, but Ashish says "Jasper is an order of magnitude faster than the other tools." We have not just proofs and bugs but a debugger that extends Jasper and finds the root cause of failure.

 

The diagram above summarizes the capabilities of FormalISA for RISC-V processors. In particular, note that no test cases, manual checkers, or verification code needs to be written. This means that it is not necessary to be a formal verification expert to use FormalISA. As Ashish told me:

Some of the testing was done by my son at 13 to make sure it is simple enough. We are taking on the complexity head-on.

In the presentation, Ashish ran through a sort of "demo" in slides of FormalISA in action. But it is too many slides to attempt to reproduce here. Of course, if you want a demo, I know Ashish and his team are standing by!

Here's one slide to give you a flavor of what the debugger looks like in use.

Ashish's last slide summarizes Axiomise's view of the world of formal verification. In particular, formal methods are a necessity, not just nice to have. And for the specific case of RISC-V processors, Axiomise has created a turnkey solution that automates the problem.

Cadence and Axiomise

In the past, Cadence worked with Oski to provide additional design consulting for customers who needed more help than we could provide with our own AEs. Oski used to have occasional meetings of "Formal Club", sometimes sponsored by Cadence. For example, see my post Decoding Formal Club: Arm and Arteris. But last year, NVIDIA acquired Oski, and so they were unavailable to work with Cadence customers (well, NVIDIA is a Cadence customer,  but you know what I mean). Axiomise was already doing similar work since 2018, and now the partnership between Cadence and Axiomise is even stronger and more important.

 

Sign up for Sunday Brunch, the weekly Breakfast Bytes email