| 講演名 | 2006-01-17 第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法(FPGAとその応用及び一般) 森友 淳史, 浜口 清治, 柏原 敏伸, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 近年の半導体回路の大規模化, 複雑化に伴い, その設計検証にはより一層の時間と資源が必要となっている.2つの設計間での等価性判定は, 典型的な設計検証問題の1つである.設計検証では一般にシミュレーションが主流だが, 等価性判定に関しては形式的検証手法の利用が普及しつつある.ブール関数レベルでの形式的な等価性判定を考えると, その検証には膨大な時間と資源がかかる.そこで, 第一階述語論理を利用し検証コストを削減する手法が考案されている.特に第一階述語論理のサブクラスである限量子を含まない等号付第一階述語論理での恒真性判定は決定可能であることから, これを用いた自動検証が可能となる.しかし, 第一階述語論理では, 算術演算などは関数記号の形で抽象化されるため, ブール関数レベルでの等価性判定と同じ結果を与えることが一般にできない.そこで, 本報告では可能な部分は限量子を含まない等号付第一階述語論理を利用して検証を行い, そうでない部分のみをブール式へと変換することで検証コストの削減を図る等価性判定アルゴリズムについて述べる. |
| 抄録(英) | In recent years, design verification becomes more difficult as the scale of semiconductor circuits becomes larger. Designs are commonly checked by simulation-based verification, and exhaustive verification is difficult by simulation-based verification. As for equivalence checking, however, formal verification methods have been spreading. Formal equivalence checking at Boolean function level requires a large amount of cost. Therefore, formal verification based on first-order logic has been considered. Since validity checking of quantifier-free first-order logic with equality which is a subclass of first-order logic is decidable, the verification methods using this logic has been proposed. In this logic, however, arithmetic operations are abstracted away by functional symbols. The result of equivalence checking with this logic can differ from that of the conventional Boolean equivalence checking. This report shows an equivalence checking algorithm of the logic formula using Boolean substitution only for function/predicate symbols which cannot be checked by first-order logic. This algorithm achieves the accuracy of equivalence checking at Boolean level. |
| キーワード(和) | 等価性判定 / ブール関数 / 第一階述語論理 |
| キーワード(英) | Equivalence Checking / Boolean Function / First-Order Logic |
| 資料番号 | VLD2005-96,CPSY2005-52,RECONF2005-85 |
| 発行日 |
| 研究会情報 | |
| 研究会 | RECONF |
|---|---|
| 開催期間 | 2006/1/10(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Reconfigurable Systems (RECONF) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法(FPGAとその応用及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Boolean Equivalence Checking Using a Subset of First-Order Logic |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 等価性判定 / Equivalence Checking |
| キーワード(2)（和/英） | ブール関数 / Boolean Function |
| キーワード(3)（和/英） | 第一階述語論理 / First-Order Logic |
| 第 1 著者 氏名（和/英） | 森友 淳史 / Atsushi MORITOMO |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Bioinformatic Engineering, Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 浜口 清治 / Kiyoharu HAMAGUCHI |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Bioinformatic Engineering, Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 柏原 敏伸 / Toshinobu KASHIWABARA |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Bioinformatic Engineering, Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2006-01-17 |
| 資料番号 | VLD2005-96,CPSY2005-52,RECONF2005-85 |
| 巻番号（vol） | vol.105 |
| 号番号（no） | 517 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |