In October 1994 Thomas Nicely, a professor of mathematics at Lynchburg College, found that his number-theory computations gave different answers on a Pentium than on other machines (fact C4). The cause was the processor's floating-point divider. It is the best-known escape in the industry, and one of the best documented.
What does the FDIV bug teach about where exhaustive and formal checks pay off?
Fact | Source |
|---|---|
The divider used the SRT algorithm, which picks each quotient digit from a lookup table indexed by bits of the partial remainder and divisor | Edelman, SIAM Review 1997 (fact C1) |
Some table entries were missing, so for rare operand pairs the divider chose a wrong digit and the quotient was wrong | Fact C1 |
Intel attributed it to five entries omitted by a script error; a 2024 die analysis found 16 missing, five of which trigger the bug | Fact C1 |
Tim Coe's example: 4195835 / 3145727 returned 1.333739... instead of 1.333820... | Fact C4 |
Intel offered unconditional replacements in December 1994 and took a pre-tax charge of about $475 million in January 1995 | Fact C1 |
Coe's operand pair, with the published flawed quotient, checked by multiplying back:
"""The Pentium FDIV bug: Tim Coe's operand pair (fact C4), checked two ways.
The flawed quotient below is the published value a flawed Pentium returned for
4195835 / 3145727. The check multiplies back: x - (x / y) * y should be 0.
"""
x, y = 4195835, 3145727
correct = x / y
flawed = 1.333739068902037589 # published result from a flawed Pentium
print(f"correct quotient {correct:.15f}")
print(f"flawed quotient {flawed:.15f}")
print(f"relative error {abs(flawed - correct) / correct:.1e}")
print(f"x - (x/y)*y correct {x - correct * y:.0f}, flawed {x - flawed * y:.0f}")
assert x - correct * y == 0 and x - flawed * y == 256
print("PASS: a one-line multiply-back check exposes the wrong quotient")It prints:
correct quotient 1.333820449136241
flawed quotient 1.333739068902038
relative error 6.1e-05
x - (x/y)*y correct 0, flawed 256
PASS: a one-line multiply-back check exposes the wrong quotientHow to read it: the error is in the fifth significant digit, far larger than any rounding error, and a one-line check that multiplies the quotient back exposes it. Detection was never the problem once the right operands were used. The problem was reaching those operands.
Rare triggers defeat random testing. If a random operand pair triggers a bug with probability p, the expected number of tests before the first hit, and the chance of missing it in N tests, are:
For a trigger that only a tiny fraction of operand pairs reach, even billions of random divisions can miss it. Lesson 4.5's long tail is the same arithmetic. And end-to-end tests of division exercise the table only indirectly, through whichever entries those operands happen to reach.
The table itself, however, is small and completely specified: each entry is defined by inequalities on the partial remainder and divisor. That makes it an ideal target for checks that do not depend on reaching rare operands:
Exhaustive check of the table: compare every entry with its mathematical definition; a few thousand comparisons.
Exhaustive or formal check of the digit selection: prove that for every reachable partial remainder the chosen digit keeps the next remainder in range.
Formal proof of the whole algorithm: the approach the industry adopted afterwards (fact C7).
The general lesson: where a structure is small and fully specified (tables, encoders, arithmetic units), check it completely rather than sample it. Random testing samples; exhaustive checking and formal proof cover.
Change | Source |
|---|---|
A mechanically checked proof of the AMD K5 floating-point division algorithm | Moore, Lynch and Kaufmann, 1998 (fact C7) |
Formal verification of divider circuits at Intel | Kaivola and Aagaard, 2000 (fact C7) |
Formal verification replacing much of the simulation-based validation of the Core i7 execution engine | Kaivola et al., CAV 2009 (fact C7) |
Floating-point units became one of the places where formal verification is now routine, which is lesson 7.5's point about where formal wins: small, well-specified, high-consequence blocks.
Question | Answer |
|---|---|
What failed? | Rare wrong quotients from missing lookup-table entries (documented) |
Where could it have been caught? | An exhaustive check of the table, or a formal proof of the division algorithm (the course's reading) |
Why was it not caught? | Unreached: rare triggers in random and end-to-end testing (the course's reading); the documented cause of the omission is a script error |
What changed? | Replacement, a $475 million charge, and formal verification of arithmetic as standard practice (documented) |
A simple multiply-back check shows the wrong quotient, but only for the rare operand pairs that reach the missing entries; random testing seldom reaches them.
It is small and each entry has a precise definition, so every entry can be compared with its definition in a few thousand checks, independent of how rarely operands reach it.
FDIV: missing lookup-table entries gave rare wrong quotients (documented).
Rare triggers defeat random testing; small fully specified structures should be checked completely.
Afterwards, formal verification of arithmetic units became standard practice.