Speaker:
Mertcan Temel

Title:
Formal Verification of Fast Integer Multipliers

Abstract:
In this talk, we will show a way to verify fast integer multipliers
that adapt the Wallace tree structure. We offer a fully automated,
ACL2-based, architecture-independent method such that it is expected
to work for various multipliers with very little or no
intervention. This method yields results as fast as 50 seconds for
32x32-bit multiplication, and 60 minutes for 64x64-bit multiplication
with a 3-to-2 compressor. We will first review the fast multiplication
algorithms in a nutshell. Then, we will show the prominent ACL2
functions and lemmas. Finally, we will talk about the methods applied
that speed up the proofs.