| Research Abstract |
昨年度は,データパスは(ランダムデータに基づき)部分的に,制御部は網羅的に検証を行うことで,人手による簡単化・抽象化を不要とする手法を確立することを目的として,タイムペトリネットモデルの拡張を行った.これは,データトランジション,条件トランジションといったデータを出力・比較するトランジションを設けたもので,これを用いることにより,データやレベル指向の記述能力が大幅に向上する.一方,実際の状態探索に要する計算量はほとんど変わらないため,単純に状態解析を行うと状態爆発問題が起こりうる.そこで,検証に必要ない部分の状態解析を効率的に除去する,partial order reductionと呼ばれる手法を,拡張したタイムペトリネットに適用することを検討してきた.本年度は,このアルゴリズムの詳細を検討し,形式的に記述した.解決すべき問題は,ある状態で発火させるべき最小のトランジション集合を求めることと,各トランジションの発火の因果関係を決定することであった.従来のタイムペトリネットに対する考え方を拡張し,新しく導入したデータトランジションや条件トランジションを扱えるように工夫した.これらの成果により,実装および正しさの証明が容易になる.本年度では実装を完了させることはできなかったが,来年度前半には完了できる見通しで,評価や正しさの証明も十分可能であると考える.
一方,この拡張したタイムペトリネットを用いれば,仕様や回路の記述に高位記述言語を用いても,それらから容易に拡張タイムペトリネットに変換できる.さらに,上記のアルゴリズムを拡張すれば,高位記述言語を直接partial order reductionを用いて解析できる見通しを得ている.これが可能になれば,高位記述のレベルで回路を検証することができ,非同期式回路の検証ツールとして完成度が非常に高まると考える.来年度はこの部分にも力を注いでいきたい.
また,3値2線式符号に基づく設計法については,基本ゲート生成アルゴリズム・簡単化アルゴリズムについて検討した,来年度はこれらの成果をまとめたいと考えている.
|
