BDD制約演算に基づく新しい像計算法について

スポンサーリンク

概要

論文の詳細を見る
本稿では、二分決定グラフ(BDD)の制約演算に基づく像計算の新しい手法を示す。像計算は、現状態(集合)から次状態集合を論理関数を用いて計算するための手法で、時相論理のモデルチェックなど順序回路の検証の分野で広く用いられている。ここでは、次状態変数を含む場合の制約演算と論理積(AND演算)の関係を示し、それを状態探索の次状態集合の計算に応用する手法を示す。制約演算により、論理積よりもBDDの節点数を削減できる可能性がある。中規模のISCASベンチマークで状態探索に適用した結果、論理積に基づくこれまでの提案手法に対して良い結果が得られた。
2001-11-29

著者

関連論文

もっと見る

スポンサーリンク