Verification of CGRA Executable Code and Debugging of Memory Dependence Violation

Microprocessor Test and Verification(2012)

引用 1|浏览0
暂无评分
摘要
We present verification and debugging of highly optimized executable code that is generated from C source code to run on CGRA (Coarse-Grained Reconfigurable Array). To generate the executable code, the CGRA compiler uses software pipelining technique that maps instructions in a loop body to multiple FUs (functional units) of CGRA for concurrent execution. Often, the programmer chooses to use aggressive optimization as a way to obtain highly performing executable code. For example, the programmer may turn off memory dependence check in order to suppress false dependence that would otherwise result in overly conservative, therefore poorly performing, executable code. A trouble is that it is not easy to verify correctness of the resulting executable code. In this paper, we propose a method to verify CGRA executable code and to detect memory dependence violation if there occurs such violation and to provide source code position where the violation occurs. We use the behavior of VLIW code as a reference and compare it with the behavior of CGRA code. In order to guide the comparison, compiler-generated mapping table information is used.
更多
查看译文
关键词
formal verification,source coding,concurrency control
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要