On Automating Proofs of Multiplier Adder Trees using the RTL Books

TL;DR

This paper introduces ctv-cp, an automated clause processor integrated into Arm's verification framework, significantly streamlining the formal verification process for complex arithmetic hardware modules.

Contribution

It presents a verified, automated clause processor that reduces manual effort in formal proofs of arithmetic hardware designs within a widely used verification environment.

Findings

Automates ACL2 proof development for integer multipliers

Integrates into Arm's existing verification framework

Reduces manual proof effort and increases verification efficiency

Abstract

We present an experimental, verified clause processor ctv-cp that fits into the framework used at Arm for formal verification of arithmetic hardware designs. This largely automates the ACL2 proof development effort for integer multiplier modules that exist in designs ranging from floating-point division to matrix multiplication.