T. Matsumoto, K. Seto, and M. Fujita (Japan)
Formal verification, Equivalence checking, Loop optimiza tion, C program, Inductive verification
In this paper, we propose an equivalence checking method for loop optimizations. Those optimizations are effective to improve the performance of both hardware and software. In our proposed method, a symbolic simulation based method is used to check the equivalence. Before applying symbolic simulation, loops are usually unrolled by certain number of times. This causes two problems. One is that the equiv alence of the whole loop executions is not guaranteed if the number of unrolling is not large enough. The other is that the verification time can be very long if the loops are unrolled many times. To solve the problems, we pro pose the method to verify the equivalence of programs in cluding loops and array accesses without unrolling. In the method, we extract the relations of array indexes and itera tors of loops, and find the symbolic values of the iterators, for which the loops need to be executed to compute the output arrays of arbitrary indexes. Then, symbolic simu lation is applied only to the specified iterations by setting the iterators to particular symbolic values. Thus, in most cases, symbolic simulation can complete the task within very small number of iterations. Finally, we show the ex perimental results on several loop optimizations.
Important Links:
Go Back
