周辺回路を考慮した論理検証のための特徴関数の生成について

概要

論文の詳細を見る
ディジタルハートウェアの形式的検証に要する時間は、その回路規模に対して指数関数的に増大するため、従来の検証手法を大規模な回路に適用する事は困難である。一般に、n入力論理回路は,2^nのすべての論理値組合せを受け付けるとは限らない。我々は、検証対象回路の周辺回路が出力する論理値集合を簡単に求めることができれば、検証すべき入力項目を削減することによって検証を効率化することができると考えている。周辺回路が出力する論理値集合は、特徴関数を用いて表現することができる。本稿では二分決定グラフ(以下BDD)を用いて特徴関数を表現する。従来、関数ベクトルF=[f_1…f_n]に対して特徴関数として、論理積(ε_1f_1)∧…∧(ε_nf_n)(ここでε_kf_kはf_k、もしくはf_kの否定を表わす)をとる方法が示されている。この方法を用いると論理積が恒偽でない場合は、出力関数ε_kf_k(k=1,..,n)に対応する解が存在することになる。これにより出力関数の組合せに等価な集合から特徴関数を生成することができる。しかし、この方法では解が存在しない場合にも論理積を計算してしまうため、効率が悪い。本報告では、BDDを用いて特徴関数を効率的に求める方法を提案する。
一般社団法人情報処理学会の論文
1996-09-04

周辺回路を考慮した論理検証のための特徴関数の生成について

スポンサーリンク

概要

著者

関連論文

スポンサーリンク