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.

翻译：在许多定点乘法实例中，并不需要全精度结果，返回保真舍入结果即可满足要求。保真舍入允许机器可表示数取在全精度结果上方或下方最近的可表示数（若全精度结果无法精确表示）。充分利用这一灵活性的乘法器可通过更小的电路面积和更低的功耗实现。最常见的实现方式是对部分积阵列进行内部截断。然而，将截断应用于最常用的乘法器架构（即Booth架构）会导致非可交换的实现。此类实现的工业应用受限于缺乏形式化验证（因为穷举仿真通常不可行）。本文提出一种可交换截断Booth乘法器架构，并推导出保真舍入的闭式充要条件。我们还给出了产生最坏情况误差的位向量，并基于ACL2提出了一种可扩展至42位乘法器的形式化验证方法。通过综合一系列可交换保真舍入乘法器，我们证明截断Booth实现的面积比外部截断乘法器最多可缩小31%。