A Study on False Negative Reduction on Formal Verification of Logic Circuits

逻辑电路形式验证中误报减少的研究

• 批准号: 20700046
• 负责人: NAKAMURA Kazuhiro
• 金额: $ 2.08万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20700046/
• 关键词: VLSI設計技術; 諭理回路; 形式的検証; 順序回路; フォールスネガティブ; 論理回路; sequential SAT

A reducing method of false nagatives on formal verification of sequential circuits with a circuit conversion is developed. In addition to the method, multi time-frame state reduction for accelerating sequential SAT is developed.

提出了一种利用电路转换减少时序电路形式验证中假否定的方法。在此基础上，提出了加速时序SAT的多时间帧状态约简方法。

项目成果

順序回路の形式的検証におけるフォールスネガティブ削減のための回路変換

用于减少时序电路形式验证中的假阴性的电路变换

• 发表时间: 2010
• 作者: 尾野紀博;中村一博;高木一義;高木直史
• 通讯作者: 高木直史

Sequential SATの高速化のためのm-Trieを用いた時間フレームを跨いだ状態併合

使用 m-Trie 进行跨时间帧的状态合并以加速 Sequential SAT

• 发表时间: 2010
• 作者: 鳥居洸佑;中村一博;高木一義;高木直史
• 通讯作者: 高木直史

順序回路の形成的検証におけるフォールスネガティブ削減のための回路変換

用于减少时序电路形成验证中的假阴性的电路变换

• 发表时间: 2010
• 作者: 成瀬智啓;中村一博;高木一義;高木直史
• 通讯作者: 高木直史

Sequential SATにおける時間フレームを跨いだ状態併合

顺序 SAT 中跨时间范围的状态合并

• 发表时间: 2009
• 作者: 成瀬智啓;中村一博;高木一義;高木直史
• 通讯作者: 高木直史