| 講演名 | 1995/10/19 算術演算回路検証のための二分モーメントグラフの高速生成手法 浜口 清治, 森田 晃史, 矢島 脩三, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | BryantとChenが発表した二分モーメントグラフは、従来手法では取り扱うことができなかった乗算など算術演算関数をコンパクトに表現することができる。しかし、効率的な検証手法としては回路分割を行う方法しか知られていなかった。本稿では、回路から分割を行わずに二分モーメントグラフを構成するための切断掃引法という手法と実験結果を報告する。これにより、64ビット以上の乗算器の検証も可能となった。 |
| 抄録(英) | BDD-based approaches cannot handle some arithmetic functions such as multiplication efficiently, while Binary Moment Diagrams proposed by Bryant and Chen provide compact representations for those functions. They reported a BMD-based polynomial-time algorithm for verifying multipliers. This approach requires high-level information such as specifications to subcomponents. This paper presents a new technique called backward construction which can construct BMDs directly from circuit descriptions without any high-level information. We have successfully verified 64-bit multipliers of several type. This result outperforms previous BDD-based approaches for verifying multipliers. |
| キーワード(和) | 形式的検証 / 等価性検証 / 二分モーメントグラフ / 算術演算回路 |
| キーワード(英) | formal verification / equivalence checking / binary moment diagram / arithmetic circuit |
| 資料番号 | VLD95-84,FTS95-46 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 1995/10/19(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 算術演算回路検証のための二分モーメントグラフの高速生成手法 |
| サブタイトル（和） | |
| タイトル（英） | Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / formal verification |
| キーワード(2)（和/英） | 等価性検証 / equivalence checking |
| キーワード(3)（和/英） | 二分モーメントグラフ / binary moment diagram |
| キーワード(4)（和/英） | 算術演算回路 / arithmetic circuit |
| 第 1 著者 氏名（和/英） | 浜口 清治 / Kiyoharu HAMAGUCHI |
| 第 1 著者 所属（和/英） | 京都大学工学部情報工学教室 Dept. of Information Science, Kyoto University |
| 第 2 著者 氏名（和/英） | 森田 晃史 / Akihito MORITA |
| 第 2 著者 所属（和/英） | 東京海上火災保険株式会社 Tokyo Marine and Fire Insurance Co., Ltd. |
| 第 3 著者 氏名（和/英） | 矢島 脩三 / Shuzo YAJIMA |
| 第 3 著者 所属（和/英） | 京都大学工学部情報工学教室 Dept. of Information Science, Kyoto University |
| 発表年月日 | 1995/10/19 |
| 資料番号 | VLD95-84,FTS95-46 |
| 巻番号（vol） | vol.95 |
| 号番号（no） | 306 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |