RTL到门级设计的等价性验证的研究

论文摘要

超大规模集成电路的验证工作在产品设计周期中所占的比例已达到三分之二。等价性验证作为现代SoC设计流程的一个重要步骤,用于验证不同抽象层设计之间的功能等效性。包含算术电路的设计的验证工作则是等价性验证的热点和难点之一。为了解决这个问题,本文作者结合自主研发等价性验证系统（ZDFV）的工作,在高效综合引擎的研究与实现、单个模块的相似性研究、数据通路的验证方法、结合半加图的算术单元验证以及基于混合SAT引擎的RTL验证流程等五个方面开展了研究:1.高效综合引擎的研究与实现:等价性验证的效率取决于两个设计的相似性,综合引擎的好坏决定了相似性。本文在充分研究Icarus Verilog可综合子集及相关综合算法的基础上,以ZDFV的综合引擎为代表,分析了高级程序语句的综合方法,提出了一种高效的综合流程,实现了模块的重用,并支持多种宏定义和编译向导。通过对Icarus Verilog和ZDFV的综合引擎的对比分析,并以IWLS2005bechmarksV1.0为测试基础,实验结果显示:在相同的测试平台下,ZDFV的综合引擎在处理多文件描述的Verilog设计时具有更好的兼容性,而对于不带层次结构描述的Verilog设计时间上的改善度可高达98%。2.单个模块的相似性研究:模块相似性在等价性验证中具有重要的指引作用,对验证引擎的性能有着关键性的影响。本文提出了一种新的从RTL到门级网表的等价性验证流程:提取电路信息、综合待验证的设计、匹配待验证设计的等价点、比较待验证设计的等价点。不同于传统验证流程,为获得最好的电路相似性,此流程深入研究了综合优化等因素在不同层次上对电路相似性的破坏,提出了在综合阶段对比IP的不同实现方案,并进行启发式决策。以验证不同实现方案的乘法电路为例,本算法的验证准确性更高,而验证时间可减少3%～28%。3.数据通路的验证:数据通路由一系列的算术表达式在行为域里表示,可按具体的变换规则进行优化组合。依照不同描述级,本文讨论了验证不同数据通路表示的各种算法,通过在寄存器传输级上比较重写数据通路以证明其等价性,提出了在数据通路级指导综合过程,有效简化了网表级等价性验证的复杂度。比如针对加法和乘法连续运算的表达式,算法从实现电路中提取变量顺序和结合顺序并加以利用,实验表明,在验证乘法连续运算的表达式时减少了83%～99%的时间,加法连续运算表达式的验证时间也可减少40%～89%。4.结合半加图的算术单元验证:论文研究了基于BMD验证乘法电路的方法,该方法使用矩分解（moment decomposition）方式,在BMD的边和节点上赋予权重信息,减少了图的节点数。讨论了一种新的电路表示方法——半加图（Half Adder Graph）,提出在综合阶段使用半加图表示算术电路,从中得到算术电路的实现方案,进一步指导算术电路的综合。统计提取电路实现和验证的时间花销,以乘法电路为例,本算法能明显提高验证引擎的性能（4%～63%）。5.基于混合SAT引擎的RTL验证流程:传统验证流程需要将电路综合为门级网表,但门级验证引擎不能有效利用一些原始的电路的信息。本文提出了一种新的基于混合SAT引擎的验证流程,讨论了混合SAT引擎的约束传递过程。以不同规模的加法单个运算和连续运算表达式为例,比较传统验证流程验证时间最多可减少99%。实验结果表明基于混合SAT引擎的RTL验证流程比传统的验证流程有明显的优势。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 课题背景
• 1.2 研究现状
• 1.2.1 等价性验证的研究现状
• 1.2.2 综合引擎的研究现状
• 1.2.3 算术电路等价性验证的研究现状
• 1.3 论文的主要工作和创新点
• 1.4 论文的组织结构
• 第2章 ZDFV的综合引擎的设计与实现
• 2.1 综合技术简述
• 2.2 综合引擎在验证系统中的位置
• 2.3 可综合的Verilog描述子集
• 2.3.1 变量声明和使用
• 2.3.2 连续赋值语句
• 2.3.3 过程赋值语句
• 2.3.4 串行语句块
• 2.3.5 高级程序语句
• 2.4 Icarus Verilog的实现
• 2.4.1 预处理
• 2.4.2 初步解析（parse）
• 2.4.3 精解析（elaborate）
• 2.4.4 综合优化（synthesis）
• 2.4.5 代码生成
• 2.5 对Icarus Verilog的改进
• 2.5.1 增加对高级程序语句的支持
• 2.5.2 提高综合引擎的通用性
• 2.5.3 采取多种手段提高运行效率
• 2.6 ZDFV综合引擎的实现
• 2.7 实验数据
• 2.8 小结
• 第3章 提高电路相似性的算法研究
• 3.1 组合电路等价性验证方法概述
• 3.1.1 功能等价性验证方法
• 3.1.2 增量等价性验证方法
• 3.2 面向通用模块的相似性算法
• 3.2.1 综合优化对电路结构的影响
• 3.2.2 算法实现细节及复杂度分析
• 3.3 实验结果
• 3.4 小结
• 第4章 数据通路的等价性验证
• 4.1 数据通路的等价性研究现状
• 4.2 算法模型和定理
• 4.3 算符排序算法
• 4.3.1 距离计算
• 4.3.2 初始变量分组
• 4.3.3 乘数被乘数的识别
• 4.3.4 验证框架
• 4.4 实例分析
• 4.5 小结
• 第5章 结合HAG的算术单元等价性验证
• 5.1 算术单元等价性验证的研究现状
• 5.2 算法模型和定义
• 5.3 电路实现方案提取算法
• 5.3.1 HAG提取算法
• 5.3.2 加法树构架提取
• 5.3.3 乘法编码方式识别
• 5.4 结合HAG的算术电路验证
• 5.5 测试结果与分析
• 5.6 小结
• 第6章 基于混合SAT引擎的RTL验证算法
• 6.1 布尔逻辑的SAT引擎
• 6.1.1 电路布尔逻辑的SAT模型
• 6.1.2 布尔逻辑的SAT引擎
• 6.2 混合SAT引擎求解电路问题
• 6.2.1 混合SAT引擎的研究现状
• 6.2.2 HDPLL算法
• 6.3 基于混合SAT引擎的RTL验证系统
• 6.3.1 实现细节
• 6.3.2 实验数据
• 6.4 小结
• 第7章 结论与展望
• 7.1 论文工作小结
• 7.2 下一步工作展望
• 参考文献
• 致谢
• 附录 1: Bench文件语法
• 附录 2: 攻读学位期间发表/录用的学术论文