基于GSTE理论的抽象与细化问题的研究

论文摘要

近年来,由于电路规模不断增大和集成度不断提高,使得超大规模集成电路(VLSI)变得越来越复杂,而设计过程又难以保证逻辑设计的正确性。同时集成电路设计时的差错所带来的损失巨大,当前没有修复芯片的技术不可能对VLSI中的错误部分进行修正。因此,设计和建立高可靠性的集成电路系统成为一个关键问题。验证作为一个的保证设计正确的重要环节,正发挥着越来越重要的作用,并引起人们越来越多的关注和兴趣。本课题在GSTE理论的基础上,研究抽象以及细化处理在该理论上的应用,希望解决由抽象所带来的效率以及验证精确性的统一问题。通过变量划分技术,对变量集有区别的进行抽象以有效表示状态空间;为有效地表示相关变量的状态集,使用参数化表示将状态空间进行压缩化处理,并利用BDD技术实现GSTE理论验证算法。由于当前形式化验证方法基于状态搜索的处理方法,因此存在处理能力有限的问题,而不能验证大规模的电路系统。当前大部分形式化验证工具都引入了抽象与细化处理,来解决状态爆炸的问题。在研究方法上,首先,本文讲述了为解决状态爆炸问题而产生的形式化验证方法,简要分析了它们的验证思想以及存在的问题。其次,讲了形式化验证方法如何对验证电路进行建模,并重点介绍当前主要的形式化验证方法:STE和GSTE,并且对电路模型的定义,验证规范的描述以及验证算法进行分析,同时针对它们验证模拟的原理和方法,分析其优缺点,并对它们进行对比分析。进一步了解了抽象处理的方法以及对电路的符号化处理技术,同时分析了GSTE的抽象处理以及细化处理的过程。在以上理论学习和分析的基础上,本文提出了基于GSTE的抽象处理以及状态参数化表示的改进算法,并在验证过程中对验证的性质进行变量的划分,只验证与断言相关的变量,有效地减少了状态数。在验证过程中引入参数化表示方法,可以对状态空间进行有效地表示,尽可能压缩状态空间并使用BDD来实现GSTE验证算法。通过这些技术有效提高了GSTE模拟验证的处理能力以及它的验证效率。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 课题背景
• 1.2 形式化验证
• 1.2.1 形式化验证的基本概念和原理
• 1.2.2 形式化验证方法的意义以及不足
• 1.3 形式化验证方法的发展
• 1.3.1 抽象方法的提出以及意义
• 1.3.2 模型验证方法
• 1.3.3 有界模型验证
• 1.3.4 无界模型检验
• 1.4 研究意义
• 1.5 主要研究内容和章节安排
• 1.5.1 主要研究内容
• 1.5.2 章节安排
• 第二章 符号轨迹赋值和推广化轨迹赋值简介
• 2.1 电路模型
• 2.1.1 硬件电路的功能模型
• 2.1.2 硬件电路的结构模型
• 2.2 符号轨迹赋值（STE）介绍
• 2.2.1 STE 电路模型的定义
• 2.2.2 STE 验证规范的相关概念
• 2.2.3 STE 验证算法过程
• 2.2.4 STE 的优点与不足
• 2.3 推广化符号轨迹赋值（GSTE）介绍
• 2.3.1 GSTE 电路模型以及性质描述
• 2.3.2 GSTE 验证算法
• 2.4 GSTE 和STE 检验方法的比较
• 2.5 本章小结
• 第三章 抽象与细化方法的研究
• 3.1 符号处理技术
• 3.1.1 二叉判定图
• 3.1.2 四值逻辑编码
• 3.2 抽象的相关概念以及原理
• 3.2.1 抽象的相关定义以及分类
• 3.2.2 抽象方法
• 3.3 细化处理
• 3.3.1 符号常量
• 3.3.2 符号变量
• 3.4 抽象及细化方法在GSTE 中的应用
• 3.5 本章小结
• 第四章 GSTE 抽象与细化方法的改进
• 4.1 问题来源
• 4.2 抽象与细化问题分析
• 4.2.1 四值模型抽象的问题分析
• 4.2.2 GSTE 抽象细化的问题分析
• 4.3 GSTE 算法改进
• 4.3.1 变量划分算法
• 4.3.2 参数化表示和提取算法
• 4.4 GSTE 抽象细化处理算法改进
• 4.4.1 改进GSTE 的软件框架
• 4.4.2 改进的GSTE 关键代码
• 4.5 算法分析及验证
• 4.5.1 对变量划分的算法的分析
• 4.5.2 对参数化表示算法的分析
• 4.5.3 算法验证
• 4.6 本章小结
• 第五章 结论与展望
• 5.1 本文总结
• 5.1.1 主要研究成果和创新点
• 5.1.2 存在的不足
• 5.2 工作的展望
• 致谢
• 参考文献
• 个人简历及硕士期间取得的学术成果