Technical Dive Into "Efficient and Exhaustive Floating Point Verification Using Sequential Equivalence Checking"
"Efficient and Exhaustive Floating Point Verification Using Sequential Equivalence Checking"
Sequential Equivalence Checking is the process of proving formal equivalence between two non-state matching implementations of a given design specification. Nowhere has the VLSI industry adopted this technology as much as to prove correctness of floating point designs against a given reference model. Any error in floating point operations can have severe consequences. ARM and Siemens have partnered to undertake the formal verification of some of the most difficult floating point blocks, including FMUL, FMA, FDIV, and FSQRT, in their CPU designs. We also worked outside the FPU, on a Branch Predictor from the same CPU designs.
Relatori
Travis Pouarz
Application Engineer
Travis Pouarz joined Siemens EDA through the acquisition of Mentor Graphics in 2016 and Calypto Design Systems in 2015. He joined Calypto in 2014 to help customers apply SLEC System to FPU C++ to RTL sequential equivalence checking problems. Before that, he spent 16 years at IBM as an AE and developer of IBM's internal combinatorial equivalence checker. He has also been involved with EDA flow development and creating formal-verification-friendly designs. He earned a degree in Electrical Engineering and Computer Science from Duke University and a Masters in Computer Engineering from the University of Texas at Austin.
Vaibhav Agrawal
Formal Verification Engineer
Vaibhav Agrawal joined ARM-Austin in 2013 as a Formal verification Engineer in the CPU validation team, where he is responsible for applying formal techniques to verify instruction fetch unit, and floating point datapath unit. Prior to joining ARM, Vaibhav spent over a decade at Intel-Austin as a design automation engineer, working on automating various aspects of RTL design and validation flows. Before joining Intel, he earned a B.Tech in EE from IIT - Delhi, and a Masters in EE from UT - Austin.