| Finite field operation is core of encoding,decoding and data encryption algorithms.In order to complete the algorithm encoding and decoding and encryption functions correctly,the design of finite field multiplier should be verified.With the fast development of science and technology,hardware design technology has been developed and improved rapidly,and the hardware circuit is becoming increasingly complex,so we face the challenge that ensure the correctness of hardware design.Using traditional method,such as simulation-based verification of hardware design has some limitations,which can no longer meet the needs of ensuring the correctness of the design.In this thesis,we use theorem proving method to verify the reliability of sequential logic multiplier in GF(2m).Through higher order logic theorem prover HOL4 to complete the function correctness verification,and its main works are:(1)This dissertation gives the principle of formal method,and compares the four kinds of common methods by their advantages and disadvantages.The theorem prover HOL4 system is studied in detail through its development process,programming language,logic foundation and Verification methods.(2)Analyzing the concept of finite field and its multiplication,we summarizes its principle and hardware implementation and analyzes LSB-First algorithm which is one of the classical finite field multiplication algorithms.(3)Formalizing the implementation of the finite-field multiplier by the hierarchical method and cycle-based method in HOL4 system.And then,this dissertation would describe the properties of finite field multiplication in HOL4 system.(4)Formally verifying the periodic characteristics and functional reliability of finite field multiplier through the basic tactic and theorem library in HOL4 system.The proof of theorem proves the reliability of the finite field multiplier design.It also demonstrates the capability and prospect of HOL4 system in the verification of encryption and coding hardware. |
PDF Full Text Request