Experimentation with SMT solvers and theorem provers for verification of loop and arithmetic transformations
Chandan Karfa, Kunal Banerjee, Debjit Sarkar, Chittaranjan Mandal · 2013
Loop and arithmetic transformations are applied extensively on array and loop intensive behaviours while designing area/energy efficient systems in the domain of multimedia and signal processing applications. Ensuring correctness of such transformations is crucial for the reliability of the designed systems. Initially, verification of these transformations using existing SMT solvers, CVC4 and Yices, and a theorem prover, ACL2, is attempted. It was observed that these tools are not efficient enough to verify loop and arithmetic transformations, especially for the non-equivalent cases. This encouraged us to develop an array data dependence graph (ADDG) based equivalence checking method for the same. The experimental results show the effectiveness of our method.