| 講演名 | 2014-09-19 様相論理によるマルチクロック同期回路の形式検証体系 西村 俊二, 尼崎 太樹, 末吉 敏則, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 数学的な理論に基づく厳密な検証が可能となることから,各種の形式検証手法が広がりつつあるが,多くの場合検証対象は単一クロックの同期回路に限られている.本稿ではマルチクロック同期回路の形式検証を可能にする検証体系を提案する.提案する検証体系は多重様相論理に基づいた演繹的な論理体系であり,定められた公理から導かれた結果についての正当性が保証される(このことを"論理体系は健全である"という).正当性の保証には,マルチクロック同期回路の振るまいとある種のステートマシンの振るまいが等しくなる事実を用いる.また,この体系を用いた例としてクロック切替え回路の検証を行う. |
| 抄録(英) | Regardless of wide using of a formal verification methods, almost all of the methods limited to single-clock synchrounous circiut. We propose a formal verification system of multi-clock synchronous circuit. The verification system is based on multimodal logic. The system is dedactive and its dedaction system is sound. The soundness will be proven by a behavioral equivalence of a multi-clock synchronous circuit and a kind of state machine. While, we show a verification example of a clock switching circuit on the system. |
| キーワード(和) | マルチクロック / 形式手法 / 形式検証 / 検証手法 / 様相論理 |
| キーワード(英) | multi-clock / formal method / formal verification / verification method / modal logic |
| 資料番号 | RECONF2014-33 |
| 発行日 |
| 研究会情報 | |
| 研究会 | RECONF |
|---|---|
| 開催期間 | 2014/9/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Reconfigurable Systems (RECONF) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 様相論理によるマルチクロック同期回路の形式検証体系 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification System of Multi-clock Synchronous Circuits on Multimodal Logic |
| サブタイトル（和） | |
| キーワード(1)（和/英） | マルチクロック / multi-clock |
| キーワード(2)（和/英） | 形式手法 / formal method |
| キーワード(3)（和/英） | 形式検証 / formal verification |
| キーワード(4)（和/英） | 検証手法 / verification method |
| キーワード(5)（和/英） | 様相論理 / modal logic |
| 第 1 著者 氏名（和/英） | 西村 俊二 / Shunji NISHIMURA |
| 第 1 著者 所属（和/英） | 熊本大学大学院自然科学研究科 Graduate School of Science and Technology, Kumamoto University |
| 第 2 著者 氏名（和/英） | 尼崎 太樹 / Motoki AMAGASAKI |
| 第 2 著者 所属（和/英） | 熊本大学大学院自然科学研究科 Graduate School of Science and Technology, Kumamoto University |
| 第 3 著者 氏名（和/英） | 末吉 敏則 / Toshinori SUEYOSHI |
| 第 3 著者 所属（和/英） | 熊本大学大学院自然科学研究科 Graduate School of Science and Technology, Kumamoto University |
| 発表年月日 | 2014-09-19 |
| 資料番号 | RECONF2014-33 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | 223 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |