| 研究概要 |
研究計画に従い,本年度は以下を行った.
1.システムLSIの形式的検証のために,論理設計レベルでの形式的検証アルゴリズムの一つであるCTL(計算木論理)と呼ばれる手法をプレスブルガー算術を扱えるように拡張し,それに伴い検証アルゴリズムも同様に拡張した.本研究では我々の研究グループが開発しているプレスブルガー算術を扱えるライブラリを用いて検証アルゴリズムを実現した.また,回路記述言語SFLのパーサを検証処理系に組み込み,SFLにより記述された回路記述を直接検証可能とした.検証対象となる回路は,例えば,16bitレジスタでは0から2の16乗-1の値を取るように有限の整数を保持する部品と見なことができる.本提案アルゴリズムでは,その計算途中ではこれらのレジスタを上下限のない整数として扱うことにより,上下限をさだめる論理式に対する計算を省略し,検証の効率化を計っている.また,このように途中の計算において上下限の計算を省略しても得られる検証結果の正当性も示している.
2.いくつかの例題(カウンタ,CPUなど)に対して,本検証系を適用し,使用されるメモリ,必要となる計算時間など基礎的なデータを集計した.本検証系では,いくつかの例題回路の検証については効率的な計算メモリおよび計算時間で検証が可能なことがわかったが,回路の種類あるいは検証する性質によっては膨大な計算メモリおよび計算時間が必要であることがわかり,来年度における研究では,これらの例題に対しても効率的な検証が可能となるように検証アルゴリズムの改良が必要であることがわかった.
|
