[Colloq] Hiring Talk, Friday, March 30, 11am

[Rachel Kalweit]

College of Computer and Information Science Colloquium

Presents a Hiring Talk By:
Panagiotis Manolios
Georgia Institute of Technology

Who will speak on:
Verifying System-Level Properties of Hardware at the
Register Transfer Level

Friday, Mach 30, 2007
11:00am
366 West Village H
Northeastern University

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.

Speaker Bio:
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.

Host: Professor Olin Shivers