@inproceedings{b4323224b38b4647b05624b23750a94b,
title = "Formally verifying graphics fpu an intel{\textregistered} experience",
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{\textregistered}, 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 Intel{\textregistered} 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.",
keywords = "Floating Point Unit, Formal verification, Graphics, Symbolic Trajectory Evaluation",
author = "Aarti Gupta and Kirankumar, \{M. V.Achutha\} and Rajnish Ghughal",
year = "2014",
doi = "10.1007/978-3-319-06410-9\_45",
language = "English (US)",
isbn = "9783319064093",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "673--687",
booktitle = "FM 2014",
address = "Germany",
note = "19th International Symposium on Formal Methods, FM 2014 ; Conference date: 12-05-2014 Through 16-05-2014",
}