2009 Fiscal Year Final Research Report
Study on Model Checking for High-Level Hardware Design Descriptions
| Project/Area Number |
19500043
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Computer system/Network
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
HAMAGUCHI Kiyoharu Osaka University, 大学院・情報科学研究科, 准教授 (80238055)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Keywords | 設計検証 / フォーマル検証 / 第1階述語論理 / モデル検査 / 高位ハードウェア設計 |
|---|
| Research Abstract |
Model checking is a technology for verifying the correctness of hardware or software designs, which has been widely used. Designs including complex arithmetic operations are hard to handle even for small designs. In this study, in particular, for high-level design descriptions, an approach that combines multiple logics has been developed and implemented, to abstract away unnecessary details. As a result, some digital signal processing designs have become tractable in term of model checking.
|
