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

Lee, Soyeon

Permalink

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

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

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.

Graduation Semester

2025-12

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2025 Soyeon Lee

Owning Collections