Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables

摘要: We present a comprehensive, self-contained, and mechanically verified proof of correctness maximally redundant SRT design for floating-point division square root extraction, supported by procedures that 1) test the admissibility proposed digit selection table, 2) determine minimal dimensions an admissible table given arbitrary radix, 3) generate these tables. For we also provide procedure generating initial approximation meets accuracy requirement algorithm ensures index derived from successive partial roots remains static throughout computation. A radix-8 instantiation algorithms has been implemented in unit AMD processor code-named Steamroller. To ensure their correctness, all our results have formalized checked ACL2 prover. evidence value this approach comparing it to more conventional published paper reports similar results, which are shown be fatally flawed.