Formally verifying graphics fpu an intel® experience

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

doi:10.1007/978-3-319-06410-9_45

Formally verifying graphics fpu an intel^® experience

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Scopus citations

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 language	English (US)
Title of host publication	FM 2014
Subtitle of host publication	Formal Methods - 19th International Symposium, Proceedings
Publisher	Springer Verlag
Pages	673-687
Number of pages	15
ISBN (Print)	9783319064093
DOIs	https://doi.org/10.1007/978-3-319-06410-9_45
State	Published - Jan 1 2014
Externally published	Yes
Event	19th International Symposium on Formal Methods, FM 2014 - Singapore, Singapore Duration: May 12 2014 → May 16 2014

Publication series

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

Other

Other	19th International Symposium on Formal Methods, FM 2014
Country/Territory	Singapore
City	Singapore
Period	5/12/14 → 5/16/14

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-06410-9_45

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

@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.",

author = "Aarti Gupta and Kirankumar, {M. V.Achutha} and Rajnish Ghughal",

year = "2014",

month = jan,

day = "1",

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",

}

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

Formally verifying graphics fpu an intel^® experience. / Gupta, Aarti; Kirankumar, M. V.Achutha; Ghughal, Rajnish.

FM 2014: Formal Methods - 19th International Symposium, Proceedings. Springer Verlag, 2014. p. 673-687 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8442 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Formally verifying graphics fpu an intel® experience

AU - Gupta, Aarti

AU - Kirankumar, M. V.Achutha

AU - Ghughal, Rajnish

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84958531720&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84958531720&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-06410-9_45

DO - 10.1007/978-3-319-06410-9_45

M3 - Conference contribution

AN - SCOPUS:84958531720

SN - 9783319064093

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 673

EP - 687

BT - FM 2014

PB - Springer Verlag

T2 - 19th International Symposium on Formal Methods, FM 2014

Y2 - 12 May 2014 through 16 May 2014

ER -