Application of formal methods to the VIPER microprocessor
The work
| Authors | W.J. Cullyer; C.H. Pygott |
|---|---|
| Editors | |
| Type | article |
| Year | 1987 |
| Citekey | cullyer1987application |
Where it appeared
| Published in | IEE Proceedings E Computers and Digital Techniques |
|---|---|
| Publisher | Institution of Engineering and Technology (IET) |
| Volume | 134 |
| Issue | 3 |
| Pages | 133 |
Identifiers
| DOI | 10.1049/ip-e.1987.0023 |
|---|---|
| OpenAlex | W4239036558 |
| ISSN | 0143-7062 |
Access
| Landing page | https://doi.org/10.1049/ip-e.1987.0023 |
|---|
Empty on purpose
| copy |
Related
| Distinct from | birtwistle1988vlsi |
|---|---|
| Distinct from | boulton1990hol |
| Distinct from | boulton1992hol |
| Distinct from | bryant1991methodology |
| Distinct from | cohn1986mechanized |
| Distinct from | cohn1987proof |
| Distinct from | cohn1988correctness |
| Distinct from | cohn1989notion |
| Distinct from | cullyer1988implementing |
| Distinct from | dhingra1987formal |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1985formal |
| Distinct from | lipovski1977hardware |
| Distinct from | patterson1980case |
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
The VIPER 32-bit microprocessor has been invented at the UK Royal Signals and Radar Establishment (RSRE) for use in highly safetycritical military and civil systems. Throughout, formal mathematical methods have been used to prove that the gate-level realisations conform to a top-level specification. The paper explains the various layers of documentation produced, starting with the use of Michael Gordon's LCF-LSM (based on Meta-Language, ML) at the higher levels, proceeding via the use of John Morison's ELLA hardware description language at lower levels, to multiple VLSI implementations. It is intended to show that this route for designing synchronous VLSI circuits promises a practical means for industry to produce validated designs.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-15 22:55 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{cullyer1987application,
title = {Application of formal methods to the VIPER microprocessor},
author = {W.J. Cullyer and C.H. Pygott},
year = {1987},
journal = {IEE Proceedings E Computers and Digital Techniques},
publisher = {Institution of Engineering and Technology (IET)},
volume = {134},
number = {3},
pages = {133},
issn = {0143-7062},
doi = {10.1049/ip-e.1987.0023},
}
This record lives at https://refs.drheap.org/cullyer1987application/ and will keep doing so.