IMPLEMENTING TEMPORAL LOGIC IN HOL AND APPLICATIONS

Date
1988-07-01
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Higher-Order Logic (HOL) system has been proved to be very powerful for hardware verification. Many of the largest proofs completed to date have been constructed using HOL system. It seems to be that the HOL system is more suitable for dealing with static object though we can define functions with parameter of time for handling dynamic objects in HOL system. On the other hand, Temporal logic which includes time in its semantics has the potential of handling timing problems. In order to mechanize the deducing process of temporal logic and explore the possibilities of applying temporal logic to hardware verification, we have tried to implement the linear timing temporal logic on the top level of HOL system by expressing the temporal logic concepts in high-order logic and proving the axioms and inference rules of a formal temporal logic system. This paper describes the ideas and results of this work, and gives some examples of applying temporal logic to hardware specification and verification. We have proved that there exists a static hazard in the combinational circuit considered under certain conditions, and the hazard is eliminated in the improved circuit. We have also specified and verified the properties of a S-R latch by the combined power of temporal logic and HOL system.
Description
Keywords
Computer Science
Citation