Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <11639.9501301042@frogland.inmos.co.uk>
Subject: Science article & Pentiums
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Mon, 30 Jan 1995 10:42:38 +0000 (GMT)
Content-Type: text
Content-Length: 1812

Tim Leonard, DTN 225-5809, HLO2-3/C11 has said:
> This week's issue of Science (20 January 1995, pp332-333) has an article about
> formal verification, using the Pentium bug to illustrate the need.  Though it
> mentions interactive theorem proving, the emphasis is on model checking, and
> BDD-based methods.  It includes the textual equivalent of sound bites from 
> Pixley, Kurshan, Rushby, Boyer, Clarke, Bryant, Dill, and others.

Not wanting to start a major Pentium discussion again, but 2 interesting
recent items.

1) I'm sure many of you know this but Intel have written off $306 million
to cover Pentium replacements.

2) The Pentium bug seems to have become part of "common knowledege". An news
article in a paper a few days ago about some new super computer just installed
in the UK (I suspect it was claimed to be the UKs most powerful computer)
ended with the line "Let's hope it isn't made of buggy Pentium chips".
Also talking to someone over the weekend who while having a Scientific/engineering
background has been a priest in the Church of England for many years I was
describing the sort of work I do and as soon as I mentioned checking that
designs did what they were meant to he immediately came back with "not like
that Pentium chip then!".

Perhaps Intel will do a remaining exercise and go back to the 686 for then
next one .... "Pentium ... can't be one of ours, all our
chips end in 86".

--------------------------------------------------------------------------
                               david shepherd
 SGS-THOMSON Microelectronics Ltd, 1000 aztec west, bristol bs12 4sq, u.k.
          tel/fax: +44 1454 611638/617910    email: des@inmos.co.uk
               www: http://www.inmos.co.uk/~des/welcome.html
       "whatever you don't want, you don't want negative advertising"