Formal Verification of Optimizing Transformations during High-level Synthesis
Proceedings of the 12th Innovations on Software Engineering Conference (formerly known as India Software Engineering Conference)(2019)
摘要
Translation validation is the process of proving that the target code is a correct translation of the source program being compiled. In this work, 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. In this work, we show that how to generate a counter-trace (cTrace) using the internal information of verifier in the case of non-equivalence reported by a translation validation method. We also show how a Bounded Model Checker (CBMC) can be used to find a counterexample for a given cTrace. Experimental results demonstrate the usefulness of our method.
更多查看译文
关键词
CBMC, Code Motion, Counter-example Generation, Equivalence Checking, Finite State Machine with Datapath (FSMD), Translation Validation
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要