High-Level Synthesis Tools should be Proven Correct

With hardware designs becoming ever more complex, and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon. However, HLS is known to be quite flaky, with each tool supporting subtly different fragments of the input language and sometimes even generating incorrect designs. We argue that a formally verified HLS tool could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. To this end, we are developing Vericert, a formally verified HLS tool, based on CompCert, a formally verified C compiler.