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