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
|
| Project Status |
Completed (Fiscal Year 2009)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2009: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2008: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2007: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(11 results)
