2012 Fiscal Year Research-status Report
システムレベル設計に対する入出力タイミングを考慮した等価性検証手法に関する研究
| Project/Area Number |
23700051
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
松本 剛史 東京大学, 大規模集積システム設計教育研究センター, 助教 (40536140)
|
|---|
| Keywords | 高位設計 / 等価性検証 |
|---|
| Research Abstract |
本研究課題では、２つの設計記述に対して、タイミングを考慮した等価性検証を行うことを目的としている。研究の初年度であった前年度に、入出力タイミングを考慮した高位設計の等価性検証の前提となる、等価性を判定するタイミングの数学的な定義を行い、その定義に基づいて、与えられた２つの設計の入出力変数・内部変数において成り立つ等価性を推定する手法の研究を行っている。今年度は、GPGPUを利用した高速な推定方法の検討・評価、および、そのようにして推定された等価性が正しいことを形式的に検証する手法・ツールの開発・改善を行った。
本研究では、入出力タイミングを考慮した等価性は、ある時刻を基準としたスループットとレイテンシの２つのパラメータによって表現する。加えて、その等価性が評価されるために必要な条件（例えば、リセットがかかっていない、など）が論理式で追加可能である。この定義に基づいて、与えられた２つの設計中から、シミュレーション結果を参照して、タイミングを考慮した内部等価点を抽出する手法を提案した。提案手法では、高度な並列計算が可能なGPGPUによる実装を前提とし、あるシミュレーション（テストパタン）に対して、与えられた時間幅の中で成り立つ変数間の等価性を網羅的に調べることができる。
推定された等価性を形式的に検証するための等価性検証ツールの開発については、企業から提供された高位設計記述を扱えるようにするための手法と実装の改善を通して、おくつかの実例題を扱える段階に達している。従来の検証手法は、記号シミュレーションと呼ばれる、設計記述から記号式を作成する作業を実行パスごとに行っていたが、より大規模な設計記述を扱うために、全ての実行パスを１つの記号式で表す方法を導入した。これにより、分岐数の多い設計例題を効率的に検証できるようになった。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
計画では、今年度は、与えられたタイミング付きの等価性を形式的に検証する手法に加えて、等価性が証明された設計記述の部分（サブモジュール）を組み合わせて、全体として成り立つ等価性をボトムアップに導出する手法の研究も完了する予定であったが、後者については初期検討にとどまった。その理由としては、前者の研究開発において、企業から提供された設計例題の検証に取り組む中で、等価性検証ツールの大幅な改善が必要となり、そのための工数が予想より多くなったためである。加えて、企業の実例題を評価するにあたって、お互いの情報のやり取りなど、例題の評価を始める環境を整えることに計画以上の時間を要したことも遅れが生じた理由である。この改善は、実績概要で述べた通り、従来は実行パスごとに実施していた記号シミュレーションを設計全体から１つの記号式を生成するように変更した点である。しかし、この改善により、従来は扱うことのできなかった大規模な例題（より正確には、実行パス数の大きな例題）を扱えるようになったため、必要な改善であったと考えている。
|
| Strategy for Future Research Activity |
これまでに、タイミングを考慮した等価性の定義、この等価性が成立する変数組をシミュレーション結果から抽出する手法、推定されたタイミングを考慮した等価性を形式的に検証する手法については、計画通りの成果を得られている。次年度は、残された研究課題である、形式的手法によって証明された（または、シミュレーション結果から推定された）タイミングを考慮した等価性がサブモジュールに対して与えられた場合に、設計全体で成り立つ等価性をボトムアップに検証する手法の研究開発を行う。このとき、各モジュールで成り立つ等価性は、複数の解釈が可能であることに注意して研究を進める。例えば、あるモジュールＡとＢが等価に動作する場合のスループットが、それぞれ、３と１であることが分かっている場合、モジュールＡに対してスループット６で入力データを与えても、モジュールＢと等価にふるまう場合がある。そのため、設計全体の等価性を検証・推定する場合には、複数のタイミングを考慮した等価性を簡潔に表現する方法が必要である。次年度は、この表現方法を検討し、実際の検証・推定については、今年度までに開発した等価性検証ツール上に追加実装する予定である。
|
| Expenditure Plans for the Next FY Research Funding |
次年度使用額については、研究期間内に予定していた学会発表のうち、国内会議１件と国際会議１件が期間内に実施できなかったため、そのための旅費および学会参加費用として使うことを予定している。発表内容は、上記の今後の研究の推進方策で述べた研究内容である、タイミングを考慮した等価性検証におけるボトムアップ検証手法の提案と評価になる予定である。
|
