Specification of Viper2 in Z

Abstract

As a continuation of the use of the specification language Z which was used to specify the Viper 1 microprocessor this paper covers the specification of the Viper 2. This was completed before the definitive HOL specification was complete, therefore there is no proof of correspondence between the two. Using Z did highlight inconsistencies in the HOL specification that may not have appeared until later in the specification. Great Britain.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1988
Accession Number
ADA205179

Entities

People

  • D. H. Kemp

Organizations

  • Royal Signals and Radar Establishment

Tags

DTIC Thesaurus Topics

  • Addressing
  • Arithmetic
  • Case Studies
  • Genes
  • Instruction Set Architecture
  • Instructions
  • Language
  • Microprocessors
  • Procedures (Computers)
  • Specifications
  • Standards

Fields of Study

  • Engineering

Readers

  • Computational Linguistics
  • Software Engineering
  • Theoretical Analysis.