VLSI搭載電子機器設計への形式的手法の適用による設計生産性並びに設計再利用性向上技術に関する研究
| Project/Area Number |
04F04350
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 外国 |
|---|
| Research Field |
Electron device/Electronic equipment
|
|---|
| Research Institution | The University of Tokyo |
|---|
| Host Researcher |
SAKUNKONCHAK Thanyapat (2006) 東京大学, 大規模集積システム設計教育研究センター, 産学官連携研究員
藤田 昌宏 (2004-2005) 東京大学, 大規模集積システム設計教育研究センター, 教授
|
|---|
| Foreign Research Fellow |
SAKUNKONCHAK Thanyapat 東京大学, 大規模集積システム設計教育研究センター, 外国人特別研究員
|
|---|
| Project Period (FY) |
2004 – 2006
|
| Project Status |
Completed (Fiscal Year 2006)
|
| Budget Amount *help |
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 2006: ¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 2005: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2004: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | システムLSI / 形式的検証技術 / 同期検証 / SpecC言語 |
|---|
| Research Abstract |
VLSIを搭載した電子機器の設計においては、設計生産性を向上させるために、設計工程のできるだけ早い段階で、設計誤りを発見・修正することが重要である。その実現手段の1つとして、テストパタンに依存しない検証ができる形式的検証の適用が有効であると考えられる。本研究では、主に、システムレベルでの設計を対象に、形式的検証の適用によって、網羅的な検証を行い、設計のやり直しを防ぐことを目的の1つとしている。
対象とする設計記述は、Cベースのシステム設計言語であるSpecC言語で記述された並列プロセスを含むものである。検証手法は、反例に基づいた設計抽象化改良技術を利用している。この手法では、検証が成功した場合には、設計誤りがないことが証明される。検証が失敗した場合であっても、設計に誤りがない可能性があり、記述の抽象化を改良して検証を繰り返す必要がある。
2006年度は、2005年度までに構築した同期検証フレームワークをベースとして、SpecC言語で記述されたシステムの同期検証を完全に行うことができるツールを目指し、実際にシステムレベル設計に利用可能なレベルに近いツールを開発した。同時平行的に、上記フレームワークに必要なabstraction refinementなどの要素技術についての改良・新規提案も行った。
|
Report
(3 results)
Research Products
(4 results)
