2006 Fiscal Year Final Research Report Summary
Research on Equivalence Checking for High-Level Hardware Design Descriptions
| Project/Area Number |
16500030
|
|---|
| 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, Gradusate School of Information Science and Technology, Associate Professor, 大学院情報科学研究科, 助教授 (80238055)
|
|---|
| Project Period (FY) |
2004 – 2006
|
| Keywords | Formal Verification / First-Order Logic / High-Level Hardware Verification / Satisfiability Checking |
|---|
| Research Abstract |
In recent years, we need to spend more of time in design verification, which occupies 60 to 80 percent of the entire design process. To ease this difficulty, formal verification technology has been adopted, but almost all the currently available technologies cannot handle descriptions whose level is higher than register-transfer level or gate level. In this research, we study on functional equivalence checking of two high-level descriptions, such as those written in C language. By abstracting arithmetic operations in descriptions by function symbols of first-order logic, and by ingnoring the specific meaning of the symbols, we can expect the improvement in the verification efficiency.
The problem is that this approach can be applied only to very similar descriptions. To compensate for this difficulty, in this research, we propose a new equivalence checking algorithm considering "equivalence constraints". An equivalence constraint is a set of rules such as "x > 1 <-> x-l>0". They are introduced to specify patterns which should be regarded as equivalent. We modified "conflict analysis" technique which has been used for boolean satisfiability checking to our approach, and we attempted equivalence checking of programs for PARCOR filter, ADPCM filter, Fourier Transform and Square Rooting. The experimental results show that, as compared with the classical boolean based verification method, we can improve the efficiency by 10-100 times for the examples including operations which are more complex than multifications, that is, non-linear operations. In addition to this improvement, for some examples which are intractable in terms of computational complexity with the classical technique, verification became feasible with our proposed method.
|
Research Products
(2 results)
