Conference:Formal Verification 2015 (click here to see full programme)
Speaker:Laurent Arditi, Principal Engineer.
Presentation Title:Formal Weapons for Microprocessor Verification
Abstract:The usage of formal verification within ARM is much wider than only Assertion Based Verification. We use formal techniques to hunt for many different classes of bugs, and have developed a range of flows with different focuses. We have also developed some best practices and tricks to increase the efficiency of formal verification, while make it usable by the masses. The presentation will show how this has been use in practice on several microprocessor design and validation projects.

  • Formal verification has many application areas
  • Formal verification is highly efficient to find bugs in designs
  • Knowledge sharing about best practices is essential
BiographyLaurent received his PhD on formal verification of microprocessors in 1996 from the University of Nice – Sophia Antipolis, France.  Laurent then worked on modeling techniques and semi-formal verification for Texas Instruments, then on high-level synthesis for Esterel Technologies.  He has been working for ARM for 9 years, first as a modeling engineer, now as formal verification expert.  As such, he is leading the formal activities within ARM, as well as applying formal verification on microprocessors in development.

View the Presentation Material:


Formal Verification 2015 is made possible through the generous support of our sponsors.
Formal Logo 2015