基于路径约束求解的难达状态激励生成方法
半形式化验证方法结合了模拟方法和形式化方法的优点,避免了各自的缺点,是一种很有前景的验证方法.本文改进并实现了一种半形式化验证方法,目标是覆盖设计中的难达状态.首先,利用基于数据依赖图的抽象方法构建设计的抽象模型,在此模型上运用形式化的前像计算获得抽象距离信息,用以指导模拟过程.其次,采用了基于路径约束求解的激励生成方法,这种方法混合了具体模拟和符号模拟技术,能够有效的产生输入向量,以一种较均衡的方式遍历设计的状态空间,帮助验证快速覆盖到目标.实验结果表明,本文方法能够有效的验证设计中的难达状态.
集成电路 半形式化验证 路径约束求解 激励生成
周艳红 王天成 吕涛 李华伟
计算机体系结构国家重点实验室,中国科学院计算技术研究所,北京100190;中国科学院大学,北京100049 计算机体系结构国家重点实验室,中国科学院计算技术研究所,北京100190
国内会议
重庆
中文
1-6
2013-07-27（万方平台首次上网日期，不代表论文的发表时间）