Formal bytes: The Axiomise Podcast Channel

Follow Formal bytes: The Axiomise Podcast Channel
Share on
Copy link to clipboard

Axiomise is a unique formal verification training, consulting and services company that loves enabling people in formal verification. This podcast is our way of sharing the joy of formal verification.

Axiomise


    • Sep 7, 2021 LATEST EPISODE
    • monthly NEW EPISODES
    • 25m AVG DURATION
    • 50 EPISODES


    Search for episodes from Formal bytes: The Axiomise Podcast Channel with a specific topic:

    Latest episodes from Formal bytes: The Axiomise Podcast Channel

    Episode 50: A fireside chat with Dr. Amin Kandou

    Play Episode Listen Later Sep 7, 2021 35:02


    In the 50th episode of our podcast, Dr Darbari talks to Dr Amin Shokrollahi. We trace Amin's journey from his early childhood, his interests in Mathematics to his current position as a CEO of Kandou - a company that specialises in low-power, high-speed, off-chip communication solutions. Amin describes himself as more of a mathematician than an electronics engineer. He outlines how he uses principles of abstraction in Mathematics/CS in real-life projects. Amin explains the retimer technology that Kando uses in their cutting-edge Matterhorn USB Type-C solution.

    Episode 49: A fireside chat with Prof. Moshe Vardi - Part 2

    Play Episode Listen Later Aug 17, 2021 46:09


    How can we make teaching formal methods more effective? What is the relationship between SQL and first-order logic? We used logic to design computers, now we use computers to perform logic reasoning, so is there a relation between machine learning and logic? How does a human brain perform reasoning? Is machine learning and logic the answer to all the major questions facing society? How do incomplete information and statistical bias fit into this? What does risk assessment mean? Tune in to our latest podcast to hear what Prof. Vardi has to say about these topics.

    Episode 48: A fireside chat with Prof. Moshe Vardi - Part 1

    Play Episode Listen Later Aug 3, 2021 34:29


    This week Dr Darbari talks to Prof. Moshe Vardi - one of the best-known names in computing and formal methods. In the first of the two episodes, we trace Moshe's journey from his early years and talk about logic, applications of logic to law, NP-complete problems, ENIAC, John von Neumann, John Backus, compilers, semantics, abstractions, descriptions. Moshe shares fascinating accounts of chat with Ed Clarke and the history of LTL, CTL, SVA and PSL. Find out why model checking works. Thank you very much, Moshe, for taking time out to talk to us.

    Episode 47: A fireside chat with Prof. Supratik Chakraborty - Part 2

    Play Episode Listen Later Jul 18, 2021 21:20


    Pleased to bring up the second part of the chat with Prof. Supratik Chakaraborty from IIT Bombay. We talk on boolean function synthesis, AI/ML, BDDs and SAT. Find out the next big thing in synthesis that has the potential to break the RSA! 

    Episode 46: A fireside chat with Prof. Supratik Chakraborty

    Play Episode Listen Later Jun 15, 2021 36:29


    Prof. Supratik Chakraborty is our guest this week. Tune in to find out how he came full circle from the corridors of IIT in his under-grad to being one of the top leaders in formal methods at IIT Bombay. In the first of the two-part podcast, Supratik talks to Dr Darbari about his passion for asynchronous circuits & formal methods, and word-level abstractions, and symbolic trajectory evaluation. Supratik shares his insights in teaching and research in formal methods and makes a strong case about why formal methods would be necessary for the design of machine learning hardware.

    Episode 45:A fireside chat with Ravi Thummarukudy

    Play Episode Listen Later Apr 27, 2021 40:53


    This week Dr Darbari talks to Ravi Thummarukudy. Hear Ravi's fascinating story from growing up in a village in Kerala with no electricity to being a CEO of one of the top design IP companies Mobiveil Inc. From IIT Madras, and days at ISRO, Ravi describes how he moved on to make Mobiveil a trustworthy name in design IP using the mantra trust but verify.

    Episode 44: Formal Verification 101 - The power of formal is now in your hands

    Play Episode Listen Later Apr 13, 2021 5:34


    This week we discuss our new formal verification course launched on 6 April, last week. If you're looking to understand how to apply formal methods, especially for industrial projects in VLSI, then we have something for you.

    Episode 43: A fireside chat with Dr. Daniel Zimmerman

    Play Episode Listen Later Mar 30, 2021 37:15


    This week, Dr. Darbari talks to Dr. Daniel Zimmerman, Principal Researcher from Galois Inc. Lot of exciting conversation on formal methods and their applications to cryptography, homomorphic computing and Daniel also reveals the secret Ninja formal methods and the work done with Amazon on deploying software analysis.

    Episode 42: A fireside chat with Bob Smith

    Play Episode Listen Later Feb 23, 2021 36:39


    This week Bob Smith is our guest. Bob is an executive director of the ESD Alliance, a SEMI Strategic Association Partner. He is responsible for the management and operations of the ESD Alliance, an international association of companies providing goods and services throughout the semiconductor design ecosystem.

    Episode 41: Invisible and visible formal verification

    Play Episode Listen Later Feb 9, 2021 17:29


    How do we know when the proof is the valid proof? Can we always see the proof? Are visible proofs required for verification? Can you trust invisible proofs for sign-off? Welcome to formal verification! Tune in to this week's podcast to learn more.

    Episode 40: A fireside chat with Dr. Zvonimir Bandic

    Play Episode Listen Later Feb 2, 2021 28:02


    In this episode, Dr. Darbari talks to a key leader in the field of the RISC-V ecosystem - Dr. Zvonimir Bandic - Senior director, Western Digital. Zvonimir traces his journey to the USA and describes the exciting field of storage and hard drives. We talk about the CHIPS alliance, open-source, and how Western Digital is influencing the RISC-V ecosystem.

    Episode 39: Abstraction in 7 minutes!

    Play Episode Listen Later Jan 19, 2021 6:50


    We demystify abstraction in today's podcast. Abstraction is the cornerstone of modern-day scalable formal verification. Classic papers in formal literature talk about abstraction as a Galois connection, but understanding abstraction when you're new to formal is not easy. We discuss it in detail in our upcoming webinar on 11 Feb 2021 but for now, here is an intuitive and simple explanation of abstraction and refinement.

    Episode 38: A fireside chat with Calista Redmond

    Play Episode Listen Later Jan 5, 2021 28:41


    We kick-off 2021 with our first podcast, talking to Calista Redmond, CEO of RISC-V International. Dr. Darbari asks Calista about the challenges and opportunities for the RISC-V revolution. Calista traces her roots from her days in IBM to what it takes to run an international organization spreading an open-source revolution in computer architecture like never seen before.

    Episode 37: A fireside chat with Harry Foster

    Play Episode Listen Later Dec 22, 2020 43:35


    Dr. Ashish Darbari delves into the findings of the 2020 Wilson Research report with Harry Foster in the last podcast this year. Together we gain more insight into design and verification trends. With 68% projects running behind schedule, and an equal number requiring respin for IC/ASIC, is the industry doing enough? With 23% of the semiconductor designs using RISC-V; and the headcount ratio of verification to design being 5:1 for processor verification, perhaps it's time to reflect and ask  - are we doing enough? With these thoughts, we sign-off 2020, wishing you all Happy holidays and merry Christmas.

    Episode 36: A fireside chat with Dr. Jason Oberg

    Play Episode Listen Later Dec 15, 2020 35:23


    We talk about hardware security this week. Tune in to bootstrap yourself with a primer on hardware security with Dr. Jason Oberg - CTO of Tortuga Logic. Jason is one of the best-known names in the industry in the field of hardware security.

    Episode 35: Six dimensions of coverage for formal verification

    Play Episode Listen Later Dec 1, 2020 15:51


    Learn how to sign-off formal verification using six dimensions of coverage. Metric-driven verification is important, but we need to consider all aspects when using formal verification including qualitative and quantitative methods. We made it easy for you to use the six dimensions of coverage to sign-off RISC-V verification. Find out about it in more detail next week at the RISC-V summit.

    Episode 34: Scenario coverage in formal verification

    Play Episode Listen Later Nov 17, 2020 11:48


    Dr. Darbari talks about a new coverage solution for formal verification - scenario coverage. He describes why you need it, what it is, and how this has been used to verify the latest core from the OpenHW group - CVE4. Let's cover our formal verification properly.

    Episode 33: A fireside chat with Dr. Lucio Lanza

    Play Episode Listen Later Nov 3, 2020 48:00


    This week Dr. Darbari talks to Dr. Lucio Lanza - Managing Director of Lanza techVentures and the 2014 recipient of the Phil Kaufman Award for Distinguished Contributions to Electronic System Design. We talk about some of the exciting things Lucio did in his early days in Olivetti, Intel, Daisy Systems, and Cadence to his current engagement in pervasive healthcare. Previously, Dr. Lanza was a non-executive director of Arm, the world’s leading semiconductor IP company, and a member of the board of directors of Harris & Harris Group, an investor in transformative companies enabled by disruptive science. He currently serves as chairman of the board of PDF Solutions, Inc., a provider of technologies to improve semiconductor manufacturing yields, and is on the board of directors of several private companies.

    Episode 32: A fireside chat with Rajat Swarup

    Play Episode Listen Later Oct 26, 2020 39:49


    Dr. Darbari got together with Rajat Swarup - a cyber-security expert and ex-Director of Information Security, Blackrock. We talk about computer security, its origins, its impact on software, hardware security, and the role of formal methods. We ask Rajat about simple ways of keeping us safe.

    Episode 31: A fireside chat with Khaled Maalej

    Play Episode Listen Later Oct 20, 2020 43:01


    Do you always need a GPU for L4/L5 autonomous driving? This week, Dr. Darbari sat down with Khaled Maalej - Founder & CEO, VSORA, a provider of high-performance silicon intellectual property (IP) solutions for artificial intelligence, digital communications, and advanced driver-assistance systems (ADAS) applications based in France. Find out how VSORA's unique solutions are powering the next generation of driverless cars. We talk about programmable DSP, performance, low-power, and verification of petaflop computers on wheels.

    Episode 30: Architectural verification and deadlocks

    Play Episode Listen Later Oct 13, 2020 11:11


    In this podcast, Dr. Darbari discusses architectural formal verification and deadlocks in processors. Deadlocks can cause all sorts of issues in the design and though you may believe that reset would be a great way of bringing the chip out of the deadlock, your customers may not want to always reboot the device. Use Axiomise formalISA to find & fix deadlocks and if you like prove that they have been fixed.

    Episode 29: A fireside chat with Michiel Ligthart

    Play Episode Listen Later Sep 22, 2020 30:52


    This week, Dr. Darbari talks to Michiel Ligthart. Discover Michiel's interesting journey from the Netherlands to the USA and find out how he ended being the president and chief operating officer of Verific Design Automation -  one of the most well-known names in the EDA industry. We talk about the impact Verific is making in the design of several EDA tools including one of our favorite formal tools that use Verific to compile 1.1 billion gate designs for functional formal verification in under an hour.

    Episode 28: A fireside chat with Professor Alastair Donaldson

    Play Episode Listen Later Sep 15, 2020 48:52


    In this week's podcast, Dr. Darbari talks to Professor Alastair Donaldson. He talks about a range of topics in software verification and describes how he went from being a keen musician to being a professor in computer science at Imperial College, London, and a software engineer at Google. We talk about formal verification, metamorphic testing, concurrency, compilers, OpenCL, OpenGL, compiler bugs, the semantics of programming languages, SMT solvers, Z3, and as Alastair points out everything that is focussed on software correctness, performance, and portability. We also discuss computer science education at Imperial College.

    Episode 27: Everything you wanted to know about architectural formal verification

    Play Episode Listen Later Sep 8, 2020 11:37


    Dr. Darbari demystifies the topic of architectural formal verification with the focus on RISC-V. He describes the similarities with simulation-based compliance testing and key benefits of using formalISA and formal verification for architectural compliance. A brand-new blog on this topic is available from Tech Design Forums.

    Episode 26: A fireside chat with Steve Hoover

    Play Episode Listen Later Aug 21, 2020 48:11


    In this podcast, Dr. Ashish Darbari talks to Steve Hoover, founder & CEO of Redwood EDA. Steve explains why he left a well-paid job at Intel to start Redwood EDA. Ashish asks Steve about why he has another language. The chat dives deep into Transactional Verilog (TL-Verilog), and why we should care about it? Steve explains how TL-Verilog will be a game-changer for RISC-V, formal methods, abstraction, UVM, tools, better debug, and open-source silicon efforts. Steve explains how his course is changing the way students learn digital design, computer architecture, and processor design. Do not forget to listen to Steve’s five tips. The new course registration deadline is 24 August. Register at: https://www.vlsisystemdesign.com/riscv-based-myth/

    Episode 25: A fireside chat with Ted Miracco

    Play Episode Listen Later Aug 11, 2020 25:02


    In this week's podcast, Dr. Darbari talks to Ted Miracco, CEO of Cylynt. Ted explains how he founded Cylynt, why it is called Cylynt, and what is the differentiation of its products. Find out how Cylynt technology is preventing software piracy and if you're a software company you may want to look at this product!

    Episode 24: A fireside chat with Bipul Talukdar

    Play Episode Listen Later Jul 29, 2020 25:36


    In this podcast, Dr. Darbari talks to Bipul Talukdar from SmartDV. Bipul tells us that SmartDV has the largest portfolio of VIPs in the industry and he explains why this is so? Find out, how Bipul made his journey from Assam in India to leading a cutting-edge application engineering team at Smart DV?

    Episode 23: A fireside chat with Matt Venn

    Play Episode Listen Later Jul 19, 2020 20:29


    Dr. Darbari talks to Matt Venn from Symbiotic EDA. Matt is working with Symbiotic EDA, promoting the use of Open Source Formal Verification tools in the IC and FPGA industries. Matt explains how Symbiotic EDA plans to disrupt the established market of formal methods by providing formal tools at a price that all can afford. Matt believes that Symbiotic EDA is incorporating new advanced technology in their tools and they provide an open-source version of their tools that gets used a lot amongst the research community. Find out why Matt believes this open-source model will give Symbiotic EDA an edge in the commercial domain as well.

    Episode 22: A fireside chat with Kiran Vittal

    Play Episode Listen Later Jul 19, 2020 20:01


    Dr. Darbari sat down with Kiran Vittal from Synopsys and asks him why does Synopsys care about formal methods? Kiran is a Senior Product Marketing Director in the Verification Group at Synopsys, with 25 years of experience in EDA and semiconductor design. Kiran outlines that Synopsys is seeing massive traction for formal methods and the year-on-year growth in Synopsys for formal methods is clear evidence of this. When asked, how can budget companies afford formal tools from Synopsys, Kiran explains that Synopsys can also offer cost-effective solutions.

    Episode 21: A fireside chat with Joe Hupcey III

    Play Episode Listen Later Jul 19, 2020 22:04


    In this year's DAC special, Dr. Darbari sat down with Joe Hupcey III from Mentor – a Siemens Business. Joe is a part of the Mentor’s Product Management team for Design & Verification Technologies; based in Mentor’s office in Silicon Valley, CA. He is responsible for the Questa Formal product line of automated applications and advanced property checking. Joe explains how from the days of 0-in acquisition Mentor has continued to invest in formal methods and now as part of Siemens, this investment is only growing. Despite selling simulation & emulation tools, Joe believes formal methods is one of the main technologies at Mentor being used in all shapes from apps to property checking.

    Episode 20: A fireside chat with Chris Komar

    Play Episode Listen Later Jul 19, 2020 20:20


    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.

    Episode 19: How is Axiomise making formal normal?

    Play Episode Listen Later Jul 16, 2020 10:50


    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.

    Episode 18: A Fireside Chat with Prof. Pascal Hitzler

    Play Episode Listen Later Jun 30, 2020 42:14


    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.

    Episode 17: A Fireside Chat with Adnan Hamid

    Play Episode Listen Later Jun 23, 2020 34:09


    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.

    Episode 16: Ten reasons to use formal verification

    Play Episode Listen Later Jun 16, 2020 20:11


    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.

    Episode 15: An informal chat with Simon Davidmann

    Play Episode Listen Later Jun 9, 2020 35:41


    In this week's episode, Dr. Ashish Darbari talks to Simon Davidmann - Founder & CEO of Imperas. Simon talks about his journey from being an inquisitive child to becoming the CEO of Imperas. His many influences on our industry include Verilog, SystemVerilog, and the fascinating work being done at Imperas in creating simulators for multiple different processor families, including Arm, RISC-V, and MIPS. Thank you, Simon Davidmann, for taking the time out to talk to us.     SHOW LESS          

    Episode 14: Have you got it covered with formal verification?

    Play Episode Listen Later Jun 2, 2020 11:33


    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.

    Episode 13: An informal chat with Sean Safarpour

    Play Episode Listen Later May 23, 2020 34:35


    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.

    Episode 12: Finding corner-case bugs in processors using architectural formal verification

    Play Episode Listen Later May 16, 2020 13:54


    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.

    Episode 11: Role of constraints in formal verification

    Play Episode Listen Later May 9, 2020 8:54


    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.

    Episode 10: A masterclass with Lauro Rizzatti

    Play Episode Listen Later May 1, 2020 34:17


    Dr. Darbari talks to Dr. Lauro Rizzatti - the emulation super Guru. Lauro traces his journey from Italy to the USA, explaining the many different, technological aspects of emulation, starting from its roots to the modern-day. Everyone in DV should find this highly educational.

    Episode 9: Why coverage is important for formal verification?

    Play Episode Listen Later Apr 25, 2020 10:36


    In this podcast, Dr. Darbari talks about the role of coverage in formal verification and sign-off. We examine why coverage is important and what can be done to sign-off the verification with confidence. We discuss the interaction between structural coverage, functional coverage in simulation, and what happens for formal verification, and what should happen?

    Episode 8: Role of specifications in verification

    Play Episode Listen Later Apr 18, 2020 13:06


    In this podcast, Dr. Darbari talks about the role of specifications in verification. Requirements & specifications play a very important part in establishing what can be obtained from a verification task. The general rule is if it ain't specified it won't be verified. After all, any testing & verification exercise needs to know what is being tested, and what is expected from a test?

    Episode 7: A masterclass with Harry Foster

    Play Episode Listen Later Apr 11, 2020 36:14


    In this podcast, Dr. Darbari talks to Harry Foster, Chief Scientist at Mentor Graphics about all things verification. Harry talks about ATPG, the origin of assertion languages, property checking, equivalence checking, and FPGAs. He shares insights about his association with Accellera and contributions to the Verification Academy. We talk about 5 tips that all verification engineers & managers will find useful to get productive with verification.

    Episode 6: Key drivers for maximizing verification ROI

    Play Episode Listen Later Apr 4, 2020 16:21


    We describe what are the key factors to maximise verification ROI, focusing on Axiomise formal verification and how we can improve the return-on-investment.

    Episode 5: Why processors need formal verification?

    Play Episode Listen Later Mar 28, 2020 15:46


    Dr. Darbari talks about why processors need formal verification in the latest podcast. He describes why processors are complex, and why formal verification is a necessity.

    Episode 4: History of formal methods

    Play Episode Listen Later Mar 21, 2020 14:01


    In this podcast, we cover the rich history of formal methods, explaining the basics of formal verification covering theorem proving, model checking and equivalence checking. We explain why formal verification is perceived to be hard. We make formal verification easier!

    Episode 3: Basics of testing and formal verification for SoCs

    Play Episode Listen Later Mar 14, 2020 10:53


    In this podcast, Dr. Ashish Darbari talks about testing and formal verification for SoCs. He describes the basics of simulation-based-verification techniques such as constrained random verification, directed testing, emulation, and formal verification. 

    Episode 2: A 30,000 ft introduction to a system-on-chip

    Play Episode Listen Later Mar 7, 2020 8:19


    In this podcast, Dr. Ashish Darbari presents a 30,000 ft introduction to a system-on-chip (SoC) and the numerous test and verification challenges that affect the design of these ubiquitous components that almost everyone on the planet owns! 

    Episode 1: Dr. Darbari talks about his passion for formal

    Play Episode Listen Later Feb 29, 2020 8:14


    Axiomise has turned two! In this first podcast, Axiomise founder & CEO Dr. Ashish Darbari talks about his passion for formal verification and the different challenges engineers face in adopting formal. Engage with us to share your views about formal verification, your challenges, and your success stories. Tune in to enjoy our regular formal bytes!  

    Claim Formal bytes: The Axiomise Podcast Channel

    In order to claim this podcast we'll send an email to with a verification link. Simply click the link and you will be able to edit tags, request a refresh, and other features to take control of your podcast page!

    Claim Cancel