| 研究概要 |
従来,非同期式回路の設計検証においては,主に素子の遅延時間は0から無限大として取り扱われてきた.しかし,どのような遅延時間に対しても正しく動作するように設計しようとすると,回路が複雑になり結果として動作速度が低下する.そこで,最近では素子の最大遅延はある有限値であると仮定し,その仮定のもとで回路を設計することが行なわれている.しかし,このようにして設計された回路は,従来のいわゆるuntimedモデルに基づく検証方式では設計の正しさを確認できない.そこで,このような回路をより正確にモデル化するために実時間制約を表現できるモデルと,それに基づく検証方式が必要となる.1年目は,まず,時間トレース理論による検証方式の理論的形式化と,タイムペトリネットに基づく検証アルゴリズムの正しさの証明を与えた.次に,時間トレース理論に基づく検証アルゴリズムは,untimedモデル用アルゴリズムに比べ,どうしても計算量が大きくなるので,仕様や回路の記述能力に,実用上差し支えない制約を与えること,および,partial order reductionと呼ばれる,検証の結果に影響しない範囲で検査する状態数を削減する技術を本手法に応用することを検討した.簡易版の実装を行った結果,確かにその有効性が確認できた.2年目の今年度は,理論面として,時間トレース理論による「正しさ」として考えられるいくつかの定義について,それらを判定するアルゴリズムの実現可能性について検討し,いくつかの十分条件を導き出した.また,partial order reduction技術の正当性を証明した.実用面としては,partial order reduction技術を本格的に実装し,様々な非同期式回路において評価を行った結果,従来手法に対し,大幅な高性能化を達成できることがわかった.さらに,状態の共有,符号化,間引き等の技術を検討,実装し,検証時間のわずかな増加でかなりの使用メモリ量の削減を行うことができた.今後,マンマシンインタフェースを整備し,ツールとして使用に耐えるような実装を行う予定である.
|
