Repository logo
 

Formal verification of source-to-source transformations for HLS

Simple item page
dc.contributor.authorPouchet, Louis-Noël, author
dc.contributor.authorTucker, Emily, author
dc.contributor.authorZhang, Niansong, author
dc.contributor.authorChen, Hongzheng, author
dc.contributor.authorPal, Debjit, author
dc.contributor.authorRodríguez, Gabriel, author
dc.contributor.authorZhang, Zhiru, author
dc.contributor.authorACM, publisher
dc.date.accessioned2024-11-11T19:34:34Z
dc.date.available2024-11-11T19:34:34Z
dc.date.issued2024-04-02
dc.description.abstractHigh-level synthesis (HLS) can greatly facilitate the description of complex hardware implementations, by raising the level of abstraction up to a classical imperative language such as C/C++, usually augmented with vendor-specific pragmas and APIs. Despite productivity improvements, attaining high performance for the final design remains a challenge, and higher-level tools like source-to-source compilers have been developed to generate programs targeting HLS toolchains. These tools may generate highly complex HLS-ready C/C++ code, reducing the programming effort and enabling critical optimizations. However, whether these HLS-friendly programs are produced by a human or a tool, validating their correctness or exposing bugs otherwise remains a fundamental challenge. In this work we target the problem of efficiently checking the semantics equivalence between two programs written in C/C++ as a means to ensuring the correctness of the description provided to the HLS toolchain, by proving an optimized code version fully preserves the semantics of the unoptimized one. We introduce a novel formal verification approach that combines concrete and abstract interpretation with a hybrid symbolic analysis. Notably, our approach is mostly agnostic to how control-flow, data storage, and dataflow are implemented in the two programs. It can prove equivalence under complex bufferization and loop/syntax transformations, for a rich class of programs with statically interpretable control-flow. We present our techniques and their complete end-to-end implementation, demonstrating how our system can verify the correctness of highly complex programs generated by source-to-source compilers for HLS, and detect bugs that may elude co-simulation.
dc.format.mediumborn digital
dc.format.mediumarticles
dc.identifier.bibliographicCitationLouis-Noël Pouchet, Emily Tucker, Niansong Zhang, Hongzheng Chen, Debjit Pal, Gabriel Rodríguez, Zhiru Zhang. 2024. Formal Verification of Source- to-Source Transformations for HLS. In Proceedings of the 2024 ACM/SIGDA International Symposium on Field Programmable Gate Arrays (FPGA '24), March 3–5, 2024, Monterey, CA, USA. ACM, New York, NY, USA, 11 pages. https://doi.org/10.1145/3626202.3637563
dc.identifier.doihttps://doi.org/10.1145/3626202.3637563
dc.identifier.urihttps://hdl.handle.net/10217/239539
dc.languageEnglish
dc.language.isoeng
dc.publisherColorado State University. Libraries
dc.relation.ispartofPublications
dc.relation.ispartofACM DL Digital Library
dc.rights©Louis-Noël Pouchet, et al. ACM 2024. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in FPGA '24, https://dx.doi.org/10.1145/3626202.3637563.
dc.subjectprogram equivalence
dc.subjectformal verifcation
dc.subjecthigh-level synthesis
dc.titleFormal verification of source-to-source transformations for HLS
dc.typeText

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
FACF_ACMOA_3626202.3637563.pdf
Size:
1.14 MB
Format:
Adobe Portable Document Format
Download

Collections

Publications