I think the main lessons from the past few years are that:
1) No single method is suitable for all aspects of verification for
any reasonable size circuit.
2) We are moving from "virtuoso" verification efforts, to design and
verification methodologies.
- - - - - -
Addressing the first point:
By acknowledging that we must rely on a variety of methods and tools
to verify a circuit, we decide where proof development systems are
most effective. I think that it is generally acknowledged that they
work well when:
1) There is a large abstraction gap between the specification and
implementation. (e.g. specifications about real numbers and
implementations with bit-vectors).
2) Regularity in the structure of the circuit can be used to
decompose the problem into smaller pieces. (e.g. n-bit adders,
multipliers, networks, etc)
3) A common structure appears in a class of circuits or a reasoning
approach is applicable a class of circuits. (e.g. Microprocessors)
Theorem proving based methods have not been as successful at reasoning
effectively about properties like set-up and hold times as
conventional tools such as timing analyzers have been. That doesn't
mean that theorem-proving based methods are ineffective in general,
just that they are not a panacea. Conventional simulation,
model-checkers and other automated tools can bang out many circuits
must faster than any proof system could. But, there are examples,
such as those that have been mentioned by others here, and which I
believe fall into the categories I've listed above, where
theorem-proving based methods are very effective.
As designs get more and more sophisticated, simulation times increase
to the point where engineers choose not to implement proposed designs
because the verification effort would be too costly. As an example,
the MIPS R8000 design team chose in-order (rather than out-of-order)
instruction issue and completion for their integer pipeline [Hsu93].
These types of design complexities are prime targets for
theorem-proving based methods --- no other known techniques have a
chance of solving them.
(As a blatant and self-serving plug for my own work, I've developed
some verification techniques for pipelined circuits. This work provides
systematic ways of decomposing some of the large and complex
verification problems (which can not be handled by conventional or
model-checking techniques) into relatively small and straightforward
tasks that can be handled by such automated tools [AL94].)
- - - - - -
Addressing the second point:
(The second point is actually due to Phil Windley.) As one piece of
evidence, at Theorem Provers in Circuit Design 94, 10 out of the 18
papers described techniques for simplifying verification efforts. In
1992 less than 1/4 of the papers focused on this topic.
As Phil has pointed out here, he routinely teaches students to verify
microprocessors that several years ago would have required a great
deal of effort by an expert. Advances such as these are possible
because we have gained enough experience with virtuoso verification to
recognize patterns and similarities between different examples. An
earlier example along these lines is Tom Melham's type definition
package for HOL. Before this package was available, defining a new
recursive type in HOL required intimate knowledge of the logic. Now,
it is almost as easy as defining a new type in a functional
programming language. In hardware verification, Phil's abstract
interpreter package for microprocessors, which students in his class
rely on, is a good example. The hardware tactics that Miriam Leeser
mentioned also fit into this category.
-mark aagaard
aagaard@cs.ubc.ca
@inproceedings{[AL94],
author = {Aagaard, Mark D. and Leeser, Miriam E.},
title = {Reasoning About Pipelines with Structural Hazards},
booktitle = tpcd-94,
year = 1994,
month = sep,
publisher = springer-verlag,
editor = {Kumar, Ramayya and Kropf, Kumar},
}
Available by ftp as
ftp://tesla.ee.cornell.edu/pub/hw-verify/pipes-tpcd94.ps.Z
[Hsu93]
http://www.mips.com/HTMLs/r8000_docs/Micro_Paper/R8000_Micro_Paper_cv.html