Paul Rubin wrote:
> Kay Schluehr <[EMAIL PROTECTED]> writes:
>
>>When I remember correctly the FDIV bug was due to a wrongly filled
>>lookup table and occurred only for certain bitpattern in the divisor.
>>I'm not sure how a formal proof on the structure of the algorithm
>>could help here? Intel repaired the table i.e. the data not the
>>algorithm that acted upon it.
No, Intel had assumed a symmetry that wasn't actually true.
> I would expect the table contents to be part of the stuff being
> proved. I hear that they do use formal proofs for their floating
> point stuff now, as does AMD. AMD apparently uses ACL2 (a theorem
> prover written in Common Lisp, info about AMD is from the ACL2 web
> site) but I don't know what Intel uses. I've figured that the FDIV
> problem was one of the motivations for this but I'm not certain of it.
Yes, here's two of the papers describing proofs of AMD
floating point unit correctness.
Division: "http://citeseer.ist.psu.edu/53148.html";
Square root: "http://portal.acm.org/citation.cfm?id=607571";
A longer paper:
http://www.computationallogic.com/news/amd.html
This stuff is hard to do, but notice that AMD hasn't had any recalls
for floating point problems.
John Nagle
--
http://mail.python.org/mailman/listinfo/python-list
