Computer Science Colloquium

System-Level Verification of Register Transfer Level Designs

Panagiotis Manolios
Georgia Institute of Technology

Monday, April 23th 11:15 a.m.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html

Host/s:

Clark Barrett barrett@cs.nyu.edu, (212) 998-3105

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 system-level verification of Register Transfer Level (RTL) designs. System-level verification involves proving theorems that capture the correctness of system components as a whole, not just proving isolated properties. To be practical, verification methods must be directly applicable to actual designs, which are defined at the register transfer level. This is a major challenge, which is why previous work has focused on the verification of ad hoc, highly abstracted designs.

In this talk, I will present several methods that we have developed for automatically reasoning about RTL designs. This includes:

- a sound and complete compositional reasoning framework based on refinement,

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

- a new algorithm for converting Boolean circuits to conjunctive normal form that gives an order of magnitude improvement in verification times over previous work.

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, as competing methods cannot handle much simpler designs.

The verification technology we developed 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.

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.

Refreshments will be served


top | contact webmaster@cs.nyu.edu