IMPLEMENTING TEMPORAL LOGIC IN HOL AND APPLICATIONS
Date
1988-07-01
Authors
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