From owner-qed Sun Nov 20 02:08:52 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id CAA08158 for qed-out; Sun, 20 Nov 1994 02:06:41 -0600
Received: from maui.cs.ucla.edu (Maui.CS.UCLA.EDU [131.179.128.11]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id CAA08153 for <qed@mcs.anl.gov>; Sun, 20 Nov 1994 02:06:35 -0600
From: chou@cs.ucla.edu
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu
	(Sendmail 4.1/3.26) id AA06890;
	Sun, 20 Nov 94 00:06:25 PST
Message-Id: <9411200806.AA06890@maui.cs.ucla.edu>
To: beeson@cats.UCSC.EDU
Subject: Re: The Pentium chip wasn't verified
Cc: qed@mcs.anl.gov
Date: Sun, 20 Nov 94 00:06:23 PST
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


> I'm passing on a message I saw today, illustrating the potential
> applications of hardware verification.

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.

Cheers,
- Ching Tsun