Dafny-HLS: verified and optimized high-level synthesis via MLIR with LLM-assisted bug repair
Lee, Soyeon
This item's files can only be accessed by the System Administrators group.
Permalink
https://hdl.handle.net/2142/132811
Description
Title
Dafny-HLS: verified and optimized high-level synthesis via MLIR with LLM-assisted bug repair
Author(s)
Lee, Soyeon
Issue Date
2025-12-11
Director of Research (if dissertation) or Advisor (if thesis)
Chen, Deming
Department of Study
Electrical & Computer Eng
Discipline
Electrical & Computer Engr
Degree Granting Institution
University of Illinois Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Keyword(s)
High-Level Synthesis
MLIR
LLM
Language
eng
Abstract
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
