Research on Equivalence Checking for High-Level Hardware Design Descriptions

近年来，我们需要花费更多的时间在设计验证上，设计验证占整个设计过程的60%到80%。为了缓解这一困难，人们采用了形式化的验证技术，但目前几乎所有可用的技术都不能处理高于寄存器传送级或门级的描述。在这项研究中，我们研究了两种高级描述的功能等价性验证，比如用C语言编写的描述。通过用一阶逻辑的函数符号来抽象描述中的算术运算，并研究符号的具体含义，可以预期验证效率的提高。为了弥补这一困难，在本研究中，我们提出了一种新的考虑等价性约束的等价性验证算法。等价约束是一组规则，如“x&gt；1&lt；-&gt；x-L&gt；0”。它们的引入是为了指定应该被视为等同的模式。我们改进了布尔可满足性检验的“冲突分析”技术，并尝试了PARCOR滤波器、ADPCM滤波器、傅里叶变换和平方根的程序的等价性检验。实验结果表明，与经典的基于布尔的验证方法相比，对于包含比乘法更复杂的运算的实例，即非线性运算，我们可以将效率提高10-100倍。除了这一改进外，对于一些经典方法难以解决的计算复杂性的例子，我们提出的方法使验证变得可行。

In recent years, we need to spend more of time in design verification, which occupies 60 to 80 percent of the entire design process. To ease this difficulty, formal verification technology has been adopted, but almost all the currently available technologies cannot handle descriptions whose level is higher than register-transfer level or gate level. In this research, we study on functional equivalence checking of two high-level descriptions, such as those written in C language. By abstracting arithmetic operations in descriptions by function symbols of first-order logic, and by ingnoring the specific meaning of the symbols, we can expect the improvement in the verification efficiency.The problem is that this approach can be applied only to very similar descriptions. To compensate for this difficulty, in this research, we propose a new equivalence checking algorithm considering "equivalence constraints". An equivalence constraint is a set of rules such as "x > 1 <-> x-l>0". They are introduced to specify patterns which should be regarded as equivalent. We modified "conflict analysis" technique which has been used for boolean satisfiability checking to our approach, and we attempted equivalence checking of programs for PARCOR filter, ADPCM filter, Fourier Transform and Square Rooting. The experimental results show that, as compared with the classical boolean based verification method, we can improve the efficiency by 10-100 times for the examples including operations which are more complex than multifications, that is, non-linear operations. In addition to this improvement, for some examples which are intractable in terms of computational complexity with the classical technique, verification became feasible with our proposed method.