Automatic Verification of Floating Point Units

Floating Point Units (FPUs) pose a singular challenge for traditional verification methods, such as coverage driven simulation, given the large and complex data paths and intricate control structures which renders those methods incomplete and error prone. Formal verification (FV) has been successfully leveraged to achieve the high level of quality desired of these critical logics. Typically, FV-based approaches to verify FPUs rely on introducing higher level abstractions to allow reasoning. This however has to be done manually, and quickly becomes tedious for optimized bit level implementations on board high performance microprocessors. Automated formal methods working directly on the bit level and providing a full end-to-end check exist but are limited to single instructions (issued in an empty pipeline), hence lack in checking control aspects related to inter-instruction interactions, or pipeline control. In this paper we present an approach based on equivalence checking to overcome the single instruction limitation for automated bit level proofs in the formal verification of FPUs. The sequential execution of instructions is modeled by two instances of the design-under-test. One of the instances acts as a reference model for the other. This allows for large numbers of internal equivalences to be leveraged by equivalence checking techniques. We show that this method is capable of proving instruction sequences for industrial FPU designs. Together with a proof of correctness of individual instructions it guarantees correctness of the FPU design as a whole. In our experience this is a one of a kind approach to perform automated end-to-end verification of FPUs.