论文标题
已验证实施有效的术语培训算法，用于在ACL2上进行乘数验证
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2
论文作者
论文摘要
自动有效地验证乘数设计，尤其是通过可证明的正确方法，这是一个困难的问题。 我们展示了如何利用定理供惯例ACL2来实现有效的重写算法进行乘数设计验证。 通过对ACL2的功能和数据结构的基本了解，我们创建了一个经过验证的程序，该程序可以自动验证各种乘数设计的速度要比其他最新的工具快得多。此外，我们系统的用户可以灵活地更改目标设计的规范，以验证乘数的变化。我们讨论了在该计划的制定过程中所面临的挑战，以及有关效率和可验证性的关键实施细节。 那些计划在定理供奉献者上实施高效程序的人或希望在另一个系统上实施我们的乘数验证方法的人可能会受益于本文的讨论。
Automatic and efficient verification of multiplier designs, especially through a provably correct method, is a difficult problem. We show how to utilize a theorem prover, ACL2, to implement an efficient rewriting algorithm for multiplier design verification. Through a basic understanding of the features and data structures of ACL2, we created a verified program that can automatically verify various multiplier designs much faster than the other state-of-the-art tools. Additionally, users of our system have the flexibility to change the specification for the target design to verify variations of multipliers. We discuss the challenges we tackled during the development of this program as well as key implementation details for efficiency and verifiability. Those who plan to implement an efficient program on a theorem prover or those who wish to implement our multiplier verification methodology on a different system may benefit from the discussions in this paper.
