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

Rachel Kalweit rachelb at ccs.neu.edu
Fri Mar 30 08:54:56 EDT 2007


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, March 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

_______________________________________________
Colloq mailing list
Colloq at lists.ccs.neu.edu
https://lists.ccs.neu.edu/bin/listinfo/colloq





More information about the Colloq mailing list