Formal verification of parametric multiplicative division implementations

Back in the 60´s Goldschmidt presented a variation of Newton-Raphson iterations for division that is well suited for pipelining. The problem in using Goldschmidt´s division algorithm is to verify that the implementation meets the precision required for the quotient and provides correct rounding, in particular if hardware resources are to be used judiciously. Previous implementations relied on error analysis that were not quite tight and that were specific to one parameter setting and target precision. Our formal verification effort focuses on a parametric division implementation based on Goldschmidt´s algorithm for different parameter settings and target precisions. We formalize a tight and parametric error analysis of Goldschmidt´s division algorithm in PVS and prove its correctness. On this basis we propose formally verified parametric division implementations.