丸岡 新治 (9851106)

有限状態機械の状態数え上げは, 検証, テスト, 合成など様々な分野で 重要な技術である. 現在では, BDD (二分決定グラフ)に基づく状態数え上げ 手法が用いられているが, その手法では中規模程度の回路にしか適用できない. 一方で, シンボリックモデルチェッキングやマルチクロックパス解析に対して, SAT (satisfiability)に基づく検証手法が提案された. これらは, 問題を CNF式 (conjunctive normal form)で表現し, その論理式をSATアルゴリズムを 用いて解析するという手法をとり, BDDに基づく手法に比べて大きな回路に 適用できることが示されている. しかし, SATに基づく手法では, 有限状態機械 の到達可能状態の集合の計算が困難であるため, たいてい有限状態機械の全ての 状態は到達可能であるという仮定のもとに利用されている. これにより, 到達不可能な状態により充足してしまうような仕様は, 意味がない 結果をもたらす場合がある. 本稿では, SATアルゴリズムを用いた状態数え上げ 手法を提案する. この手法により, 到達可能状態の集合をCNF式で得ることが できる. われわれは, CNF式を生成するためにいくつかのheuristicsを導入した. また, これらの手法を実装し到達可能状態に関する問題点を解決した.