講演名 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
発行日