Reasoning About Digital Circuits

From bibtex.

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. We present 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, we present the propositional and first-order syntax and semantics of ITL. We demonstrate 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. Throughout the dissertation, we examine such concepts as device equivalence and internal states. Propositional ITL is shown to be undecidable although useful subsets are of relatively reasonable computational complexity.