This paper presents the AMD-K7 IEEE 754 and x87 compliant floating point division and square root algorithms and implementation. The AMD-K7 processor employs an iterative implementation of a series expansion to converge quadratically to the quotient and square root. Highly accurate initial approximations and a high performance shared floating point multiplier assist in achieving low division and square root latencies at high operating frequencies. A novel time-sharing technique allows independent floating point multiplication operations to proceed while division or square root computation is in progress. Exact IEEE 754 rounding for all rounding modes and target precisions has been verified by conventional directed and random testing procedures, along with the formulation of a mechanically-checked formal proof using the ACL2 theorem prover.