On the Systematic Creation of Faithfully Rounded Commutative Truncated Booth Multipliers

TL;DR

This paper introduces a formal, scalable method for designing and verifying faithful, commutative truncated Booth multipliers that are smaller and more efficient than traditional implementations, with proven correctness.

Contribution

It presents a formal verification framework and a new architecture for faithful, commutative truncated Booth multipliers, enabling smaller and verified fixed-point multipliers.

Findings

Truncated Booth multipliers can be up to 31% smaller than traditional implementations.

A formal verification methodology using ACL2 scales to 42-bit multipliers.

Derived necessary and sufficient conditions for faithful rounding in these multipliers.

Abstract

In many instances of fixed-point multiplication, a full precision result is not required. Instead it is sufficient to return a faithfully rounded result. Faithful rounding permits the machine representable number either immediately above or below the full precision result, if the latter is not exactly representable. Multipliers which take full advantage of this freedom can be implemented using less circuit area and consuming less power. The most common implementations internally truncate the partial product array. However, truncation applied to the most common of multiplier architectures, namely Booth architectures, results in non-commutative implementations. The industrial adoption of truncated multipliers is limited by the absence of formal verification of such implementations, since exhaustive simulation is typically infeasible. We present a commutative truncated Booth multiplier architecture and derive closed form necessary and sufficient conditions for faithful rounding. We also provide the bit-vectors giving rise to the worst-case error. We present a formal verification methodology based on ACL2 which scales up to 42 bit multipliers. We synthesize a range of commutative faithfully rounded multipliers and show that truncated booth implementations are up to 31% smaller than externally truncated multipliers.