Dr. Ashish Darbari is the founder & CEO of Axiomise. As founder & CEO of Axiomise, he has led the company to successfully deploy the unique combination of training, consulting, services, and verification IP to a range of customers. Dr. Darbari has expertise in all aspects of formal methods including theorem proving, property checking, and equivalence checking. A keen innovator in formal verification, Dr. Darbari has numerous papers in top conferences and 44 US, UK, and EU patents in formal verification.
Although he has a Doctorate in formal verification from the University of Oxford, to learn formal verification from him, you don’t need a Ph.D.! He is a Fellow of British Computing Society and IETE, and a senior member of ACM and IEEE.
Describe the formal verification landscape and challenges companies are facing today?
Before I describe the landscape for formal or challenges, let me first say why we need formal methods?
Why formal methods?
It is not easy to catch all the bugs using simulation as the design complexity makes it very hard for anyone to conceive of all possible ways of catching the bugs by driving all interesting combinations of stimulus. Humans should not build stimulus generators; they should describe what needs to be verified by writing checks and capturing environmental constraints. Stimulus generation should be free and checking should be exhaustive. This is what you get with formal verification – no stimulus to write and proofs that are built for you automatically. Sounds amazing, isn’t it? And yet, formal verification has not become mainstream.
Harry Foster’s report in 2020 should be an eye-opener for all of us. 68% of ASIC designs and 83% of FPGA designs fail in their first attempt, while for processor design houses the ratio of verification to designer head count is 5:1. If you’re putting five times more verification engineers than designers and still failing to spin out correctly in the first attempt, what does it say about the quality of verification and cost of investment. We need to find corner case bugs earlier, prove that they don’t exist and ensure that silicon that is in the planes and our cars is safe and secure. We cannot afford an Ariane 5 explosion, a Meltdown type security scenario or an FDIV as there is much more silicon used now a days in our lives. Formal verification is the only way to build proofs of bug absence and formal property checking is the only way to guarantee that.
Formal verification landscape
Okay, so let’s talk about the FV landscape by giving you a 30,000 ft perspective on history of formal first if I may.
Historical perspective
Formal verification use in the industry started at least in late 80s to early 90s with most of the work done at IBM. When Intel hit the FDIV road block, they made significant investments in formal methods and at one point the Intel’s Strategic CAD Labs was one of the best places to be to do formal. Throughout this period, the focus was on in-house proprietary tool development with bespoke languages, compilers and methodology that was kept secret. However, in early 2000s things started to change and more companies started to look at using formal property checking. People may remember 0in, IFV and Magellan as the tools of the early 2000 era.
A seismic shift happened when Jasper Design Automation now part of Cadence, started making breakthroughs in adoption of formal apps through their JasperGold platform and this in my view changed the game for formal in a significant way. For many design engineers struggling with problems such as connectivity checking, CDC, X-checking, and unreachable code coverage waivers formal tools became the answer.
I don’t know of any semi-conductor design house that does not use a formal tool to solve these problems in 2021. While this was a great advancement for formal application, the bulk of the verification work was still left in the hands of dynamic simulation.
Dynamic simulation is still widely used as the de-facto verification technology, not formal verification.
Main players
There are three main EDA providers for commercial formal tools and each of these are driving the increase in tool adoption through apps. But what is not covered by the apps is the mainstream functional verification that is currently done by simulation. Simulation quality depends upon stimulus quality and humans should not be writing stimulus generators, tools should.
We are currently the only company in the world that has over two decades of experience using formal and is offering fully dedicated solutions in formal verification shrinking schedules for our customers and helping them find bugs earlier through shift-left paradigm and at the same time providing them with guarantees of bug absence through formal proofs. You know the best part is that all of this is that they can use any formal tool they like.
Why did you start Axiomise?
I started Axiomise because I love formal, and we can help customers use it to find bugs earlier and overcome the problems customers face with formal verification adoption.
Let me describe the challenges with formal adoption and this will help us understand why I needed to start Axiomise.
Challenges with formal adoption – The main reason for lack of formal adoption is a lack of methodology know-how and lack of vendor-neutral custom solutions. I know so many design houses have formal tools that are only used for apps. Though property checking adoption has picked up, it does not mean property checking is used to formally verify designs in all the cases. In many cases, assertions are written for simulation.
The main problem with formal verification adoption is that when formal properties are sent to formal tools for execution the tools cannot always guarantee proof convergence. What it means is that the outcome of running a proof may be unknown as we ran out of time or compute power. The formal tool usually reports a number which defines the extent to which the design was explored. What do you do in that case?
You need a sign-off method that is accurate, predictable, and reusable to ensure you can trust your explored results. Formal verification use in the industry has not always yielded predictable results in predictable time. This makes it very hard for any management to embrace formal fully. People understand simulation is incomplete, will miss bugs and they will cover their bases with functional coverage, but they are happy with that as they know what can be done. With formal methods this know-how has been not consistent, and not widely shared amongst the community. Although bespoke solutions were designed sporadically a lot of these were tied into a specific vendor’s solution.
Axiomise – Enabling predictable formal verification
I started Axiomise in Feb 2018, to make formal predictable for everyone in design verification including designers as well as architects. We are formal verification methodology experts. Our expertise is in executing formal verification for design verification in a holistic manner – right from the very first hour of design bring up all the way to tape out to the physical design teams and beyond to post-silicon debug. We believe if you start well, you will end well. We captured this methodology at a high-level.
By starting well, in many cases, using powerful abstractions and problem reduction strategies, we can avoid proof convergence issues altogether and can guarantee a known outcome and make schedules predictable. By offering a multi-dimensional sign-off methodology such as our vendor-neutral six-dimensional coverage solution we can guarantee that bugs are not missed, proofs are not obtained for trivial reasons and when proofs are bounded, we can deploy a systematic method to close the gaps.
How does Axiomise differentiate?
No two customers are the same, and that’s why we have different solutions for different customers. Not only do we offer different solutions, are solutions are also differentiated.
We are currently the only provider that provides a unique combination of solutions covering formal verification.
- We are the only company in the world fully dedicated in formal methods offering a complete solution from training to consulting & services to custom software which is all vendor neutral.
- We have been using formal methods for over two decades, and we teach what we practice, and practice what we teach.
- We shrink your DV schedule by helping you to roll out formal earlier and find more bugs.
- You will need less DV engineers per project if you were to adopt formal with our help reducing your costs and increasing verification ROI.
- We provide you with the secret recipes and methodology that will allow you to obtain high proof convergence and sign-off your verification with our six-dimension coverage solution.
- We can provide you with consistent, and predictable FV methodology that can be used by your entire DV teams. Knowledge that our customers require remain with them.
Our solutions
Training- Those customers who have DV engineers can learn the art of scalable formal methodology from us through our dedicated instructor-led training programmes. We have already taught over a hundred so far. Those individuals who work in organizations where formal adoption is not yet considered can still learn formal through our online, on-demand courses and can then request instructor-led course through their organizations. Please check out our training page to see how to sign up and see what some of our customers have to say.
Educational Podcasts – We have also been actively doing podcasts over the whole of last year and this year talking about interesting verification topics and a lot on formal verification. I believe we were one of the first ones to start podcasting on verification topics. If you haven’t already heard our podcasts, tune in to Axiomise podcasts on our website, or youtube.com, or your favourite podcast app.
Consulting & services – For many organizations, they just do not have enough dedicated verification engineering resource, so we work with their designers to not only teach them what we are doing but also at the same carry out the work. This way, they can see formal in its full glory on their designs and get the opportunity to learn.
Training, Consulting & Services – In many cases, we have delivered instructor-led courses as well as consulting and service work so customers can get the complete experience and build expertise in their own teams. We are helping design houses build their own dedicated FV teams this way.
Custom solutions – formalISA – We have noted that in some cases, engineering companies do not have the power to make sustained human resource investment in their organizations due to cost reasons but would still like to get the benefits of formal. This is typically the case with many RISC-V companies trying to build processors using the open-source RISC-V architecture. Not every company has deep pockets to invest in dedicated FV teams and that is where we can help them by giving them a push-button automated custom FV solution such as our formalISA app. Within a few hours, we can verify RISC-V processors exhaustively. Axiomise is a strategic member of the RISC-V international foundation and members of the OpenHW group. You can find out more about formalISA by visiting our site, or reading our latest blog on SemiWiki.
What real world problems are you solving today?
Tackling the challenges of formal proof convergence, sign-off and adoption on a wide variety of multi-million gate designs from high-speed 10G/100G ethernet switches, to processors (RISC-V being our focus), to GPUs, AI/ML hardware, to designs used in automotive and medical diagnostics.
Where is Axiomise going tomorrow?
We will be driving more momentum in the industry by driving formal adoption so formal becomes the mainstream verification choice. It will allow us to collectively build a safer and secure ecosystem. We will be doing this through custom training, consulting and service arrangements but also building new automated custom solutions for our customers.
I saw you have a paper at the upcoming Design Automation Conference, can you outline what you will present?
Yes, indeed, I have a paper on security verification titled, “Comprehensive processor security verification: A CIA problem”. I will be talking about addressing the security verification challenge in the context of processor verification and will be presenting results on security issues found in several RISC-V cores.
How would a company engage with Axiomise?
Contact us by emailing us at info@axiomise.com or contact us through www.axiomise.com and we can get on a call to figure out what you need. You can also follow us on our LinkedInhttps://www.linkedin.com/company/axiomise and Twitter pages and don’t forget to sign up on our Youtube channel for podcasts, and interesting talks and webinars. We are here to help.
Also Read:
CEO Interview: Jothy Rosenberg of Dover Microsystems
CEO Interview: Mike Wishart of Efabless
CEO Interview: Maxim Ershov of Diakopto
Share this post via:
Next Generation of Systems Design at Siemens