2000 Fiscal Year Final Research Report Summary
"A Study on design and verification of parallel sequential machines"
| Project/Area Number |
11680358
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Osaka 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
|
| Keywords | Design and verification technique / out-of-order pipelined CPU / symbolic model checking / real-times systems / parallel sequential machines / parallel control systems / Presburger sentences |
|---|
| 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).
|
