DVCLUB Europe | Formal Verification

Two Case Studies in Formal Deployment on ARM CPUs : Instruction-Fetch and Floating-Point Datapath

Conference:DVCLUB Europe | Formal Verification | May 2018
Speaker:Vaibhav Agrawal, Principal Engineer, Arm
Abstract:ARM has consistently invested in applying formal technologies for design verification. In this presentation, we will discuss 2 case studies about successful use of formal for verifying parts of high end Cortex-A class CPUs. First, we will present instruction fetch unit verification, which is a highly control intensive block. Second, we will talk about verification of floating-point datapath.

  • Highlight the difference in methodologies and results between a control intensive vs datapath intensive blocks
  • Formal vs simulation? Or, formal and simulation?
  • Data on bugs found
Speaker Biography:Vaibhav Agrawal is a Verification Engineer at ARM in Austin, USA, where he has applied formal techniques to verify “Instruction-Fetch” unit, and “Floating-point datapath” units in ARM’s locally designed A-class Cores. Prior to joining ARM, Vaibhav was a design automation engineer at Intel-Austin, where he worked on various aspects of RTL design and validation flows. He has a Masters in EE from UT-Austin, and a B.Tech in EE from Indian Institute of Technology, Delhi.
Presentation Downloads:Visit the main Formal Verification page to download the presentations.


DVCLUB Europe is made possible through the generosity of our sponsors.