Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Sun, 20 Nov 1994 08:10:59 +0000
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