有限遅延幅モデルにおける非同期式論理回路の形式的検証に関する研究

1997 Fiscal Year Annual Research Report

• Project/Area Number: 09680329
• Research Category: Grant-in-Aid for Scientific Research (C)
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 米田 友洋 東京工業大学, 大学院・情報理工学研究科, 助教授 (30182851)
• Keywords: 形式的検証 / 非同期式回路 / 有限遅延幅モデル / タイムペトリネット / 時間トレース理論 / Partial order reduction

Research Abstract

従来,非同期式回路の設計検証においては,主に素子の遅延時間は0から無限大として取り扱われてきた.しかし,どのような遅延時間に対しても正しく動作するように設計しようとすると,回路が複雑になり結果として動作速度が低下する.そこで,最近では素子の最大遅延はある有限値であると仮定し,その仮定のもとで回路を設計することが行なわれている.しかし,このようにして設計された回路は,従来のいわゆるuntimedモデルに基づく検証方式では設計の正しさを確認できない.そこで,このような回路をより正確にモデル化するために実時間制約を表現できるモデルと,それに基づく検証方法が必要となる.今年度は,まず,時間トレース理論による検証方式の理論的形式化と,タイムペトリネットに基づく検証アルゴリズムの正しさの証明を与えた.次に,時間トレース理論に基づく検証アルゴリズムは,untimedモデル用アルゴリズムに比べ,どうしても計算量が大きくなるので,仕様や回路の記述能力に,実用上差し支えない制約を与えること,および,partial order reductionと呼ばれる,検証の結果に影響しない範囲で検査する状態数を削減する技術を本手法に応用することを検討した.簡易版の実装を行った結果,確かにその有効性が確認できた.今後,まず,partial order reductionに基づくアルゴリズムの正当性の形式的な証明,および,メモリ効率を改善する手法の開発,そして,最終的にツールとして使用に耐えうるように,実装の調整を行う予定である.