フォーマル手法およびシミュレーション手法の統合によるハードウェア検証の効率化

• 研究課題/領域番号: 22500047
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 計算機システム・ネットワーク
• 研究機関: 島根大学 (2012); 大阪大学 (2010-2011)
• 研究代表者: 浜口 清治 島根大学, 総合理工学研究科, 教授 (80238055)
• 研究期間 (年度): 2010 – 2012
• 研究課題ステータス: 完了 (2012年度)
• 配分額: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円); 2012年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2011年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2010年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
• キーワード: 設計検証技術 / フォーマル検証 / シミュレーションベース検証 / SAT ソルバ / SATソルバ / 有界モデル検査 / カバレッジ駆動検証 / 制約付きランダムパタン生成 / アサーションベース検証

研究概要

フォーマル手法およびシミュレーション手法はハードウェア検証における2つの方式として実用的に用いられてきている.しかし,この2つの方式を組み合わせる方法については,まだ十分研究されていない.本研究では,カバレッジと呼ばれる量的基準に関して,シミュレーション手法で得られた結果をもとに,達成度が不足している部分に対してフォーマル手法を適用することにより,カバレッジの改善が見られることを,数千ゲート程度のブロックモジュールに対する実験によって示した.

研究成果

• [雑誌論文] Approximate Model Checking using a Subset of First-Order Logic (2010)
  • 著者名/発表者名: Kiyoharu Hamaguchi
  • 雑誌名: IPSJ Transactions on System LSI Design Methodology 巻: 3 ページ: 268-282
  • NAID: 130000418475
  • 査読あり
• [学会発表] 石木裕介(発表者),浜口清治,若宮直紀 (2012)
  • 著者名/発表者名: 石木裕介(発表者),浜口清治,若宮直紀
  • 学会等名: DA シンポジウム 2012
  • 発表場所: 岐阜県下呂市水明館
  • 年月日: 2012-08-29
• [学会発表] 動作レベル回路設計記述の等価性判定における複数の論理体系を利用した抽象化 (2012)
  • 著者名/発表者名: 浜口清治
  • 学会等名: DAシンポジウム2012
  • 発表場所: 岐阜県下呂市 水明館