Hardware Proofs Using LCF-LSM and ELLA.

Abstract

A method is described for writing the formal specifications for a digital system, a high level of design which satisfies this requirement and then a gate level realisation, using the languages LCF -LSM and ELLA. Given these formal descriptions, this papers shows how to carry out mathematical proofs to establish that the high level design respects the specification and the gate level design agrees with precisely with the high level design. By this means, a chain of correspondence proof is created from the specification to the ultimate realisation, as required during the development of safety critical and security critical hardware. There methods have been used to develop formal proofs for the VIPER microprocessor and this paper forms an essential tutorial for those studying the validation of this new 32 - bit processor. (Great Britain)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1985
Accession Number
ADA168248

Entities

People

  • C. H. Pygott
  • W. J. Cullyer

Organizations

  • Royal Signals and Radar Establishment

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Arithmetic
  • Circuits
  • Clocks
  • Diagrams
  • Digital Circuits
  • Electronic Circuits
  • Equations
  • Foreign Languages
  • Language
  • Logic
  • Microprocessors
  • Nand Gates
  • Security
  • Sequences
  • Simulators
  • Specifications
  • Validation

Readers

  • Military History of the United States in the 20th Century.
  • Software Engineering
  • Theoretical Analysis.