抽象距离引导的半形式化验证方法

摘要：

传统模拟验证方法和形武化验证方法在面临复杂大规模设计时，性能和处理能力的缺陷日益突出。为了融合二者的优点，避免各自不足，本文改进并实现了一种半形式化的验证方法。首先，提出了控制状态变量和一般控制变量的概念，以及从代码中识别和提取这两类变量的方法。利用此方法能够从目标设计中较为精细的抽象出部分核心电路逻辑，获得抽象距离信息。然后通过一种抽象信息引导的激励生成算法，对获得的抽象信息的有效性进行了检验。实验结果表明，这种方法仅需花费较小的计算代价，获得了较为精确的抽象信息，能够高效的引导验证覆盖到难达的状态。并且与设计规模相关性较小，具有较为广泛的适用性。

关键词： 集成电路 设计验证 半形式化方法 抽象距离引导

作者: 张弢 吕涛 李晓维

作者单位: 中国科学院计算机系统结构重点实验室 中国科学院计算技术研究所，北京 100190 中国科学院研究生院，北京 100190 中国科学院计算机系统结构重点实验室 中国科学院计算技术研究所，北京 100190

会议类型: 国内会议

会议名称: 第十三届全国容错计算学术会议

会议地点: 海拉尔

会议语种:中文

页码: 494-498

在线出版日期: 2009-07-20（万方平台首次上网日期，不代表论文的发表时间）