Microcode Verification Using SDVS (State Delta Verification System): The Method and a Case Study.

Abstract

This report describes SDVS (State Delta Verification System), its application to micromode verification, and the verification of a particular example referred to as the H-machine example. The example illustrates how particular microcode that interprets a computer instruction set can be proved correct and how this proof is accomplished with an existing, automated verification system. Keywords include: verification, microcode, symbolic execution, ISPS, correctness proofs, theorem provers, and formal machine descriptions.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 30, 1984
Accession Number
ADA175253

Entities

People

  • B. H. Levy

Organizations

  • The Aerospace Corporation

Tags

Communities of Interest

  • Advanced Electronics
  • Space

DTIC Thesaurus Topics

  • Case Studies
  • Computations
  • Computer Architecture
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computers
  • Computing System Architectures
  • Decoding
  • Formal Languages
  • Instruction Set Architecture
  • Instructions
  • Language
  • Microcode
  • Programming Languages
  • Simulations
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.