Accession Number : ADA136634

Title :   Reasoning About Digital Circuits.

Descriptive Note : Doctoral thesis,

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Moszkowski,B C

PDF Url : ADA136634

Report Date : Jul 1983

Pagination or Media Count : 149

Abstract : Predicate logic is a powerful and general descriptive formalism with a long history of development. However, since the logic's underlying semantics have no notion of time, statements such as I increases by 2 and The bit signal X rises from 0 to 1 can not be directly expressed. The author presents a formalism called interval temporal logic (ITL) that augments standard predicate logic with time-dependent operators. ITL is like discrete linear-time temporal logic but includes time intervals. The behavior of programs and hardware devices can often be decomposed into successively smaller intervals of activity. State transitions can be characterized by properties relating the initial and final values of variables over intervals. Furthermore, these time periods provide a convenient framework for introducing quantitative timing details. After giving some motivation for reasoning about hardware, he presents the propositional and first-order syntax and semantics of ITL. Demonstrated is ITL's utility for uniformly describing the structure and dynamics of a wide variety of timing-dependent digital circuits. Devices discussed include delay elements, adders, latches, flip-flops, counters, random-access memories, a clocked multiplication circuit and the Am2901 bit slice. ITL also provides a means for expressing properties of such specifications. Also examine are such concepts as device equivalence and internal states. Propositional ITL is shown to be undecidable although useful subsets are of relatively reasonable computational complexity. (Author)

Descriptors :   *Computer logic, *Circuits, *Digital systems, Multiplication, Latches, Flip flop circuits, Multiplexing, Syntax, Semantics, Random access computer storage, Counters, Shift registers, Theses

Subject Categories : Electrical and Electronic Equipment
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE