| 講演名 | 2006-11-29 SATアルゴリズムとその形式的検証への応用(デザインガイア2006-VLSI設計の新しい大地を考える研究会) 藤田 昌宏, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | まず、論理式の充足可能性判定問題(SAT問題)を解くアルゴリズム(SAT手法と呼ぶ)について、DPLL法を中心にその歴史と現状について解説する。次に、SAT手法を特に形式的な設計検証に適用する技術について、現状を解説する。近年のSAT手法の大きな進歩により、実用規模のハードウェア設計検証や、ソフトウェアのバグハンティングが可能になってきている。本稿はその状況を平易に解説することを目標としている。 |
| 抄録(英) | In this paper, algorithms for Boolean satisfiability checking problems are reviewed concentrating on the algorithms relating to DPLL method. Then their applications to formal verification of hardware and software are presented. Owing to the recent great improvements on SAT algorithms, realistic sizes of hardware designs and software programs can be formally verified or analyzed with the SAT techniques. This paper aims to concisely give the state-of-the-art SAT algorithms and the current status of their application to formal verification. |
| キーワード(和) | SAT / SATアルゴリズム / BCP / 形式的検証 / 等価性検証 / モデルチェッキング |
| キーワード(英) | SAT / SAT algorithm / BCP / formal verification / equivalence checking / model checking |
| 資料番号 | VLD2006-67,DC2006-54,RECONF2006-39 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2006/11/22(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | SATアルゴリズムとその形式的検証への応用(デザインガイア2006-VLSI設計の新しい大地を考える研究会) |
| サブタイトル（和） | |
| タイトル（英） | SAT algorithms and their application to formal verification |
| サブタイトル（和） | |
| キーワード(1)（和/英） | SAT / SAT |
| キーワード(2)（和/英） | SATアルゴリズム / SAT algorithm |
| キーワード(3)（和/英） | BCP / BCP |
| キーワード(4)（和/英） | 形式的検証 / formal verification |
| キーワード(5)（和/英） | 等価性検証 / equivalence checking |
| キーワード(6)（和/英） | モデルチェッキング / model checking |
| 第 1 著者 氏名（和/英） | 藤田 昌宏 / Masahiro FUJITA |
| 第 1 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, The University of Tokyo |
| 発表年月日 | 2006-11-29 |
| 資料番号 | VLD2006-67,DC2006-54,RECONF2006-39 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 388 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |