• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

並行動作順序回路システムの設計と検証に関する研究

研究課題

研究課題/領域番号 11680358
研究種目

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 計算機科学
研究機関大阪大学

研究代表者

谷口 健一  大阪大学, 大学院・基礎工学研究科, 教授 (00029513)

研究分担者 北道 淳司  大阪大学, サイバーメディアセンター, 講師 (20234271)
岡野 浩三  大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
東野 輝夫  大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
山口 弘純  大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
北嶋 暁  大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
研究期間 (年度) 1999 – 2000
研究課題ステータス 完了 (2000年度)
配分額 *注記
3,400千円 (直接経費: 3,400千円)
2000年度: 1,300千円 (直接経費: 1,300千円)
1999年度: 2,100千円 (直接経費: 2,100千円)
キーワード設計検証 / Out-of-order CPU / 記号モデル検査 / 実時間システム / 並列動作順序回路 / 並列制御部 / プレスブルガー文真偽判定 / 順序機械 / 並行システム / パイプラインCPU / 動的性質 / モデル検査 / 拡張有限状態機械 / 時間オートマトン / プレスブルガー文 / out-of-order型パイプラインCPU
研究概要

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

報告書

(3件)
  • 2000 実績報告書   研究成果報告書概要
  • 1999 実績報告書

研究成果

(21件)

すべて その他

すべて 文献書誌

  • [文献書誌] 竹中崇: "あるクラスのOut-of-order型パイプラインCPUの設計の正しさの十分条件とその形式的検証"情報処理学会論文誌. 第40巻第4号. 1587-1596 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Kozo Okano: "Specification of Real-time Systems using a Timed Automata Model with Shared Variables and Verification of Partial-deadlock Freeness"Proceedings of IEEE International Conference on Parallel Processing Workshops 1999. 576-581 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] 北濱優子: "CPU設計導入教育への形式的設計手法の適用"情報処理学会論文誌. 第41巻第11号. 3114-3121 (2000)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Kozo Okano: "Formal Verification of CPU in Laboratory Work"Proceedings of the 2001 International Conference on Microelectronic Systems Education (MSE 2001). (to appear). (2001)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] 竹中崇: "整数入力を保持するレジスタを持つEFSMに対する記号検査アルゴリズム"電子情報通信学会第13回回路とシステム(軽井沢)ワークショップ論文集. 555-560 (2000)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] 平田雅之: "整数入力のみを保持する変数を持つEFSM群に対する動的性質の検証"電子情報通信学会技術報告. SS Vol.2000 No.24. 9-16 (2000)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Takashi Takenaka: "A Formal Verification Method of Pipelined Microprocessors with Out-of-order Execution"Transactions of Information Processing Society of Japan. Vol.40, No.4. 1587-1596 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Kozo Okano: "Specification of Real-time Systems using a Timed Automata Model with Shared Variables and Verification of Partial-deadlock Freeness"Proceedings of IEEE International Conference on Parallel Processing Workshops. 576-581 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Yuko Kitahama: "Applying Formal Verification Method to Education in Design of CPU"Transactions of Information Processing Society of Japan. Vol.41, No.11. 3114-3121 (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Kozo Okano: "Formal Verification of CPU in Laboratory Work"Proceedings of the 2001 International Conference on Microelectoronic Systems Education (MSE2001). (to appear). (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Takashi Takenaka: "Symbolic Model Checking of a Class of Extended Finite State Machines with Integer Input Variables"Proceedings of IEICE the 13^<th> Workshop on Circuits and Systems in Karuizawa. 555-560 (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Masayuki Hirata: "Symbolic Model Checking Algorithm for a System consisting of Extended Finite State Machines with Integer Input Registers"IEICE Technical Report of Software Science. Vol.2000, No.24. 9-16 (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2000 研究成果報告書概要
  • [文献書誌] Kozo OKANO: "Formal Verification of CPU in Laboratory Work"Proceedings of 2001 International Conference on Microelectronic Systems Education. (to appear). (2001)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 平田雅之: "整数入力のみを保持する変数を持つEFSM群に対する動的性質の検証システムの試作"情報処理学会第62回全国大会講演論文集. (to appear). (2001)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 北濱優子: "CPU設計導入教育への形式的設計手法の適用"情報処理学会論文誌. Vol.41,No.11. 3114-3121 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 平田雅之: "整数入力のみを保持する変数を持つEFSM群に対する動的性質の検証"電子情報通信学会技術報告. SS Vol.2000 No.24. 9-16 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 竹中崇: "整数入力を保持するレジスタを持つEFSMに対する記号検査アルゴリズム"第13回回路とシステム(軽井沢)ワークショップ論文集. 555-560 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 辻川竜宏: "全称子で束縛された冠頭標準形プレスブルガー文の真偽判定分散実行"情報処理学会第60回全国大会講演論文集. 第1集. 337-338 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 竹中 崇: "整数入力値を保持するレジスタを持つ EFSM に対する記号モデル検査アルゴリズム"電子情報通信学会第13回回路とシステム(軽井沢)ワークショップ. (発表予定) (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] Kozo Okano: "Specification of Real-time Systems using a Timed Automata Model with Shared Variables and Verification of Partial-deadlock Freeness"Proceedings of the 1999 ICPP Workshops. 576-581 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] 竹中 崇: "あるクラスの Out-of-order 型パイプライン CPU の設計の正しさの十分条件とその形式的検証"情報処理学会論文誌. Vol.40,No.4. 1587-1596 (1999)

    • 関連する報告書
      1999 実績報告書

URL: 

公開日: 1999-03-31   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi