Equivalence Checking for System-Level Designs Having Different Input-Output Timings

具有不同输入输出时序的系统级设计的等效性检查

• 批准号: 23700051
• 负责人: MATSUMOTO Takeshi
• 金额: $ 2.33万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23700051/
• 关键词: 等価性検証; システムレベル設計; 形式的検証; 高位設計

In this work, design verification methods for embedded systems or VLSIs are studied. The purpose of design verification is to check whether a given design is correct or not and provide failing patterns if incorrect. We focus on equivalence checking of given two designs. Our target of verification is system-level design, which is a highly abstracted design level and has become widely applied recently. We proposed equivalence checking methods that can deal with different input/output timings between given two designs. In addition, we have developed a method to detect potentially equivalent internal variables in designs. The purposed of this work is to improve the ability of equivalence checking for system-level designs by those proposed methods.

在这项工作中，研究了嵌入式系统或 VLSI 的设计验证方法。设计验证的目的是检查给定的设计是否正确，如果不正确则提供失败的模式。我们专注于给定两种设计的等效性检查。我们验证的目标是系统级设计，这是一个高度抽象的设计级别，最近得到了广泛的应用。我们提出了等效检查方法，可以处理给定两种设计之间的不同输入/输出时序。此外，我们还开发了一种方法来检测设计中潜在的等效内部变量。这项工作的目的是通过所提出的方法提高系统级设计的等效性检查的能力。

项目成果

FOF : Functionally Observable Fault and its ATPG techniques

FOF：功能可观察故障及其 ATPG 技术

• 发表时间: 2013
• 作者: M. Fujita; T. Matsumoto; S. Jo
• 通讯作者: S. Jo

プログラム可能データパスとSMT ソルバーを利用した高位設計デバッグ手法

使用可编程数据路径和 SMT 求解器的高级设计调试技术

• 发表时间: 2014
• 作者: 松本剛史; 城怜史; 藤田昌宏
• 通讯作者: 藤田昌宏

Debugging Processors with Advanced Features by Reprogramming LUTs on FPGA

通过在 FPGA 上重新编程 LUT 来调试具有高级功能的处理器

• 发表时间: 2013
• 作者: Satoshi Jo; Amir Masoud Gharehbaghi; Takeshi Matsumoto; Masahiro Fujita
• 通讯作者: Masahiro Fujita

An Efficient Method to Localize Correct Bugs in High-Level Designs Using Counterexamples and Potential Dependence

使用反例和潜在依赖性在高层设计中定位正确错误的有效方法

• 发表时间: 2012
• 作者: T. Matsumoto; S. Ono; M. Fujita
• 通讯作者: M. Fujita

論理関数の充足不可能性に注目した論理回路デバッグ手法の検討

针对逻辑功能不满足性的逻辑电路调试方法研究

• 发表时间: 2012
• 作者: 李在城; 松本剛史; 藤田昌宏
• 通讯作者: 藤田昌宏