1992 Fiscal Year Final Research Report Summary
Research on Computer Aided Formal Verification Based on Temporal Logics
| Project/Area Number |
03650301
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
情報工学
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
HIRAISHI Hiromi Kyoto Sangyo Univ., Engineering, Professor, 工学部, 教授 (40093299)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
ISHIURA Nagisa Osaka Univ., Engineering, Lecturer, 工学部, 講師 (60193265)
|
|---|
| Project Period (FY) |
1991 – 1992
|
| Keywords | Logic Design Verification / Formal Verification / Temporal Logic / Computer Aided Design / Binary Decision Diagram |
|---|
| Research Abstract |
Aiming at establishment of fundamental formal verification methodology, we investigated formal design verification of finite state machines using temporal logics and have got the following major results.
1. Branching time regular temporal logic : We proposed a new branching time model temporal logic called BRTL which has more expressive power than the conventional CTL while keeping its verification complex similar to that of CTL. We showed efficient symbolic model checking algorithm of BRTL and developed an experimental verification system. We applied the system to a verification of an 8 bit microprocessor (KUE-Chip 2) and showed its effectiveness.
2. Formal Verification Algorithms : We proposed two original algorithms for verification. One is a vectorized algorithm for manipulation of binary decision diagrams (BDD's) which is essential in symbolic model checking. The vectorized algorithm achieved 20 times vector acceleration ratio. The other one is a bottom-up inverse image computation algorithm which is a key operation of symbolic model checking based on temporal logics. This algorithm achieved up to 40 times speed up in KUE-Chip 2 verification.
3. Formal Verification of Practical Logic Systems : We verified the design of KUE-Chip 2 microprocessor using BRTL and showed that the design contains design errors and that the design is correct except these design errors. In the verification, we abstracted the internal memory as input/output commands to the memory. This abstraction made it possible to verify the correctness of the whole chip. We also verified cache coherency protocol of Future Bus (IEEE standard of hierarchical bus for multi-microprocessor system) using CTL. In this case, we abstracted the shared memory and caches as 1 bit memories and showed that the cache coherency property is well modeled by the abstraction.
|
