Abstract: Assertion Based Verification (ABV) is an important part of the functional verification. In order to be efficient and provide a good Return on Investment (RoI), some important methodology rules must be in place. We will present these and how we have successfully applied ABV on different generations and classes of ARM microprocessor designs. We show that the right target for ABV is not to prove the correctness, but to find real bugs. Various flavours of ABV are also presented such as X-propagation, coverage completeness and security verification.

Biography: Laurent 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 8 years, first as a modeling engineer and 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 Materials:

• DVClub Europe Presentation
• Video Presentation