Formally verifying a floating-point division routine with Gappa – part 1
3 days ago
- #formal-verification
- #floating-point
- #Arm
- Arm Optimized Routines released optimized assembly-language routines for basic floating-point arithmetic under an open-source license.
- These routines perform operations like addition, multiplication, and division using only 32-bit integer instructions for Arm CPUs without hardware floating-point support.
- The double-precision division function 'ddiv' was polished and verified using formal verification tools like Gappa and Rocq, uncovering a bug in the original version.
- The 'ddiv' function implements IEEE 754-compliant double-precision floating-point division, handling special cases like NaNs, infinities, and denormalized numbers.
- The primary challenge in 'ddiv' is accurately computing the quotient of 53-bit mantissas using an approximate method involving Newton-Raphson iteration.
- The function starts with an 8-bit approximation from a lookup table and refines it through three Newton-Raphson iterations to achieve high precision.
- Gappa was used to verify the error bounds of the approximate method, ensuring compliance with IEEE 754 rounding requirements.
- The verification process involved modeling the machine code in Gappa, providing hints for algebraic rearrangements, and running 128 separate cases for the lookup table.
- A bug was found in the original 'ddiv' code during formal verification, highlighting the importance of rigorous testing.
- The final part of the calculation involved discarding low-order terms, requiring additional hints to Gappa for accurate error analysis.