From owner-qed Wed Dec 14 09:57:19 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA00479 for qed-out; Wed, 14 Dec 1994 09:53:02 -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 JAA00474 for ; Wed, 14 Dec 1994 09:52:56 -0600 Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id IAA03005; Wed, 14 Dec 1994 08:56:27 -0700 Message-Id: <199412141556.IAA03005@chelm.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Wed, 14 Dec 1994 08:56:27 -0700 In-Reply-To: David Shepherd "Re: Hardware verification" (Dec 12, 10:46am) reply_to: yodaiken@chelm.nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: David Shepherd , yodaiken@sphinx.nmt.edu (Victor Yodaiken) Subject: Re: Hardware verification Cc: qed@mcs.anl.gov Sender: owner-qed@mcs.anl.gov Precedence: bulk On Dec 12, 10:46am, David Shepherd wrote: Subject: Re: Hardware verification >Victor Yodaiken has said: >> >> There is an interesting discussion on this issue in the RISKs forum. >> Does anyone know what INMOS got wrong in their floating point spec? > >Not sure we had anything wrong with our spec! In RISKS, Kahan was claimed to have said that INMOS got the spec wrong -- I have no idea what he meant or whether he would agree with this report. >5) The Pentium bug seems to have been caused by "missing entries" >in a division lookup table. I'm fairly certain that our production >testing used evaluations that would exercise every entry in our >division and multiply lookup tables - we caught some yield hazards >in revB that way (multiply table outputs were not fast enough in >75% of chips!) - if Intel had used this type of testthen surely So how much of the verification was testing and how much was mathematical proof?