システムLSIの形式的検証のためのプレスブルガー算術処理を含む検証手法の研究
| Project/Area Number |
12780219
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
北道 淳司 大阪大学, サイバーメディアセンター, 講師 (20234271)
|
|---|
| Project Period (FY) |
2000 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2001: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2000: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | 形式的検証 / システムLSI / プレスブルガー算術 / 計算木論理 / 時相倫理 / BDD / 計算本論理 / 時相論理 |
|---|
| Research Abstract |
昨年度の研究に引き続き,以下を行った.
システムLSIの形式的検証のために論理設計レベルでの形式的検証アルゴリズムの一つであるCTL(計算木論理)モデル検査法と呼ばれる手法をプレスブルガー算術を扱えるように拡張した.一般にCTLモデル検査アルゴリズムの正当性は状態空間が有限であることを利用することによって保証されている.本研究で取り扱う拡張されたCTLモデル検査アルゴリズムは,計算途中では無限の状態を取り扱う(しかし,表現する式は計算機内では小さなデータ構造で表現できる)にもかかわらず,最終的に得られる計算結果が正しいことを証明し,拡張CTLモデル検査アルゴリズムの正当性を保証している.
また,提案アルゴリズムを実際に実現し,共有リソースヘの同時アクセスを禁止する制御回路などいくつかの例題回路に対して,本手法を適用した.本手法により,レジスタのビット数が大きくなっても検証時間が変わらないような有効な場合があることがわかった.一般にはレジスタのビット数が大きくなる検証に必要な計算時間および計算メモリは著しく大きくなる.これらの本手法の有効性について研究発表を行った.
また,さらに,プレスブルが一算術を扱うためのライブラリの高速化および省メモリ化を行うために,検証アルゴリズムを改良を行った.これらに関しては,本年度の研究成果発表は行えなかったが,次年度以降,検証アルゴリズムの更なる改善を行う予定である.
|
Report
(2 results)
Research Products
(3 results)
