Re: The Pentium chip wasn't verified
Victor Yodaiken (yodaiken@sphinx.nmt.edu)
Sun, 20 Nov 1994 12:30:08 -0700
On Nov 20, 12:06am, chou@cs.ucla.edu 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.