Please use this identifier to cite or link to this item:
|Title:||IMPLEMENTING TEMPORAL LOGIC IN HOL AND APPLICATIONS|
|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.|
|Appears in Collections:||Technical Reports|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.