Formal Specification of the VIPER Microprocessor in HOL
Abstract
The VIPER microprocessor was invented at RSRE to satisfy the need for a highly trusted 32-bit computer which can be used in safety critical applications. The need for such a chip, has arisen in areas such as the arming and fuzing of weapons, fly by wire control systems in high performance military and civil aircraft and in the instrumentation of nuclear reactors. The majority of widely available microprocessors are regarded as unsatisfactory for safety critical applications because they have instruction sets that are too rich and that lead to programmer confusion and problems with formal verification of the software to run on them. Also, they are documented in natural language (with its inherent ambiguities) and their designs are validated by simulation (a process that cannot give a 100% guarantee of correctness). The aim of the VIPER project has therefore been to design a processor architecture well matched to critical applications, to define it rigorously (this document) and to attempt to prove by mathematical means the correctness of circuits designed to meet this specification (in addition to their conventional validation by simulation). This Report specifies the VIPER architecture in two ways: (a) Informally, using a conventional description of the instruction set; and (b) Formally, using the notation of the HOL system (Higher Order Logic), developed at the University of Cambridge. The purpose of this Report is to provide an unambiguous description of the functional behaviour of VIPER.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1990
- Accession Number
- ADA242147
Entities
People
- C. H. Pygott
Organizations
- Royal Signals and Radar Establishment