存储控制器形式化验证方法研究与实现
发布时间：2021-07-24 15:17
存储控制器是很多芯片的关键接口部件,存储控制器正确稳定的运行是整个芯片稳定工作的前提保证。在验证存储控制器正确性时,如果采用单一的模拟验证方法则会遇到激励不能遍历所有状态空间的问题,这样便无法证明设计输出的接口信号是否完全符合DDR4等存储器接口标准。不仅如此,为了提升访存效率,设计人员需要对存储控制器读写请求的调度方法进行优化,因此读写请求的仲裁方法有较高的复杂性,所以本文主要针对存储控制器读写请求队列仲裁逻辑的正确性和存储控制器各个输出命令间时序关系的正确性进行验证分析和研究。本文首先分析了存储控制器验证环节遇到的困难,介绍了目前国内外验证存储控制器的常用方法和几种存储控制器命令间时序关系正确性验证中断言的自动生成方法。然后介绍了三种常用的形式验证方法,说明了模型检测原理和环境创建方法、并简要说明验证中采用的基于断言的验证方法。通过介绍存储控制器工作原理、结构组成、输出命令间时序关系、请求仲裁策略说明了存储控制器的结构和功能。形式验证方法是运用数学原理来验证设计的正确性,可以自动遍历所有需要验证的状态空间,相比模拟验证表现出了更好的完备性和高效性,所以本文提出了一种基于模型检测的形...
【文章来源】：安徽大学安徽省 211工程院校
【文章页数】：76 页
【学位级别】：硕士
【部分图文】：
基于TDML的SVA断言生成方法
安徽大学硕士学位论文9错误，工具发现错误时可以提供错误场景帮助验证人员分析错误。根据形式验证结果分析覆盖率状况，并通过分析后的结果优化形式验证环境，提高形式验证覆盖率。图2.1模型检测验证方法示意图下图2.2是模型检测查错示意图，在模型检测时首先是根据设计需求定义输入可以搜索的状态范围，在状态搜索过程中工具会首先建立一个初始状态，并进行扩展进入下一个状态，除非有明确的状态约束，否则扩展将一直进行。在查找过程中可能会出现状态重复的情况，但是不管过程如何，工具都会遍历所有的状态空间，然后工具会将所有状态的输出值和模型检测中的标准值进行对比检查，在进行断言检查的过程中，如果出现了输出值不符合断言属性的状况，模型检测工具会反方向运行，推导出出错时的输入状态，这就是上文中提到的工具给出反例的原理。图2.2模型检测查错示意图
安徽大学硕士学位论文9错误，工具发现错误时可以提供错误场景帮助验证人员分析错误。根据形式验证结果分析覆盖率状况，并通过分析后的结果优化形式验证环境，提高形式验证覆盖率。图2.1模型检测验证方法示意图下图2.2是模型检测查错示意图，在模型检测时首先是根据设计需求定义输入可以搜索的状态范围，在状态搜索过程中工具会首先建立一个初始状态，并进行扩展进入下一个状态，除非有明确的状态约束，否则扩展将一直进行。在查找过程中可能会出现状态重复的情况，但是不管过程如何，工具都会遍历所有的状态空间，然后工具会将所有状态的输出值和模型检测中的标准值进行对比检查，在进行断言检查的过程中，如果出现了输出值不符合断言属性的状况，模型检测工具会反方向运行，推导出出错时的输入状态，这就是上文中提到的工具给出反例的原理。图2.2模型检测查错示意图
【参考文献】：
期刊论文
[1]一种基于脚本语言的DDR控制器的验证方法[J]. 罗军,郭涛,张修钦,王玉冰. 集成电路应用. 2018(06)
[2]基于属性的形式验证技术及应用[J]. 游余新. 中国集成电路. 2013(12)
博士论文
[1]基于UML2.0模型的测试与验证方法[D]. 张琛.西安电子科技大学 2012
[2]列车运行控制系统分层形式化建模与验证分析[D]. 吕继东.北京交通大学 2011
[3]基于功能信息的验证工程学及若干验证技术研究[D]. 张多利.合肥工业大学 2005
硕士论文
[1]面向MC-SoC的验证方法研究与实现[D]. 郭少成.电子科技大学 2019
[2]基于Coq的工控程序验证[D]. 周敏.东南大学 2018
[3]基于SystemC的多通道DDR控制器建模设计[D]. 沈鹏程.南京大学 2018
[4]基于模型检测的外设控制器验证方法研究及应用[D]. 王思琦.湖南大学 2018
[5]基于LCoS时序彩色显示的DDR2 SDRAM控制器的设计与验证[D]. 王长森.湘潭大学 2018
[6]高频动态编码信号采集与存储系统研究[D]. 方国昌.中北大学 2018
[7]MC-SOC中存储控制器的设计与验证[D]. 陈捷.电子科技大学 2018
[8]从Murphi到Ocaml语言的编译器及其在模型检测中的应用[D]. 范帅.北京交通大学 2017
[9]向量定点运算单元的形式化验证[D]. 朱青.西安电子科技大学 2017
[10]一种基于DDR4控制器的访存调度优化策略[D]. 剧诺璇.西安电子科技大学 2017
本文编号：3300903
【文章来源】：安徽大学安徽省 211工程院校
【文章页数】：76 页
【学位级别】：硕士
【部分图文】：
基于TDML的SVA断言生成方法
安徽大学硕士学位论文9错误，工具发现错误时可以提供错误场景帮助验证人员分析错误。根据形式验证结果分析覆盖率状况，并通过分析后的结果优化形式验证环境，提高形式验证覆盖率。图2.1模型检测验证方法示意图下图2.2是模型检测查错示意图，在模型检测时首先是根据设计需求定义输入可以搜索的状态范围，在状态搜索过程中工具会首先建立一个初始状态，并进行扩展进入下一个状态，除非有明确的状态约束，否则扩展将一直进行。在查找过程中可能会出现状态重复的情况，但是不管过程如何，工具都会遍历所有的状态空间，然后工具会将所有状态的输出值和模型检测中的标准值进行对比检查，在进行断言检查的过程中，如果出现了输出值不符合断言属性的状况，模型检测工具会反方向运行，推导出出错时的输入状态，这就是上文中提到的工具给出反例的原理。图2.2模型检测查错示意图
安徽大学硕士学位论文9错误，工具发现错误时可以提供错误场景帮助验证人员分析错误。根据形式验证结果分析覆盖率状况，并通过分析后的结果优化形式验证环境，提高形式验证覆盖率。图2.1模型检测验证方法示意图下图2.2是模型检测查错示意图，在模型检测时首先是根据设计需求定义输入可以搜索的状态范围，在状态搜索过程中工具会首先建立一个初始状态，并进行扩展进入下一个状态，除非有明确的状态约束，否则扩展将一直进行。在查找过程中可能会出现状态重复的情况，但是不管过程如何，工具都会遍历所有的状态空间，然后工具会将所有状态的输出值和模型检测中的标准值进行对比检查，在进行断言检查的过程中，如果出现了输出值不符合断言属性的状况，模型检测工具会反方向运行，推导出出错时的输入状态，这就是上文中提到的工具给出反例的原理。图2.2模型检测查错示意图
【参考文献】：
期刊论文
[1]一种基于脚本语言的DDR控制器的验证方法[J]. 罗军,郭涛,张修钦,王玉冰. 集成电路应用. 2018(06)
[2]基于属性的形式验证技术及应用[J]. 游余新. 中国集成电路. 2013(12)
博士论文
[1]基于UML2.0模型的测试与验证方法[D]. 张琛.西安电子科技大学 2012
[2]列车运行控制系统分层形式化建模与验证分析[D]. 吕继东.北京交通大学 2011
[3]基于功能信息的验证工程学及若干验证技术研究[D]. 张多利.合肥工业大学 2005
硕士论文
[1]面向MC-SoC的验证方法研究与实现[D]. 郭少成.电子科技大学 2019
[2]基于Coq的工控程序验证[D]. 周敏.东南大学 2018
[3]基于SystemC的多通道DDR控制器建模设计[D]. 沈鹏程.南京大学 2018
[4]基于模型检测的外设控制器验证方法研究及应用[D]. 王思琦.湖南大学 2018
[5]基于LCoS时序彩色显示的DDR2 SDRAM控制器的设计与验证[D]. 王长森.湘潭大学 2018
[6]高频动态编码信号采集与存储系统研究[D]. 方国昌.中北大学 2018
[7]MC-SOC中存储控制器的设计与验证[D]. 陈捷.电子科技大学 2018
[8]从Murphi到Ocaml语言的编译器及其在模型检测中的应用[D]. 范帅.北京交通大学 2017
[9]向量定点运算单元的形式化验证[D]. 朱青.西安电子科技大学 2017
[10]一种基于DDR4控制器的访存调度优化策略[D]. 剧诺璇.西安电子科技大学 2017
本文编号：3300903
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/3300903.html
