Reasoning About Digital Circuits.
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Predicate logic is a powerful and general descriptive formalism with a long history of development. However, since the logics 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 ITLs 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
- Electrical and Electronic Equipment
- Computer Hardware