Computer Science Colloquium
System-Level Verification of Register Transfer Level Designs
Georgia Institute of Technology
Monday, April 23th 11:15 a.m.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html
Clark Barrett firstname.lastname@example.org, (212) 998-3105
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
- a sound and complete compositional reasoning framework based
- 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
- 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.
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
| contact email@example.com