Hardware Verification with respect to Program Specification
| Project/Area Number |
14580377
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
KIMURA Shinji Waseda University, Graduate School of Information, Production and Systems, Professor, 情報生産システム研究科, 教授 (20183303)
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 2004: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2003: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2002: ¥1,500,000 (Direct Cost: ¥1,500,000)
|
|---|
| Keywords | High-level Design Verification / C based Hardware Design / Reconfigurable Hardware / Verification of Arithmetic Circuits / Equivalence Verification / Uninterpreted Function / 設計検証 / 高位検証 / 再構成可能素子の検証 / テクノロジーマッピング検証 / 映像処理向け検証 / 再構成可能アーキテクチャ検証 / マルチメディア処理向け検証 / 無評価関数 / Cプログラム検証 |
|---|
| Research Abstract |
With the recent development of integrated circuit technology, we can integrate 1 million transistors in one chip. For the design of such huge circuits, high-level design methodologies have been developed and applied to many application specific chips. In the high-level design, programming languages are used to describe the functionality and the description is automatically converted to hardware modules based on high-level synthesis algorithms. So the modification and verification should be done at programming level and high-level verification methods are needed. In this research, we have developed several basic algorithms to show the correctness of hardware modules with respect to the program specification.
At first, we have surveyed the current research on the equality with uninterpreted function and its application to software and hardware verification. We have also checked the current equality systems such as SVC, CLVL, etc. We have applied these systems for the verification of arith
… More
metic circuits and shown the limitation of such systems. We have also applied the equality checking systems for the verification of parallel and pipeline circuits.
In the equality checking, the algorithm uses logic formulae to represent and decide the equality. For the acceleration of the decision procedure, we proposed a prototyping system based on new look-up-table architecture of Field Programmable Gate Array. We have devised the architecture and proposed a mapping method for the new architecture. The architecture is more area-efficient and faster compared to the usual loop-up-table architecture.
For the program specification, we have proposed a control-data-flow graph based data-path optimization methods. Especially, we focused on the bit-width of data-paths and proposed an optimization method of integer operations and an error estimation method for floating point operations. With the optimization and estimation algorithms, we can verify application specific circuits written in C programs.
We have also worked on the high-level test and proposed a test pattern compaction method with small area overhead for system-on-chip design. Less
|
Report
(4 results)
Research Products
(28 results)
