2008 年度研究成果報告書

モジュールの依存関係に基づく並列論理設計検証

研究課題

研究課題/領域番号	18500043
研究種目	基盤研究(C)
配分区分	補助金
応募区分	一般
研究分野	計算機システム・ネットワーク
研究機関	京都産業大学
研究代表者	平石裕実京都産業大学, コンピュータ理工学部, 教授 (40093299)
研究期間 (年度)	2006 – 2008
キーワード	設計検証 / モデル検査 / モジュール分割 / 共有二分決定グラフ / 並列アルゴリズム
研究概要	形式的論理設計検証手法として記号モデル検査を取り上げ、モジュールの依存関係や内部の制御構造に着目して変数順を決めるアルゴリズムを提案し、これにより効率を数倍から数百倍向上出来ることを示した。また、分割した遷移関係を用いるアルゴリズムの中で、値が変化しない変数を早期に削除することにより、数倍から数十倍の効率向上が得られることを示した。さらに、並列論理関数処理として動的並列化法を提案し、その有効性も示した。