Formally verifying graphics fpu an intel® experience

Aarti Gupta, M. V.Achutha Kirankumar, Rajnish Ghughal

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 Intel® 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.

Original languageEnglish (US)
Title of host publicationFM 2014
Subtitle of host publicationFormal Methods - 19th International Symposium, Proceedings
PublisherSpringer Verlag
Pages673-687
Number of pages15
ISBN (Print)9783319064093
DOIs
StatePublished - Jan 1 2014
Externally publishedYes
Event19th International Symposium on Formal Methods, FM 2014 - Singapore, Singapore
Duration: May 12 2014May 16 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8442 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other19th International Symposium on Formal Methods, FM 2014
CountrySingapore
CitySingapore
Period5/12/145/16/14

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formally verifying graphics fpu an intel<sup>®</sup> experience'. Together they form a unique fingerprint.

  • Cite this

    Gupta, A., Kirankumar, M. V. A., & Ghughal, R. (2014). Formally verifying graphics fpu an intel® experience. In FM 2014: Formal Methods - 19th International Symposium, Proceedings (pp. 673-687). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8442 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-06410-9_45