|
1、高位合成を利用したデータパス抽象化による等価性検証手法
まず、前年度までに提案した手法に対する証明を行った。等価性検証手法は数学的手法によるものであるため、手法自体に数学的正当性が求められる。したがって、昨年度までに提案した手法だけでは不十分であり、今回提案した証明と併せて始めて完全であると言える。具体的には、等価なデータパスを持つ二つのFSMDに対して成立するルールに対する数学的証明を行った。
次に、それらのルールを適用するアルゴリズムを提案した。それらのルールは単独では意味を持たず、ルールを適用するアルゴリズムと併せて意味を持つものである。したがって、今回提案したアルゴリズムにより実設計への適用が可能となる。
さらに、既存の等価性検証手法との比較実験を行った。提案した手法はルールベースであるため、特定の設計については既存手法よりも高速に等価性が証明できる可能性がある手法である。今回の比較実験により、条件分岐を多く含む設計に対しては、既存手法よりも提案手法の方が高速に等価性を証明できることを確認した。
2、多段プロパティ分割とその改良を用いた限定モデル検査手法
まず、前年度までに提案した二段階の手法に対し、更に多段階の限定モデル検査を適用する手法を提案した。第一段階の初期状態を無視したモデル検査による反例への到達可能性を検査する第二段階を、同様の分割手法で再帰的に分割する。これにより、更なるモデル検査の効率化に寄与できると考えられる。
次に、実装をパブリックなモデル検査器であるNuSMVをベースとしたものに変更した。パブリックなモデル検査器を使用することにより、実験において提案手法による効果が確認しやすくなり、さらに汎用的な実験が可能となった。発表文献では、この新しく実装したツールを用いた実験を行っている。
|
