Abstract:

No effective security verification method for hardware design is available for a long time. To solve this problem, this paper proposes a Fine-granularity Gate Level Formal Verification Method for Hardware Security, which is able to describe the security properties of the circuit and construct the semantic circuit in the customized formal language on Coq. With the help of the Hoare Logic theory, a provable theorem for verifying the security property of the semantic circuit is generated. The process of verification relies on tactics to generate and validate the proof in human-computer interaction. The results show that this method not only verifies the security properties of the semantic model, but also solves the problem of insufficient verification coverage in simulation. In conclusion, this method can raise accuracy and efficiency of verification.

Key words: hardware design, security verification, theorem proof, formal semantic model, fine-granularity