Arm: Efficient and Exhaustive Floating Point Verification using Sequential Equivalence Checking

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.

Back in 1995, the Pentium FDIV bug cost Intel $475 million. Today, the industry does not have any appetite for floating-point (FP) bugs. Given this expectation, and the astronomical number of input operand combinations required to exhaustively validate these operations, simulation-based verification cannot suffice. For example, exhaustive simulation of operations requiring two 16-bit Half Precision input operands takes 150 days of CPU time. For operations requiring two 32-bit Single Precision (SP) input operands, exhaustive simulations are impossible and 64-bit double precision (DP) are much worse.¹

Thus, all CPU/GPU design companies have explored Formal Techniques in some form for exhaustive FP verification. Intel has been the pioneer in this domain, developing and using internal tools and technologies. However, in the last decade, with the availability of sequential equivalence checking (SEC) as a formal technology² from the big-three EDA vendors and other EDA players, the industry has seen a trend toward the use of SEC to prove equivalence of FP designs against C/C++/SystemC reference models for operations (like FADD, FMUL, FDIV, FSQRT and FDIV). The FP designs in the high-end Cortex® A-class CPUs from ARM® (e.g. Cortex A72) use interesting algorithms and design techniques to meet aggressive power, performance and area (PPA) targets.

This makes for a strong case for exhaustive verification of these designs using formal techniques. In 2014, ARM began apartnership with Calypto Design Systems (now a division at Siemens Digital Industries Software) to explore using SLEC (the division’s sequential equivalence checking tool) to formally verify these designs. The golden reference models were extracted from an architectural C/C++ model developed and owned by ARM. Over the past 2 years, Siemens and ARM have worked together to prove different FP operations across 4 generations of high end Cortex A-class ARM CPUs (starting with Cortex A72). In the latest generation, so far, we have managed to prove single precision (SP) and double precision (DP) FMUL, SP/DP FDIV, SP FSQRT and SP FMA.

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.