使用 RTL 书籍自动化乘法树证明
计算机科学中的逻辑
2025-07-28 v1 符号计算
摘要
我们提出了一个实验性的、在 ACL2 中验证的子句处理器 ctv-cp，它融入了 Arm 用于形式化验证算术硬件设计的框架。这大大自动化了来自浮点除法到矩阵乘法等设计范围内整数乘法模块的 ACL2 证明开发工作。
引用
@article{arxiv.2507.19010,
title = {On Automating Proofs of Multiplier Adder Trees using the RTL Books},
author = {Mayank Manjrekar},
journal= {arXiv preprint arXiv:2507.19010},
year = {2025}
}
备注
In Proceedings ACL2 2025, arXiv:2507.18567