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 ; 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