1990 Fiscal Year Final Research Report Summary
Researches on Formal Logic Design Verification Based on Regular Temporal Logic
| Project/Area Number |
01550285
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機工学
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
HIRAISHI Hiromi Kyoto Univ., Faculty of Engineering, Assoc. Professor, 工学部, 助教授 (40093299)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OGINO Hiroyuki Kyoto Univ., Faculty of Engineering, Staff, 工学部, 教務職員 (40144323)
ISHIURA Nagisa Kyoto Univ., Faculty of Engineering, Instructor, 工学部, 助手 (60193265)
TAKAGI Naofumi Kyoto Uiv., Faculty of Engineering, Instructor, 工学部, 助手 (10171422)
|
|---|
| Project Period (FY) |
1989 – 1990
|
| Keywords | Temporal Logic / Formal Verification / Logic Design / Model Checking |
|---|
| Research Abstract |
The major goal of this research is to establish fundamental methods for formal logic design verification based on temporal logic. We have got the following results :
1. We proposed and systematized various classes of regular temporal logic including * regular temporal logic which can handle omega sequences of time. They are expressively equivalent to sequential machines in a sense, and their various properties are clarified. We also proposed a branching time regular temporal logic and showed its model checking algorithm of linear time complexity.
2. We developed a formal verification system for sequential machines based on regular temporal logic. The verification algorithm adopted in the system is highly tuned for verification of sequential machines. It checks the correctness of a machine under verification directly, which reduces necessary work area drastically. It succeeded to verify practical sequential machines of medium size (the number of transitions is less than around 10,000).
3. Aiming at timing verification, we proposes an extended real time temporal logic. Based on this logic, the formal timing verification algorithm for timed sequential machines, which is a model of sequential circuits with gate delays, is shown.
4. In order to clarify how large sequential machines can be verified by using the current most powerful supercomputers, we showed a vectorized model checking algorithm of computation tree logic, which is suitable for execution on vector processors. We also implemented the algorithm, and some benchmark results show that it can verify large practical sequential machines with more than 1 million transition edges in a few minutes.
|
