【作者】 翁延玲；

【导师】 严晓浪；

【作者基本信息】 浙江大学 ， 电路与系统， 2008， 博士

【摘要】 超大规模集成电路的验证工作在产品设计周期中所占的比例已达到三分之二。等价性验证作为现代SoC设计流程的一个重要步骤,用于验证不同抽象层设计之间的功能等效性。包含算术电路的设计的验证工作则是等价性验证的热点和难点之一。为了解决这个问题,本文作者结合自主研发等价性验证系统（ZDFV）的工作,在高效综合引擎的研究与实现、单个模块的相似性研究、数据通路的验证方法、结合半加图的算术单元验证以及基于混合SAT引擎的RTL验证流程等五个方面开展了研究:1.高效综合引擎的研究与实现:等价性验证的效率取决于两个设计的相似性,综合引擎的好坏决定了相似性。本文在充分研究Icarus Verilog可综合子集及相关综合算法的基础上,以ZDFV的综合引擎为代表,分析了高级程序语句的综合方法,提出了一种高效的综合流程,实现了模块的重用,并支持多种宏定义和编译向导。通过对Icarus Verilog和ZDFV的综合引擎的对比分析,并以IWLS₂005_bechmarks_V1.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】 VLSI verification takes about two thirds of the whole design time. In modern design flow of SoC, to guarantee the functional consistency of different abstract layers, a formal verification technique called Equivalence Checking （EC） is widely used. One challenging problem in EC is the verification of arithmetic designs. In the past few years, the author took part in the research and development of ZDFV Equivalence Checking System. Based on ZDFV work, the thesis focuses on the following key problems: how to construct an efficient synthesis engine; how to improve the structural similarity of the two designs; how to verify data path designs efficiently; how to use half adder graph to perform arithmetic unit verification; and how to use the hybrid SAT engine in the existing verification flow. The thesis includes the following original ideas and contributions.1. Research on developing high efficient synthesis engine. Synthesis engine transforms a RTL design into a gate level netlist. The quality of the result gate netlist has a significant effect on the entire verification performance. With studying and analyzing of Icarus Verilog synthesis engine and other synthesis systems/ algorithms, an effective synthesis flow was proposed and implemented in ZDFV. The synthesis engines supports module reuse, macro definition and synthesis directives. Experiments on widely used IWLS₂005_bechmarks_Vl .0 benchmark designs show that, compared with Icarus system, our synthesis method reduces the total synthesis and flattening time by 98%.2. Study on improving the module level similarity. The state-of-the-art equivalence checking algorithms fully exploit the similarity of the two designs. Better similarity means better performance. A new flow for RTL to gate level netlist equivalence checking was proposed. Our new flow first extracts design information, then synthesize the design, find internal potential equivalent point pairs and verify these potential equivalent point pairs. Unlike traditional flows, the new flow analyzes how different level of synthesis optimizations may affect the design similarity. The synthesis decision making takes different IP implementations into consideration and use heuristics to get better similarity. Experiments conducted on multipliers with different implementations show this leads to 3% to 28% running time reduction of the verification engine.3. Equivalence checking of datapath: Datapath consists of series arithmetic operations, which can be optimized according to some transformation rules. Verification of different level representations of datapath was discussed. A RTL datapath rewriting technique was developed to achieve better design similarity. For adder and multiplier tree expressions, the proposed technique also considers the variable ordering and variable combinations. Experiments on multiplier tree and adder tree expressions exhibit running time reduction of 83% to 99%, and 40% to 80% respectively.4. Arithmetic unit check with half adder graph technique: Binary Moment Diagram （BMD） technique has been used in multiplier equivalence checking. Unlike BDD, BMD adds weight （moment） on edges and thus reduces the node quantity of the diagram. A new circuit abstraction method, half adder graph was proposed to represent arithmetic circuits during the synthesis period. The new synthesis engine first analyzes the implementation of the arithmetic unit to gets its architectural information. Then use the information to guide the synthesis of the corresponding RTL design. Applying this approach on multiplier circuits, the performance of verification engine has been improved by 4%～63%.5. A new equivalence checking flow based on hybrid SAT engine: In traditional equivalence checking flow, since the verification engines are gate-based, the RTL designs have to been synthesized to gate level netlists first. In this RTL to gate translation process, some structural information of the designs is lost. In this research, a hybrid SAT engine based verification flow was proposed. The constraint propagation process in the hybrid SAT engine was discussed. Compared with traditional flow, up to 99% verification time reduction was achieved when verifying single adder unit and adder tree expressions.更多还原