FSMへの変換に基づくHW/SW協調設計の形式的検証手法に関する研究

摘要

本稿では，ハードウェアがVerilogやVHDLなどによりRTLで，ソフトウェアがC言語などによりプログラムコードで記述された，ハードウェア／ソフトウェア協調設計記述に対して形式的検証を適用する手法を提案する．提案する手法の特徴は，設計におけるハードウェアとソフトウェアの両記述を自動的に抽象化されたFSMへと変換し，既存のプロパティ検証器で一緒に検証を行う点である．本稿で扱う形式的検証は，プロパティ検証と，ハードウェア／ソフトウェア分割前のソフトウェア設計と分割後のハードウェア／ソフトウェア協調設計間の等価性検証である．両者について検証全体の流れと，幾つかの例題に対しての実験結果を示した．