Axiomise at #59DAC, Formal Update

Monday at DAC I was able to meet with Dr. Ashish Darbari, the CEO and founder of Axiomise. Ashish had a busy DAC, appearing as a panelist at,  “Those Darn Bugs! When Will They be Exterminated for Good?”; and then presenting,  “Taming the Beast: RISC-V Formal Verification Made Easy.”

I had read a bit about Axiomise as a formal verification training and consulting services company on SemiWiki, and this was my first meeting with Dr. Darbari. With 46 patents in the field of formal verification, I knew that he was an expert in this area. Formal verification techniques have been used across many safety-critical market design segments: Automotive, security, healthcare, aerospace, ML, IoT and mobile computing.

I recalled that in the early days of formal verification that new users were almost required to have a PhD. in order to use and interpret the results, so I wanted to learn why formal techniques have not been widely adopted yet. Some of the larger design groups often want to become better trained in using formal tools, but may not have developed the training resources quite yet, so taking a training course from Axiomise is a quick way to get trained in the best practices.

Functional verification has been in use ever since digital simulation was invented, yet that was not sufficient to detect the famous Intel floating-point division bug back in 1994. Formal techniques would catch that bug today. Processor design companies are big adopters of formal to ensure that what is specified is what gets designed. When Ashish worked at Imagination Technologies,  a team of four formal experts supported 51 projects over a three year time span, training almost 100 engineers. Imagination Technologies is well-know for developing sophisticated IP, like: GPU, CPU, AI, and Ethernet.

What sets Axiomise apart is their training and consulting approach is tool vendor agnostic, so they don’t prefer one vendor over another one, the more formal tools to choose from the better. They basically have a very symbiotic relationship with EDA vendors. The actual training in formal can be done either in person or online, and engineers can make a class purchase using credit card. There are seven levels of online courses offered so far, including: theory, labs, demos, case studies, theorem proving, property checking, and equivalency checking.

Teams doing RISC-V designs should know that obtaining exhaustive ISA compliance is a big task, and that Axiomise has an app called formalISA to prove and cover, quite quickly, and without having to:

• Write a test case
• Write text sequences
• Write a scoreboard or checkers
• Write constraints
• Randomize stimulus

On premise training is an option for larger clients, which makes it easier for engineers to get up to speed without taking out time to travel for training.

For modern processor designs there can be 5X more verification engineers than design engineers, as the verification challenges have become so much larger. Using a formal approach for verification to complement functional verification and hardware emulation can save time.

Summary

Dr. Ashish Darbari is outgoing, affable, confident, experienced and a formal expert with decades of experience. What sets him apart is the unique combination of industry experience and a passion for all things formal. If you attend DAC or DVCon you will likely see him on an organizing committee. I look forward to following his career, and that of Axiomise for years to come, as they make verification more manageable by working smarter.

Related Blogs

• CEO Interview: Dr. Ashish Darbari of Axiomise
• Accelerating Exhaustive and Complete Verification of RISC-V Processors
• Life in a Formal Verification Lane
• Why I made the world’s first on-demand formal verification course