| 講演名 | 2006-11-28 算術演算回路の形式的検証手法とその評価(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会) 渡邉 裕樹, 本間 尚文, 青木 孝文, 樋口 龍雄, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では,筆者らの提案する算術アルゴリズム記述言語ARITHを用いた算術演算回路の形式的設計について述べる.ARITHでは,多進数系や冗長数系を含む多様な数系に基づく算術アルゴリズムを整数方程式により記述可能である.ARITHによって記述された算術演算回路は,数式処理を用いた検証によってその機能の正当性が検証される.本稿では,提案する検証手法と従来の*BMDに基づく形式的検証手法を比較し,両者の利点を組み合わせることで効率的な検証が可能となることを示す. |
| 抄録(英) | This paper presents the formal design of arithmetic circuits based on arithmetic description language called ARITH. By using ARITH, we can describe a wide variety of arithmetic algorithms including those using unconventional number systems. The functionality of arithmetic algorithms in ARITH can be formally verified using formula manipulation methods. In this paper, we compare the proposed formula-based method with the conventional *BMD-based method, and demonstrate that the combination of the two methods enables to verify arithmetic circuits in an efficient way. |
| キーワード(和) | 算術アルゴリズム / 形式的検証 / データパス / ハードウェア記述言語 |
| キーワード(英) | arithmetic algorithms / formal verification / datapaths / hardware description language |
| 資料番号 | VLD2006-54,DC2006-41 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2006/11/21(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 算術演算回路の形式的検証手法とその評価(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会) |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification Method for Arithmetic Circuits and Its Evaluation |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 算術アルゴリズム / arithmetic algorithms |
| キーワード(2)（和/英） | 形式的検証 / formal verification |
| キーワード(3)（和/英） | データパス / datapaths |
| キーワード(4)（和/英） | ハードウェア記述言語 / hardware description language |
| 第 1 著者 氏名（和/英） | 渡邉 裕樹 / Yuki WATANABE |
| 第 1 著者 所属（和/英） | 東北大学 大学院情報科学研究科 Graduate School of Information Sciences Tohoku University |
| 第 2 著者 氏名（和/英） | 本間 尚文 / Naofumi HOMMA |
| 第 2 著者 所属（和/英） | 東北大学 大学院情報科学研究科 Graduate School of Information Sciences Tohoku University |
| 第 3 著者 氏名（和/英） | 青木 孝文 / Takafumi AOKI |
| 第 3 著者 所属（和/英） | 東北大学 大学院情報科学研究科 Graduate School of Information Sciences Tohoku University |
| 第 4 著者 氏名（和/英） | 樋口 龍雄 / Tatsuo HIGUCHI |
| 第 4 著者 所属（和/英） | 東北工業大学 工学部 電子工学科 Department of Electronic Engineering, Faculty of Engineering, Tohoku Institute of Technology |
| 発表年月日 | 2006-11-28 |
| 資料番号 | VLD2006-54,DC2006-41 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 390 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |