Classic Round-Up Variant of Fast Unsigned Division by Constants: Algorithm and Full Proof

TL;DR

This paper presents a detailed analysis and proof of a classic algorithm for fast unsigned division by constants, including a simplified variant for bounded dividends, aiming to optimize division operations in hardware and software.

Contribution

It provides a full proof of correctness for the classic round-up variant of fast division by constants and introduces a simpler variant for bounded dividends.

Findings

Proves correctness of the classic division algorithm

Introduces a simplified division variant for bounded dividends

Enhances understanding of division optimization techniques

Abstract

Integer division instruction is generally expensive in most architectures. If the divisor is constant, the division can be transformed into combinations of several inexpensive integer instructions. This article discusses the classic round-up variant of the fast unsigned division by constants algorithm, and provides full proof of its correctness and feasibility. Additionally, a simpler variant for bounded dividends is presented.