| Project/Area Number |
17500047
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Computer system/Network
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
KIMURA Shinji Waseda University, Graduate School of Information, Production, and Systems, Professor (20183303)
|
|---|
| Project Period (FY) |
2005 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥3,630,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥330,000)
Fiscal Year 2007: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2006: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2005: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | equivalence logic / equivalence hardware verification / uninterpreted function / term rewriting system / high level verification |
|---|
| Research Abstract |
For the formal hardware verification at high level, the equivalence checking system based on the equivalence logic with un-interpreted functions and similarities has been studied. The original equivalence logic manipulates the equivalence of variables, and has been shown to be effective for the verification of pipeline processor. The equivalence logic with similarities is a logic system to manipulate the similarity between variables. For example, if we design a circuit with fixed-point number system, and we would like to show the correctness with respect to a C program using floating number system, then the exact equivalence cannot be shown and we should cope with the similarity At first, we have developed a prototyping system which converts Verilog description to the equivalence logic formula, a prototyping system converting C descriptions to the equivalence logic formulae, and a prototype equivalence checking system based on the time expansion and published equivalence logic checking system(like CVCL/YICES). We have tested the prototype system and Sound that the computation is proportional to the exponential with respect to the number of time expansions, and we have worked on the SAT based equivalence checking and the transitivity constraints issue. For similarities, we are working on the optimization of the number of bits of variables in the floating to fixed point conversion, and the similarity based on the difference of the values and one based one the difference with values of other live variables. We have also applied the proposed equivalence checking to the multi-threading processor design and the acceleration of equivalence verification using the prototyping environment.
|
