Abstract:In order to solve the correctness issues of computer system design, a formal method which is complete on the test space is studied a general method of formal verification of hardware system in HOL4 is discussed in this paper. The method includes how to use the higher-order logic to describe the implementation and specification of hardware system and the general process of proving goals in HOL4. Meanwhile, taking multiplier as example, a functional decomposition method for modeling the design of circuit logically is proposed. Relevant properties of the circuit are ratiocinated and verified using the theorem prover HOL4, which proves that the model of the circuit design satisfies the properties.