2011 Fiscal Year Research-status Report
システムレベル設計に対する入出力タイミングを考慮した等価性検証手法に関する研究
| Project/Area Number |
23700051
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
松本 剛史 東京大学, 大規模集積システム設計教育研究センター, 助教 (40536140)
|
|---|
| Project Period (FY) |
2011-04-28 – 2013-03-31
|
| Keywords | 高位設計 / 等価性検証 |
|---|
| Research Abstract |
本研究課題では、２つの設計記述に対して、タイミングを考慮した等価性検証を行うことを目的としており、本年度は、入出力タイミングを考慮した高位設計の等価性検証の前提となる、等価性を判定するタイミングの数学的な定義を行い、その定義に基づいて、与えられた２つの設計の入出力変数・内部変数において成り立つ等価性を推定する手法の研究を行った。入出力タイミングを考慮した等価性は、ある時刻を基準としたスループットとレイテンシの２つのパラメータによって表現することを基本とした。加えて、その等価性が評価されるために必要な条件（例えば、リセットがかかっていない、など）を論理式で追加することができる。これにより、タイミングを考慮した等価性検証の問題を表現することができるようになる。続いて、この定義に基づいて、与えられた２つの設計中から、タイミングを考慮した内部等価点を抽出する手法を提案した。この内部等価点の抽出には、膨大な数の変数の組合せを比較する必要があるため、通常の計算機による実行では、非常に限られた範囲の変数の組合せ・スループット値・レイテンシ値しか対象とすることができない。そこで、高い並列実行が可能なGPGPUによる実装を検討し、その初期実装を行った。このGPGPUによる実装では、等価性を比較すべき２つの出力変数に依存を与える可能性のある部分に対して、与えられたスループット値・レイテンシ値の範囲内で成立する等価性を網羅的に抽出することができる。抽出された内部等価点の情報から、等価性を比較する２つの設計全体の入出力において、どのようなタイミングを考慮した等価性が成り立つかを演繹的に推定する手法についても合わせて研究を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究課題では、２つの設計記述に対して、タイミングを考慮した等価性検証を行うことを目的としており、本年度の研究において、研究計画通り、その前提となるタイミングを考慮した等価性の定義について一定の成果を出すことができた。設計者自身がこの定義に従って、設計記述間の等価性を表現することは実用上は難しいため、次の段階として、この定義に基づいて、設計記述の入出力において成り立つ等価性を推定することに取り組み、通常の計算機による実行では限られた範囲の変数組合せ・スループット値・レイテンシ値しか扱うことができないことが明らかとなり、これを解決するためにGPGPUを用いた内部等価点抽出を考えるに至った。これによって、内部等価点の抽出に関しても目標を達成できたと考えている。以上より、当初の研究計画と照らして、研究はおおむね順調に進展していると考えている。
|
| Strategy for Future Research Activity |
最終年度となる次年度は、複数のテストパタンの実行結果から抽出されたタイミング付きの内部変数の等価性から、比較する２つの設計において、全体として成り立つ可能性のある等価性を推定する手法を確立する。これは、抽出された内部等価点の情報から演繹的に求めることができると考えている。また、このような方法で推定されたタイミング付き等価性は、いくつかのテストパタンの実行結果から抽出されているため、全ての入力パタンについて成り立つことは保証されていない。そこで、推定された等価性を実際に形式的検証手法によって証明する必要がある。この検証において、内部等価点の利用による効率化を従来手法に追加した効率的な手法の開発を行う。以上の研究によって、最終的には、時間経過を含む実際の設計記述において、等価性検証を行うことを目的とする。
|
| Expenditure Plans for the Next FY Research Funding |
今年度に購入予定だったワークステーション一式については、研究の進捗状況から、通常のCPUを搭載したワークステーションよりもGPGPUを搭載したものの方が、研究に役立つ可能性が生じたため、購入を延期している。次年度前半において、より研究に有意なものを選択し、購入する予定である。その他については、当初の研究計画に従って、ハードウェア設計記述言語のフロントエンドソフトウェアの購入や研究成果発表のための費用として使用する予定である。
|
