| 講演名 | 2002/3/1 設計誤り問題に対する形式的検証診断の方法について 平塚 聡, 房岡 璋, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本論文では、モデルベース推論に基づいた、組合せ回路の設計誤りの発見および訂正の手法を提案する.特に複数のinverter誤りを含む場合に対する設計検証を対象とする.この問題の計算量はNP困難であり、通常の検証と比べてtractableなアルゴリズムを見出すことは難しい.本論文では設計回路の各coneに対して論理式を生成して仕様と比較することにより検証と診断を同時に進めるアルゴリズムを提案する.このアルゴリズムにおいては、冗長でない設計回路の各coneの論理式の少なくとも一部分は、設計が正しければ機能仕様の部分式であるという性質を利用し、探索における不要なバックトラックを回避する. |
| 抄録(英) | In this report, we propose a method to detect and correct design faults in a combinational boolean network automatically, based on the model-based inference. We focus on the design verification based on the fault model of multiple inverter errors. The complexity of this problem is NP-hard and it is harder than the usual verification to find a tractable algorithm. We present an effective algorithm which consists of the generation of the logical formula and its comparison to the specification for each cone in gate implementation. In this algorithm, the heuristic search method is incorporated to avoid the unnecessary backtracking based on the property that a part of the logical fomula of each cone must be subformulas of functional specifications if the gate implementation is correct and irredundant. |
| キーワード(和) | モデルベース推論 / 形式的検証 / 多重誤り |
| キーワード(英) | model-based reasoning / formal verification / multiple faults |
| 資料番号 | VLD2001-166 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2002/3/1(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 設計誤り問題に対する形式的検証診断の方法について |
| サブタイトル（和） | |
| タイトル（英） | A Formal Verification and Diagnosis Method for Design Fault Problems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデルベース推論 / model-based reasoning |
| キーワード(2)（和/英） | 形式的検証 / formal verification |
| キーワード(3)（和/英） | 多重誤り / multiple faults |
| 第 1 著者 氏名（和/英） | 平塚 聡 / Satoshi HIRATSUKA |
| 第 1 著者 所属（和/英） | 立命館大学理工学部情報学科 Department of Computer Science, Faculty of Science and Engineering, Ritsumeikan University |
| 第 2 著者 氏名（和/英） | 房岡 璋 / Akira FUSAOKA |
| 第 2 著者 所属（和/英） | 立命館大学理工学部情報学科 Department of Computer Science, Faculty of Science and Engineering, Ritsumeikan University |
| 発表年月日 | 2002/3/1 |
| 資料番号 | VLD2001-166 |
| 巻番号（vol） | vol.101 |
| 号番号（no） | 695 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |