From owner-qed Sun Nov 20 13:28:52 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA11414 for qed-out; Sun, 20 Nov 1994 13:26:43 -0600
Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id NAA11409 for <qed@mcs.anl.gov>; Sun, 20 Nov 1994 13:26:36 -0600
Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id MAA00199; Sun, 20 Nov 1994 12:30:08 -0700
Message-Id: <199411201930.MAA00199@chelm.nmt.edu>
From: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Sun, 20 Nov 1994 12:30:08 -0700
In-Reply-To: chou@cs.ucla.edu
       "Re: The Pentium chip wasn't verified" (Nov 20, 12:06am)
reply_to: yodaiken@chelm.nmt.edu
X-Mailer: Mail User's Shell (7.2.5 10/14/92)
To: chou@cs.ucla.edu, beeson@cats.UCSC.EDU
Subject: Re: The Pentium chip wasn't verified
Cc: qed@mcs.anl.gov
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

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.