Formal Verification of Optimized Digital HardwareDate: 2010-04-01 Add to Google Calendar
Time: 3:00 PM
Location: Holmes Hall Rm 389
Speaker: Dr. Peter-Michael Seidel
Abstract: According to the international technology roadmap for semiconductors (ITRS) "verification has become the dominant cost in the modern hardware and software system design process," thereby restricting design sizes, and limiting design exploration and optimization that can by carried out in the tight schedules of general-purpose and application-specific processor developments. Formal methods have emerged as an alternative approach for the functional verification of digital hardware that can improve scalability and that can overcome many of the limitations of traditional validation techniques such as simulation and testing. One powerful class of formal verification approaches is based on theorem proving. In this talk I will present our approach, opportunities and challenges of theorem proving in the formal verification of complex digital designs.
Bio: Dr. Peter-Michael Seidel is a senior member of the technical staff at Advanced Micro Devices since June 2007. He is leading the formal verification efforts for AMD's low-power processor core development and focuses on theorem-proving and model checking based verification and specification techniques for complex functional units. Prior to working for AMD, Dr. Seidel has beena faculty in the Computer Science and Engineering Department of Southern Methodist University, conducting research that has also had a focus on formal methods and optimization in computer architecture, computer arithmetic and VLSI design. Dr. Seidel has published numerous results of his work in international refereed conference proceedings and journals. He holds one U.S. patent and has three U.S. patents pending on the optimization of computer arithmetic circuitry and software. Dr. Seidel is currently general chair of the IEEE conference on Computer Design (ICCD) and member of the program committee for the IEEE Symposium on Computer Arithmetic (Arith). He is a member of the ACM and a senior member of the IEEE.