モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法

摘要

ハードウェアモジュールインタフェースを検証するために様々な手法が提案されているが，本論文ではモニタベース形式検証に焦点を当てる．本論文では，インタフェース仕様全体をより包括的に検証することを目指し，まず正規表現ベースの仕様記述言語でモジュールインタフェースの仕様を記述し，次にその記述から動作モデルを構築し，最終的にモニタ回路を生成する．モニタ回路の生成は自動的に行われるため，複雑な仕様に対するモニタ回路を人手で設計する際に誤りが混入することを防ぐことができる．モジュールの検証を行うことを考えると，仕様に記述されていない入力パターンに対するチェックも行われてしまうため，通常では入力を制約する回路を付加する必要がある．これに対して，本論文では付加回路を必要とせず，入力制約をモニタ中に反映する手法について述べる．入力制約はインタフェース仕様記述から自動的に抽出される．これによりモジュール単体での検証が可能となる．実験では設計例としてバスプロトコルであるAMBA AHBに従って設計された回路について，実際に仕様を記述し，モニタを生成し，形式検証を行った結果を示す．