仕様が漸化式で与えられた組含せ回路の形式的設計検証

概要

論文の詳細を見る
形式的設計検証は設計が仕様を満足するかどうかを厳密かつ完全に保証しようというものであり、これまで様々な手法が提案されてきた。特に二分決定グラフ(BDD)が提案されてから飛躍的に進歩し、組合せ回路の論理照合や、順序回路の命題時相論理モデルチェッキングなどは実用レベルに達しつつある。しかしながら、形式的設計検証では仕様を厳密かつ正確に与えることが必要であり、これは容易ではない。特に組合せ回路の論理照合では、仕様として論理関数を与えるのが一般的であり、同じものを2回設計して比較しているに過ぎないという見方もできる。本稿では、算術演算回路のような組合せ回路の仕様としてその性質を漸化式で与えることとし、これを設計された回路が満足するかどうか形式的設計検証する方法について考える。漸化式は設計対象の数学的な性質等から容易に導出できることが多いと考えられる。漸化式をBDD上で効率良く取り扱うため、関数f(x)を表すBDDから関数f(x+1(mod 2_n))を表すBDDを生成する真理値巡回演算のアルゴリズムを示す。
一般社団法人情報処理学会の論文
1994-03-07