This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Hardware Specification with Temporal Logic: An Example
March 1982 (vol. 31 no. 3)
pp. 223-231
G.V. Bochmann, D?partement d'Informatique et de Recherche Op?rationnelle, Universit? de Montreal
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.
Index Terms:
VLSI design, Arbiter, design verification, hardware specification, hardware verification, logic design, modal logic, self-timed systems, temporal logic
Citation:
G.V. Bochmann, "Hardware Specification with Temporal Logic: An Example," IEEE Transactions on Computers, vol. 31, no. 3, pp. 223-231, March 1982, doi:10.1109/TC.1982.1675978
Usage of this product signifies your acceptance of the Terms of Use.