| Project/Area Number |
09680348
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
HIRAISHI Hiromi Kyoto Sangyo Univ., Faculty of Engineering, Professor, 工学部, 教授 (40093299)
|
|---|
| Project Period (FY) |
1997 – 1998
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥3,700,000 (Direct Cost: ¥3,700,000)
Fiscal Year 1998: ¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 1997: ¥2,200,000 (Direct Cost: ¥2,200,000)
|
|---|
| Keywords | Design Verification / Logic Design / Formal Verification / Temporal Logic / Symbolic Model Checking / Distributed Algorithm / BDD / 論理設計検証 / 様相論理 / 並列アルゴリズム |
|---|
| Research Abstract |
The major results of this research are as follows :
1.Extended Time-Space Modal Logic : In order to treat finite bit-slice circuit, we extend the Time-Space Modal Logic by introducing bit-position counter. This counter generates a signal that disables outputs from the specified bit position.
2.Verification of Concurrent Processes : A couple of new image computation algorithms are introduced. They are suitable for verification of many concurrent processes. The main idea is early smoothing and substitution of process variables and stable state variables. This method gains more than 10 times speed up. We also showed a non-deterministic substitution method for state variables.
3.Distributed Process Ordering Algorithm : We give BDD variable ordering based on process ordering. A distributed branch-and-bound algorithm for process ordering is proposed. The experimental measurements on 25 computers show that it gains super-linear speed up over 25 computers.
4.Verification of Task Control Architecture (TCA) : As an example of many concurrent processes, we tried to verify deadlock free property of TCA.Verification of deadlock free property of concurrent processes requires fairness constraints in general, which is very time-consuming. We introduced a new method for verification of deadlock free property of TCA without using fairness constraints. This method gains more than 100 times speed up.
|
