Mechanically verifying a family of multiplier circuits
The work
| Authors | Deepak Kapur; M. Subramaniam |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1996 |
| Citekey | kapur1996mechanically |
Where it appeared
| Published in | Computer Aided Verification (CAV) |
|---|---|
| Publisher | Springer Berlin Heidelberg |
| Pages | 135--146 |
Identifiers
| DOI | 10.1007/3-540-61474-5_64 |
|---|---|
| ISSN | 0302-9743 |
| ISBN | 978-3-540-61474-6 |
Access
| Landing page | https://doi.org/10.1007/3-540-61474-5_64 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/3-540-61474-5_64.pdf |
Related
| Distinct from | bryant1986graphbased |
|---|---|
| Distinct from | burch1992symbolic |
| Distinct from | kocher1996timing |
| Distinct from | manjrekar2025automating |
| Distinct from | yang2025forword |
From crossref.
Abstract
A methodology for mechanically verifying a family of parameterized multiplier circuits, including many well-known multiplier circuits such as the linear array, the Wallace tree and the 7-3 multiplier is proposed. A top level specification for these multipliers is obtained by abstracting the commonality in their behavior. The behavioral correctness of any multiplier in the family can be mechanically verified by a uniform proof strategy. Proofs of properties are done by rewriting and induction using an automated theorem prover RRL (Rewrite Rule Laboratory).
A copy is held
pdf, 1001.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-16 18:34 UTC |
| Approved by | a person 2026-09-16 20:47 UTC |
Filed under
Cite it as
@inproceedings{kapur1996mechanically,
title = {Mechanically verifying a family of multiplier circuits},
author = {Deepak Kapur and M. Subramaniam},
year = {1996},
booktitle = {Computer Aided Verification (CAV)},
publisher = {Springer Berlin Heidelberg},
pages = {135--146},
isbn = {978-3-540-61474-6},
issn = {0302-9743},
doi = {10.1007/3-540-61474-5_64},
}
This record lives at https://refs.drheap.org/kapur1996mechanically/ and will keep doing so.