Electrical and Computer Engineering at Carnegie Mellon University

Randal Bryant

Professor – CS, ECE

Department	Electrical and Computer Engineering
Office	4301 Newell-Simon Hall
Telephone	(412)-268-8821
Fax	(412)-268-5577
Email	bryant@cs.cmu.edu
Website	http://www.cs.cmu.edu/~bryant/
Assistant	June Fischerkeller

Research Interests

Professor Bryant's primary research interest is in formally verifying hardware designs. This interest grew out of earlier work in logic simulation and symbolic circuit analysis. Formal verification promises to eliminate the uncertainty that lingers even after extensive evaluation by techniques such as simulation.

During the course of developing hardware verification tools, he has become interested in symbolic representations and manipulation of discrete functions. The approach followed involves representing functions by directed acyclic graphs, known as Binary Decision Diagrams (BDDs). These methods are now being applied not just to circuit verification, but also to such areas as: temporal logic model checking, logic circuit optimization, automated theorem proving and truth maintenance systems.

Most recently, he has focused on the verification of superscalar microprocessors. In an effort to maximize the speed of program execution, modern processors apply techniques such as out-of-order execution, speculation and many forms of caching. Verifying that such a system faithfully preserves the sequential execution model of the instruction set architecture is both an intellectual and a logistical challenge. Recently developed techniques allow much of the data processing operations to be abstracted away, allowing the verifier to concentrate on control and communication. By exploiting properties of these abstract models, increasingly complex processors can be formally verified.