Automatic verification of estimate functions with polynomials of bounded functions

The correctness of some arithmetic functions can be expressed in terms of the magnitude of errors. A reciprocal estimate function that returns an approximation of 1/x is such a function that is implemented in microprocessors. This paper describes an algorithm to prove that the error of an arithmetic function is less than its requirement. It divides the input domain into tiny segments, and for each segment we evaluate a requirement formula. The evaluation is carried out by converting an arithmetic function to what we call a polynomial of bounded functions, and then its upper bound is calculated and checked if it meets the requirement. The algorithm is implemented as a set of rewriting rules and computed-hints of the ACL2 theorem prover. It has been used to verify reciprocal estimate and reciprocal square root estimate instructions of one of the IBM POWER™ processors.