Application of temporal logic to the assistance of hardware logic design

The specification of digital systems in temporal logic, a verification method between specification and gate-level designs, and a method for synthesizing state diagrams from specification are presented. Timing relations shown usually be timing diagrams can be described, and verification and synthesis can be done automatically. A hardware description language called Tokio, which is based on temporal logic and is an extension of Prolog, is also presented. The above techniques can be applied to Tokio.<>