2002 Fiscal Year Final Research Report Summary
Parallel and Distributed Formal Logic Design Verification for Workstation Cluster System
| Project/Area Number |
12680361
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
HIRAISHI Hiromi Kyoto Sangyo University, Research Institute of Advanced Technology, Professor, 先端科学技術研究所, 教授 (40093299)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Keywords | Design \verification / Logic Design / Formal Verification / Parallel Processing / Distributed Processing / Cluster System |
|---|
| Research Abstract |
Parallel and distributed formal logic design verification algorithms have been studied. Major results include:
1. Parallel processing of Binary Decision Diagrams (BDD): An algorithm for decomposition of BDDs based on dynamic cofactoring of logic functions has been proposed. Refinement of cofactoring occurs according to the progress of construction of BDDs and the decomposed BDDs are processed in parallel on cluster machines. We obtained super-linear effect by this parallel algorithm.
2. Parallel optimization algorithm: An efficient parallel optimization and searching algorithm has been proposed. It is based on dynamic job divisions and assignments and is suitable for parallel execution on cluster system. We applied it to optimum ordering problem and obtained super-linear effect.
3. Design verification of parallel systems: Early process variable elimination method has been proposed to improve efficiency of symbolic model checking of concurrent process systems. In addition, a new approach to verification of dead-lock free property of robot control programs based on Task Control Architecture (TCA) has been proposed. By combining these two methods, we obtained more than 100 times speed up in verification of dead-lock free property of TCA.
4. Parallel sorting algorithm: Parallel bitonic sorting algorithm has been evaluated on cluster system. On cluster system connected by other network using multiple switching hubs, it has been shown that the communication between switching hubs become bottle neck of the parallel bitonic sorting. On the other hand, it has been shown that cluster system connected by cLAN network with full band-width configuration, which is VIA connection, has no bottle neck in parallel bitonic sorting
|
