A Temporal Logic for Multi-Level Reasoning About Hardware,

Abstract

The paper describes a logical notation for reasoning about digital circuits. The formalism provides a rigorous and natural basis for device specification as well as for proving properties such as correctness of implementation. Conceptual levels of circuit operation ranging from detailed quantitative timing and signal propagation up to functional behavior are integrated in a unified way. A temporal predicate calculus serves as the formal core of the notation, resulting in a versatile tool that has more descriptive power than any conventional hardware specification language. The logic has been applied to specifying and proving numerous properties of circuits ranging from delay elements up to the AM2901 ALU bit slice. Presentations of a delay model and a multiplication circuit illustrate various features of the notation.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1982
Accession Number
ADA324174

Entities

People

  • Ben Moszkowski

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Algorithms
  • Boolean Algebra
  • Circuits
  • Clocks
  • Commerce
  • Computational Complexity
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Diagrams
  • Digital Circuits
  • Information Theory
  • Instruction Set Architecture
  • Language
  • Logic
  • Specifications

Readers

  • Computational Linguistics
  • Integrated Circuit Design and Technology.
  • Systems Analysis and Design