Scalable Verification of a Generic End-Around-Carry Adder for Floating-Point Units by Coq
The work
| Authors | Qian Wang; Xiaoyu Song; William N. N. Hung; Ming Gu; Jiaguang Sun |
|---|---|
| Editors | |
| Type | article |
| Year | 2015 |
| Also known as | wang2014scalable |
| Citekey | wang2015scalable |
Where it appeared
| Published in | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
|---|---|
| Publisher | Institute of Electrical and Electronics Engineers |
| Volume | 34 |
| Issue | 1 |
| Pages | 150--154 |
Identifiers
| DOI | 10.1109/tcad.2014.2363391 |
|---|---|
| OpenAlex | W2002586923 |
Access
| Landing page | https://doi.org/10.1109/tcad.2014.2363391 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Theorem proving has been demonstrated as a powerful technique for datapath verification. This paper considers a generic logic-level architecture of end-around-carry adder, which is extensively used in floating-point arithmetic. The architecture is component-based and parameterized for easy customization. The design architecture is formalized and verified in the mechanical theorem prover Coq. The scalable proof provides necessary underpinnings for verifying customized and new implementations.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 02:05 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{wang2015scalable,
title = {Scalable Verification of a Generic End-Around-Carry Adder for Floating-Point Units by Coq},
author = {Qian Wang and Xiaoyu Song and William N. N. Hung and Ming Gu and Jiaguang Sun},
year = {2015},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
publisher = {Institute of Electrical and Electronics Engineers},
volume = {34},
number = {1},
pages = {150--154},
doi = {10.1109/tcad.2014.2363391},
}
This record lives at https://refs.drheap.org/wang2015scalable/ and will keep
doing so. It used to be called wang2014scalable, and those addresses still resolve to this one.