High-level Hardware Verification Based on Equivalence Logic with Similarities

基于相似等价逻辑的高级硬件验证

• 批准号: 17500047
• 负责人: KIMURA Shinji
• 金额: $ 2.32万
• 依托单位: Waseda University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2005
• 资助国家: 日本
• 起止时间: 2005 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17500047/
• 关键词: equivalence logic; equivalence hardware verification; uninterpreted function; term rewriting system; high level verification

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.

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

项目成果

Transition traversal coverage estimation for symbolic model checking

• DOI: 10.1109/icasic.2005.1611460
• 发表时间: 2005-12
• 期刊: 2005 6th International Conference on ASIC
• 作者: Xingwen Xu;Shinji Kimura;K. Horikawa;T. Tsuchiya

Bit-Length Optimization Method for High-Level Synthesis based on Non-Linear Programming Technique

基于非线性规划技术的高级综合位长优化方法

• 发表时间: 2006
• 期刊: IEICE Trans.Fundamentals E89-A
• 作者: Nobuhiro DOI;Takashi HORIYAMA;Masaki NAKANISHI;and Shinji KIMURA
• 通讯作者: and Shinji KIMURA

Issue Mechanism for Embedded Simultaneous Multithreading Processor

• DOI: 10.1093/ietfec/e91-a.4.1092
• 发表时间: 2008-04
• 期刊: IEICE Trans. Fundam. Electron. Commun. Comput. Sci.
• 作者: C. Zang;S. Imai;S. Frank;S. Kimura

Coverage Estimation Using Transition Perturbation for Symbolic Model Checkinsr in Hardware Verification

使用转移扰动进行硬件验证中符号模型检查的覆盖率估计

• 发表时间: 2006
• 期刊: IEICE Trans. Fundamentals E-89, No.12
• 作者: Kazunari HORIKAWA;Takehiko TSUCHIYA
• 通讯作者: Takehiko TSUCHIYA

動的再構成可能配線について

关于动态可重配置路由

• 发表时间: 2006
• 作者: Youhua Shi;Nozomu Togawa;Shinji Kimura;Masao Yanagisawa;Tatsuo Ohtsuki;木村 晋二
• 通讯作者: 木村 晋二