摘要
为解决硬件电路形式化验证过程中,验证对象的结构过于庞大复杂难以进行形式化描述与验证的问题,提出一种结构建模法。对两种不同的结构建模方法 (分解法和迭代法)分别进行讨论,分析两种方法的异同点以及适用性,详述结构建模过程中需要用到的层次化技术和模块化技术。以超前进位产生器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.
出处
《计算机工程与设计》
北大核心
2016年第1期259-263,共5页
Computer Engineering and Design
基金
国家自然科学基金项目(61373034)
关键词
结构建模
形式化验证
定理证明
分解法
迭代法
74LS182
structure modeling
formal verification
theorem proving
discomposed method
iterative method
74LS182
