基于形式验证方法的数字LTE芯片逻辑等价性分析及研究
发布时间：2021-05-15 06:25
纵观整个芯片设计流程,从最初的架构设计到最后的投片,验证是用时最长且重要性最高的环节。对目前纳米级的设计规模而言,传统的动态验证方式已经不足以完成对整体设计的验证工作。形式验证方法因为验证覆盖的完备性,面对大规模设计的高效性,非常切合芯片后端物理实现的验证需求,因而越发广泛地被业界采用。如何对验证失败的情况进行分析,快速准确地定位问题,并提供可行的调试方案,已成为实际工程领域关注的重点。本论文在较为全面地研究总结当前广泛应用于芯片后端设计实现的形式验证技术的基础上,结合自身在实习期间的项目经历,对形式验证在数字LTE芯片实际工程中所采用的逻辑等价性对比进行了分析,取得了较为理想的结果。主要内容包括:首先在数字LTE芯片形式验证的流程方面,论文将芯片形式验证的流程细化为环境搭建、初始化、读入文件和约束、选项设置和等价性对比五个步骤,使后续工作中对结果进行分析和调试的范围更加清晰。结合LEC工具的指令对具体的运行脚本进行规范,明确了验证过程中必要的指令及相关选项。并且基于平展化和层次化这两种不同的逻辑等价性对比方式,分别对其各自的原理、实现方法和特点进行分析。然后在逻辑等价性对比结果方面,...
【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校
【文章页数】：83 页
【学位级别】：硕士
【文章目录】：
摘要
ABSTRACT
缩略语对照表
第一章 绪论
1.1 论文背景及意义
1.2 国内外研究现状
1.3 论文研究重点及章节安排
第二章 验证方法学综述
2.1 动态验证技术
2.2 静态验证技术
2.2.1 静态时序验证
2.2.2 设计规则验证
2.2.3 版图验证
2.3 形式验证方法
2.3.1 定理证明
2.3.2 模型检测
2.3.3 等价性验证
2.4 工程中的形式验证
2.4.1 形式验证工具简介
2.4.2 LEC的等价性验证方法
2.5 本章小结
第三章 LEC形式验证的流程
3.1 LEC形式验证准备阶段
3.1.1 环境搭建
3.1.2 初始化
3.1.3 读入文件和约束
3.1.4 选项设置
3.2 LEC形式验证对比阶段
3.2.1 平展化模式
3.2.2 层次化模式
3.3 本章小结
第四章 逻辑等价性验证的结果分析
4.1 平展化模式的调试思路
4.2 平展化模式的结果分析
4.2.1 文件缺失
4.2.2 名称错误
4.2.3 UPF问题
4.2.4 扫描信号参与逻辑
4.2.5 设计或综合问题
4.3 层次化模式的调试思路
4.4 层次化模式的结果分析
4.4.1 DesignWare问题
4.4.2 实例化问题
4.5 等价性验证中断问题
4.5.1 中断的成因及危害
4.5.2 避免中断的方法
4.5.3 传统的中断解决方法
4.5.4 采用隔离对比法解决中断
4.6 本章小结
第五章 总结与展望
5.1 论文工作总结
5.2 进一步的工作展望
参考文献
致谢
作者简介
【参考文献】：
期刊论文
[1]基于逻辑的形式化验证方法:进展及应用[J]. 陈钢,于林宇,裘宗燕,王颖. 北京大学学报(自然科学版). 2016(02)
[2]片上系统高层等价性检验研究进展[J]. 胡健,李暾,李思昆. 计算机辅助设计与图形学学报. 2016(03)
[3]集成电路技术和产业发展现状与趋势[J]. 方圆,徐小田. 微电子学. 2014(01)
[4]SpaceWire译码电路在HOL4中的形式化验证[J]. 张玉鹏,施智平,关永,李黎明,赵春娜,张杰. 小型微型计算机系统. 2013(08)
[5]模型检测中状态爆炸问题研究综述[J]. 侯刚,周宽久,勇嘉伟,任龙涛,王小龙. 计算机科学. 2013(S1)
[6]基于IP技术的模拟集成电路设计研究[J]. 李群,樊丽春. 科技创新导报. 2013(08)
[7]数字电路IP软核任务流方法验证[J]. 何朝军,李哲英. 电子测量技术. 2011(08)
[8]集成电路技术的发展[J]. 陈飚. 微处理机. 2011(03)
[9]利用SMT约束分解方法求解RTL可满足性问题[J]. 赵燕妮,边计年,邓澍军. 计算机辅助设计与图形学学报. 2010(02)
[10]基于混合自动机的PSL模型研究[J]. 张萌,高德远,樊晓桠. 计算机应用研究. 2010(01)
博士论文
[1]模型检测中关键技术的研究及其应用[D]. 刘志锋.南京大学 2011
[2]集成电路的逻辑等价性验证研究[D]. 杨军.浙江大学 2007
[3]超大规模集成电路形式验证的方法研究[D]. 卢永江.浙江大学 2005
硕士论文
[1]基于图论的形式化验证方法的研究与实现[D]. 陈凌宇.电子科技大学 2016
[2]基于SOC Encounter的ASIC芯片后端设计研究[D]. 骆礼厅.西安电子科技大学 2014
[3]基于UVM的高效验证平台设计及可重用性研究[D]. 黄欣.上海交通大学 2014
[4]基于多项式符号代数的电路形式验证[D]. 闫硕.北京交通大学 2011
[5]异步FIFO的设计与形式化验证[D]. 刘彬.国防科学技术大学 2011
[6]大规模数字集成电路中的验证技术及其应用[D]. 廉玉平.浙江大学 2010
[7]0.35um标准单元库的设计技术研究及实现[D]. 黄义定.江南大学 2006
本文编号：3187129
【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校
【文章页数】：83 页
【学位级别】：硕士
【文章目录】：
摘要
ABSTRACT
缩略语对照表
第一章 绪论
1.1 论文背景及意义
1.2 国内外研究现状
1.3 论文研究重点及章节安排
第二章 验证方法学综述
2.1 动态验证技术
2.2 静态验证技术
2.2.1 静态时序验证
2.2.2 设计规则验证
2.2.3 版图验证
2.3 形式验证方法
2.3.1 定理证明
2.3.2 模型检测
2.3.3 等价性验证
2.4 工程中的形式验证
2.4.1 形式验证工具简介
2.4.2 LEC的等价性验证方法
2.5 本章小结
第三章 LEC形式验证的流程
3.1 LEC形式验证准备阶段
3.1.1 环境搭建
3.1.2 初始化
3.1.3 读入文件和约束
3.1.4 选项设置
3.2 LEC形式验证对比阶段
3.2.1 平展化模式
3.2.2 层次化模式
3.3 本章小结
第四章 逻辑等价性验证的结果分析
4.1 平展化模式的调试思路
4.2 平展化模式的结果分析
4.2.1 文件缺失
4.2.2 名称错误
4.2.3 UPF问题
4.2.4 扫描信号参与逻辑
4.2.5 设计或综合问题
4.3 层次化模式的调试思路
4.4 层次化模式的结果分析
4.4.1 DesignWare问题
4.4.2 实例化问题
4.5 等价性验证中断问题
4.5.1 中断的成因及危害
4.5.2 避免中断的方法
4.5.3 传统的中断解决方法
4.5.4 采用隔离对比法解决中断
4.6 本章小结
第五章 总结与展望
5.1 论文工作总结
5.2 进一步的工作展望
参考文献
致谢
作者简介
【参考文献】：
期刊论文
[1]基于逻辑的形式化验证方法:进展及应用[J]. 陈钢,于林宇,裘宗燕,王颖. 北京大学学报(自然科学版). 2016(02)
[2]片上系统高层等价性检验研究进展[J]. 胡健,李暾,李思昆. 计算机辅助设计与图形学学报. 2016(03)
[3]集成电路技术和产业发展现状与趋势[J]. 方圆,徐小田. 微电子学. 2014(01)
[4]SpaceWire译码电路在HOL4中的形式化验证[J]. 张玉鹏,施智平,关永,李黎明,赵春娜,张杰. 小型微型计算机系统. 2013(08)
[5]模型检测中状态爆炸问题研究综述[J]. 侯刚,周宽久,勇嘉伟,任龙涛,王小龙. 计算机科学. 2013(S1)
[6]基于IP技术的模拟集成电路设计研究[J]. 李群,樊丽春. 科技创新导报. 2013(08)
[7]数字电路IP软核任务流方法验证[J]. 何朝军,李哲英. 电子测量技术. 2011(08)
[8]集成电路技术的发展[J]. 陈飚. 微处理机. 2011(03)
[9]利用SMT约束分解方法求解RTL可满足性问题[J]. 赵燕妮,边计年,邓澍军. 计算机辅助设计与图形学学报. 2010(02)
[10]基于混合自动机的PSL模型研究[J]. 张萌,高德远,樊晓桠. 计算机应用研究. 2010(01)
博士论文
[1]模型检测中关键技术的研究及其应用[D]. 刘志锋.南京大学 2011
[2]集成电路的逻辑等价性验证研究[D]. 杨军.浙江大学 2007
[3]超大规模集成电路形式验证的方法研究[D]. 卢永江.浙江大学 2005
硕士论文
[1]基于图论的形式化验证方法的研究与实现[D]. 陈凌宇.电子科技大学 2016
[2]基于SOC Encounter的ASIC芯片后端设计研究[D]. 骆礼厅.西安电子科技大学 2014
[3]基于UVM的高效验证平台设计及可重用性研究[D]. 黄欣.上海交通大学 2014
[4]基于多项式符号代数的电路形式验证[D]. 闫硕.北京交通大学 2011
[5]异步FIFO的设计与形式化验证[D]. 刘彬.国防科学技术大学 2011
[6]大规模数字集成电路中的验证技术及其应用[D]. 廉玉平.浙江大学 2010
[7]0.35um标准单元库的设计技术研究及实现[D]. 黄义定.江南大学 2006
本文编号：3187129
本文链接：https://www.wllwen.com/shekelunwen/ljx/3187129.html
