Department of Computer Science and Technology

Technical reports

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

Miriam Ellen Leeser

April 1988, 151 pages

This technical report is based on a dissertation submitted December 1987 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Queens’ College.

DOI: 10.48456/tr-132

Abstract

The structure of circuits is specified with Prolog; their function and timing behaviour is specified with interval temporal logic. These structural and behavioural specifications are used to formally verify the functionality of circut elements as well as their timing characteristics. A circuit is verified by deriving its behaviour from the behaviour 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 modelled as switch-level devices with delay. In order to model delay, the direction of signal flow through the 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 behaviour of the 1-bit adder is abstracted to a purely functional behavior which can be used to derive the behaviour of an arbitrary n-bit adder.

Full text

Only available on paper (could be scanned on request).

BibTeX record

@TechReport{UCAM-CL-TR-132,
  author =	 {Leeser, Miriam Ellen},
  title = 	 {{Reasoning about the function and timing of integrated
         	   circuits with Prolog and temporal logic}},
  year = 	 1988,
  month = 	 apr,
  institution =  {University of Cambridge, Computer Laboratory},
  address =	 {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
          	  phone +44 1223 763500},
  doi = 	 {10.48456/tr-132},
  number = 	 {UCAM-CL-TR-132}
}