分割二分決定グラフによる有限状態機械の到達可能性解析のPCクラスタを用いた並列実装手法の提案

• Item type: Journal(1)
• 公開日: 2005-03-15
• タイトル: 分割二分決定グラフによる有限状態機械の到達可能性解析のPCクラスタを用いた並列実装手法の提案
• タイトル / 言語: en
• タイトル: Parallelized Implementation of Reachability Analysis Using Partitioned-ROBDDs on PC-cluster
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 設計技術と設計自動化
• 著者所属: 東京大学大学院工学系研究科電子工学専攻
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属(英): en
• 著者所属(英): Electronic Engineering, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, The University of Tokyo
• 著者名: 小島, 慶久; 藤田, 昌宏
• 著者名(英): Yoshihisa, Kojima; Masahiro, Fujita
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 順序回路の形式的検証において，より大規模・複雑な回路を対象とするために，分割二分決定グラフ（POBDD: Partitioned-reduced Ordered Binary Decision Diagram）による有限状態機械（FSM: Finite State Machine）の到達可能性解析（Reachability Analysis）アルゴリズムが提案されている．この分割二分決定グラフの到達可能性解析では，いつ，どのように論理空間を分割するか決定するためのパラメータによって計算時間が大幅に変化することが経験的に知られており，適切なパラメータを選ぶことが重要となる．一方，分割二分決定グラフを用いた到達可能性解析アルゴリズムは，分割されたパーティション内の到達可能性解析とパーティション間での到達状態のやりとりに帰着でき，これらの計算は独立性が比較的高いため，並列化による高速化が期待できる．つまり，問題に適したパラメータを見つけることと，パーティション単位で計算の並列化をうまく組み合わせることが高速化に効果的であると期待できる．そこで本論文では，パーティション単位で到達可能性解析を並列化する際に，パーティション内の状態の変化の有無に着目して不要な計算や通信を防ぐ並列化手法を提案する．さらに，本研究では，パラメータ探索やパーティション単位での並列化の手法を実験するための環境を構築し，その上にこの並列化手法を実装した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: The reachability analysis algorithm of finite state machines (FSMs) using Partitionedreduced Ordered Binary Decision Diagrams (POBDDs) has been proposed to target more large and complex circuits in sequential circuit verification. It is empirically known that the computation time of the algorithm drastically changes depending on the POBDD parameters which decide how and when to decompose the logical space, thus choosing good parameters is very important in the algorithm. On the other hand, it is expected that parallelization works well because the computations used in the algorithm (namely, reachability analysis in each partition and exchanging reached states between partitions) are highly independent. Consequently, it should be effective to combine both of i) to find and apply the good parameters for given target circuits and ii) to parallelize computations for each partition. In this paper, we propose a parallelized method which aims to avoid redundant computations or communications focusing on the changes of the states in the partitions. We built a PC cluster environment for experiments of parameter-searching and parallelization by partition, and we implemented this algorithm on this environment.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 46, 号 3, p. 803-815, 発行日 2005-03-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764