High-level Hardware Verification Based on Equivalence Logic with Similarities

针对高层次的形式化硬件验证，研究了基于无解释函数和相似性的等价逻辑的等价性验证系统。原始的等价逻辑处理变量的等价性，并已被证明是有效的流水线处理器的验证。具有相似性的等价逻辑是处理变量之间相似性的逻辑系统。例如，如果我们用定点数系统设计一个电路，我们想证明相对于使用浮点数系统的C程序的正确性，那么不能证明精确的等价性，我们应该科普相似性。首先，我们开发了一个原型系统，它将Verilog描述转换为等价逻辑公式，一个将C语言描述转换为等价逻辑公式的原型系统，以及一个基于时间扩展和已发表的等价逻辑检验系统（如CVCL/YICES）的原型等价检验系统。我们已经测试了原型系统和声音的计算是成比例的指数相对于时间的扩张，我们已经工作的SAT基于等价性检查和传递性约束问题。对于相似性，我们正在研究浮点到定点转换中变量位数的优化，以及基于值的差异的相似性和基于与其他活动变量值的差异的相似性。我们也将建议的等价性检查应用到多线程处理器的设计和加速使用原型环境的等价性验证。

For the formal hardware verification at high level, the equivalence checking system based on the equivalence logic with un-interpreted functions and similarities has been studied. The original equivalence logic manipulates the equivalence of variables, and has been shown to be effective for the verification of pipeline processor. The equivalence logic with similarities is a logic system to manipulate the similarity between variables. For example, if we design a circuit with fixed-point number system, and we would like to show the correctness with respect to a C program using floating number system, then the exact equivalence cannot be shown and we should cope with the similarity At first, we have developed a prototyping system which converts Verilog description to the equivalence logic formula, a prototyping system converting C descriptions to the equivalence logic formulae, and a prototype equivalence checking system based on the time expansion and published equivalence logic checking system(like CVCL/YICES). We have tested the prototype system and Sound that the computation is proportional to the exponential with respect to the number of time expansions, and we have worked on the SAT based equivalence checking and the transitivity constraints issue. For similarities, we are working on the optimization of the number of bits of variables in the floating to fixed point conversion, and the similarity based on the difference of the values and one based one the difference with values of other live variables. We have also applied the proposed equivalence checking to the multi-threading processor design and the acceleration of equivalence verification using the prototyping environment.