SemiWiki.com - Podcast EP274: How Axiomise Makes Formal Predictable and Normal with Dr. Ashish Darbari

Episode Date: February 14, 2025

Dan is joined by Dr. Ashish Darbari, CEO of Axiomise. Axiomise was founded in 2017 by Dr. Darbari, who has spent over two decades in the industry and top research labs increasing formal verification adoption. At Axiomise, they believe the only way to make formal methods mainstream for all semiconductor design verification is to… Read More

Hello, my name is Daniel Nenny, founder of SemiWiki, the open forum for semiconductor professionals. Welcome to the Semiconductor Insiders podcast series. My guest today is Dr. Ashish Dabari, CEO of Axiomize. Axiomize was founded in 2017 by Dr. Ashish Dabari, who spent over two decades in the industry and top research labs, increasing formal verification adoption. At Axiomize, they believe the only way to make formal methods mainstream for all semiconductor design verification is to enable and empower the end user of formal, the hundreds of designers and verification engineers in the semiconductor industry.

Dr. Dabari was joined by Neil Dunlop in 2022 between Neil and Ashish, the Axiomize leadership team has over 60 years of formal verification experience on various projects. Welcome back to the podcast Ashish. Well, thank you, Dan. So we haven't talked in a while, what's new with Axiomize? Yeah, so exciting times for all of us, Dan.

We're seeing a growing push for quality verification. More and more customers are pushing us to sign off their silicon designs with zero bugs. And as you know, Formal is the only exhaustive technology that can do this. It's looking pretty awesome for Formal. the only exhaustive technology that can do this. It's looking pretty awesome for formal. As you know, we founded Axiomize in 2017

with the dream of making formal predictable and normal. The magic recipe here was how do we enable customers and how do we empower them? And what we've been doing quite successfully is by actually showing customers how they can get the best out of formal tools to sign off their chips, sort of end-to-end verification if you like,

without leaking bugs. And without a solid training program, this could never have been done. So I'm quite pleased to tell you that with all of the work that I put in initially in building hands-on training programs and then started delivering them to big silicon design houses, it was quite obvious that a lot of them liked the instructor-led training program. That still is something we do a lot of. But for some companies, Dan, it didn't work out very well

and they wanted to start even earlier before the instructor-led program. So, you know, we designed and launched industries first and only on-demand course, FE101, back in 2021, combining all the essential aspects of formal, you know, theorem-proving, equivalence checking, and model checking. I mean, I've always believed that formal is more than property checking,

and for a 101 course, engineers deserve to have a complete introduction, not just focus on the peripheries. So however, in the last four years, you've learned that for some customers, they want a training solution that is only focused on principles of property checking applications. So last year, we launched a new course called Essential Introduction to Practical Formal Verification.

And both of these courses are now being brought by customers to train vast number of DV engineers, designers, and even architects. So while we are continuing to grow the workforce, enabling them with formal training, a lot of the time we have to dive deep and quite fast often on customer projects to help them get the best out of functional formal verification. And we've made amazing strides in that direction. We've been helping some pretty awesome silicon design houses. But everybody doesn't have engineers to train, and not always people have the requirements

to get service work done. And sometimes people just want automation, and this is where custom solutions kick in. We have been building all of these custom solutions for custom silicon because silicon is getting more and more customized these days, not just because of the RISC-V open standard, but also because of the artificial intelligence and machine learning chips that are coming out. For RISC-V specifically, we had made a significant investment in 2019. And since then, we have been always doing more of that. And Formaliza is a great example in that domain, but we have made those investments.

So it really is coming together of all of these solutions over the last few years in a really nice way. That's what is happening at XMI. Yeah, that's exciting. So what is Formal ISA? What is the key differentiation in the market? Right, so we call this FormalIZA, and it's basically a solution

that is empowered totally by Formal, and it does exhaustive verification and certification of RISC-V implementations. And certification meaning it is proving the compliance of the given RISC-V processor implementation against the RISC-V specification published by the RISC-V International Foundation. But as with Formal, which you can't get with simulation, we can build guarantees coming out of proofs, and we can show that these instructions in the RISC-V spec are always guaranteed

to be preserved in the implementation. And if not, then we pick up counterexamples, which then are due to architecture or microarchitecture bugs. And again, what we've seen is they could be functional bugs, they could be functional safety bugs or even security, or in some cases even power performance or area related issues. And then apart from the fact that this is the only tool in the market that is vendor neutral and has been used with all the formal tools in the market, it has also consistently found bugs and

proofs every time we rolled it out on new processor designs. You may be familiar, last year in November we reported applying it on Cherry OTI BeX, which is considered to be a security processor has been built by guys in Cambridge, and Microsoft has made a significant investment in this, and the idea is to avoid memory leaks. And this processor, again, is in an embedded class, has been designed specifically with security instructions in mind.

Was previously verified by the Microsoft DV teams and some other formal verification teams. And when we put the app on this, very interesting new bugs were caught by us. A lot of very interesting commentary exists on GitHub and where we are finding a great niche area for Formalysa is in discovering these bugs that are often we call the simulation resistant.

