Statement for the 21st Century Engineering Consortium

Warren Hunt
IBM Austin
February 1998

[excerpt of a message to a CAV98 panel]

I consider theorem proving and its application to industrial design to
be a fundamentally different paradigm than that currently practiced by
industry.  At IBM we invest heavily in models (Spice, differential
equations, VHDL, etc.) but there is almost no use of analysis.  That
is, we often write equations (both continuous and discrete) but we do
not manipulate (integrate, rewrite, etc.) them.  We do, however,
perform extensive simulation.

I often explain our use of models to IBM management within a high
school calculus framework.  Imagine that some design could be modeled
by a differential equation, and that the correctness of this design
could be checked by determining whether the integral of this equation
(model) is greater than zero on some interval.  At IBM we would check
this by using rectangle approximation (simulation).  Any engineer can
do this, and it is relatively straightforward to build tools to
perform rectangle approximation for well-behaved equations.  It is
much more difficult, especially with large models, to instead
integrate a complex equation on the open interval and then evaluate
this integral on the interval of interest.  I liken integration for
continuous mathematics to that of theorem proving for discrete logics.

Integration is fundamentally different than rectangle approximation.
The value of performing the integral is that an exact answer (assuming
the integral can be computed) can be found for the area under any part
of the curve.  Our rectangle approximation approach works adequately
for well-behaved equations, but can give poor results when the
equations are not so well-behaved.  In fact, large parts of the area
may be completely ignored if we do not use a fine enough delta when
computing the area.  The problem of performing an integration is that
it requires a profound understanding of the mathematics represented by
the equation to be integrated.  This is also true when analyzing
discrete formulas; that is, proving correctness of some FSM model may
require a deep understanding of the operations being performed by the
FSM model.

For some parts of calculus (such as simple polynomials) we can write a
program that automatically perform integration.  In the
theorem-proving community we have written such programs (e.g.,
equivalence checkers, model checkers).  However, we have no program to
integrate an arbitrary equation nor do we have a theorem prover that
can determine the validity of an arbitrary discrete model.  At some
point our tools become only tactical mechanical assistants for which
we must provide the strategy.

Unfortunately, this is not the message that industrial management
wants to hear about applying theorem proving to design.  Industry is
driven by cost.  That is, will some approach to design be more cost
effective than another?  A manager is very reluctant to change how
things are done unless there is some kind of cost advantage.
Regarding equivalence checking, this has been demonstrated at IBM; it
is cheaper to use equivalence checking to see if transistor nests
implement some Boolean function than using exhaustive simulation.  Can
we expand from this point?  I surely hope so.  The industrial use of
model-checking is helping.

...think about
how we can make theorem-proving the cheapest way to perform design.
Why is it considered so expensive?  Should we concentrate on
specification only?  In other words, how can we make theorem proving
the most cost effective way of performing design?  What elements would
such a framework contain?  I know that these questions may lead us to
consider other issues.  For instance, what university-level (and
high-school) courses should be taught to ensure an expanding group of
available practitioners?

...