準形式的モデル検査のハードウェア実装による高速化の検討

摘要

近年設計が大規模になり、複雑化が進むにつれて検証の重要性が増している。 現在の重要な検証手法の一つであるモデル検査には適用する回路規模が大きくなると状態爆発を起こし、実用的な時間内で検査が終了しないという問題がある。 そのため回路規模や検証時間の面でより効率的なモデル検査が必要とされている。現在の効率的なモデル検査手法の1つに、コンパイルドシミュレーションを基にした準形式的限定モデル検査[8]がある。 本稿ではそのアルゴリズムの一部をハードウェアで実装し、各々の処理に対してハードウェア·ソフトウェア協調実行に向けた最適化を行うことで高速化したモデル検査を提案する。また例題を用いた実験によって実際に高速に検証を行い、提案手法の有効性を確認した。