Formally verifying a floating-point division routine with Gappa – part 1
We have recently released a set of optimized assembly-language routines for basic floating-point arithmetic, in Arm Optimized Routines, under an open-source license. These functions perform the same operations as hardware floating point instructions, for example addition, multiplication, and division. However, they are implemented using only integer 32-bit Arm instructions, for Arm CPUs without hardware floating point. Existing open-source libraries such as libgcc and compiler-rt offer similar