Editing Pentium FDIV bug (section)

==Discovery and response==
Thomas Nicely, a professor of mathematics at Lynchburg College, had written code to enumerate [[prime number|primes]], [[twin prime]]s, [[prime triplet]]s, and [[prime quadruplet]]s. Nicely noticed some inconsistencies in the calculations on June 13, 1994, shortly after adding a Pentium system to his group of computers, but was unable to eliminate other factors (such as programming errors, [[motherboard]] chipsets, etc.) until October 19, 1994.<ref name="siam"/> On October 24, 1994, he reported the issue to Intel.<ref name="NicelyFAQ">{{cite web|url=http://www.trnicely.net/pentbug/pentbug.html|title=Pentium FDIV flaw FAQ|author=Nicely|first=Thomas|date=August 19, 2011|website=trnicely.net|archive-url=https://web.archive.org/web/20190618044444/http://www.trnicely.net/pentbug/pentbug.html|archive-date=June 18, 2019|url-status=dead|access-date=June 18, 2019}}</ref> Intel had reportedly become aware of the issue independently by June 1994, and had begun fixing it at this point, but chose not to publicly disclose any details or recall affected CPUs.<ref name="nytcompany">{{cite web |last1=Markoff |first1=John |title=COMPANY NEWS; Flaw Undermines Accuracy of Pentium Chips |url=https://www.nytimes.com/1994/11/24/business/company-news-flaw-undermines-accuracy-of-pentium-chips.html |website=The New York Times |access-date=April 11, 2021 |date=November 24, 1994 |archive-date=August 14, 2024 |archive-url=https://web.archive.org/web/20240814063016/https://www.nytimes.com/1994/11/24/business/company-news-flaw-undermines-accuracy-of-pentium-chips.html |url-status=live }}</ref>

On October 30, 1994, Nicely sent an email describing the bug to various academic contacts, requesting reports of testing for the flaw on [[Intel 80486DX4|486-DX4s]], Pentiums and [[Pentium compatible processor|Pentium clones]].<ref name="NicelyFAQ" /> The bug was quickly verified by others, and news of it spread quickly on the [[Internet]]. The bug acquired the name "Pentium FDIV bug" from the [[x86 instruction listings|x86 assembly language mnemonic]] for floating-point division, the most frequently used instruction affected.<ref name="NicelyFAQ" />

The story first appeared in the press on November 7, 1994, in an article in ''[[Electronic Engineering Times]]'', "Intel fixes a Pentium FPU glitch" by Alexander Wolfe,<ref>{{cite web|title=Intel fixes a Pentium FPU glitch|url=http://davefaq.com/Opinions/Stupid/Pentium.html#glitch|author=Alexander Wolfe|date=November 9, 1994|website=Electronic Engineering Times|access-date=January 19, 2011|archive-date=December 18, 2010|archive-url=https://web.archive.org/web/20101218150110/http://davefaq.com/Opinions/Stupid/Pentium.html#glitch|url-status=live}}</ref> and was subsequently picked up by [[CNN]] in a segment aired on November 22, 1994. It was also reported on by the ''New York Times'' and the ''Boston Globe'', making the front page in the latter.<ref name="nytcompany" /><ref name="clevemoler">{{cite web |last1=Moler |first1=Cleve |title=A Tale of Two Numbers |url=https://www.mathworks.com/content/dam/mathworks/tag-team/Objects/a/72895_92024v00Cleve_Tale_Two_Numbers_Win_1995.pdf |website=MATLAB News and Notes |publisher=MathWorks |access-date=April 21, 2021 |date=Winter 1995 |archive-date=August 14, 2024 |archive-url=https://web.archive.org/web/20240814062858/https://www.mathworks.com/content/dam/mathworks/tag-team/Objects/a/72895_92024v00Cleve_Tale_Two_Numbers_Win_1995.pdf |url-status=live }}</ref>

At this point, Intel acknowledged the floating-point flaw, but claimed that it was not serious and would not affect most users. Intel offered to replace processors to users who could prove that they were affected. However, although most independent estimates found that the bug would have a very limited impact on most users, it caused significant negative press for the company. During a 2019 talk, while reflecting on development of ''[[Quake_(video_game)|Quake]]'', [[John Romero]] described how frequently and persistently this bug could be reproduced by [[Michael Abrash]]. Abrash spent hours tracking down exact conditions needed to produce the bug, which would result in parts of a game level appearing unexpectedly when viewed from certain camera angles.<ref>{{cite web|url=https://www.youtube.com/watch?v=22FU31ZUgNA&t=1519|title=BTD12: The Programming Principles of Id Software|access-date=July 17, 2023|date=August 6, 2019|publisher=TNG Technology Consulting GmbH|archive-date=August 25, 2023|archive-url=https://web.archive.org/web/20230825100711/https://www.youtube.com/watch?v=22FU31ZUgNA&t=1519|url-status=live}}</ref> [[IBM]] paused the sale of PCs containing Intel CPUs, and Intel's stock price decreased significantly.<ref name="CRN">{{cite web |last1=Yeraswork |first1=Zewde |title=Lessons Learned: Pentium Flaws Aid Intel In Sandy Bridge Chipset Recall |url=https://www.crn.com/news/components-peripherals/229400535/lessons-learned-pentium-flaws-aid-intel-in-sandy-bridge-chipset-recall.htm |website=CRN |access-date=April 11, 2021 |date=March 30, 2011 |archive-date=August 14, 2024 |archive-url=https://web.archive.org/web/20240814063035/https://www.crn.com/news/components-peripherals/229400535/lessons-learned-pentium-flaws-aid-intel-in-sandy-bridge-chipset-recall |url-status=live }}</ref> The motive behind IBM's decision was questioned by some in the industry; IBM produced the [[PowerPC]] CPUs at the time, and potentially stood to benefit from any reputational damage to the Pentium or Intel as a company. However, the decision led to corporate buyers of PC equipment demanding replacements of existing Pentium CPUs, and soon afterwards other PC manufacturers began offering "no questions asked" replacements of flawed Pentium chips.<ref name="wsjhumblepie" />

The growing dissatisfaction with Intel's response led to the company offering to replace all flawed Pentium processors on request on December 20.<ref>{{cite web|url=http://findarticles.com/p/articles/mi_m0EIN/is_1994_Dec_20/ai_15939945 |archive-url=https://archive.today/20120710222033/http://findarticles.com/p/articles/mi_m0EIN/is_1994_Dec_20/ai_15939945 |url-status=dead |archive-date=July 10, 2012 |title=Intel adopts upon-request replacement policy on Pentium processors with floating point flaw; Will take Q4 charge against earnings |access-date=December 24, 2006 |date=December 20, 1994 |publisher=Business Wire }}</ref> On January 17, 1995, Intel announced a pre-tax charge of $475 million against earnings, ostensibly the total cost associated with replacement of the flawed processors.<ref name="NicelyFAQ" /> This is equivalent to ${{Format price|{{Inflation|US-GDP|475000000|1995}}}} in {{Inflation/year|US-GDP}}.{{Inflation/fn|US-GDP}} Intel was criticised for barring resellers and OEMs from participating in the recall program, requiring end-users to replace chips themselves. Intel's justification for this, posted on its support web page, was that "it is the individual decision of the end user to determine if the flaw is affecting their application accuracy".<ref name="CRN" />

A 1995 article in ''[[Science (journal)|Science]]'' describes the value of number theory problems in discovering computer bugs and gives the mathematical background and history of [[Brun's constant]], the problem Nicely was working on when he discovered the bug.<ref name="Cipra Pentium Bug">{{cite journal
|last= Cipra  |first= Barry Arthur  |author-link = Barry Arthur Cipra
 | date = January 13, 1995
 | title = How number theory got the best of the Pentium chip
 | journal = Science
 | volume = 267
 | issue = 5195
 | pages = 175
 | doi = 10.1126/science.267.5195.175
 | pmid = 17791336
|bibcode= 1995Sci...267..175C |s2cid= 19898103 }}</ref>

Intel's response to the FDIV bug has been cited as a case of the [[public relations]] impact of a problem eclipsing the practical impact of said problem on customers.<ref name="ieee">{{cite journal |last1=Price |first1=D. |title=Pentium FDIV flaw-lessons learned |journal=IEEE Micro |date=April 1995 |volume=15 |issue=2 |pages=86–88 |doi=10.1109/40.372360}}</ref> While most users were unlikely to encounter the flaw in their day-to-day computing, the company's initial reaction to not replace chips unless customers could guarantee they were affected caused pushback from a vocal minority of industry experts. The subsequent publicity generated shook consumer confidence in the CPUs, and led to a demand for action even from people unlikely to be affected by the issue. [[Andy Grove]], Intel's CEO at the time was quoted in ''The Wall Street Journal'' as saying "I think the kernel of the issue we missed ... was that we presumed to tell somebody what they should or shouldn't worry about, or should or shouldn't do".<ref name="wsjhumblepie" />

In the aftermath of the bug and subsequent recall, there was a marked increase in the use of [[formal verification]] of hardware floating point operations across the semiconductor industry. Prompted by the discovery of the bug, a technique applicable to the SRT algorithm called "word-level model checking" was developed in 1996.<ref name="wordlevel">{{cite book |last1=Clarke |first1=E. M. |last2=Khaira |first2=M. |last3=Zhao |first3=X. |title=Proceedings of the 33rd annual conference on Design automation conference - DAC '96 |chapter=Word level model checking---avoiding the Pentium FDIV error |date=1996 |pages=645–648 |doi=10.1145/240518.240640 |isbn=0897917790 |s2cid=2500033 |chapter-url=https://dl.acm.org/doi/10.1145/240518.240640 |access-date=April 29, 2021 |archive-date=April 29, 2021 |archive-url=https://web.archive.org/web/20210429164257/https://dl.acm.org/doi/10.1145/240518.240640 |url-status=live }}</ref> Intel went on to use formal verification extensively in the development of later CPU architectures. In the development of the [[Pentium 4]], [[symbolic trajectory evaluation]] and theorem proving were used to find a number of bugs that could have led to a similar recall incident had they gone undetected.<ref name="memcod">{{cite book |last1=O'Leary |first1=J. |title=Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04 |chapter=Formal verification in intel cpu design |date=2004 |pages=152 |doi=10.1109/MEMCOD.2004.1459841 |isbn=0-7803-8509-8 |chapter-url=https://www.computer.org/csdl/proceedings-article/memcod/2004/01459841/12OmNzBOimc |access-date=April 29, 2021 |archive-date=April 29, 2021 |archive-url=https://web.archive.org/web/20210429164258/https://www.computer.org/csdl/proceedings-article/memcod/2004/01459841/12OmNzBOimc |url-status=live }}</ref> The first Intel microarchitecture to use formal verification as the primary method of validation was [[Nehalem (microarchitecture)|Nehalem]], developed in 2008.<ref>{{cite journal |last1=Kaivola |first1=Roope |last2=Ghughal |first2=Rajnish |last3=Narasimhan |first3=Naren |last4=Telfer |first4=Amber |last5=Whittemore |first5=Jesse |last6=Pandav |first6=Sudhindra |last7=Slobodová |first7=Anna |last8=Taylor |first8=Christopher |last9=Frolov |first9=Vladimir |last10=Reeber |first10=Erik |last11=Naik |first11=Armaghan |title=Replacing Testing with Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation |journal=Computer Aided Verification |date=2009 |volume=5643 |pages=414–429 |doi=10.1007/978-3-642-02658-4_32 |doi-access=free }}</ref>