パイプライン処理の形式的並列設計検証手法に関する研究

研究課題

研究課題/領域番号	06780266
研究種目	奨励研究(A)
配分区分	補助金
研究分野	計算機科学
研究機関	奈良先端科学技術大学院大学
研究代表者	木村晋二奈良先端科学技術大学院大学, 情報科学研究科, 助教授 (20183303)
研究期間 (年度)	1994
研究課題ステータス	完了 (1994年度)
配分額 *注記	1,000千円 (直接経費: 1,000千円) 1994年度: 1,000千円 (直接経費: 1,000千円)
キーワード	パイプライン処理 / 形式的検証 / 暗黙状態数え上げ / 並列論理設計検証 / BDD / 二分決定グラフ / パイプライン検証
研究概要	本研究では、パイプライン処理方式の形式的な並列設計検証手法の研究を行なった。とくに、パイプラインプロセッサの制御方式の検証に着目し、二分決定グラフを用いた暗黙状態数え上げに基づき、命令をパイプライン処理するときのパイプラインの乱れであるハザードが生じるかどうかを判定する手法を示した。通常ハザードの検出はシミュレーションで行われているが、本手法はこのシミュレーションを記号的にすべての場合について網羅的に行う手法である。具体的には、連続する二つの命令を記号的に与えて記号実行を行う。着目している二つの命令以外はNOP命令にする。またそれと同時に二命令の間にNOP命令を適当な数だけはさんだ命令列を記号実行し、最初の命令列と比較を行なうことで、ハザードを生じるかどうかおよび、ハザードを消すためにどのような機構を備えているかを検出する。記号実行の部分は順序回路の暗黙状態数え上げ手法を用いている。実行はプログラムカウンタの値を除いて、すべてのレジスタの値が定常状態になるまで行なう。記号実行の結果は論理関数として表される。検証は、各命令列について定常状態になるまでのクロック数および定常状態の各レジスタの値が等しいかどうかを比較することで行なう。記号実行対象の回路の演算回路部分の簡単化のために剰余BDDと呼ばれる新しい二分決定グラフを提案した。また、並列化に関しては、暗黙状態数え上げの並列化手法を示した。本並列化手法は、二分決定グラフのグラフ自体をデータフローグラフと見て並列性を抽出するという新しい手法である。これにより、10CPUで4倍程度の高速化を達成した。今後は、本検証手法をスーパースカラプロセッサの検証に適用することや、二分決定グラフのグラフ構造を用いた並列化手法と通常の二分決定グラフの演算の並列化手法と組み合わせることなどが必要である。