-
题名适用于形式化验证的断言优化方法
- 1
-
-
作者
李东方
刘诗宇
王纪
王志昊
闫皓
-
机构
中国航天科工集团第二研究院
-
出处
《中国电子科学研究院学报》
北大核心
2023年第2期166-175,188,共11页
-
基金
国防基础科研计划资助项目(XX2020204B028)
-
文摘
在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响锥模型不能分析断言中时序关系对状态空间的影响的问题,提出长序列模型,分析形式化验证中断言与状态空间大小的定性关系。在此基础上,提出适用于形式化验证的断言优化方法,方法包含断言逻辑化简、辅助验证逻辑、参考模型和断言禁用条件,并以某商用HDLC IP核为例,对比优化前后的验证结果,证明优化的有效性。
-
关键词
断言优化
形式化验证
状态空间爆炸
影响锥模型
长序列模型
-
Keywords
assertion optimization
formal verification
state space explosion
cone of influence
long sequence
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-
