Events - Colloquia & Seminars

CCIS Colloquium Spring 2007

Verifying System-Level Properties of Hardware at the Register Transfer Level

Speaker: Panagiotis Manolios

Affiliation: Georgia Institute of Technology

Date: Friday, March 30, 2007

Talk: 11:00 a.m., 366 WVH

Abstract

Verification has become the dominant cost in the design of hardware, often accounting for up to 70% of total design costs. One of the major challenges in the area is verifying system-level properties of Register Transfer Level (RTL) designs. System-level verification involves proving theorems that capture the correctness of the system as a whole, and we use the theory of refinement for this purpose. RTL verification is crucial because hardware designs are defined at the Register Transfer Level.

In this talk, I will present several techniques for automatically reasoning about RTL designs. This includes:

- a new algorithm for solving quantifier-free formulas over the extensional theory of fixed-size bit-vectors and fixed-size bit-vector arrays (memories),

- techniques based on-term rewriting that lead to further improvements, and

- a new algorithm for converting Boolean circuits to conjunctive normal form.

These algorithms have been implemented in BAT, the Bit-level Analysis Tool. Using BAT we can prove that a 32-bit 5-stage pipelined machine model refines its instruction set architecture in less than 2 minutes. This is a significant improvement over what was previously possible.

The verification technology we developed for reasoning about RTL-level designs is generally applicable, and I will briefly describe how it has been used to solve problems in the areas of computational biology and large-scale, component-based system design. This is joint work with Sudarshan Srinivasan and Daron Vroon.

Brief Biography

Pete's primary research interest is mechanized formal verification and validation. What guides his research is the vision that formal methods can be used to revolutionize the design and implementation of highly reliable, robust, secure, and scalable systems in a variety of important application areas.

Pete is an Assistant Professor in the College of Computing at the Georgia Institute of Technology. He is also an Adjunct Assistant Professor in the School of Electrical and Computer Engineering. He has a B.S. and an M.A. in Computer Science from Brooklyn College and a Ph.D. in Computer Sciences from the University of Texas at Austin.