The application of temporal logic to digital systems design

Considers the use of temporal logic in a role broadly comparable to that currently played in digital circuit design by Hardware Description Languages (HDLs), such as VHDL and ELLA are conventionally used first to specify, or describe, a circuit at some level of abstraction, and then to simulate the circuit definition thus generated. Current HDLs suffer from two drawbacks: (i) they have no formal semantic basis, and are thus unable to provide support for the process of verifying that the structural description correctly implements a given behavioural specification; (ii) their notion of behavioural specification is essentially algorithmic, and is thus at a relatively low level of abstraction, particularly when compared with notations-such as Z and VDM-currently available for use in software specification. The authors indicate how a particular system of temporal logic, Moszkowski´s Interval Temporal Logic (ITL), together with the associated programming language, Tempura, provide a notation for circuit definition capable of overcoming these drawbacks, while at the same time presenting the designer with a conceptual framework which is relatively appealing at the intuitive level