Re: The Pentium chip wasn't verified

Victor Yodaiken (
Sun, 20 Nov 1994 12:30:08 -0700

On Nov 20, 12:06am, wrote:
Subject: Re: The Pentium chip wasn't verified
>There have been lots of work on verifying hardware using theorem
>provers, notably HOL. I'm not an expert on the subject, but I think
>browsing through the proceedings of HOL workshops and TPCD (Theorem
>Provers in Circuit Design) conferences of the last few years would
>give you a good idea about the state of the art.

The state of the art is, in a word, weak.
The Avra Cohn paper on the Viper chip is recommended
reading for anyone with illusions about the subject. For certain small
parts of the operation of some circuits, automated model checking has
some indications of being useful. Automated theorem proving is more
of a problem.