Project/Area Number  03650301 
Research Category 
GrantinAid for Scientific Research (C).

Research Field 
情報工学

Research Institution  Kyoto Sangyo University 
Principal Investigator 
HIRAISHI Hiromi Kyoto Sangyo Univ., Engineering, Professor, 工学部, 教授 (40093299)

CoInvestigator(Kenkyūbuntansha) 
ISHIURA Nagisa Osaka Univ., Engineering, Lecturer, 工学部, 講師 (60193265)

Project Fiscal Year 
1991 – 1992

Project Status 
Completed(Fiscal Year 1992)

Budget Amount *help 
¥2,800,000 (Direct Cost : ¥2,800,000)
Fiscal Year 1992 : ¥1,000,000 (Direct Cost : ¥1,000,000)
Fiscal Year 1991 : ¥1,800,000 (Direct Cost : ¥1,800,000)

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 (KUEChip 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 bottomup 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 KUEChip 2 verification. 3. Formal Verification of Practical Logic Systems : We verified the design of KUEChip 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 multimicroprocessor 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.
