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

From bibtex.

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 behavior 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.