From owner-qed Mon Nov 21 17:46:19 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id RAA28109 for qed-out; Mon, 21 Nov 1994 17:45:17 -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 RAA28104 for ; Mon, 21 Nov 1994 17:45:10 -0600 Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id QAA01251; Mon, 21 Nov 1994 16:48:39 -0700 Message-Id: <199411212348.QAA01251@chelm.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Mon, 21 Nov 1994 16:48:39 -0700 In-Reply-To: "Phil Windley" "Re: The Pentium chip wasn't verified" (Nov 21, 7:51am) reply_to: yodaiken@chelm.nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: "Phil Windley" , qed@mcs.anl.gov Subject: Re: The Pentium chip wasn't verified Cc: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Sender: owner-qed@mcs.anl.gov Precedence: bulk On Nov 21, 7:51am, "Phil Windley" wrote: Subject: Re: The Pentium chip wasn't verified >The state of the art has progressed significantly since Avra's paper. >Avra's work was state of the art for 1988. Much has changed. A number of >people are now routinely verifying pipelined uP's as complex as the MIPS >R2000. Superscalar pipeline verifications are on the horizon. As Cohn's paper noted, "verification" means different things to different people. >For an excellent paper about verifying uP's using model checking >technology, see Burch's (jrb@cadence.com) paper in CAV94. He has verified >the DLX uP from Hennesey and Patterson. "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. >I have a paper on using HOL to verify a 5 stage pipeline uP (similar to >DLX) at 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? >I routinely teach a class of graduate >students (with no previous verification experience) how to verify uP's as >complex as VIPER in a semester. 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?