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

摘要

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