Use of Formal Verification at Centaur Technology
The work
| Authors | Warren A. Hunt; Sol Swords; Jared Davis; Anna Slobodova |
|---|---|
| Editors | David S. Hardin |
| Type | incollection |
| Year | 2010 |
| Citekey | hunt2010use |
Where it appeared
| Published in | Design and Verification of Microprocessor Systems for High-Assurance Applications |
|---|---|
| Publisher | Springer US |
| Pages | 65--88 |
Identifiers
| DOI | 10.1007/978-1-4419-1539-9_3 |
|---|---|
| OpenAlex | W2121127534 |
| ISBN | 978-1-4419-1538-2 |
Access
| Landing page | https://doi.org/10.1007/978-1-4419-1539-9_3 |
|---|
Related
| Distinct from | cohn1988correctness |
|---|---|
| Distinct from | davis2014microcode |
| Distinct from | gammie2013synchronous |
| Distinct from | gupta2014formally |
| Distinct from | hunt1994fm8501 |
| Distinct from | kaivola2015proceedings |
| Distinct from | manjrekar2025automating |
| Distinct from | oleary1999formally |
| Distinct from | oulkaid2025modeles |
| Distinct from | reid2016endtoend |
From crossref.
Abstract
We describe the formal methodology we are using to verify components of a commercial 64-bit, x86-compatible microprocessor design at Centaur Technology. This methodology is based on the ACL2 theorem prover. In this methodology, we mechanically translate the RTL design into a formal HDL for which we have an interpreter in ACL2. We use AIG- and BDD-based symbolic simulation and theorem proving techniques to show that the hardware models satisfy their specifications, which are ACL2 functions. Completed verifications yield theorems admitted by ACL2, ensuring that the verification is based on sound reasoning. We have used this methodology to verify instructions such as SIMD floating-point addition and subtraction, integer and floating-point multiplication, comparisons, bit-wise logical operations, and integer/float conversions. We discuss our floating-point addition verification as a case study.
Cite it as
@incollection{hunt2010use,
title = {Use of Formal Verification at Centaur Technology},
author = {Warren A. Hunt and Sol Swords and Jared Davis and Anna Slobodova},
editor = {David S. Hardin},
year = {2010},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
publisher = {Springer US},
pages = {65--88},
isbn = {978-1-4419-1538-2},
doi = {10.1007/978-1-4419-1539-9_3},
}
This record lives at https://refs.drheap.org/hunt2010use/ and will keep doing so.