2004 Fiscal Year Annual Research Report
形式的検証手法を利用したデジタルシステムの設計デバッグ技術に関する研究
| Project/Area Number |
14350178
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
藤田 昌宏 東京大学, 大規模集積システム設計教育研究センター, 教授 (70323524)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小松 聡 東京大学, 大規模集積システム設計教育研究センター, 助手 (90334325)
|
|---|
| Keywords | システムLSI / 形式的検証 / デバッグ |
|---|
| Research Abstract |
集積回路の大規模化、複雑化により設計検証期間がLSI設計工程全体の70〜80%以上を占めるようになっており、近年では設計検証技術が設計生産性を決定する重要な要素となっている。また、誤りを修正する「デバッグ工程」を支援する手法やツールにはいまだ実用的なものが無く、それらの技術を確立することで高品質な設計を迅速に行うことが可能になると考えられる。本研究は従来から研究されているレジスタ転送レベル(論理レベル)だけでなく、仕様記述レベルからハードウェア・ソフトウェアが一体となったシステムレベルの設計記述も研究対象としており、今年度は特に(1)SpecC言語で記述されたシステム記述に対するスライシング技術、(2)C言語で記述された2つの記述間の等価性検証における反例解析技術、に関する研究を重点的に行った。
プログラムスライシングは、プログラムから記述間の依存関係を表す依存グラフを構築し、到達可能性判定によって依存関係のある文を抽出する手法であり、プログラムのデバッグに利用可能な手法である。
(1)では、これをシステムレベル記述言語であるSpecC言語に適用する手法を提案・実装すると共に、これを応用したデバッグ手法として、並列処理を含むシステムレベル記述においてバグを含んでいる可能性の高い未初期化変数や未使用変数を検出する手法を提案した。
(2)では、C言語記述間の等価性検証を記号シミュレーション手法を用いて行い、検証結果が等価でない場合に、その結果を解析することによって、どの部分に等価でない原因があるのかを特定する。これにより、上位設計での設計記述変更によって、等価でない部分が生じた部分を知ることができ、デバッグに有用である。例題を用いた実験では、等価でない部分を非常に狭い範囲で特定できるという結果が得られた。
|
