论文部分内容阅读
超大规模集成电路的验证工作在产品设计周期中所占的比例已达到三分之二。等价性验证作为现代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验证流程比传统的验证流程有明显的优势。