Combining ACL2 and an automated verification tool to verify a multiplier

We have extended the ACL2 theorem prover to automatically prove properties of VHDL circuits with IBM's Internal SixthSense verification system. We have used this extension to verify a multiplier used in an industrial floating point unit. The property we ultimately verify corresponds to the correctness of the component that produces a pair of bit-vectors whose summation is equal to the product. This property is beyond the scale of the SixthSense system alone. In this paper we show how we verified the multiplier by illustrating key ACL2 lemmas and theorems, and also properties checked by SixthSense. Categories and Subject Descriptors B.5.2 [Register-Transfer-level implementation]: Design Aids--Verification; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving--Deduction Keywords Hardware verification, theorem proving, model checking General Terms verification, design

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Erik Reeber, Jun Sawada
• Keywords: ACL2 2006, ACL2 Theorem Prover, Computational Linguistics, Internal SixthSense Verification, SixthSense