Formal bytes: The Axiomise Podcast Channel

In this year's DAC special, Dr. Darbari sat down with Chris Komar, Product Engineering Group Director from Cadence Design Systems to find out what is hot with formal verification at Cadence, and why Cadence invests in formal methods? Chris emphasizes that formal is no longer “nice to have” but a “must-have”. Chris has been in EDA for the last 20 years focused on formal verification, starting with equivalence checking and has focused on formal property verification for the last 17 years.

In this DAC special, Dr. Darbari explains how Axiomise is making formal normal by combining training, and custom formal verification solutions. He talks about formalISA, a new app launched this week, and how it is able to obtain proofs, bugs, and coverage for establishing ISA compliance for RISC-V processors without writing a single line of verification code.

We are very excited to say that this week, Dr. Darbari is joined by Prof. Pascal Hitzler to discuss machine learning and formal methods. Prof. Hitzler is one of the rare experts in the world who works in the exciting field of neuro-symbolic learning and the semantic web. We gain insights into what makes machine learning click, what neural network-based deep learning is missing, and how rule-based reasoning grounded in formal methods can help.

This week, Dr. Darbari has a fireside chat with the super-guru of Portable Stimulus - Adnan Hamid, Founder & CEO of Breker Verification Systems. Adnan, a true global citizen, describes his personal journey and how he discovered working in the field of portable stimulus where Breker is producing revolutionary products.

In this podcast, Dr. Ashish Darbari outlines the ten reasons why formal verification should be used. Save money, find more bugs, find bugs quicker, prove bug absence, ship safe and secure chips.

In this podcast, Dr. Darbari talks about the connection between constraints and coverage in formal verification. He discusses why the two topics are closely connected using the concepts of controllability and observability and why proof-core and COI coverage are not the best mechanisms to sign-off formal verification, especially for inconclusive proofs.

This week, Dr. Darbari has an informal chat about formal verification with Dr. Sean Safarpour - Group Director, Synopsys, and head of VC Formal product line. Sean talks about his journey from being a graduate student to leading a world-class team of engineers at Synopsys. Sean talks about tools, technology, methodology, coverage, and more.

What happens when you apply formal verification to find architectural flaws in processors? In this podcast, Dr. Ashish Darbari talks about an interesting way of using Axiomise ISA formal proof kit to find bugs in RISC-V cores. He describes how by using the combination of automated formal properties from the Axiomise proof kit together with constraints we can not only find bugs but also root-cause the precise nature of simulation resistant bugs. You might like this podcast if you ever wondered how constraints together with automated formal can be used to address the complex challenges of finding corner-case bugs in your CPU designs.

One of the biggest challenges with formal verification is scoping out what constraints are needed, and how they will be coded in formal verification for efficient predictable results. In this podcast, we discuss the role of constraints in formal verification.