Microcode Verification Project.

Abstract

Within the scope of this project, a formalism for representing state transitions in a computationally tractable way has been invented, and a proof system based on this formalism has been designed and implemented. The representations of state transitions are called 'state deltas'. The basic proof system has been specialized for proofs about machine language and microcode by the addition of simplification rules for bitstring arithmetic, and by the addition of a translator from the ISPS machine description language to state deltas. Some experimentation with the system has been driven by a preliminary attempt to verify parts of the microcode of the Fault-Tolerant Spaceborne Computer (FTSC). The primary success to date has been the verification of the basic algorithm used for computing floating point square root. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1980
Accession Number
ADA088189

Entities

People

  • Dono Van-mierop
  • Leo Marcus
  • Stephen D. Crocker

Organizations

  • University of Southern California

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Coding
  • Computations
  • Computer Programming
  • Computer-Aided Design
  • Computers
  • Databases
  • Detectors
  • Engineering
  • Environment
  • Floating Point Operations
  • Instruction Set Architecture
  • Language
  • Microcode
  • Software Development
  • Square Roots

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.