Reasoning about the function and timing of integrated circuits with Prolog and temporal logic

From bibtex.

Abstract

The structure of circuits is specified with Prolog; their function and timing behavior is specified with interval temporal logic. These structural and behavioral specifications are used to formally verify the functionality of circuit elements as well as their timing characteristics. A circuit is verified by deriving its behavior from the behavior of its components. The derived results can be abstracted to functional descriptions with timing constraints. The functional descriptions can then be used in proofs of more complex hardware circuits. Verification is done hierarchically, with transistors as primitive elements. Transistors are modeled as switch-level devices with delay. In order to model delay, the direction of signal flow through each transistor must be assigned. This is done automatically by a set of Prolog routines which also determine the inputs and outputs of each circuit component. Interval temporal logic descriptions are expressed in Prolog and manipulated using PALM: Prolog Assistant for Logic Manipulation. With PALM, the user specifies rewrite rules and uses these rules to manipulate logical terms. In the case of reasoning about circuits, PALM is used to manipulate the temporal logic descriptions of the components to derive a temporal logic description of the circuit. These techniques are demonstrated by applying them to several commonly used complementary metal oxide semiconductor (CMOS) structures. Examples include a fully complementary dynamic latch and a 1-bit adder. Both these circuits are implemented with transistors and exploit 2-phase clocking and charge sharing. The 1-bit adder is a sophisticated full adder implemented with a dynamic CMOS design style. The derived timing and functional behavior of the 1-bit adder is abstracted to a purely functional behavior which can be used to derive the behavior of an arbitrary n-bit adder.