2009 Fiscal Year Annual Research Report
| Project/Area Number |
20700046
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
中村 一博 Nagoya University, 情報科学研究科, 助教 (90335076)
|
|---|
| Keywords | VLSI設計技術 / 諭理回路 / 形式的検証 / 順序回路 / フォールスネガティブ |
|---|
| Research Abstract |
論理回路の形式的検証の正確さを向上させる目的で、順序回路の形式的検証におけるフォールスネガティブ削減のための回路変換の研究を行った。
初期状態から非常に多くの状態を遷移して初めて発現するような設計誤りを検出すル検証では、初期状態からの到達可能性を考慮しない限定モデル検査を用いた検証が行われる。このような検証では、到達不能状態に起因するフォールスネガティブが発生することが知られている。フォールスネガティブとは、検証アルゴリズムが、本来、初期状態から到達不能デアルため仕様違反ではない動作を誤ってバグと判定してしまうことである。このようなフォールスネガティブを削減することは、誤検出されたバグの対応に費やされる検証時間を削減する上で重要な問題である。そこで、回路変換を行うことにより、到達不能状態における動作を、誤検出されないような動作に変更することで、フォールスネガティブを削減する手法を開発した。
本手法では、回路が正しい動作をしている間は常に成り立っている不変条件が成り立たない到達不能状態において、フォールスネガティブにならないような動作を回路に追加する。ここで、回路に追加する動作は、不変条件が成り立たなければエラー状態に遷移するというものである。
本研究の成果は国内研究会で発表した。
|
Research Products
(1 results)
