| 講演名 | 2001/11/22 BDD制約演算に基づく新しい像計算法について 木村 晋二, /, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では、二分決定グラフ(BDD)の制約演算に基づく像計算の新しい手法を示す。像計算は、現状態(集合)から次状態集合を論理関数を用いて計算するための手法で、時相論理のモデルチェックなど順序回路の検証の分野で広く用いられている。ここでは、次状態変数を含む場合の制約演算と論理積(AND演算)の関係を示し、それを状態探索の次状態集合の計算に応用する手法を示す。制約演算により、論理積よりもBDDの節点数を削減できる可能性がある。中規模のISCASベンチマークで状態探索に適用した結果、論理積に基づくこれまでの提案手法に対して良い結果が得られた。 |
| 抄録(英) | In the paper, we show a new image computation method based on the BDD constrain operator. The image computation is to compute the next state set from the current state set using the logic functions, and is widely used in the formal verification of sequential circuits. We have shown a property on the relation between the constrain operator and the conjunction operator for transition relations of state variables. The constrain operator can reduce BDD node size compared with the conjunction operator. The new method outperforms for several ISCAS benchmarks comparing recent conjunction based methods. |
| キーワード(和) | 二分決定グラフ / BDD / 一般化コファクタ / 像計算 / コンストレイン演算 / 記号的状態探索 |
| キーワード(英) | Binary Decision Diagram / BDD / Generalized Cofactor / Image Computation / Constraint / Symbolic State Traversal |
| 資料番号 | VLD2001-101,ICD2001-46,FTS2001-48 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2001/11/22(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | BDD制約演算に基づく新しい像計算法について |
| サブタイトル（和） | |
| タイトル（英） | A New Image Computation Method Based on Generalized Cofactor of Binary Decision Diagramns |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 二分決定グラフ / Binary Decision Diagram |
| キーワード(2)（和/英） | BDD / BDD |
| キーワード(3)（和/英） | 一般化コファクタ / Generalized Cofactor |
| キーワード(4)（和/英） | 像計算 / Image Computation |
| キーワード(5)（和/英） | コンストレイン演算 / Constraint |
| キーワード(6)（和/英） | 記号的状態探索 / Symbolic State Traversal |
| 第 1 著者 氏名（和/英） | 木村 晋二 / Shinji KIMURA |
| 第 1 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Grad.School of Information Science, Nara Institute of Science and Technology |
| 第 2 著者 氏名（和/英） | / / David DILL |
| 第 2 著者 所属（和/英） | / Stanford University |
| 発表年月日 | 2001/11/22 |
| 資料番号 | VLD2001-101,ICD2001-46,FTS2001-48 |
| 巻番号（vol） | vol.101 |
| 号番号（no） | 467 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |