|
論理回路の形式的検証の正確さを向上させる目的で、回路の状態の到達可能性解析の高速化と正確さ向上を図る研究を行った。
Sequential SAT問題は、順序回路と目的が与えられ、目的を満たすような入力系列が存在するかどうかを判定する問題である。あるプロパティを満たさないことを目的とすることで、初期状態からプロパティを違反する状態への到達可能性を、有限サイクル分に限定せずに検証することができる。このsequential SAT問題を解くアルゴリズムを、従来の手法では併合されなかった異なる時間フレームに属する状態同士の併合を行うことにより、探索する状態空間を小さくし、高速化する手法を開発した。提案手法と従来の状態併合を用いてsequential SAT問題を解くアルゴリズムを実装し、実験を行ったところ、提案手法によってsequential SAT問題をより高速に解けることが確認できた。本研究の成果は国内研究会で発表した。
また、初期状態から多くの状態を遷移して初めて発現するような設計誤りを検出するような検証では、初期状態からの到達可能性を考慮しない限定モデル検査を用いた検証が行われ、このような検証では、到達不能状態に起因する設計誤りの誤検出が発生することが知られている。そこで、検証のための回路変換により、この誤検出を削減する手法の開発を行った。
|
