On Automating Proofs of Multiplier Adder Trees using the RTL Books

Manjrekar, Mayank

doi:10.4204/EPTCS.423.5

计算机科学 > 计算机科学中的逻辑

arXiv:2507.19010v1 (cs)

[提交于 2025年7月25日 ]

标题：使用 RTL 书籍自动证明乘法器加法树

标题： On Automating Proofs of Multiplier Adder Trees using the RTL Books

Authors:Mayank Manjrekar (Arm Inc.)

摘要：我们提出了一种实验性且经过验证的子句处理器 ctv-cp，它适用于 Arm 用于算术硬件设计形式验证的框架。这大大自动化了针对整数乘法模块的 ACL2 证明开发工作，这些模块存在于从浮点除法到矩阵乘法的各种设计中。

摘要： 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.

评论：	在ACL2 2025会议论文集中，arXiv:2507.18567
主题：	计算机科学中的逻辑 (cs.LO) ; 符号计算 (cs.SC)
引用方式：	arXiv:2507.19010 [cs.LO]
	(或者 arXiv:2507.19010v1 [cs.LO] 对于此版本)
	https://doi.org/10.48550/arXiv.2507.19010
期刊参考：	EPTCS 423, 2025, pp. 51-55
相关 DOI:	https://doi.org/10.4204/EPTCS.423.5

提交历史

来自： EPTCS [查看电子邮件]
[v1] 星期五， 2025 年 7 月 25 日 07:07:28 UTC (27 KB)

全文链接：

获取论文：

查看许可

当前浏览上下文:

cs.LO

新的 | 最近的 | 2025-07

切换浏览方式为:

cs
cs.SC

参考文献与引用

导出 BibTeX 引用

计算机科学 > 计算机科学中的逻辑

标题：使用 RTL 书籍自动证明乘法器加法树

标题： On Automating Proofs of Multiplier Adder Trees using the RTL Books

提交历史

获取论文：

参考文献与引用

收藏

文献和引用工具

与本文相关的代码，数据和媒体

演示

推荐器和搜索工具

arXivLabs：与社区合作伙伴的实验项目

计算机科学 > 计算机科学中的逻辑

标题： 使用 RTL 书籍自动证明乘法器加法树 显示英文标题

标题： On Automating Proofs of Multiplier Adder Trees using the RTL Books

提交历史

获取论文：

参考文献与引用

BibTeX 格式的引用

收藏

文献和引用工具

与本文相关的代码，数据和媒体

演示

推荐器和搜索工具

arXivLabs：与社区合作伙伴的实验项目

标题：使用 RTL 书籍自动证明乘法器加法树