Hardware Specification with Temporal Logic: An Example
- 1 March 1982
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-31 (3), 223-231
- https://doi.org/10.1109/tc.1982.1675978
Abstract
The use of temporal logic for the specification of hardware modules is explored. Temporal logic is an extension of conventional logic. While traditional logic is useful for specifying combinational circuits, it is shown how the extensions of temporal logic apply to the specification of memory, as well as the safeness and liveness properties of active circuits representing processes. These ideas are demonstrated by the example of a self-timed arbiter. An implementation of the arbiter is also given, and its formal verification by a kind of reachability analysis is discussed. This verification approach is also useful for finding design errors, as demonstrated by an example.Keywords
This publication has 3 references indexed in Scilit:
- The Modal Logic of ProgramsPublished by Defense Technical Information Center (DTIC) ,1979
- Architecture of Distributed Computer SystemsLecture Notes in Computer Science, 1979
- Formal verification of parallel programsCommunications of the ACM, 1976