From owner-qed Tue Nov 22 09:15:06 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA04800 for qed-out; Tue, 22 Nov 1994 09:11:08 -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 JAA04792 for ; Tue, 22 Nov 1994 09:11:00 -0600 Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id IAA01573; Tue, 22 Nov 1994 08:14:16 -0700 Message-Id: <199411221514.IAA01573@chelm.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Tue, 22 Nov 1994 08:14:16 -0700 In-Reply-To: "Phil Windley" "Re: The Pentium chip wasn't verified" (Nov 21, 9:51pm) reply_to: yodaiken@chelm.nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: "Phil Windley" , yodaiken@sphinx.nmt.edu (Victor Yodaiken) Subject: Re: The Pentium chip wasn't verified Cc: mel@ee.cornell.edu, qed@mcs.anl.gov Sender: owner-qed@mcs.anl.gov Precedence: bulk On Nov 21, 9:51pm, "Phil Windley" wrote: Subject: Re: The Pentium chip wasn't verified >Certainly, and I didn't claim that there was no more left to do. I merely >pointed out that 6 year old work wasn't the state of the art. Cohn's paper is not an uptodate survey of current work, but that's not why I mentioned it. >I do think that there are problems that can be solved now. Miriam Leeser >(of Cornell) has been doing work on verifying hardware much like the FP >hardware that caused the bug in the Pentium. I don't think that finding >such bugs is beyond the state of the art. It's my impression that applying theorem proving to any but the most trivial hardware now requires an immense effort and that there are important limitations on what can be modeled. The relative success of model checking methods and the incorporation of simulation and model checking into many of the "theorem proving" efforts indicates, to me, that the state of the art is still quite limited. That's not to say that no progress is being made and I'd be happy to find out that my impression is based on nothing more than outdated literature. In much of computer science, however, there is a tendency to overestimate progress, and the hardware verification community has not been an exception.