基于形式化方法的有限域乘法器的建模与验证

Modeling and verification of finite field multiplier using formal method

针对有限域乘法器设计正确性的问题进行研究,阐述了有限域乘法器在高阶逻辑定理证明器HOL4中进行形式化建模和验证的过程。通过分析电路的结构特性和时序特性,提出了结合层次化和基于周期的形式化建模方法,构建4位多项式基有限域乘法器的形式化模型;最后在HOL4系统中完成对其相关性质的验证。实验结果证明了该有限域乘法器设计的正确性,同时表明所提出的建模方法对时序逻辑电路的验证是有效的。

This paper focused on the correctness of finite field multiplier, and described the detailed process of formal modeling and verification of finite field multiplier in higher-order logic theorem prover HOL4. Based on analyzing the structural characteris-tics and time sequence characteristics of the circuit, a formal modeling method which combine hierarchical technology and periodic-based method is proposed. And the formal model of a 4-bit polynomial-based finite field multiplier has been constructed. Finally,its properties are proved in the HOL4 system. The experimental results show the correctness of the finite field multiplier design,and show that the proposed modeling method is valid for the verification of sequence circuit.