针对GSTE的电路模型抽取

论文摘要

集成电路产业已经成为国民经济的朝阳产业,每年在全球产生数千亿美元的生产价值。从世界上第一个块集成电路芯片诞生至今,集成电路芯片的面积越来越小,单位面积集成的电路元器件数越来越多,如今一块芯片上已集成了数亿个门。随成电路集成度的增高,人们发现制约集成电路发展的一个重要因素是芯片设计与芯片制造的严重脱节。阻碍芯片设计发展的一个重要因素便是如何验证芯片设计的正确性。传统的模拟验证已经难以满足芯片设计的要求。而形式化验证方法因其是基于严格的数学方法来确保芯片设计的正确性,因此已经在芯片设计领域受到越来越多的重视。实现形式化验证的理论并形成相关验证工具软件的一个关键点就是电路模型的抽取和仿真。本论文首先研究和学习了形式化验证的相关理论知识,包括该理论的主要分支,发展情况。并对目前形式化验证领域的主流算法GSTE进行了深入学习和研究,并对比了该算法与传统算法的不同。其次对当前学术界以及工业界的一些常用工具SMV,VIS,FORTE等进行研究和源码剖析。并对当前电路设计语言VERILOG进行学习研究后,在基于以上工具所提供的电路描述语言的基础上简化VERILOG。设计了一套针对GSTE算法的验证工具的电路描述语言的语法和语义。然后让软件能够方便的对电路进行描述并对电路模型进行抽取。最后设计了系统的框架以及技术路线。然后,研究了电路设计前端语言描述与数字电路形式化验证算法的结合点。分析了电路模型在计算机内存中表示的相关数据结构。研究了如何将一个用语言描述的电路抽取为适合采用GSTE算法来进行验证的电路模型,使得GSTE算法能够应用在实际的电路设计领域。使用编译工具LEX,YACC实现了本软件的电路输入前端,在对语法树进行语义推理后产生了电路模型的二叉判定图数据结构后,交由后端GSTE验证算法进行电路模型的形式化验证。本论文在对数字电路仿真进行了相关研究后,基于抽取的电路模型,实现对该电路模型的仿真,能够得到相应的波形图,从来能方便的对GSTE算法进行演示。最后对全文进行了系统全面的概括总结,并指出了本文所设计工具的不足以及下一步的改进方向,并展望了形式化验证算法在电路设计领域的良好应用前景。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 引言
• 1.2 研究背景与意义
• 1.2.1 研究背景
• 1.2.2 研究意义
• 1.3 主要研究内容
• 1.4 章节安排
• 第二章 验证概念与方法介绍
• 2.1 模型检测介绍
• 2.1.1 模型检测系统模型
• 2.1.2 模型检测验证规范
• 2.1.3 模型检测算法介绍
• 2.1.4 模型检测总结
• 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.3.3 GSTE 算法介绍
• 2.3.4 GSTE 算法总结
• 2.4 本章小结
• 第三章 软件总体框架以及描述语言设计
• 3.1 现有验证工具比较
• 3.1.1 验证工具SMV
• 3.1.2 验证工具VIS
• 3.1.3 验证工具COSPAN
• 3.1.4 验证工具FORTE
• 3.2 电路描述语言以及性质描述语言设计
• 3.2.1 电路描述语言VERILOG 介绍
• 3.2.2 电路建模语言设计
• 3.2.3 电路性质描述语言设计
• 3.3 验证工具框架设计
• 3.4 技术路线和方案
• 3.5 本章小结
• 第四章 电路模型抽取与仿真的实现
• 4.1 电路模型介绍
• 4.1.1 方程表示法
• 4.1.2 自动机表示法
• 4.1.3 网表表示法
• 4.2 二叉判定图介绍及电路模型的表示
• 4.2.1 BDD 介绍
• 4.2.2 电路模型的BDD 表示
• 4.3 LEX 和YACC 介绍及电路模型抽取前端实现
• 4.3.1 LEX 呢YACC 介绍
• 4.3.2 电路模型抽取前端实现
• 4.4 电路模型抽取算法及实现
• 4.5 仿真算法及实现
• 4.6 实现结果
• 4.7 本章小结
• 第五章 总结与展望
• 5.1 本文总结
• 5.1.1 主要研究成果和创新点
• 5.1.2 存在的不足
• 5.2 下一步工作的展望和设想
• 致谢
• 参考文献
• 个人简历及硕士期间取得的学术成果