Word Level Model Checking -- Avoiding the Pentium FDIV Error
The work
| Authors | E. M. Clarke; M. Khaira; X. Zhao |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1996 |
| Citekey | clarke1996word |
Where it appeared
| Published in | 33rd Design Automation Conference (DAC '96) |
|---|---|
| Publisher | ACM |
Identifiers
| DOI | 10.1145/240518.240640 |
|---|
Access
| Landing page | https://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Formally%20Verifying%20Arithmetic%20Circuits%20Avoiding%20the%20Pentium%20FDIV%20Bug.pdf |
|---|
Related
| Distinct from | bryant1991complexity |
|---|---|
| Distinct from | chakraborty2015wordlevel |
| Distinct from | chen1996verification |
| Distinct from | clarke1986automatic |
| Distinct from | jacobi2002formal |
| Distinct from | kaufmann2024extracting |
| Distinct from | kleinekathofer2026trace |
From bibtex.
Abstract
The highly-publicized division error in the Pentium has emphasized the importance of formal verification of arithmetic circuits. Symbolic model checking techniques based on binary decision diagrams (BDDs) have been successful in verifying control logic. However, lack of proper representation for functions that map boolean vectors into the integers has prevented this technique from being used for verifying arithmetic operations. We have developed a new technique for verifying arithmetic circuits. The new technique, called word level model checking, has been used successfully to verify circuits for division and square root computation that are based on the SRT algorithm used by the Pentium. The technique makes it possible to handle both the control logic and the data paths in the circuit. The total number of state variables exceeds 600 (which is much larger than any circuit previously handled by other symbolic model checkers).
A copy is held
pdf, 441.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 07:34 UTC |
| Approved by | a person 2026-09-23 14:08 UTC |
Cite it as
@inproceedings{clarke1996word,
title = {Word Level Model Checking -- Avoiding the Pentium FDIV Error},
author = {E. M. Clarke and M. Khaira and X. Zhao},
year = {1996},
booktitle = {33rd Design Automation Conference (DAC '96)},
publisher = {ACM},
doi = {10.1145/240518.240640},
}
This record lives at https://refs.drheap.org/clarke1996word/ and will keep doing so.