中文摘要：

为解决硬件电路形式化验证过程中,验证对象的结构过于庞大复杂难以进行形式化描述与验证的问题,提出一种结构建模法。对两种不同的结构建模方法 （分解法和迭代法）分别进行讨论,分析两种方法的异同点以及适用性,详述结构建模过程中需要用到的层次化技术和模块化技术。以超前进位产生器74LS182为例,详细分析验证对象的结构建模过程,给出结构建模前后验证对象的结构描述、验证流程等结果。通过对比结构建模前后验证对象的验证规模、难易程度和时间开销等,凸显了结构建模对硬件电路形式化验证过程的优化效应。

英文摘要：

Based on formal verification of hardware,to solve the formal description and verification problem of large-scale and complex structure of verification object,a structure modeling method was proposed.Two different structure modeling methods（discomposed method and iterative method）were discussed.The similarities,differences and applicability of two structure modeling methods were analyzed.Both hierarchical technology and modular technology used in structure modeling process were detailed.An example of carry lookahead generator 74LS182 was given.The process of structure modeling of verification object was analyzed.The structure description and verification flow were given.By contrasting the before structure modeling and the after one,the verified scale,difficult degree and time costs etc.were given.The optimization effect of structure modeling on the formal verification process of hardware was highlighted.