2005 Fiscal Year Annual Research Report
VLSI搭載電子機器設計への形式的手法の適用による設計生産性並びに設計再利用性向上技術に関する研究
| Project/Area Number |
04F04350
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
藤田 昌宏 東京大学, 大規模集積システム設計教育研究センター, 教授
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKUNKONCHAK Thanyapat 東京大学, 大規模集積システム設計教育研究センター, 外国人特別研究員
|
|---|
| Keywords | システムLSI / 形式的検証技術 / 同期検証 / SpecC言語 |
|---|
| Research Abstract |
VLSIを搭載した電子機器の設計においては、設計生産性を向上させるために、設計工程のできるだけ早い段階で、設計誤りを発見・修正することが重要である。その実現手段の1つとして、テストパタンに依存しない検証ができる形式的検証の適用が有効であると考えられる。本研究では、主に、システムレベルでの設計を対象に、形式的検証の適用によって、網羅的な検証を行い、設計のやり直しを防ぐことを目的の1つとしている。
対象とする詩計記述は、Cベースのシステム設計言語であるSpecC言語で記述された並列プロセスを含むものである。検証手法は、反例に基づいた設計抽象化改良技術を利用している。この手法では、検証が成功した場合には、設計誤りがないことが証明される。検証が失敗した場合であっても、設計に誤りがない可能性があり、記述の抽象化を改良して検証を繰り返す必要がある。2005年度は、2004年度までに考案した抽象化手法や順序関係の線形計画法への定式化を実装した。線形計画法で表された問題を解く部分については、商用のソルバーを利用している。実装されたプロトタイプツールを用いて検証手法の評価を行ったところ、SpecC言諸で記述されたいくつかの例題に対して、設計記述中のデッドロックの有無を自動検証することができるようになった。検証時間については、抽象化を適用しているため十分に短く、約5万行のSpecC記述に対する検証を40秒で行うことができた。今後、より大きな設計対象に適用できるとともに、よりロバストに検証を行うことができることができるように実装を進めていく予定である。
|
