Formally Verifying Graphics FPU An Intel~® Experience

摘要

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~®'s 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.