Carnegie Mellon Dean Credited with Seminal Formal Verification Breakthroughs
SAN JOSE, Calif. & NEW YORK — (BUSINESS WIRE) — September 8, 2009 — Dr. Randal E. Bryant, Dean and University Professor of the School of Computer Science at Carnegie Mellon University, has been selected to receive this year’s Phil Kaufman Award for his impact in theory and practice on Electronic Design Automation (EDA).
The award, given by the Electronic Design Automation Consortium and the IEEE Council on Electronic Design Automation, will be presented to Dr. Bryant for his seminal technological breakthroughs in the area of formal verification. The Phil Kaufman Award dinner will be held November 4 at the Dolce Hayes Mansion in San Jose, Calif.
“Dr. Randy Bryant’s breakthroughs have enabled formal methods to tackle realistic problems in industry and have a significant impact on product quality,” remarks John Darringer, president of CEDA. “We are delighted to honor him with this year’s Phil Kaufman Award.”
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.
“Randy Bryant is well deserving of this award,” says Dr. Walden C. Rhines, chairman of the EDA Consortium and chairman and CEO of Mentor Graphics Corporation. “His contributions have helped to build formal verification into what is now a $100 million segment of the EDA market.”
In nominating Dr. Bryant, Dr. Rob A. Rutenbar, Stephen J. Jatras professor of Electrical and Computer Engineering at Carnegie Mellon University, notes: “The EDA community owes much to Randy Bryant’s vision and seminal technical contributions.”
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.
“Randy Bryant has had a remarkable career,” adds Dr. Robert K. Brayton, Cadence Distinguished Professor of Electrical Engineering and Computer Science at the University of California at Berkeley, and a Phil Kaufman Award recipient. “Several novel inventions which can be attributed directly to him have had broad and huge influences, stimulating much academic research and the creation of new CAD industries.”
Justin Rattner, Intel senior fellow, vice president and chief technology officer at Intel, agrees. “Professor Bryant has demonstrated extraordinary abilities in developing a profound set of novel technologies that have become the core building blocks of many of the most successful CAD verification and synthesis capabilities that are being used on Intel’s products.”
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.
About the Phil Kaufman Award
The Phil Kaufman Award, presented annually since 1994, honors an
individual who has had a demonstrable impact on the field of EDA. It was
established as a tribute to deceased EDA industry pioneer Phil Kaufman,
who turned innovative technologies such as silicon compilation and
emulation into businesses that have benefited electronic designers. For
more information on the award and to register to attend the event, go to