順序機械の設計検証のための暗黙状態数え上げの並列化に関する研究

1993 Fiscal Year Annual Research Report

• Project/Area Number: 05780253
• Research Institution: Nara Institute of Science and Technology
• Principal Investigator: 木村 晋二 奈良先端科学技術大学院大学, 情報科学研究科, 助教授 (20183303)
• Keywords: 順序回路の検証 / 暗黙状態数え挙げ / 二分決定グラフ / 並列二分決定グラフ処理 / Shannon展開法

Research Abstract

本研究では、論理関数の効率的な表現方法である二分決定グラフを用いた、順序回路の到達可能状態の数え挙げ手法の並列化を行った。本手法は暗黙状態数え挙げ(Implicit State Enumeration)と呼ばれ、順序回路の検証やテスト生成に使用されている。暗黙状態数え挙げは、基本的に初期状態から到達できる状態集合を網羅する手法である。順序回路において現状態と入力から次状態を決める関数は、状態を二進符合化することにより論理関数として表される。また、これまでに到達した状態集合なども、集合に属する時に1となる論理関数である特性関数で表される。本研究ではこれらの論理関数を並列二分決定グラフ処理手法で扱うことの研究を行なった。これらの論理関数の処理は、基本的には論理演算の複数個の列となるので、ここでは一般化した問題として、与えられた論理演算の列をいかに高速に処理するかの研究を行なった。並列処理手法としては、Shannon展開法を用いたもの、出力毎に処理する手法を用いたもの、Shannonの展開法を一般化したものの三つについて研究を行ない、多くの主記憶容量を要する論理関数に対してはShannonの展開法が優れていることと、一般的なベンチマークの回路に対しては出力毎の分割法が有効であるという結果を得た。Shannon展開の一般化については現在も研究を継続している。富士通研究所のAP1000を使用した実験では、乗算器の処理を512プロセサを用いて130倍程度の高速化を達成した他、一般的なベンチマーク回路に対しても64プロセサで、良い場合に27倍程度、平均で13倍程度の高速化を達成した。今後は暗黙状態数え挙げ処理特有の性質をより深く研究し、それを用いた並列化について考察する必要がある。

Research Products

• [Publications] 木村 晋二: "BDDの並列処理技術" 情報処理. 34. 624-630 (1993)
• [Publications] 木村 晋二: "非共有記憶型並列計算機上での二分決定グラフの並列処理アルゴリズムについて" 情報処理学会DAシンポジウム93. 129-132 (1993)
• [Publications] 木村 晋二: "分散記憶型並列計算機に対する並列二分決定グラフ構成アルゴリズム" 情報処理学会第47回全国大会6H-8. 6-153-154 (1993)
• [Publications] 永見 康一: "定義域限定に基づく論理関数分割を用いた並列論理検証" 情報処理学会第48回全国大会5B-2. 6-71-72 (1994)