2A-3
形式的手法を用いた論理設計検証網羅性解析に関する一方式
○山本達也（富士通研），高山浩一郎（富士通）
ハードウエアの論理検証において, 論理シミュレーションと形式的
手法を連携し, 検証網羅性を解析する手法を提案する. 本手法では,
形式言語で記述された機能仕様に対し, シミュレーション結果から
抽出した動作シーケンスを制約としてモデル検査を実行する. これ
により, シミュレーションで未カバーな仕様上の動作シーケンスを
検証シナリオとして自動生成する.
形式的検証ツールSPINを用いたプロトタイプを構築した. USB3.0
を例題として, プロトコル仕様に対する網羅性解析を実施し, 本手
法の有効性を確認した.
footer 情報処理学会 セキュリティ プライバシーポリシー 倫理綱領 著作権について