2001 Fiscal Year Annual Research Report
| Project/Area Number |
13558028
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 大学院・基礎工学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
北道 淳司 大阪大学, サイバーメディアセンター, 講師 (20234271)
東野 輝夫 大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
森岡 澄夫 日本アイ・ビー・エム, (株)・基礎研究所, 副主任研究員
山口 弘純 大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
|
|---|
| Keywords | 並列同期回路 / 自動検証 / CTL / プレスブルガー文 |
|---|
| Research Abstract |
本研究は,同期式順序回路を対象にハードウェアの高位設計検証の自動化を目指すものである.今年度は,まず,VHDLのような高位の記述言語から状態遷移モデルヘの記述変換系を実装した.そして,得られた複数の状態遷移機械上において,CTL記述で与えられた(正しさを保証するため)性質を,自動証明する方法について検討し,その方法にもとづく自動証明支援系のプロトタイプをワークステーション上で実装した.実際の証明対象性質によっては,入力変数の値自体に依存しない場合があることなどを利用し,証明の手間を削減する方法を考案した.また,この証明方法はプレスブルガー文の真偽判定機能を用いることにより,整数型などのデータを直接扱えることが特徴である.これについての中間結果を情報処理学会全国大会で報告した.また,並行システムを記述する手法としてペトリネットモデルに着目し,このモデルで記述された2つのサブシステムからなるシステムの全体仕様からの並行動作仕様自動導出の方法について検討し,プロトタイプシステムを実装し,これについての中間結果を情報処理学会全国大会で報告した.一方,これらの結果の適用性や今後の課題を検討するための設計検証の例題について研究分担者らと議論した.Open core記述の例題から,CPU core, USBなどの回路を中心に例題候補の選定を行い,現在詳細を検討中である.次年度以降は,今年度考案した検証方法のVHDL記述への適用や実用例題への適用などについて検討していく予定である.
|
