2024-03-28T20:24:44Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001042522023-11-17T02:17:36Z06504:07684:07618
形式的手法を用いた論理設計検証網羅性解析に関する一方式jpnアーキテクチャhttp://id.nii.ac.jp/1001/00104228/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=104252&item_no=1&attribute_id=1&file_no=1Copyright (c) 2014 by the Information Processing Society of Japan富士通研富士通山本達也高山浩一郎ハードウエアの論理検証において, 論理シミュレーションと形式的手法を連携し, 検証網羅性を解析する手法を提案する. 本手法では,形式言語で記述された機能仕様に対し, シミュレーション結果から抽出した動作シーケンスを制約としてモデル検査を実行する. これにより, シミュレーションで未カバーな仕様上の動作シーケンスを検証シナリオとして自動生成する.形式的検証ツールSPINを用いたプロトタイプを構築した. USB3.0を例題として, プロトコル仕様に対する網羅性解析を実施し, 本手法の有効性を確認した.AN00349328第76回全国大会講演論文集2014117182014-03-112014-10-02