Formal Specification of the VIPER Microprocessor in HOL
ROYAL SIGNALS AND RADAR ESTABLISHMENT MALVERN (UNITED KINGDOM)
Pagination or Media Count:
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.
- Computer Programming and Software