ゼロサプレス型BDD表現を用いた有限状態機械の一解析手法
スポンサーリンク
概要
- 論文の詳細を見る
有限状態機械(Finite State Machine(FSM))は、Software/Hardwareにより実現されるシステムを解析するための一表現方法である。最近、FSMの解析手法として一般化してきた手法に、FSMの状態遷移関係を論理式として間接的に表現し解析を行なうという手法がある。この手法は、古典的な状態系列を探索する方法とは異なり論理関数処理のみで、状態遷移の存在の有無や、次状態や前状態の集合を計算することが可能である。さらに、2分決定グラフ(BDD)[1]を用いることにより従来手法では不可能であった規模の状態数を持つFSMの解析を行なうことが可能となってきている。FSMの論理関数処理手法においては、遷移関数を表す論理式がBDDとして表現できない、すなわち、BDDを構成するノード数が爆発する場合に解析が行なえない。BDDのノード数は各論理変数のノードへの対応づけ(変数順)に依存するため、動的に変数の順序づけを行なうことによりBDDのサイズを小さくする手法が提案されている。しかし、動的な変数の順序づけを用いた場合、実際の論理関数の計算時間よりも変数の順序づけにかかる時間が大きく、必要とされる記憶量は削減されるが全体的な処理性能が著しく改善されてはいない。BDDを用いた論理関数処理によるBDDのノード数が増大する問題の原因は、遷移関係そのものが(入力、出力、状態)の組の集合であるものを、論理関数として表現するところにある。一般に遷移関係を表現する論理関数では、状態を表現するための変数が全て一つの遷移関数に寄与することは稀ない。なぜなら、FSMの次状態は一つの現状態と入力、出力変数の値によって決定されるからである。このため、BDDを用いて表すと一つの遷移関係を表現する場合でも、その遷移に寄与しない状態変数の値を明示的に示さなければならないので非効率的になる。そこで、遷移関係を集合表現として捉え直すことにより、効率的な表現が可能となると考えられる。本報告では、集合表現を効率的に扱えるゼロサプレス型BDD(ZBDD)[2]を用いた有限状態機械の表現手法、及び、操作手法について述べる。提案する手法は、状態遷移関係を積項集合として表現することを基本としている。そのため、ゼロサプレス型BDDの特徴がいかされ、効率的な表現方法となっている。さらに、状態遷移の有無、状態集合の導出等がグラフをたどる操作により効率的に行なえる。
- 一般社団法人情報処理学会の論文
- 1995-09-20
著者
関連論文
- 性能指向型FPGAの検討
- 論理合成システムSERAPHIMテンプレート化合成手法
- ゼロサプレスBDDによるペトリネットのCTL記号モデル検査
- ゼロサプレス型BDD表現を用いた有限状態機械の一解析手法
- 4. プロセス代数を用いた形式的検証 ( 論理設計の形式的検証)