
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 timedependent operators. ITL is like discrete lineartime 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 firstorder syntax and semantics of ITL. Demonstrated is ITL's utility for uniformly describing the structure and dynamics of a wide variety of timingdependent digital circuits. Devices discussed include delay elements, adders, latches, flipflops, counters, randomaccess 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