- Travis W. Pouarz - Mentor Graphics
- Vaibhav Agrawal - ARM® Inc.
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 correctness of floating point designs against a given reference model. Any error in floating point operations can have severe consequences. ARM and Mentor 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 a partnership with Calypto Design Systems (now a division at Mentor Graphics) 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, Mentor 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.
View & Download:
Read the entire Efficient and Exhaustive Floating Point Verification Using Sequential Equivalence Checking technical paper.