Reliability Research Of Booth Multiplier Based On Formal Methods

With the rapid development of VLSI, reliability verification of system has been the focus of researchers. Multiplier is a core computing components in the high performance microprocessor. Therefore, it is essential to verify the reliability of multiplier. This paper uses theorem proving to study the reliability of Booth multiplier and conducts some related verification in the HOL4 system. The main work has been done are:Firstly, the paper introduces some basic concepts of formal methods and highlights the theorem proving methods and HOL4 system including the development history of HOL4 system, modeling language of HOL4 system and proving methods.Secondly, this paper completes the formalization of the implementation and specification of second order Booth multiplier. And Booth encoding module, compression module and final summation module have been analyzed using formal methods. Then this paper completes the formal modeling of these three modules.Thirdly, on the basis of the compression module and the final summation module, this paper accomplishes the hierarchical analysis of the combined module and the formal modeling of implementation and specification of the combined module in HOL4 system.Finally, this paper fulfills the formal verification of Booth algorithm, Booth encoding module, compression module, final summation module and combined module using the embedded axioms, inference rules and defined theorems in HOL4 system. This paper not only proves that the second order Booth multiplier is reliable, also shows the powerful function on the verification of hardware system and algorithm, which plays a significant role in further development of HOL4 system.