| 研究分担者 |
北道 淳司 大阪大学, サイバーメディアセンター, 講師 (20234271)
岡野 浩三 大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
東野 輝夫 大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
山口 弘純 大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
北嶋 暁 大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
|
|---|
| 研究概要 |
1.並行動作順序回路としてきわめて有用な,あるクラスのout-of-order型パイプラインCPUに対する設計検証法を整理し,論文にまとめた.
2.時間制約付きで複数の並行動作回路を記述できるモデルとして,Alurの時間オートマトンを大域変数付きに拡張したモデルTASVを提案し,TASV上でのデッドロックフリー性を効率よく判定する判定手法を考案した.この手法を国際会議で発表した.また,それを理論的に整理して論文としてまとめ,論文誌に投稿した.
3.拡張有限状態機械(EFSM)の動的性質(望みどおりの要求性質を満たす状態にいつかは必ずたどりつける,デッドロック状態に陥ることはない,など)を自動検証できるように,単体のEFSMに対する動的性質の検証アルゴリズムを考案した.自動検証を可能にするための十分条件も定めた.任意桁の整数レジスタを扱えるようプレスブルガー文真偽判定ルーチンを有効に使う工夫も行った.その結果をワークショップで発表した.
4.さらにEFSMを複数個に拡張したモデルを考案し,それに対する動的性質の自動検証アルゴリイムを考案した.提案するモデルでは,各EFSM間の同期,非同期が自由に指定できる.評価のための例題としてオークションシステムをとりあげ,動的性質をPC上で数分以内に検証可能であることを確かめた.結果を研究会などで発表した.
5.CPU高位設計の自動検証作業を経験させるために,学部学生の設計実験において,本研究室で開発した自動検証ツールを3年前より導入している.この学生実験では,最終的に,複数の順序回路で表現されたCPU制御部を作成する.学生の作業履歴や設計CPUを調べた結果,検証ツールが誤りのない設計を行うのには特に有効であることを確認し,論文2編にまとめた.
|
