近年のVLSI設計技術の進歩により、大規模で複雑な論理回路が設計されるように なっている。これに伴い、設計段階において、設計された論理回路が正しく動 作することを保証する設計検証が重要となっている。
従来より、論理回路の設計検証手法として、論理シュミレーションがよく用いられている。しかし、設 計された論理回路が任意の入力に対して論理回路が正しく動作するかどうかを 調べるには、すべての入力パターンについて確認する必要があり、これを実際 に行うと、非現実な時間を要する。このため、実際には回路設計者が特定の入 力パターンを決めて、シュミレーションを行っている。この検証手法のほかに、 設計の正しさを数学的に証明し、それにより任意の入力について保証する形式 的検証がある。
本研究では、そのような形式的検証手法の1つである順序回路(有限状態機械) の到達可能性解析について、解析手法を提案する。到達可能性解析問題とは、 順序回路の初期状態から到達してはいけない状態(bad state)に到達できるか どうかの判定を行う問題である。この解析問題では初期状態から状態遷移をた どり、新たに到達する状態がなくなる(不動点)までに、bad stateに到達する かどうかの判定を行う。従来より、到達可能性解析問題を解く手法として、二 分決定グラフ(BDD)を用いる手法と充足可能性判定(SAT)を用いる手法がある。 提案手法では、充足可能性判定にSATだけではなく、QSAT(Quantified SAT)も 用いて解析を行う。bad stateへの到達を判定する際はSATを用いて充足可能性 判定を行い、不動点への到達を判定する際にはQSATを用いて充足可能性判定を 行う。QSATを用いるとSATだけを用いる場合に比べ、式サイズが爆発的に大き くなることを防ぐことが期待できる。提案手法に基づく順序回路の到達可能性 解析システムを実現する。