Dafny-HLS: verified and optimized high-level synthesis via MLIR with LLM-assisted bug repair

High-Level Synthesis (HLS) improves hardware design productivity by generating Register-Transfer Level (RTL) from high-level language descriptions (e.g., C/C++). While recent MLIR-based HLS frameworks enable multi-level optimization and automated design space exploration, they are based on the critical assumption that input programs are functionally correct. Moreover, subtle logic bugs in HLS often evade compilers, compromising hardware reliability. Dafny, a verification-aware programming language, could address these correctness issues through specification-based formal verification. However, no existing path connects Dafny to HLS, and its specifications have never been used to guide LLM-based repair of HLS logic bugs. To bridge these gaps, we propose Dafny-HLS, an end-to-end framework that generates synthesizable HLS C/C++ from verified Dafny programs via MLIR. Dafny-HLS (1) ensures functional correctness through Dafny specifications that verify the intended behavior, (2) provides specification-guided LLM-assisted repair of HLS logic bugs, (3) translates verified Dafny programs to MLIR using Dafny-MLIR, the first bridge from Dafny to MLIR, and (4) produces optimized, synthesizable C/C++ code with the ScaleHLS backend. We evaluate our approach on ten PolyBench kernels and multiple neural network layers, including the first formally specified and verified convolutional layer in Dafny. Our LLM-assisted repair achieves up to 95% auto-repair success on neural network layers and 74% on PolyBench kernels, while optimized HLS C/C++ outputs with the ScaleHLS backend deliver 97.6×–384.2× speedups on PolyBench and 258.1×–1014.5× across neural network workloads, compared to the direct MLIR-to-HLS C emission baseline. By combining formal verification, LLM-assisted bug repair, and MLIR-based optimization, Dafny-HLS enables reliable, high-productivity hardware design and verification.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Electrical & Computer Engr

Grantor

University of Illinois Urbana-Champaign

Year dc:date

2025

Author dc:creator

• Lee, Soyeon

Contributors dc:contributor

• Chen, Deming

• High-Level Synthesis
• MLIR
• LLM

Statement dc:rights

• Copyright 2025 Soyeon Lee

Language dc:language

en

Handle dc:identifier

https://hdl.handle.net/2142/132811

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/132811