第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム(テストと検証,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)

スポンサーリンク

概要

論文の詳細を見る
自動的にハードウェア設計の形式的検証を行う手法にモデルチェッキング技術があるが,モデルチェッキングには,扱うシステムが大規模になると状態数が爆発してしまい,計算量的に適用できないという問題がある.計算量を軽減するための1つの方法として,EUFと呼ばれる第一階述語論理のサブクラスを用いてシステムを抽象化する手法が提案されているが,EUFを用いたモデルチェッキングは一般に決定不能であることが知られている.本稿では,EUFの項の高さに上限を与えることで,現れうる項の形を制限し,状態集合の数え上げを終了させる手法を提案する.また数え上げた状態集合に対して,指定した不変条件の成立を保証できる近似アルゴリズムを提案する.さらに,アルゴリズムを簡単な回路設計に適用した例を示す.
社団法人電子情報通信学会の論文
2007-11-13

著者

関連論文

もっと見る

スポンサーリンク