Sciweavers

Share
ACL2
2006
ACM

Combining ACL2 and an automated verification tool to verify a multiplier

10 years 6 months ago
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
Erik Reeber, Jun Sawada
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ACL2
Authors Erik Reeber, Jun Sawada
Comments (0)
books