Specification of Viper1 in Z

Abstract

The Viper1 microprocessor has already been specified mathematically in HOL. HOL, however, is not well known outside the hardware verification community. This paper covers the specification Viper1 in the Z specification language. Various features of Viper1 have been specified in Z which did not occur in the top level HOL specification. It has not been possible to prove any correspondence between this specification and the original HOL specification. The work involved in writing the Viper1 specification has proved useful in writing the initial Viper2 specification. Great Britain.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1988
Accession Number
ADA205479

Entities

People

  • D. H. Kemp

Organizations

  • Royal Signals and Radar Establishment

Tags

DTIC Thesaurus Topics

  • Addressing
  • Algorithms
  • Arithmetic
  • Instruction Set Architecture
  • Instructions
  • Language
  • Microprocessors
  • Specifications
  • Standards

Readers

  • Aerospace Test and Evaluation
  • Computational Linguistics