Formally Verifying Graphics FPU: An Intel® Experience
The work
| Authors | Aarti Gupta; M. V. Achutha KiranKumar; Rajnish Ghughal |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2014 |
| Citekey | gupta2014formally |
Where it appeared
| Published in | International Symposium on Formal Methods |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 8442 |
| Pages | 673--687 |
Abstract
Verification of a Floating Point Unit (FPU) has always been a challenging task and its completeness is always a question. Formal verification (FV) guarantees 100% coverage and is usually the sign-off methodology for FPU verification. At Intel , Symbolic Trajectory Evaluation (STE) FV has been used for over two decades to verify CPU FPUs. With the ever-increasing workload share between core-CPU and Graphics Processing Unit (GPU) and the augmented set of data standards that GPU has to comply with, the complexity of graphics FPU is exploding. This has made use of FV imperative to avoid any bug escapes. STE which has proved to be the state of the art methodology for CPU’s FPU verification was leveraged in verifying IntelR ’s Graphics FPU. There were many roadblocks along the way because of the extra flexibility provided in graphics FPU instructions. This paper presents our experience in formally verifying the graphics FPU.
A copy is held
pdf, 753.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | import via bibtex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-26 15:20 UTC |
Cite it as
@inproceedings{gupta2014formally,
title = {Formally Verifying Graphics FPU: An Intel® Experience},
author = {Aarti Gupta and M. V. Achutha KiranKumar and Rajnish Ghughal},
year = {2014},
booktitle = {International Symposium on Formal Methods},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {673--687},
}
This record lives at https://refs.drheap.org/gupta2014formally/ and will keep doing so.