>It's my impression that applying theorem proving
>to any but the most trivial hardware now requires an immense effort and
>that there are important limitations on what can be modeled. The
>relative success of model checking methods and the incorporation
> of simulation and model checking into many of the "theorem proving"
>efforts indicates, to me, that the state of the art is still quite limited.
>That's not to say that no progress is being made and I'd be happy to
>find out that my impression is based on nothing more than outdated
>literature. In much of computer science, however,
>there is a tendency to overestimate progress, and the hardware verification
>community has not been an exception.
There have been great strides made in automating aspects of theorem
proving for specific tasks such as hardware verification. Much of the
"immense effort" you talk about is now taken care of by sophisticated
tactics. For example, Mark Aagaard, Phil Windley and I have written
tactics for both Nuprl and HOL that automate the proof of many
hardware modules between the RTL and the gate level. An n-bit adder
is one tactic application, an n-bit counter is currently two tactics.
The price you pay for this is having to specify hardware modules in a
way the tactics expect them. If you want the full flexibility of
theorem proving, you may lose some of the automation. We provide
tools that make the specification task easy, and have yet to find a
circuit at this level that we wanted to describe another way.
A hot research topic right now is combining theorem proving with other
tools such as model checking. I think this is recognition that you
should use the right tool for the job. Model checking does a good job
of automating state space exploration. Reasoning about finite state
machine logic will remain tedious in a theorem proving environment
because theorem provers are good at exploiting structure and
hierarchy, not reasoning about large amounts of random logic. On the
other hand, model checking breaks down with large regular structures,
especially those found in arithmetic circuits. SO the model checking
community is also turning to theorem proving to help solve their
problems.
With any approach, be it simulation, formal verification, etc. there
are limitations on what can be modeled. The problem with theorem
proving and hardware verification isn't so much what can be modeled,
as what is appropriate to spend time on. Detailed timing
analysis, for example can be specified in a theorem proving
environment, but other tools are much more appropriate for doing this
kind of reasoning.
The important thing, no matter what approach you take, is to be clear
about what it is you are modeling and what you are ignoring.
Miriam Leeser