Formal For All!
“Do I need a PhD to use formal verification?”
“Can formal methods really scale?”
“Is it too difficult to write formal properties that actually prove something?”
“If I can’t get a proof, should I just hope for the best?”
“Do formal methods even offer useful coverage metrics?”
…
Discouraging words to say the least, but we don’t have to live in the shadows they create anymore!
AI technologies are getting adopted faster than ever and the implementation of AI algorithms are no longer limited to purely software. In fact, breakthroughs in AI performance and the need to reduce energy consumption footprint are driving crazy innovations in hardware designs. So, for the first time, power, performance and area (PPA) along with functional verification has become a mainstream challenge; not to mention that with the adoption of AI hardware in embedded, IoT and edge – safety & security is now even a bigger challenge!
In a recent keynote at DVCon India given by Dr. Ashish Darbari, founder & CEO of Axiomise, he described how 1030 simulation cycles are not finding the bugs causing expensive respins. The respins are estimated to be 76% for ASICS with 84% of FPGA designs going through non-trivial bug escapes – the data coming from the well-known Wilson Research survey, 2022.
Axiomise: Making formal normal through consulting, training and automated IP
At Axiomise, we have been driving a vision of making formal normal and predictable for all kinds of semiconductor design verification. With over 60+ person years of combined formal verification experience in applying formal methods for silicon verification, the Axiomise team has verified over 150 designs covering GPU blocks, networking switches, programmable routers, NoCs, coherent fabrics, video IP components and hyper-scalers implemented with the three major CPU architectures including RISC-V, Arm, and x86. We have been able to achieve this through a combination of consulting & services engagements powered by automation derived from custom IP such as formalISA app for RISC-V and bespoke formal assertion IP for standard bus protocols such as AXI and ACE.
We love bringing in this experience to the masses and we have been delivering training through a unique combination of on-demand and instructor-led courses for the last 7 years at Axiomise. Our trained portfolio of hundreds of engineers now covers some of the Who’s Who of the industry.
Back to the drawing board
While we were training smart engineers in the industry, we learnt what is working for them and what is not and based on this experience we have come out with our most condensed and practical course yet! Learn the essentials of model checking from an industry expert who has pioneered a lot of the methods and abstractions used by experts in the industry today.
With 65 patents, and nearly 3 decades of experience, Axiomise founder and CEO Dr. Ashish Darbari brings this course, Essential Introduction to Practical Formal Verification, to anyone who has the desire to set foot on this journey.
With formal, we can find bugs early in design cycle, accomplishing the shift-left vision as well as prove bug absence through mathematical proofs.
Essential Introduction to Practical Formal Verification
Our goal is to make formal normal. And that’s how we’ve approached making this course, not just in making sure we start from scratch and build up knowledge as we go along, but also ensuring that the complex subject of formal is presented in a way that makes it easy for everyone to get started with formal. The course takes the complex topics of abstraction, problem reduction, design validation, verification and coverage and presents them with examples, and case studies to make it easier to understand the scope of formal for large design verification.
The course is delivered as an on-demand, video based online course, with lots of quizzes to test your understanding, live demos, example code to play with, a certificate at the end, and of course some food for thought to encourage you to go further and not just stop there.
Reaching out to non-English speaking audience
We made a genuine effort to reach out to non-English speaking audience in the world by providing subtitles for every video in 5 languages other than English. We have subtitles in available in French, Spanish, Portuguese, Japanese, and Chinese.
Priced with accessibility in mind, our goal is that with your help we can break free of just-good-enough designs and create a new standard for what we expect the future to look like. When it comes to depending more and more on our electronic devices and all the safety critical aspects, they can be a part of, one bug is enough for a catastrophe!
Every journey begins with a first step
One bug is one bug too many! We can never know when or where the next escaped catastrophic bug will appear, but we do live in a world where it could have been prevented, if the standard was to actually prove bug absence. And who knows, somewhere, maybe even close by, the most obscure and dangerous bug could be in the process of being written within a piece of code right now as you read this text.
Let’s get started in deploying formal for semiconductor design and work collectively to make formal normal!
Authors
Nicky Khodadad, Formal Verification Engineer, Axiomise
Ashish Darbari, Founder and CEO, Axiomise
Also Read:
An Enduring Growth Challenge for Formal Verification
2024 Outlook with Laura Long of Axiomise
RISC-V Summit Buzz – Axiomise Accelerates RISC-V Designs with Next Generation formalISA®
Share this post via:
More Headwinds – CHIPS Act Chop? – Chip Equip Re-Shore? Orders Canceled & Fab Delay