PITTSBURGH-Randal E. Bryant, University Professor and dean of Carnegie Mellon University's School of Computer Science, will receive this year's Phil Kaufman Award from the Electronic Design Automation Consortium and the IEEE Council on Electronic Design Automation (CEDA) for his impact on theory and practice on Electronic Design Automation (EDA).

The award recognizes Bryant's seminal technological breakthroughs in the area of formal verification - the use of mathematical techniques to prove that a hardware or software design functions as intended.

"Dr. Randy Bryant's breakthroughs have enabled formal methods to tackle realistic problems in industry and have a significant impact on product quality," said John Darringer, president of CEDA. "We are delighted to honor him with this year's Kaufman Award."

Though his early work focused on simulation, where a design is tested for a representative set of cases, Bryant eventually shifted to work on formal verification, where the design is shown to operate correctly under all possible conditions. 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.

Today it is standard practice for hardware engineers to use OBDD-based equivalence checkers and symbolic model checkers. Along with Carl Seger, now at Intel Corp., 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.

The Kaufman Award, presented annually since 1994, 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. The Kaufman Award dinner will be held Nov. 4 at the Dolce Hayes Mansion in San Jose, Calif.

"Randy Bryant is well deserving of this award," says 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 Bryant, Rob A. Rutenbar, the Stephen J. Jatras Professor of Electrical and Computer Engineering at Carnegie Mellon, said, "The EDA community owes much to Randy Bryant's vision and seminal technical contributions."

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 used by more than 130 schools worldwide, with translations in Chinese and Russian. A revised version of the book 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 a member of the Carnegie Mellon faculty 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.