Design Verification Club

Overview:
Billionaires choose different ways to spend their wealth. Some collect sports teams, or build space ships, or fund telescope arrays. One has chosen to design massively parallel supercomputers to revolutionize molecular dynamics simulation. If your job was to ensure his vision could be realized, where would you start?

Join us on Monday Nov 8th to hear from Dr. Michael Theobald of D. E. Shaw Research as he describes the verification challenges of the Anton supercomputer.  Michael will cover the background of the project and walk us through how they approached verification, the decisions they made, and why they made them.  He’ll also review what to do if your design is harder to verify than necessary and informally cover their use of formal methods.

Speaker:
Michael Theobald, D.E. Shaw Research

Abstract:
In this talk, I will introduce the formal verification challenges encountered in the design of Anton, a massively parallel, special-purpose machine for molecular dynamics simulations. I will review approaches that have had the most impact on the design verification of the chip, such as bug hunting, root-cause analysis, coverage closure and deadlock detection. A particular outcome of the verification effort for Anton is a method that attempts to identify hard-to-verify logic early in the design cycle, based on model checking. This approach allows early modifications of the RTL code that enhance its verifiability for both formal and simulation methods, reducing the long tail of verification time and effort.

Bio:

Michael Theobald designs practical formal verification methods for complex circuits at D.E. Shaw Research. He is involved in the development of a special-purpose machine for molecular dynamics, called Anton. Michael also teaches as an Adjunct Professor in the Computer Science Department at Columbia University.

Michael received a Ph.D. from Columbia University in 2002 and a Diplom from Johann Wolfgang Goethe-Universitaet, Frankfurt, both in computer science. Prior to joining D.E. Shaw Research in 2004, he was a Postdoctoral Fellow in the Computer Science Department at Carnegie Mellon University with Edmund Clarke.

Presentation Notes:

Slides for this presentation are unavailable.