The Study Of Hardware Verification In Theorem Prover HOL

With the increasing development in hardware design technology, the designs of hardware are getting larger and larger, more complex everyday. However, it becomes increasingly difficult to ensure these devices free of design errors. The traditional verification methods are: simulation, testing and emulation, but these methods are not complete, formal verification methods are used into hardware design, then formal hardware verification technology is produced. With these approaches, the behaviors and requirements of the system are described mathematically, and formal proof is used to verify that the behaviors behaves according to the requirements. At present, formal verification can generally be divided into two main categories: reachability analysis and deductive methods. Every kind of model checkers and equivalence checkers are examples of the first approach. Many different theorem provers have been used for deductive verification. Every formal verification approaches have their advantages and disadvantages, the main advantage of model checking is automation ,its main drawback is the state explosion problem. The theorem proving can deal with infinite states system but requires lots of expertise.The paper give an introduction to the formal method: its origins, classification and significance ,and discusses the advantages and disadvantages compared with the traditional method . This paper give a study on theorem prover HOL system. We mainly show meta language, HOL logic, the proof styles. Then introduces using the system to do hardware verification as well as the key technologies: abstraction mechanisms and hierarchical verification . At last ,we verify the designs of the parity checker with reset signal and the design of Arithmetic Logic Unit (ALU) which is the important part of CPU using HOL-4 system, and receive the experiment results.