システムLSIの形成的検証のためのプレスブルガー算術処理を含む検証手法の研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12780219
• Research Institution: Osaka University
• Principal Investigator: 北道 淳司 大阪大学, サイバーメディアセンター, 講師 (20234271)
• Keywords: 形式的検証 / システムLSI / プレスブルガー算術 / 計算本論理 / 時相論理 / BDD

Research Abstract

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

Research Products

• [Publications] 佐藤友哉,北道淳司,東野輝夫: "システム設計レベルにおける回路の性質検証のための整数データを処理可能なCILモデル検査法の提案と安装"情報処理学会研究報告 2000-SLDM-97. Vol.2000 No.79. 17-24 (2000)
• [Publications] 佐藤友哉,北道淳司,東野輝夫: "プレスブルガー算術に拡張したCTLモデル検査法によるSFLで記述した回路の性質検証"第17回パルテノン研究会 資料集. 96-105 (2000)