基于GSTE验证的细化问题的研究

论文摘要

随着集成电路的设计规模越来越大、复杂度越来越高,产品上市时间却越来越紧迫,集成电路的验证变得越来越困难。2003年度的国际半导体技术发展报告指出,验证已经成为集成电路设计流程中的最大瓶颈。传统的模拟验证因其测试周期长、不能完全覆盖,已经不适合当前对集成电路验证的需求。形式化验证其原理是使用严格的数学推理来证明一个系统满足全部或部分规范,从而提高了验证的正确率,保证了市场需求。另外,它作为对传统基于模拟验证方法的补充,日益引起人们的关注。本课题在较为全面、深入地研究和总结国内外形式验证技术研究成果的基础上,对当前主流形式化验证方法中的推广化符号轨迹赋值(GSTE)验证方法进行了深入的研究和扩展,以期进一步减少伪报错现象,提高GSTE验证方法在集成电路验证中的正确性。本课题在研究方法上,首先,针对符号轨迹赋值(STE)验证方法的基本理论和技术,详细分析其优点和不足。对STE验证规范做出的图形化扩展和断言图,以及基于断言图的验证算法做认真的论证和分析。然后,分析GSTE验证方法,比较STE和GSTE的优缺点。进一步分析由于GSTE继承STE的抽象行为,而带来的伪报错问题产生的原因。在以上学习和分析的基础上,本文提出GSTE中SMC算法的改进算法,并通过验证平台FORTE对改进后的算法进行编码实现和验证。结果显示,在降低伪报错和查错方面都有较大改良和提高。另外,在不熟悉电路的情况下,进行集成电路验证时,可以通过使用GSTE中改进的SMC算法来验证电路的正确性。若非常熟悉本电路的设计,也可以按照回路进行手动扩展。同时,针对验证工具的自动化程度,本课题创造性地提出并设计了自动插入故障容错结构工具。在实际的某个电路设计流程中,如果验证结果返回为错误,对于没有参加本电路设计的人员来讲,发现错误并改正错误将是非常困难的。大部分电路设计的修改和优化,只是涉及电路部分结构的变化。如何能更有效、更准确地给出问题所在,是保证验证电路设计正确性的首要问题。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 引言
• 1.2 验证的基本概念和系统验证的原则
• 1.2.1 验证的基本概念
• 1.2.2 系统验证的原则
• 1.3 验证方法综述
• 1.3.1 形式化验证
• 1.3.2 其他验证方法
• 1.4 研究意义、选题依据
• 1.5 主要研究内容和章节安排
• 1.5.1 主要研究内容
• 1.5.2 章节安排
• 1.6 本章小结
• 第二章 符号轨迹赋值和推广化符号轨迹赋值简介
• 2.1 STE（符号轨迹赋值）介绍
• 2.1.1 电路模型
• 2.1.2 验证规范
• 2.1.3 断言图
• 2.1.4 验证过程
• 2.2 符号处理技术
• 2.2.1 二叉判定树
• 2.2.2 三值逻辑编码
• 2.2.3 STE 的优点与不足
• 2.3 GSTE（推广化符号轨迹赋值）介绍
• 2.3.1 GSTE 的产生
• 2.3.2 双向GSTE
• 2.3.3 符号四元组模型扩展
• 2.4 GSTE 和STE、传统符号模型检验方法的比较
• 2.4.1 GSTE 和STE 的比较
• 2.4.2 GSTE 与传统模型检验方法的关系
• 2.5 本章小结
• 第三章 伪报错问题的起源、研究、细化和检验
• 3.1 GSTE 中模型检验强可满足性算法（SMC）算法简介
• 3.1.1 相关定义
• 3.1.2 GSTE 中的SMC 算法
• 3.2 伪报错的来源
• 3.3 GSTE 中SMC 算法的改进
• 3.3.1 GSTE 中SMC 的改进算法
• 3.3.2 改进前后SMC 算法的比较
• 3.4 通过FORTE 实现改进算法的验证
• 3.4.1 搭建FORTE 验证平台
• 3.4.2 解析EXLIF（Extended Logic Interchange Format Syntax）文件
• 3.4.3 解析FL（Functional Programming Language）文件
• 3.4.4 介绍关键代码和部分修改FORTE 的源代码
• 3.4.5 使用FORTE 平台进行验证
• 3.5 本章小结
• 第四章 自动插入故障容错结构工具的设计
• 4.1 问题来源
• 4.2 系统设计
• 4.2.1 系统结构
• 4.2.2 算法描述
• 4.3 编程分析
• 4.4 系统验证
• 4.5 本章小结
• 第五章 结论与展望
• 5.1 本文总结
• 5.1.1 主要研究成果和创新点
• 5.1.2 存在的不足
• 5.2 下一步工作的展望和设想
• 致谢
• 参考文献
• 个人简历及硕士期间研究成果