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 -