Accession Number : ADA324174

Title :   A Temporal Logic for Multi-Level Reasoning About Hardware,

Corporate Author : STANFORD UNIV CA

Personal Author(s) : Moszkowski, Ben

PDF Url : ADA324174

Report Date : DEC 1982

Pagination or Media Count : 30

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.

Descriptors :   *REASONING, *COMPUTER LOGIC, *CIRCUITS, DIGITAL SYSTEMS, PROPAGATION, MODELS, SPECIFICATIONS, TIME, SIGNALS, DELAY, LANGUAGE, POWER, BEHAVIOR, CALCULUS, MULTIPLICATION.

Subject Categories : Electrical and Electronic Equipment
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE