Formally Verifying Graphics FPU

Autor: Rajnish Ghughal, Aarti Gupta, M. V. Kirankumar
Rok vydání: 2014
Předmět:
Zdroj: Lecture Notes in Computer Science ISBN: 9783319064093
FM
Popis: 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.
Databáze: OpenAIRE