Hardware Verification: Theory and Practice
Jacob A. Abraham
Computer Engineering Research Center
The University of Texas at Austin

Full Paper in Postscript File

This tutorial is intended for designers who have to wrestle with the problem
of verifying the correctness of their extremely large designs.  Multi-million
transistor processor chips are becoming commonplace, and designs will break
the 10 million transistor mark in the next few years.  Verification approaches
based on extensive simulation (currently in use) are proving to be inadequate,
and companies are beginning to use formal techniques for finding bugs in
designs.

This tutorial will discuss the basic techniques which can be used for
verifying complex designs, and the extent to which they are being used today.
Existing state-of-the-art tools will be described and demonstrated, running on
a laptop under Linux.  Methods of dealing with complexity (such as the use of
abstraction) which will allow the designer to deal with the extremely large
state spaces will also be described.

Outline:

Simulation-based approaches and limitations
Introduction to theorem proving
Checking combinational circuit equivalence
Sequential circuit verification
Introduction to Model Checking
Abstractions to reduce complexity


A. Abraham is a professor in the Department of Electrical and 
Computer Engineering at the University of Texas at Austin. He is also 
Director of the Computer Engineering Research Center and holds a 
Cockrell Family Regents Chair in Engineering.
Prof. A. Abraham's research interests include VLSI design and test, 
formal verification and fault-tolerant computing. He the principal 
investigator of several contracts and grants in these areas, and a 
consultant to industry and government. He has over 200 publications 
and has supervised more 30 PhD dissertations.