Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Mon, 12 Dec 1994 10:58:46 +0000
Received: from localhost (listserv@localhost) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) id EAA27660 for qed-out;
          Mon, 12 Dec 1994 04:52:13 -0600
Received: from oberon.inmos.co.uk (oberon.inmos.co.uk [192.26.234.4]) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id EAA27655 
          for <qed@mcs.anl.gov>; Mon, 12 Dec 1994 04:52:06 -0600
Received: from frogland.inmos.co.uk by oberon.inmos.co.uk;
          Mon, 12 Dec 1994 10:52:00 GMT
From: David Shepherd <des@inmos.co.uk>
Message-Id: <5639.9412121046@frogland.inmos.co.uk>
Subject: Re: Hardware verification
To: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Mon, 12 Dec 1994 10:46:07 +0000 (GMT)
Cc: qed@mcs.anl.gov
In-Reply-To: <199412112347.QAA01406@chelm.nmt.edu> from "Victor Yodaiken" at Dec 11, 94 04:47:01 pm
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 2667
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

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!

However there were some interesting issues

1) In work on a software implementation of IEEE 754 the person doing it
tested it against an 8087 ... this showed up errors in the
implementation but also showed up what we considered to be a class of
errors in the 8087 - if I recall correctly then I think it was
something like denormed multiply results seemed to get rounded twice (I
suspect once after the multiplication and then again after
denormalisation)

2) While this was happening some people at Oxford PRG specified the
IEEE standard and produced an implementation and (hand) sketch proof
which actually overtook the INMOS testing.

3) I managed to show that the INMOS and Oxford software implementations
were equivalent. Meanwhile the Oxford people took our code and found
several bugs in it - it turned out that they'd been given "old"
code and they'd found several "known bugs".

4) On the T800 I verified the microcode - however we still had
some small problems due to subsequent "transcription" errors

i) we used an awk-like tool to translate from "occam-microcode" into
the microcode assembly language - one pattern was slightly wrong which
caused a single microword to be mistranslated.

ii) The translation created  microcode instruction names which were
basically <instname>-<num> - the person doing the testing demanded
"informative" names and in the process the fpgt instruction got
mangled and became ">" on different signed argumenst and "<="
on the same sign.

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
they'd have found the fdiv error very quickly.

--------------------------------------------------------------------------
david shepherd:                           sgs-thomson microelectronics ltd 
email:des@inmos.co.uk                                      1000 aztec west
tel: 01454-616616 x 638                                        almondsbury
www: http://www.inmos.co.uk/~des/welcome.html                      bristol
                                                                  bs12 4sq
"whatever you don't want, you don't want negative advertising"          uk