A Verifiable High Level Data Path Synthesis Framework

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.