1998 Fiscal Year Annual Research Report
有限遅延幅モデルにおける非同期式論理回路の形式的検証に関する研究
| Project/Area Number |
09680329
|
|---|
| Research Institution | TOKYO INSTITUTE OF TECHNOLOGY |
|---|
Principal Investigator |
米田 友洋 東京工業大学, 大学院・情報理工学研究科, 助教授 (30182851)
|
|---|
| Keywords | 形式的検証 / 非同期式回路 / 有限遅延幅モデル / タイムペトリネット / 時間トレース理論 / Partial order reduction |
|---|
| Research Abstract |
従来,非同期式回路の設計検証においては,主に素子の遅延時間は0から無限大として取り扱われてきた.しかし,どのような遅延時間に対しても正しく動作するように設計しようとすると,回路が複雑になり結果として動作速度が低下する.そこで,最近では素子の最大遅延はある有限値であると仮定し,その仮定のもとで回路を設計することが行なわれている.しがし,このようにして設計された回路は,従来のいわゆるuntimedモデルに基づく検証方式では設計の正しさを確認できない.そこで,このような回路をより正確にモデル化するために実時間制約を表現できるモデルと,それに基づく検証方式が必要となる.今年度は,理論面として,時間トレース理論による「正しさ」として考えられるいくつかの定義について,それらを判定するアルゴリズムの実現可能性について検討し,いくつかの十分条件を導き出した.また,partial order reductionと呼ばれる,検証の結果に影響しない範囲で検査する状態数を削減する技術の正当性を証明した.実用面としては,partial order reduction技術を本格的に実装し,様々な非同期式回路において評価を行った結果,従来手法に対し,大幅な高性能化を達成できることがわかった.さらに,状態の共有,符号化,間引き等の技術を検討,実装し,検証時間のわずかな増加でかなりの使用メモリ量の削減を行うことができた.今後,マンマシンインタフェースを整備し,ツールとして使用に耐えるような実装を行う予定である.
|
