适用于形式化验证的断言优化方法

摘要：

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确.断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础.文中针对影响锥模型不能分析断言中时序关系对状态空间的影响的问题,提出长序列模型,分析形式化验证中断言与状态空间大小的定性关系.在此基础上,提出适用于形式化验证的断言优化方法,方法包含断言逻辑化简、辅助验证逻辑、参考模型和断言禁用条件,并以某商用HDLC IP核为例,对比优化前后的验证结果,证明优化的有效性.

关键词：断言优化、形式化验证、状态空间爆炸、影响锥模型、长序列模型

所属期刊栏目：18

分类号：TP311.5(计算技术、计算机技术)

资助基金：国防基础科研计划资助项目XX2020204B028

在线出版日期：2023-06-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：166-175,188