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

摘要

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

目录

文摘

英文文摘

第一章 绪论

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.3.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 工作的展望

致谢

参考文献

个人简历及硕士期间取得的学术成果