VLSI搭載電子機器設計への形式的手法の適用による設計生産性並びに設計再利用性向上技術に関する研究

点击翻译按钮获取中文摘要

VLSIを搭載した電子機器の設計においては、設計生産性を向上させるために、設計工程のできるだけ早い段階で、設計誤りを発見・修正することが重要である。その実現手段の1つとして、テストパタンに依存しない検証ができる形式的検証の適用が有効であると考えられる。本研究では、主に、システムレベルでの設計を対象に、形式的検証の適用によって、網羅的な検証を行い、設計のやり直しを防ぐことを目的の1つとしている。対象とする設計記述は、Cベースのシステム設計言語であるSpecC言語で記述された並列プロセスを含むものである。検証手法は、反例に基づいた設計抽象化改良技術を利用している。この手法では、検証が成功した場合には、設計誤りがないことが証明される。検証が失敗した場合であっても、設計に誤りがない可能性があり、記述の抽象化を改良して検証を繰り返す必要がある。2006年度は、2005年度までに構築した同期検証フレームワークをベースとして、SpecC言語で記述されたシステムの同期検証を完全に行うことができるツールを目指し、実際にシステムレベル設計に利用可能なレベルに近いツールを開発した。同時平行的に、上記フレームワークに必要なabstraction refinementなどの要素技術についての改良・新規提案も行った。