Technical reports

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

M.E. Leeser

February 1988, 50 pages

DOI: 10.48456/tr-126

Abstract

This article describes the application of formal methods to transistor level descriptions of circuits. Formal hardware verification uses techniques based on mathematical logic to formally prove that a circuit correctly implements its behavioral specification. In the approach described here, the structure of circuits and their functional behavior are described with Interval Temporal Logic. These specifications are expressed in Prolog, and the logical manipulations of the proof process are achieved with a Prolog system. To demonstrate the approach, the bahavior of several example circuits is derived from the behavior of their components down to the transistor level. These examples include a dynamic latch which uses a 2-phase clocking scheme and exploits charge storage. Timing as well as functional aspects of behavior are derived, and constraints on the way a circuit interacts with its environment are reasoned about formally.

Full text

PDF (2.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-126,
  author =	 {Leeser, M.E.},
  title = 	 {{Reasoning about the function and timing of integrated
         	   circuits with Prolog and temporal logic}},
  year = 	 1988,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-126.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-126},
  number = 	 {UCAM-CL-TR-126}
}