状態遷移表現への変換に基づくハードウェア/ソフトウェア協調設計の形式的検証手法

摘要

現在広く普及している，ハードウェアがレジスタ転送レベルで，ソフトウェアがC言語などのプログラムコードで記述された，ハードウェア/ソフトウェア協調設計記述に対して形式的検証を適用する手法を提案する．扱う形式的検証は，プロパティ検証と，ハードウェア/ソフトウェア分割前のプログラムコードによる仕様記述と分割後のハードウェア/ソフトウェア協調設計間の等価性検証である．両者に共通する手法の特徴は，ハードウェア記述とソフトウェア記述を自動的に両記述間の通信が抽象化された，データパスをもつ有限状態機械へと変換することにより時間に関する概念の差を埋めて，それらをRTLで記述し既存のRTL記述用形式的検証器で一括して検証を行う点である．既存のRTL記述用形式的検証器で検証する理由は，この種の商用ツールが現在最もツールとして信頼性があり，性能も高いからである．本論文では，特にソフトウェアをC言語（ANSI-C）で記述した場合の詳細な手法と，二つの例題に対しての実験結果を示す．