Application of formal methods to the VIPER microprocessor
作者:
W.J.Cullyer,
C.H.Pygott,
期刊:
IEE Proceedings E (Computers and Digital Techniques)
(IET Available online 1987)
卷期:
Volume 134,
issue 3
页码: 133-141
年代: 1987
DOI:10.1049/ip-e.1987.0023
出版商: IEE
数据来源: IET
摘要:
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.
点击下载:
PDF
(1014KB)
返 回