Randal Bryant

Professor – CS Courtesy Professor – ECE
Office 4301 Newell-Simon Hall
Telephone (412)-268-8821
Fax (412)-268-5577
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.

In the News

  • 50th Design Automation Conference (DAC)
  • CSSI Affiliates Receive Honors at Design Automation Conference
  • ECE Faculty Win Awards at DAC
  • ECE Alumnus Wins Outstanding Dissertation Award from ACM SIGDA
  • Bryant's National Academy of Engineering Reception Held
  • Bryant Elected to National Academy of Engineering
  • CMU Faculty Awarded More Than $24 Million in Grants From NSF's ITR Initiative
  • Bryant's Paper Most Cited on Scientific Digital Library
  •  Randal  Bryant

    Research Area



    Formal hardware and software verification


    PhD, 1981
    Electrical Engineering and Computer Science
    Massachusetts Institute of Technology

    EE, 1978
    Electrical Engineering
    Massachusetts Institute of Technology

    SM, 1977
    Electrical Engineering
    Massachusetts Institute of Technology

    BS, 1973
    Applied Mathematics
    University of Michigan, Ann Arbor