结构建模法在硬件电路形式化验证中的应用  

Application of structure modeling method in formal verification of hardware

作　　者：张杰[1] 王亚丽[1] 李黎明[2] 李晓娟[2] 

机构地区：[1]北京化工大学信息科学与技术学院,北京100029 [2]首都师范大学信息工程学院,北京100048

出　　处：《计算机工程与设计》2016年第1期259-263,共5页Computer Engineering and Design

基　　金：国家自然科学基金项目(61373034)

摘　　要：为解决硬件电路形式化验证过程中,验证对象的结构过于庞大复杂难以进行形式化描述与验证的问题,提出一种结构建模法。对两种不同的结构建模方法 (分解法和迭代法)分别进行讨论,分析两种方法的异同点以及适用性,详述结构建模过程中需要用到的层次化技术和模块化技术。以超前进位产生器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.

关 键 词：结构建模 形式化验证 定理证明 分解法 迭代法 74LS182 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]