数字电路后端的形式验证方法研究及应用

论文摘要

随着集成电路设计领域的发展,芯片集成度越来越高,功能越来越强大,验证的地位也越来越高。其中形式验证中的等价性检查贯穿于整个后端设计流程之中。有代码与综合后网表之间的验证等价性检查;综合后的网表与布局布线后设计之间的等价性检查。论文描述了数字电路后端验证的发展和流程。研究了等价性检查的方法,包括组合电路检查方法、时序电路检查方法。论文通过macphydl加速器模块完成了等价性检查。检查首先准备了加速器模块RTL代码与网表的信息。加速器网表的面积,RTL代码标准库（startliblphvt9t）中各个模块的面积、数量等参数。其次完成了模块验证流程。1.由准备过程产生流程与编译脚本,等价性检查在操作系统linux底下的目录。2.由抽取过程从加速器模块RTL代码中得到需要编译的代码,并且产生编译脚本。3.在编译过程中检查RTL代码与网表,并且得到要进行比较的gat文件。4.在比较过程中加上约束,给各个状态机赋输入与状态初值,查看下一状态与输出值。最后加速器模块有5000个输出不等价,有8000个下一状态不等价。由信号连接错误产生的不等价通过修改网表得到解决;由时钟门引起的不等价通过加约束删除网表中多余的时钟门得到解决;由无驱动引起的不等价通过加约束给无驱动信号赋值得到解决;由不匹配引起的不等价通过手动匹配管脚得到解决。最终结果5176个输出,10062个下一状态全等价。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 数字电路后端验证发展
• 1.1.1 数字电路后端的流程
• 1.1.2 后端中形式验证与静态时序分析的比较
• 1.2 形式验证介绍
• 1.2.1 定理证明
• 1.2.2 模型检查
• 1.2.3 等价性检查
• 1.3 本章小结
• 第二章 等价性检查的理论研究
• 2.1 等价性检查的方法
• 2.1.1 组合电路的等价性检查方法
• 2.1.2 时序电路的等价性验证方法
• 2.2 等价性验证的算法
• 2.2.1 算法介绍
• 2.2.2 割集生成算法
• 2.2.3 依赖性处理
• 2.2.4 BDD的量化算法
• 2.7 本章小结
• dl通信模块加速器的简介'>第三章 machphy_dl通信模块加速器的简介
• 3.1 模块介绍
• dl数据和控制流程的系统顶层描述'>3.2 关于macphy_dl数据和控制流程的系统顶层描述
• dl的顶层模块描述'>3.3 Macphy_dl的顶层模块描述
• dl模块的等价性验证'>第四章 对macphy_dl模块的等价性验证
• dl模块的等价性检查原理'>4.1 macphy_dl模块的等价性检查原理
• 4.1.1 加速器模块的状态机比较
• 4.1.2 加速器模块中的匹配
• 4.1.3 加速器模块中的gat文件
• 4.1.4 加速器模块的黑盒子（blackbox）效应
• 4.1.5 加速器模块等价性检查约束
• 4.1.6 加速器模块验证调试工具faultfinder的用法
• 4.1.7 加速器模块验证报告的理解
• 4.1.8 加速器模块验证中不匹配与不支持信息
• 4.1.9 加速器模块中等价性验证中的比较
• dl模块的等价性检查流程'>4.2 macphy_dl模块的等价性检查流程
• 4.2.1 准备过程（prepare）
• revised）'>4.2.2 抽取过程（extract/extract_revised）
• revised）'>4.2.3 编译过程（compile/compile_revised）
• 4.2.4 等价性比较过程（run）
• 4.3 模块验证不等价问题处理
• 4.3.1 信号连接错误产生的不等价
• 4.3.2 时钟门（clock gating）引起的不匹配
• 4.3.3 无驱动（undriven）引起的不等价
• 4.3.4 不匹配（no matched pin）引起的不等价
• 4.3.5 扫描链（scan）对比较结果的影响
• 4.4 小结
• 第五章 结论
• 5.1 意义
• 5.2 成果
• 5.3 有待探索的问题
• 致谢
• 参考文献
• 科研成果