From owner-qed Mon Nov 21 22:47:43 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id WAA00800 for qed-out; Mon, 21 Nov 1994 22:47:09 -0600 Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id WAA00795 for ; Mon, 21 Nov 1994 22:47:03 -0600 Received: from puma.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA27348; Mon, 21 Nov 1994 21:50:01 -0700 Received: from localhost by puma.cs.byu.edu (1.38.193.4/CS-Client) id AA08328; Mon, 21 Nov 1994 21:51:46 -0700 Message-Id: <9411220451.AA08328@puma.cs.byu.edu> To: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Cc: mel@ee.cornell.edu, qed@mcs.anl.gov Subject: Re: The Pentium chip wasn't verified In-Reply-To: Your message of Mon, 21 Nov 1994 16:48:39 -0700. <199411212348.QAA01251@chelm.nmt.edu> Date: Mon, 21 Nov 1994 21:51:46 -0700 From: "Phil Windley" Sender: owner-qed@mcs.anl.gov Precedence: bulk On Mon, 21 Nov 1994 16:48:39 -0700 Victor Yodaiken writes +-------------------- | As Cohn's paper noted, "verification" means different things to different | people. Granted. | "Verifying" the behavior of a very simplified textbook example that | omits, for example, the complex timing that makes these things | tough is still the material of research papers. 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. | Nice html document too. But it is important to note the immense | gap between a verification of an example pipeline when such issues | as setup time and interrupts are abstracted out and a | verification of an actual processor. Does your pipleline allow | forwarding? Aliasing? Branch predication? Yes, yes, and see Mike Coe's thesis (in ftp://lal.cs.byu.edu/pub/hol/lal-papers) for the third. Interrupts are are also covered in Mike's work. | Do you teach them to verify that the block description is an | accurate model of the lower level circuit behavior? Do you teach them | to verify correctness of interrupt operation? Do you teach them to | verify that setup times are always respected and that the memory | interface is properly designed? What does "verify" mean in this | situation? The word verify *is* imprecise. One needs to talk about correctness models in detail. In this stiuation it means that the RTL description of the electronic block model correctly implements the instruction set semantics. Going below the EBM is important and a number of people (including us) are working on this. As I said before, I'm not claiming that everything has been worked out, but 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. --phil--