組合せ論理回路のセルフテスティング性の形式的検証とその並列化

摘要

本稿では、組合せ論理回路のセルフテスティング性の検証について、二分決定グラフ（BDD）及び拡張二分決定グラフ（XBDD）を用いた論理関数処理による方法を示し、またそれらの並列化手法について提案する。 まず、組合せ論理回路のセルフテスティング性の形式的検証を、回路の入力と出力の符号語の特徴関数を利用した判定関数の充足可能性判定問題に帰着し、それをBDDを用いて解く方法を示す。 次に、より少ない節点拳で論理関数を表現できるXBDDを利用する方法を示し、さらに故障並列などの手法を用いた並列化により高速化をはかり、実際にMPI を用いてワークステーションクラスタに実装して実験した結果により、その有効性を示す。