• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

"A Study on design and verification of parallel sequential machines"

Research Project

Project/Area Number 11680358
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionOsaka University

Principal Investigator

KENICHI Taniguchi  Osaka University, Graduate School of Engineering Science, Professor, 大学院・基礎工学研究科, 教授 (00029513)

Co-Investigator(Kenkyū-buntansha) KITAMICHI Junji  Osaka University, Cybermedia Center, Assistant Professor, サイバーメディアセンター, 講師 (20234271)
OKANO Kozo  Osaka University, Graduate School of Engineering Science, Assistant Professor, 大学院・基礎工学研究科, 講師 (70252632)
HIGASHINO Teruo  Osaka University, Graduate School of Engineering Science, Professor, 大学院・基礎工学研究科, 教授 (80173144)
YAMAGUCHI Hirozumi  Osaka University, Graduate School of Engineering Science, Research Associate, 大学院・基礎工学研究科, 助手 (80314409)
KITAJIMA Akira  Osaka University, Graduate School of Engineering Science, Research Associate, 大学院・基礎工学研究科, 助手 (00304030)
Project Period (FY) 1999 – 2000
Project Status Completed (Fiscal Year 2000)
Budget Amount *help
¥3,400,000 (Direct Cost: ¥3,400,000)
Fiscal Year 2000: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 1999: ¥2,100,000 (Direct Cost: ¥2,100,000)
KeywordsDesign and verification technique / out-of-order pipelined CPU / symbolic model checking / real-times systems / parallel sequential machines / parallel control systems / Presburger sentences / 順序機械 / 並行システム / パイプラインCPU / 動的性質 / モデル検査 / 拡張有限状態機械 / 時間オートマトン / プレスブルガー文 / out-of-order型パイプラインCPU
Research Abstract

(1) We have proposed a method to design an out-of-order pipelined CPU and to verify its correctness. An experimental result shows that our method is useful.
(2) We have modeled TASV, which is an extended version of Alur's timed automata. The model has global variables. We have devised an efficient method to check deadlock freeness of the model which utilizes one-way reference relations of global variables.
(3) We have proposed an automatic symbolic model checking method for an extended finite state machine (EFSM), which can decide temporal properties like "it eventually reaches desired states", "it is deadlock free", and so on. We have given a sufficient condition for the checking to be decidable. In an implementation of the method, we use a library for Presburger sentences to treat arbitrary precision integer registers.
(4) We have also proposed an automatic symbolic model checking method for EFSMs, by extending the previous work. As an example, we have described a simple auction system in the model and checked some dynamic properties on it. We found that such properties can be checked on a PC within a few minutes.
(5) We have introduced automatic verification tools into a laboratory work for undergraduates. In the laboratory work, students determine CPU instruction sets and CPU architectures, and then refine the CPU designs to a logic-design level. The final design has multi FSMs as a CPU controller. We have analyzed the workloads and investigated the correctness of the final CPUs. We found that the formal methods is useful to design correct sequential machines (especially parallel sequential machines).

Report

(3 results)
  • 2000 Annual Research Report   Final Research Report Summary
  • 1999 Annual Research Report
  • Research Products

    (21 results)

All Other

All Publications (21 results)

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

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] 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)

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

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] Kozo Okano: "Formal Verification of CPU in Laboratory Work"Proceedings of the 2001 International Conference on Microelectronic Systems Education (MSE 2001). (to appear). (2001)

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

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

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] Kozo Okano: "Formal Verification of CPU in Laboratory Work"Proceedings of the 2001 International Conference on Microelectoronic Systems Education (MSE2001). (to appear). (2001)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2000 Final Research Report Summary
  • [Publications] Kozo OKANO: "Formal Verification of CPU in Laboratory Work"Proceedings of 2001 International Conference on Microelectronic Systems Education. (to appear). (2001)

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

    • Related Report
      2000 Annual Research Report
  • [Publications] 北濱優子: "CPU設計導入教育への形式的設計手法の適用"情報処理学会論文誌. Vol.41,No.11. 3114-3121 (2000)

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

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

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

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

    • Related Report
      1999 Annual Research Report
  • [Publications] 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)

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

    • Related Report
      1999 Annual Research Report

URL: 

Published: 1999-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi