|
本研究は、論理レベルよりも高位の記述、特に機能レベルと呼ばれる設計記述に対する形式的検証の自動化を目標としている。仕様記述には第1階述語論理の部分クラスを用いる。これにより、算数演算器などを論理レベルに展開することなく、高い抽象度のままで直接扱うことができる。仮定している部分クラスでは、等価性判定が容易であるため、自動検証が従来の論理レベルよりも抽象度の高いレベルで可能になる。
本器研究では、まず、第一階述語論理の部分クラスを遷移関数の記述に用いることができるよう拡張した拡張順序機構に対する検証について検討した。具体的には、第1階述語論理の部分クラスに時相演算子を加えた論理体系を示して、これを性質の記述に用いた場合の検証アルゴリズムを示した。また、機能レベル記述とレジスタ転送レベルの記述を比較するためには、たとえ出力のタイミングが異なっていても、等価であるとみなさなければならない場合があるが、これについて、2つの拡張順序機械に対し、出力信号値が変化した直後の値同士を比較するアルゴリズムを考察した。
以上の結果をもとに、まず、基礎となる第一階述語論理の部分クラスに対する恒真性判定アルゴリズムの実装を行った。次に、これを用いて、上記の2つのアルゴリズムの実装し、いくつかの例題について実験を行った。今回作成したプロトタイプは、検証に非常に多くのの時間と記憶領域を必要とする。これに対して、第一階述語論理の部分クラスに対する恒真性判定アルゴリズムについて、命題論理式に対する高速充足可能性判定システムを利用する手法を実装し、実験を開始しているほか、検証アルゴリズムそのものについても、いくつかの効率改善手法を検討しており、ひきつづき詳細化および実験を行っていく予定である。
|
