Arm: Efficient and exhaustive floating point verification using sequential equivalence checking

Sequential Equivalence Checking is the process of proving formal equivalence between two non-state matching implementations of a given design specification. Nowhere has the VLSI industry adopted this technology as much as to prove the correctness of floating point designs against a given reference model. Any error in floating point operations can have severe consequences. ARM and Siemens EDA have partnered to undertake the formal verification of some of the most difficult floating point blocks, including FMUL, FMA, FDIV, and FSQRT, in their CPU designs. We also worked outside the FPU, on a Branch Predictor from the same CPU designs.

This paper will introduce a formal sequential equivalence checking tool and present how it is used. It will talk about the models used for comparison. It will talk about the FPU operations, and then discuss in varying levels of detail what we did to perform the equivalence check on FPU format conversions, FADD, FMUL, FMA, FDIV, and FSQRT. We then branch out to describe the formal equivalence check we did on a Branch Predictor from the same CPU design and the results are summarized. Formal verification’s place in methodology is touched on and we describe our ongoing work.