存储控制器是很多芯片的关键接口部件,存储控制器正确稳定的运行是整个芯片稳定工作的前提保证。在验证存储控制器正确性时,如果采用单一的模拟验证方法则会遇到激励不能遍历所有状态空间的问题,这样便无法证明设计输出的接口信号是否完全符合DDR4等存储器接口标准。不仅如此,为了提升访存效率,设计人员需要对存储控制器读写请求的调度方法进行优化,因此读写请求的仲裁方法有较高的复杂性,所以本文主要针对存储控制器读写请求队列仲裁逻辑的正确性和存储控制器各个输出命令间时序关系的正确性进行验证分析和研究。本文首先分析了存储控制器验证环节遇到的困难,介绍了目前国内外验证存储控制器的常用方法和几种存储控制器命令间时序关系正确性验证中断言的自动生成方法。然后介绍了三种常用的形式验证方法,说明了模型检测原理和环境创建方法、并简要说明验证中采用的基于断言的验证方法。通过介绍存储控制器工作原理、结构组成、输出命令间时序关系、请求仲裁策略说明了存储控制器的结构和功能。形式验证方法是运用数学原理来验证设计的正确性,可以自动遍历所有需要验证的状态空间,相比模拟验证表现出了更好的完备性和高效性,所以本文提出了一种基于模型检测的形式验证方法来验证存储控制器正确性。本文首先对两个功能模块分别搭建参考模型、约束模块输入、编写形式验证断言、再运用形式验证工具验证存储控制器对应功能正确性,并在总结分析形式验证结果的基础上调整验证环境提高形式验证覆盖率,完成了存储控制器各个输出命令间时序关系的正确性验证和存储控制器读写请求队列仲裁逻辑的正确性验证。在验证存储控制器输出命令间时序关系正确性时,由于相关的DDR4标准比较复杂,可能会出现人工编写的形式验证断言无法快速标准化和准确化的问题,所以本文结合DDR4标准的特点开发出了该模块形式验证断言的自动生成工具。通过总结命令间延时的计算方法,编写脚本,运用脚本处理DDR4标准中的数据来生成断言。该工具可以根据当前验证模式设定的基础值,生成对应断言,进一步的提升了形式验证效率和验证准确性。