Translation validation of code motion transformations involving loops

R Chouksey, C Karfa, P Bhaduri - IEEE Transactions on …, 2018 - ieeexplore.ieee.org
R Chouksey, C Karfa, P Bhaduri
IEEE Transactions on Computer-Aided Design of Integrated Circuits …, 2018ieeexplore.ieee.org
Translation validation is the process of proving that the target code is a correct translation of
the source program being compiled. In this paper, we propose a translation validation
method to verify code motion transformations involving loops applied during the scheduling
phase of high-level synthesis (HLS). Our method is capable of ignoring false computations
during translation validation. We have also identified a scenario involving code motion
across loops where the state-of-the-art translation validation method gives false positive …
Translation validation is the process of proving that the target code is a correct translation of the source program being compiled. In this paper, we propose a translation validation method to verify code motion transformations involving loops applied during the scheduling phase of high-level synthesis (HLS). Our method is capable of ignoring false computations during translation validation. We have also identified a scenario involving code motion across loops where the state-of-the-art translation validation method gives false positive results. Our method can prove the nonequivalence of the concerned finite state machines with data paths in this scenario. We detected a bug in the HLS tool SPARK involving loop invariant code motion using our method. Experimental results demonstrate the usefulness of our method.
ieeexplore.ieee.org
以上显示的是最相近的搜索结果。 查看全部搜索结果