A Verifiable High Level Data Path Synthesis Framework
Gorker Alp Malazgirt, Ender Culha, Alper Şen, Faík Başkaya, Arda Yurdakul · 2012
This work presents a synthesis framework that generates a formally verifiable RTL from a high level language. We develop an estimation model for area, delay and power metrics of arithmetic components for Xilinx Spartan 3 FPGA family. Our estimation model works 300 times faster than Xilinx's toolchain with an average error of 6.57\% for delay and 3.76\% for area estimations. Our framework extracts CDFGs from ANSI-C, LRH(+) [1] and VHDL. CDFGs are verified using the symbolic model checker NuSMV [2] with temporal logic properties. This method guarantees detection of hardware redundancy and word-length mismatch related bugs by static code checking.