Project/Area Number  05558030 
Research Category 
GrantinAid for Developmental Scientific Research (B).

Research Field 
計算機科学

Research Institution  KYOTO UNIVERSITY 
Principal Investigator 
YAJIMA Shuzo Kyoto University, Faculty of Engineering, Professor, 工学部, 教授 (20025901)

CoInvestigator(Kenkyūbuntansha) 
HIRAISHI Hiromi Kyoto Sangyo University, Faculty of Engineering, Professor, 工学部, 教授 (40093299)
OGINO Hiroyuki Kyoto University, Faculty of Engineering, Staff, 工学部, 教務職員 (40144323)
TAKENAGA Yasuhiko Kyoto University, Faculty of Engineering, Instructor, 工学部, 助手 (20236491)
HAMAGUCHI Kiyoharu Kyoto University, Faculty of Engineering, Lecturer, 工学部, 講師 (80238055)
高木 直史 京都大学, 工学部, 助教授 (10171422)

Project Fiscal Year 
1993 – 1994

Project Status 
Completed(Fiscal Year 1994)

Budget Amount *help 
¥10,700,000 (Direct Cost : ¥10,700,000)
Fiscal Year 1994 : ¥4,000,000 (Direct Cost : ¥4,000,000)
Fiscal Year 1993 : ¥6,700,000 (Direct Cost : ¥6,700,000)

Keywords  Temporal Logic / Logic Design / Formal Verification / Logic Function Manipulation / Binary Decision Diagram / Formal Specification / Model Checking / 時相論理 / 論理設計 / 形式的検証 / 論理関数処理 / 二分決定グラフ / モデルチェッキング / 仕様記述 / 論理開数処理 / 形式的論理設計検証 / 順序回路 
Research Abstract 
We studied the following topics on formal verifiers of logic designs based on temporal logic. (1) Formal verifier of logic designs (a) Temporal logics based on linear models are much more expressive and succinct in describing specifications. We implemented a verification algorithm based on logic function manipulation and showed its effectiveness for practical examples. (b) We developed a abstraction technique based on array structures in large logic circuits. In order to apply this technique to large examples, we needed to develop a method for verifying circuits, such as multipliers, which were intractable with known techniques. Using binary moment diagrams, we developed a new method, and showed through experiments that we can handle multipliers in polynomial time. We are dealing with incorporating the above two methods. (2) Highspeed manipulation of logic functions. (a) We clarified the computational complexity of Boolean operations and minimization problems over binary decision diagrams. (b) We extended the binary decision diagrams to allow Vnodes, and showed its expressive power. We also investigated the expressive powers of various branching programs. (c) We developed a new method for handling extremely large binary decision diagrams on secondary storages. We showed its effectiveness through experiments. (3) User interface of the system We implemented a new capability on MultiScreen MultiWindow systems to enable drawings of binary decision diagrams or logic circuits.
