On Automating Proofs of Multiplier Adder Trees using the RTL Books
The work
| Authors | Mayank Manjrekar |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2025 |
| Citekey | manjrekar2025automating |
Where it appeared
| Published in | Proceedings of the 19th International Workshop on the ACL2 Theorem Prover and Its Applications |
|---|---|
| Series | Electronic Proceedings in Theoretical Computer Science |
| Volume | 423 |
| Pages | 51--55 |
Identifiers
| arXiv | 2507.19010 from its landing_page_url |
|---|---|
| DOI | 10.4204/eptcs.423.5 |
Access
| Landing page | https://arxiv.org/abs/2507.19010 |
|---|
Related
| Distinct from | biere1999symbolic |
|---|---|
| Distinct from | bryant1986graphbased |
| Distinct from | bryant2018binary |
| Distinct from | gupta2014formally |
| Distinct from | kapur1996mechanically |
| Distinct from | lee2026formal |
| Distinct from | peng2015extending |
From bibtex.
Abstract
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.
A copy is held
pdf, 213.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 07:24 UTC |
| Approved by | a person 2026-09-16 09:05 UTC |
Cite it as
@inproceedings{manjrekar2025automating,
title = {On Automating Proofs of Multiplier Adder Trees using the RTL Books},
author = {Mayank Manjrekar},
year = {2025},
booktitle = {Proceedings of the 19th International Workshop on the ACL2 Theorem Prover and Its Applications},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {423},
pages = {51--55},
doi = {10.4204/eptcs.423.5},
}
This record lives at https://refs.drheap.org/manjrekar2025automating/ and will keep doing so.