Sunday Industrial Experience Report, 15. November, 15:00 - 16:00

Formal Verification Challenges of a
Supercomputer-Class Machine
Designed for Molecular Dynamics

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.