2000 Fiscal Year Annual Research Report
| Project/Area Number |
11680358
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 大学院・基礎工学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
北道 淳司 大阪大学, サイバーメディアセンター, 講師 (20234271)
岡野 浩三 大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
東野 輝夫 大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
山口 弘純 大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
北嶋 暁 大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
|
|---|
| Keywords | 順序機械 / 設計検証 / 並行システム / パイプラインCPU / 動的性質 / モデル検査 |
|---|
| Research Abstract |
(1)昨年に引き続き,拡張有限状態機械(EFSM)の動的性質(望みどおりの要求性質を満たす状態にいつかは必ずたどりつける,デッドロック状態に陥ることはない,など)を自動検証できるように,単体のEFSMに対する動的性質の検証アルゴリズムの検討をおこなった.考案した検証法では,自動検証を可能にするため回路に対する十分条件を定めた.そのもとで,検証では,整数を直接扱えるようプレスブルガー文真偽判定ルーチンを有効に使う工夫も行った.
(2)引き続き,EFSMを複数個に拡張したモデルに対する動的性質の検証アルゴリズムを考案し,そのアルゴリズムの実装と評価実験を行った.この手法において自動検証を可能にするためのモデルを定めた.そのモデルでは,各EFSM間の同期,非同期が自由に指定できる.評価のための例題としてオークションシステムをとりあげ,「いつかはいずれかのバイヤーが落札する」,「複数のバイヤーが共に落札することはない」などの諸性質をPC上で数分以内で検証可能であることを確かめた.
(3)CPU高位設計の自動検証作業を経験させるために,学部学生のCPU設計実験において,本研究室で開発した自動検証ツールを3年前より導入している.
この学生実験では,CPUの高位の要求記述から始めて,最終的には,複数の順序回路で表現されたCPU制御部を作成する.
学生の作業履歴や設計CPUを調べた結果,検証ツールが誤りのない設計を行うのには特に有効であることを確認し,その結果を今年度,論文2編にまとめた.
(4)昨年,時間制約付きで複数の並行動作回路を記述できるモデルとして,Alurの時間オートマトンを大域変数付きに拡張したモデルTASVを提案し,そのモデル上でのデッドロックフリー性を効率よく判定する判定手法を考案した.
今年度はそれを理論的に整理して論文としてまとめ,論文誌に投稿した.
|
-
[Publications] Kozo OKANO: "Formal Verification of CPU in Laboratory Work"Proceedings of 2001 International Conference on Microelectronic Systems Education. (to appear). (2001)
-
[Publications] 平田雅之: "整数入力のみを保持する変数を持つEFSM群に対する動的性質の検証システムの試作"情報処理学会第62回全国大会講演論文集. (to appear). (2001)
-
[Publications] 北濱優子: "CPU設計導入教育への形式的設計手法の適用"情報処理学会論文誌. Vol.41,No.11. 3114-3121 (2000)
-
[Publications] 平田雅之: "整数入力のみを保持する変数を持つEFSM群に対する動的性質の検証"電子情報通信学会技術報告. SS Vol.2000 No.24. 9-16 (2000)
-
[Publications] 竹中崇: "整数入力を保持するレジスタを持つEFSMに対する記号検査アルゴリズム"第13回回路とシステム(軽井沢)ワークショップ論文集. 555-560 (2000)
-
[Publications] 辻川竜宏: "全称子で束縛された冠頭標準形プレスブルガー文の真偽判定分散実行"情報処理学会第60回全国大会講演論文集. 第1集. 337-338 (2000)
