| Presentation | 2007/3/9 Equivalence Checking of Loop Optimizations in C Programs without Loop Unrolling Takeshi MATSUMOTO, Kenshu SETO, Masahiro FUJITA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In designing systems such as embedded systems, where many restrictions must be satisfied, loop optimization plays an improtant role. In this paper, an equivalence checking of loop optimization is proposed. In the previous methods based on symbolic simulation, loops must be unrolled before verification. This results in that the equivalence is proved just for the unrolled programs and verification takes much time when the number of unrolling is large. In the proposed method, first, statements and the corresponding symbolic values of the iterators that are required to compute the output variables are identified. Then, symbolic simulation is applied only to the statements. Therefore, the equivalence can be checked without unrolling loops. The experimental results show that the proposed method can verify the real loop optimizations in short time. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Equivalence checking / Loop optimization / Data dependence graph / Symbolic simulation |
| Paper # | CPSY2006-94,DC2006-108 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2007/3/9(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Dependable Computing (DC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Equivalence Checking of Loop Optimizations in C Programs without Loop Unrolling |
| Sub Title (in English) | |
| Keyword(1) | Equivalence checking |
| Keyword(2) | Loop optimization |
| Keyword(3) | Data dependence graph |
| Keyword(4) | Symbolic simulation |
| 1st Author's Name | Takeshi MATSUMOTO |
| 1st Author's Affiliation | Dept. of Electronics Engineering, University of Tokyo() |
| 2nd Author's Name | Kenshu SETO |
| 2nd Author's Affiliation | VLSI Design and Education Center, University of Tokyo |
| 3rd Author's Name | Masahiro FUJITA |
| 3rd Author's Affiliation | VLSI Design and Education Center, University of Tokyo |
| Date | 2007/3/9 |
| Paper # | CPSY2006-94,DC2006-108 |
| Volume (vol) | vol.106 |
| Number (no) | 604 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |