1991 Fiscal Year Final Research Report Summary
Research on Efficient Manipulation of Boolean Functions Using Shared Binary Decision Diagrams and Its Application to Computer Aided Logic Design
| Project/Area Number |
02452162
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
情報工学
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
YAJIMA Shuzo Kyoto University, Faculty of Engineering, ProFessor, 工学部, 教授 (20025901)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OGINO Hiroyuki Kyoto University, Faculty of Engineering, Staff, 工学部, 教務職員 (40144323)
TAKENAGA Yasuhiko Kyoto University, Faculty of Engineering, Instructor, 工学部, 助手 (20236491)
ISHIURA Nagisa Osaka University, Faculty of Engineering, Lecturer, 工学部, 講師 (60193265)
TAKAGI Naofumi Kyoto University, Faculty of Engineering, Assoc. Professor, 工学部, 助教授 (10171422)
HIRAISHI Hiromi Kyoto University, Faculty of Engineering, Assoc. Professor, 工学部, 助教授 (40093299)
|
|---|
| Project Period (FY) |
1990 – 1991
|
| Keywords | Boolean Function / Binary Decision Diagram / Boolean Function Manipulation / computer Aided Design / Symbolic Simulation / Timing Verification / Logic Design Verification / Computational complexity |
|---|
| Research Abstract |
We have carried out researches on efficient representation and manipulation of Boolean functions, and applied them to computer aided logic design.
1. Efficient Representation and Manipulation of Boolean Functions
We have carried out researches on the efficient representation of Boolean functions using Shared Binary Decision Diagrams (SBDDs). For efficient manipulation of SBDDS, we have proposed attributed edges. We have developed a vector algorithm for manipulating SBDDs. We have also investigated variables ordering methods for minimizing SBDDs.
2. Computer Aided Logic Design Using Shared Binary Decision Diagrams
We have applied Boolean function manipulation to fault diagnosis and timing verification of logic circuits. On fault diagnosis, we have developed efficient fault simulation methods for multiple faults and novel methods of generating compact test sets. On timing verification, we have developed methods for simulating logic circuits with nondeterministic delays.
3. Formal Verification of Logic Design Using Shared Binary Decision Diagrams
We have proposed a method to represent state transition diagrams using SBDDs. Based on the method, we have developed a formal verification algorithm on branching time regular temporal logic, and implemented a formal verification system for sequential machines.
4. Computational Complexity of Boolean Function Manipulation
We have clarified the class of functions efficiently expressed by BDDs. We have also developed a paranelization methods for manipulating BDDs and clarified the computational complexity.
5. Systems for Computer Aided Logic Design
We have developed a package software so as to make it easy to manipulate SBDDs on tools for computer aided logic design.
|
