高位ハードウェア設計記述に対するモデル検査手法の研究

2009 年度 研究成果報告書

• 研究課題/領域番号: 19500043
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 計算機システム・ネットワーク
• 研究機関: 大阪大学
• 研究代表者: 浜口 清治 大阪大学, 大学院・情報科学研究科, 准教授 (80238055)
• 研究期間 (年度): 2007 – 2009
• キーワード: 設計検証 / フォーマル検証 / 第1階述語論理 / モデル検査 / 高位ハードウェア設計

研究概要

モデル検査は計算機のハードウェアやソフトウェアの正しさを自動的かつ網羅的に検証する技術であり,近年利用がすすんでいる.しかし,複雑な演算を含む設計では,小規模な設計でも扱うことが難しい.本研究では,特にハードウェアの高位設計記述を対象に,複数の論理体系を組み合わせる手法により,不必要な部分の詳細を考慮せずモデル検査を行う方法を開発・実装した.ディジタル信号処理など,従来の手法では扱うことができなかった例に対するモデル検査に成功した.

研究成果

• [雑誌論文] Approximate Model Checking using a Subset of First-Order Logic (2011)
  • 著者名/発表者名: Kiyoharu Hamaguchi, Kazuya Masuda, Toshinobu Kashiwabara
  • 雑誌名: IPSJ Transactions on System LSI Design Methodology 5(In printing)
  • 査読あり
• [雑誌論文] Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic (2010)
  • 著者名/発表者名: Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara
  • 雑誌名: IPSJ Transactions on System LSI Design Methodology 4 ページ: 105-117
  • 査読あり
• [学会発表] 第一階述語論理のサブクラスに対する近似的モデル検査アルゴリズム (2009)
  • 著者名/発表者名: 増田和也, 浜口清治, 柏原敏伸
  • 学会等名: 情報処理学会研究報告
  • 年月日: 20090000
• [学会発表] SMTソルバーを利用した近似的な非有界モデル検査アルゴリズムにおける複数の論理体系の組み合わせ手法 (2009)
  • 著者名/発表者名: 浜口清治
  • 学会等名: 組み込みシステムシンポジウム2009論文集
  • 年月日: 20090000
• [学会発表] Toshinobu Kashiwabara Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic (2008)
  • 著者名/発表者名: Hiroaki Shimizu, Kiyoharu Hamaguchi
  • 学会等名: 6th International Conference on Automated Technology for Verification and Analysis
  • 発表場所: LNCS
  • 年月日: 20080000
• [学会発表] 第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム (2007)
  • 著者名/発表者名: 清水博章, 浜口清治, 柏原敏伸
  • 学会等名: 情報処理学会研究報告
  • 年月日: 20070000