C/C++ to RTL Equivalence Checking for FPUs and More
Complex data flows make verifying hand-crafted RTL for Floating Point and other arithmetic-heavy micro architectures a hard problem. Formal verification can help. This web seminar will highlight using Siemens' SLEC (Sequential Logic Equivalence Checking) technology to verify these complex circuits, including FMUL and FDIV. This seminar covers starting with a specification in C++, C, or SystemC, that is either user-created or that is delivered with the SLEC tool, and how that specification can be verified against hand-crafted and optimized RTL.
What You Will Learn
- Why you'd want to use Sequential Formal Equivalance Checking
- In brief, how you can drive SLEC to do the check
- The various design model inputs that SLEC can use
- What design blocks have used SLEC for this check
- More detail about checking Floating Point designs
Who Should View
- RTL designers
- Hardware managers
- Project leads responsible for verification methodology
- C++ model owners may be interested as well
Meet the speaker
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.