Formal Verification of VIPER's ALU
The work
| Authors | Wai Wong |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1993 |
| Citekey | wong1993formal |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| School | University of Cambridge Computer Laboratory |
| Pages | 78 |
Identifiers
| DOI | 10.48456/tr-300 |
|---|---|
| report_number | UCAM-CL-TR-300 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-300.html |
|---|
Related
| Distinct from | cantuortiz1997proof |
|---|---|
| Distinct from | cohn1987proof |
| Distinct from | cohn1988correctness |
| Distinct from | curzon1994formal |
| Distinct from | curzon1994formalb |
| Distinct from | ferres2025survey |
| Distinct from | vantassel1993femtovhdl |
| Distinct from | zhu2026equivfusion |
From bibtex.
Abstract
This research describes the formal verification of an arithmetic logic unit of the VIPER microprocessor. VIPER is one of the first processors designed using formal methods. A formal model in HOL has been created which models the ALU at two levels: on the higher level, the ALU is specified as a function taking two 32-bit operands and returning a result; on the lower level the ALU is implemented by a number of 4-bit slices which should take the same operands and return the same results. The ALU is capable of performing thirteen different operations. A formal proof of functional equivalence of these two levels has been completed successfully. The complete HOL text of the ALU formal model and details of the proof procedures are included in this report. It has demonstrated that the HOL system is powerful and efficient enough to perform formal verification of realistic hardware design.
A copy is held
pdf, 521.3 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 03:14 UTC |
| Approved by | a person 2026-10-02 10:01 UTC |
Filed under
Cite it as
@techreport{wong1993formal,
title = {Formal Verification of VIPER's ALU},
author = {Wai Wong},
year = {1993},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
pages = {78},
doi = {10.48456/tr-300},
}
This record lives at https://refs.drheap.org/wong1993formal/ and will keep doing so.