Microcode Verification Project.

Abstract

The goal of the microcode verification project at ISI is the development of both the theory and tools for verification of microcode. The strategy has been to push the development of a working system, letting the theoretical issues and the human engineering questions emerge during system development. The ISPS language is used for encoding our machine descriptions. The State Delta formalism is used for reasoning about the course of the computation. A system to check proofs of microcode validity is currently built. The system is composed of a data base and simplifier that perform some automatic deductions to make checking of the proofsteps manageable, as well as a proof language and a user interface. A particular computer (the FTSC) is used to establish a focus for the project and to provide a source of examples. This document reports the results of verifying the microcode of the square root instruction of the FTSC, and the results of verifying the complete microcode of a much smaller fictitious example machine.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1980
Accession Number
ADA082461

Entities

People

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

Organizations

  • University of Southern California

Tags

Communities of Interest

  • Materials and Manufacturing Processes
  • Weapons Technologies

DTIC Thesaurus Topics

  • Coding
  • Computational Science
  • Computations
  • Computer Programming
  • Computers
  • Engineering
  • Floating Point Operations
  • Human Factors Engineering
  • Information Processing
  • Instruction Set Architecture
  • Instructions
  • Language
  • Notation
  • Operating Systems
  • Software Development
  • Square Roots
  • User Interface

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Programming and Software Development.
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.