The ESL Edge

Randal E. Bryant joins Aart de Geus, Phil Moorby, Joe Costello, Richard Newton, Alberto Sangiovanni-Vincentelli, Hugo De Man, Carver A. Mead and other EDA industry greats in being presented with the Phil Kaufman award (2009) for his contributions to the EDA industry. Randy was singled out for his contributions in the formal verification space.

Dr. Bryant’s research focuses on methods for formally verifying digital hardware and some forms of software. Notably, he developed efficient algorithms based on ordered binary decision diagrams (OBDDs) to manipulate the logic functions that form the basis for computer designs. His work revolutionized the field, enabling reasoning about large-scale circuit designs for the first time.

I spoke with Ziyad Hanna, VP of research and chief architect at Jasper Design Automation who has worked with and followed Randy’s research for many years. Ziyad says of Randy – “he is a real innovator with great hands on research. He is indeed one of the fathers of formal in the last 3 decades.”

Dr. Bryant’s Accomplishments

In 1979, while a Ph.D. student at the Massachusetts Institute of Technology, Bryant developed the MOSSIM, the first switch-level simulator. This form of simulation models the transistors in a very-large scale integrated (VLSI) circuit as simple switches, making it possible to simulate entire, full-custom chips. Subsequently, Bryant and his graduate students developed successive simulators MOSSIM II and COSMOS. Major companies used these to simulate microprocessors and other complex systems. Switch-level models were also incorporated into the Verilog Hardware Description Language.

Over time, Dr. Bryant’s focus shifted from simulation, where a design is tested for a representative set of cases, to formal verification, where the design is shown to operate correctly under all possible conditions. It was in this context that he developed algorithms based on ordered binary decision diagrams (OBDD). His OBDD data structure provides a way to represent and reason about Boolean functions. OBDDs form the computational basis for tools that perform hardware verification, logic circuit synthesis, and test generation.

Today it is standard practice for hardware engineers to use OBDD-based equivalence checkers, and symbolic model checkers. Along with Dr. Carl Seger, now at Intel Corporation, Dr. Bryant developed symbolic trajectory evaluation (STE), a formal verification method based on symbolic simulation. STE is now in use at several semiconductor companies, and variants of it are used in commercially available property checking tools.

Dr. Bryant is an educator as well as a technical visionary. He and Carnegie Mellon Professor David O’Halloran co-authored a book, Computer Systems — A Programmer’s Perspective, that is currently used by more than 130 schools worldwide, with translations in Chinese and Russian; a revised version is set for publication later this year.

An IEEE and ACM Fellow and a member of the National Academy of Engineering, Bryant earned a bachelor’s degree in applied mathematics from the University of Michigan, and a doctorate in electrical engineering and computer science from MIT. He was on the faculty of the California Institute of Technology from 1981 to 1984 and has been on the faculty of Carnegie Mellon University since 1984. He received the 1989 IEEE W.R.G. Baker Award for papers describing the theoretical foundations of the COSMOS simulator, and the 2007 IEEE Emmanuel R. Piore Award for his simulation and verification work.

The award, given by the Electronic Design Automation Consortium and the IEEE Council on Electronic Design Automation