And we're also able to then establish when the fixes are applied with guarantees through proofs that the fixes have been applied correctly. And where the designs do not have bugs, we're able to prove convergence. And if I'm not wrong, if I average out the proof convergence on so many different processor designs that we've tested, I think the convergence is greater than 95%, which is amazing for technology, which is not easy to use by most people in the industry.

And what is also interesting is like most formal solutions people do expect you to build proofs and find bugs. But as you know, debug tends to be the most expensive activity in any DB cycle. The i.r solution that we built is actually revolutionizing the concept of debug. It's completely intelligent debug solution. We launched this in 2022-23. It creates very precise debug reports automatically,

without a human in the loop, and can be handed over to designers without any human involvement whatsoever. And also then when you talk about how much did you do and how well did you do your verification, we built the six-dimensional coverage solution and specifically enhanced it with scenario coverage. We're seeing great results with that as well. Then to close it all off when it comes to reporting

and dashboards, we built the scheduler and reporter for Formal called Surf. We kind of piece together all of the aspects of design verification with Form formal, all in this formalizer solution. We've applied this to more than 12 different open source processors in order, out of order, pretty complex scores. And as I said, the success speaks for itself. It's been a great journey for us. Excellent. You know, I just read that you guys launched a new app

called Footprint Area Analyzer for Silicon Design. Can you tell us more about that? Oh yeah, so that got launched pretty recently. So what happened is this, over the years I've found that lots of cases during functional verification, you know, we can find that we have gates and registers in the design that never get used for anything. And it happens because of the way we write our assertions in formal here at Axiomize.

We are always able to uncover these corner cases of area redundancy. So I always wonder, wouldn't it be nice to be able to expose these redundancies in a hardware without tool, sorry, with a tool without necessarily building a sophisticated bespoke FPV test bench because building a test bench requires access to specifications, you have to put in all the code, a lot of human effort is involved. Wouldn't it be nice if a tool just automatically found this out? Because in many cases, the redundancies

are there in the design, not waiting for any verification work to find them. So basically, if this was not done through formal, I think the chances with UVM would be quite difficult to find. Because this is not really a verification problem. I think the chances with UVM would be quite difficult to find. Because this is not really a verification problem. Verification engineers, simulation or even formal ones do not do area verification.

This is an architecture designer problem. This is part of the PPA holy grail where people are trying to optimize performance, save power and optimize area, especially with AI chips, which is very good because when mobile computing was on, everybody was talking about low power and then HPC was considered to be not sensitive to the power needs, but now with AI chips hungry for energy, everybody is looking

to build low power solutions. So PPA is now center stage, even for high performance compute. So what we've done is we've built this push button tool that can provide a very quick feedback loop on hardware utilization and redundancy. So what it does is it takes in a design and it does all of the analysis

on different components in the design and it can categorize them and tell you which components are totally redundant, which components are partially utilized, quite fine-grained model of redundancy. It is not purely syntactical, but it actually does a semantic analysis under the hood automatically and then projects out these reports in a very easy to read format. And we've been testing this as part of the bring up. So it's quite a cool solution, and such solutions do not exist

in the industry today at all. Interesting. So how extensively has this app been tested? I mean, is it out in production? Are people using it? Yeah, so we've been trying to work with some of our customers and we've been testing different benchmarks

in the open source domain. So we've tested this on 80 plus designs so far, processors, GPUs, NOX, SOC peripherals. We've learned a lot about how different people build their designs and how very surreal redundancies remain in them. So we found loads of hidden, unutilized redundant gates and registers. So in the near future, we will be putting out a white paper or some kind of report where we can present our results. But yeah, I mean, it's early days.

We've literally just launched it, but the testing in-house has been quite thorough. Excellent. So how does someone get a hold of this app? Yeah, so people can register their interest on our website. Go to www.aximized.com slash footprint and we will get back and get in touch with you and we'll let you know how to download it and how to use it. Terrific. So what other plans do you have for 2025 and beyond? You know, give me a crisp wall view of the future. Yeah, so we are continuing to invest more

in building these custom solutions and we want to push the frontiers of these even more this year and also in coming years, we are looking to build lots more of these custom solutions. Also, a lot of requests is coming down my way for training more engineers across the industry. Also, the demand for services is growing so we will be of course engaging with strategic customers to do more work on signing off some quality work. So yeah exciting time for

us in Formal. This is of course reflected in our company growth and the attention we are getting from some of the best-known names and semiconductors. Yeah and we'll see you at DesignCon 2025 coming up in a couple weeks and we can talk again there. 3DCon is yeah we'll be there with my team. We are hoping to show demos of the footprint and formalize app and talk to people about how we can help make sure that chips don't have bugs before they hit the market, you know That would be exciting discussion Well, I look forward to seeing you there. We'll talk again. Great. Great talking to you then. Thank you That concludes our podcast thank you all for listening and have a great day.