時相論理に基づく順序回路検証システムの二分決定グラフを用いた改良

スポンサーリンク

概要

論文の詳細を見る
我々は、命題論理レベルのLinear Time Temporal Logic(LTTL)で仕様を与え、ディジタルシステムの制御部同期回路を検証するシステムを既に開発しているが、論理表現として積和形(カバー表現)を用いたため、対象となる回路が大きくなると実行速度の点で問題となることがあった。近年コンパクトな論理表現法として注目されている二分決定グラフ(BDD)を用いると、実用的な論理関数の多くが変数の数の多項式オーダの記憶領域で表現でき、論理演算がBDDのノードのサイズに比例した計算時間で実行できることが知られている。また、Branching Time Temporal Logicの一つであるCTLについて、BDDを用いて検証を効率化できることが報告[3]されている。本稿では、[3]で提案されているBDDによる順序回路表現を用いたLTTLに基づく検証システムの改良について述べる。
1990-09-04

著者

関連論文

もっと見る

スポンサーリンク