2001 Fiscal Year Annual Research Report
ワークステーションクラスタによる並列分散型形式的論理設計検証
| Project/Area Number |
12680361
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕実 京都産業大学, 先端科学技術研究所, 教授 (40093299)
|
|---|
| Keywords | 設計検証 / 論理設計 / 形式的検証 / 並列処理 / 分散処理 / クラスタシステム |
|---|
| Research Abstract |
本年度は、VIAに基づく超高速スイッチで結合された約100台の専用PCクラスタを用いて、クラスタシステムの基本性能評価、二分決定図の並列アルゴリズム、並列プログラムの検証等の研究を行い、以下のような成果を得た。
1.VIAに基づく専用PCクラスタの評価:
種々のレベルでの並列分散検証アルゴリズムで必要となる各種のデータ転送パタンに対してVIAに基づく専用PCクラスタにおける転送速度等の基本性能評価を行った。基本的な送受信で50-90MB/sec、分配収集で1段辺り75-100MB/secの転送速度を実現出来た。
2.共有二分決定図の並列分散処理アルゴリズムの構築:
まず、共有二分決定図(BDD)のこのコファクタ分解をベースにして、基本論理演算の並列アルゴリズムを構築し、性能評価を行った結果、並列度の0.3-0.5倍程度の加速率を達成でき、また、BDDの総節点数の増加が2.5-3.5倍程度になることが判明した。また、設計検証で重要なスムージング演算、サポート演算、代入演算、像計算、逆像計算等の並列アルゴリズムを検討し、BDDのストリーミング送受信に基づく並列アルゴリズムを提案した。今後、性能評価のためのプログラム開発を行う予定である。
3.並列分散プログラムの検証:
メッセージパッシング方式の並列分散プログラムの設計検証に関して、デッドロックが無いことを検証するための数学モデルを種々検討した。この問題は、一般的にプログラムの停止性判定問題を含むため決定不能であるが、プログラムの形に制限を加えることによりfalse negativeな検証は可能になる可能性があり、どのような制限を加えればよいかについて検討していく予定である。
|
Research Products
(1 results)
