Hardware Proofs Using LCF-LSM and ELLA
The work
| Authors | W.J. Cullyer; C.H. Pygott |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1985 |
| Citekey | cullyer1985hardware |
Where it appeared
| Publisher | Royal Signals and Radar Establishment |
|---|---|
| Number in series | 3832 |
| School | Royal Signals and Radar Establishment |
Identifiers
| report_number | DRIC-BR-99176 |
|---|
Access
| Landing page | https://archive.org/details/DTIC_ADA168248 |
|---|
From bibtex.
Abstract
A method is described for writing the formal specification for a digital system, a high level design which satisfies this requirement and then a gate level realisation, using the languages LCF - LSM and ELLA. Given these formal descriptions, this paper shows how to carry out mathematical proofs to establish that the high level design respects the specification and the the gate level design agrees precisely with the high level design. By this means, a chain of correspondence proof is created from specification to the ultimate realisation, as required during the development of safety critical and security critical hardware. These methods have been used to develop formal proofs for the VIPER microprocessor and this paper forms an essential tutorial for those studying the validation of this new 32 - bit processor.
A copy is held
pdf, 1.9 MB. 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-10-23 00:37 UTC |
| Approved by | a person 2026-10-23 07:51 UTC |
Filed under
Cite it as
@techreport{cullyer1985hardware,
title = {Hardware Proofs Using LCF-LSM and ELLA},
author = {W.J. Cullyer and C.H. Pygott},
year = {1985},
publisher = {Royal Signals and Radar Establishment},
school = {Royal Signals and Radar Establishment},
}
This record lives at https://refs.drheap.org/cullyer1985hardware/ and will keep doing so.