基于SystemVerilog的URAT模块功能验证

论文摘要

随着半导体工艺的发展,芯片设计的规模和复杂度日益增大,传统的验证方法已经满足不了当今的芯片验证中遇到的许多问题。以科学验证理论为基础的新的高效的验证方法,是芯片功能验证能够顺利完成的保障。本文研究的内容是与大连某世界知名电气公司合作的项目,即对一个参数可配置的UART接口电路模块进行全面的RTL级的前端功能验证,包括VMM验证和形式化验证,以确保UART的设计完全满足所提出的功能要求。文章介绍了基于System Verilog验证语言的VMM验证方法和形式化验证方法,以及VCS和0-In验证工具的使用方法,并分别使用这两种方法对UART接口模块进行了功能验证。根据UART模块的设计要求,分解出需要验证的功能测试点和断言性质,搭建了一个层次化、可重用、可扩展的VMM验证平台和一个形式化的验证环境。设计并编写了测试向量以及断言检验器程序,共检验出一个设计代码错误和12行冗余代码。对修改后设计代码的VMM验证的功能覆盖率和代码覆盖率分别达到100%和94.47%,没有发现逻辑错误,形式化验证的所有断言检验器全部通过,满足了验证的出口条件。本文还提出了将VMM验证与使用0-In工具的形式化验证相结合的功能验证方法,即先做形式化验证检验时序相关的性质,查找代码bug；再做VMM验证,检验逻辑功能的正确性。这种方法克服了传统验证方法中验证平台可重用性差、定向激励覆盖率低以及过分依赖仿真验证导致完备性不足等缺点,可以提高功能验证的效率和质量。

论文目录

• 摘要
• Abstract
• 1 绪论
• 1.1 课题背景和意义
• 1.2 芯片验证的发展史及现状
• 1.3 课题所作的主要工作及论文结构
• 2 集成电路的功能验证方法
• 2.1 SystemVerilog语言
• 2.2 VMM验证方法
• 2.2.1 VMM验证方法学特点
• 2.2.2 VMM验证流程
• 2.2.3 VMM标准库介绍
• 2.3 形式化验证方法
• 2.3.1 形式化验证的一般方法
• 2.3.2 形式化验证的流程
• 3 UART模块的VMM验证
• 3.1 UART模块介绍
• 3.1.1 UART模块的功能
• 3.1.2 UART模块的接口说明
• 3.2 VCS验证工具及其工作流程
• 3.3 UART模块的测试点分解
• 3.4 UART模块验证环境搭建
• 3.4.1 接口组件（Interface）
• 3.4.2 数据结构类（CBusTrans/UartTrans）
• 3.4.3 配置信息类（SystemConfigure/UartConfigure）
• ms_scenario_gen）'>3.4.4 场景发生器组件（vmm_ms_scenario_gen）
• 3.4.5 寄存器抽象层组件（RAL）
• 3.4.6 记分板组件（Scoreboard）
• 3.4.7 CPU端事务处理组件（CBusDriver）
• 3.4.8 UART端事务处理组件（UartPort）
• 3.4.9 验证环境（UartEnv）
• 3.4.10 测试向量（TestCase）
• 4 UART模块的形式化验证
• 4.1 O-In验证工具及其工作流程
• 4.2 断言
• 4.3 形式化验证整体框架
• 4.4 顶层控制文件
• 4.5 形式化假设
• 4.6 初始化序列
• 4.7 形式化检验器
• 4.7.1 寄存器控制模块检验器
• 4.7.2 发送模块检验器
• 4.7.3 接收模块检验器
• 5 验证结果及分析
• 5.1 VMM验证结果
• 5.1.1 bug检出
• 5.1.2 功能覆盖率
• 5.1.3 代码覆盖率
• 5.2 形式化验证结果
• 5.2.1 bug检出
• 5.2.2 验证结果
• 5.3 结果分析
• 5.3.1 两种验证结果的比较
• 5.3.2 两种验证方法的结合
• 结论
• 参考文献
• 附录A UART内部模块连接图
• 攻读硕士学位期间发表学术论文情况
• 致谢