From owner-qed Mon Nov 21 08:51:15 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id IAA18299 for qed-out; Mon, 21 Nov 1994 08:47:17 -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 IAA18293 for ; Mon, 21 Nov 1994 08:47:02 -0600 Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA05143; Mon, 21 Nov 1994 07:49:50 -0700 Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA05200; Mon, 21 Nov 1994 07:51:29 -0700 Message-Id: <9411211451.AA05200@jaguar.cs.byu.edu> To: qed@mcs.anl.gov Cc: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Subject: Re: The Pentium chip wasn't verified In-Reply-To: Your message of Sun, 20 Nov 1994 12:30:08 -0700. <199411201930.MAA00199@chelm.nmt.edu> Date: Mon, 21 Nov 1994 07:51:28 -0700 From: "Phil Windley" Sender: owner-qed@mcs.anl.gov Precedence: bulk On Sun, 20 Nov 1994 12:30:08 -0700 Victor Yodaiken writes +-------------------- | 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. 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. 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. I have a paper on using HOL to verify a 5 stage pipeline uP (similar to DLX) at ftp://lal.cs.byu.edu/pub/hol/lal-papers/pipeline.ps.gz (In HTML at http://lal.cs.byu.edu/people/windley/papers/pipeline/pipeline.html) Tahar (tahar@ira.uka.de) and Kumar (Karlsruhe) have verified the DLX uP. As I said, if your conception of the state of the art in uP verifiction is VIPER, you're out of date. uP's far beyond VIPER in complexity can now be verified with little problem. 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. Best Regards, --phil-- __________________________________________________________________________ Phillip J. Windley, Asst. Professor | windley@cs.byu.edu Laboratory for Applied Logic | Dept. of Computer Science, TMCB 3370 | Brigham Young University | Phone: 801.378.3722 Provo UT 84602-6576 | Fax: 801.378.7775 ------------------------------------------------------------------------ If you use WWW, I can be found here orhere.