ワークステーションクラスタによる並列分散型形式的論理設計検証

2002 Fiscal Year Annual Research Report

• Project/Area Number: 12680361
• Research Institution: Kyoto Sangyo University
• Principal Investigator: 平石 裕実 京都産業大学, 先端科学技術研究所, 教授 (40093299)
• Keywords: 設計検証 / 論理設計 / 形式的検証 / 並列処理 / 分散処理 / クラスタシステム

Research Abstract

本年度は、イーサーネットワークとVIAに基づく超高速cLANネットワークで結合された100台のPCクラスタシステムを用いて、並列分散型検証アルゴリズム、並列分散システムの検証、並列ソーテイングアルゴリズム等の研究を行い、以下のような成果を得た。
1.論理関数の一般化コファクタ分解に基づく並列分散型検証アルゴリズムにおいて、計算の進行レベルやBDD節点数の増加レベルに基づき動的に論理関数の分割を進めていく手法を提案した。この手法では、一般化コファクタ分解を行うための核になる論理関数の選択が自動的に行われる。これにより、並列度以上の高速化を達成するスーパーリニア効果が得られ、提案したアルゴリズムの有効性を示した。
2.多くの並行動作を行うプロセスからなる並列分散システムの検証において、デッドロックの有無の検証の研究を行い、静的デッドロックに対して、プロセス変数の事前削除と静的デッドロックの記述変換を行う手法を提案した。これにより、静的デッドロックの有無の検証が大幅に高速化された。
3.大規模な並列分散システムの検証において、ある種のヒューリスティックに基づいてプロセスをソートすることにより検証が高速化される場合があることが判明したため、並列ソーテイングアルゴリズムの研究も行い、イーサーネットを用いたクラスタシステムではスイッチ間の通信がボトルネックになるのに対し、cLANネットワークではそのようなボトルネックが生じないことが明らかになった。

Research Products

• [Publications] Hiromi Hiraishi: "Symbolic Model Checking of Deadlock Free Property of Task Control Architecture"IEICE Trans. Information and Systems. E85-D・10. 1579-1586 (2002)
• [Publications] 屋敷康寛, 平石裕美: "クラスタシステムにおける並列バイトニックソートの性能評価"京都産業大学先端科学技術研究所所報. 2. (2003)