{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/132811"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/132811","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Dafny-HLS: verified and optimized high-level synthesis via MLIR with LLM-assisted bug repair","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Lee, Soyeon"],"institution":"University of Illinois Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Chen, Deming"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-12","date_published":"2025-12","updated_at":"2026-07-22T22:25:07Z","subjects":["High-Level Synthesis","MLIR","LLM"],"languages":["en"],"rights":["Copyright 2025 Soyeon Lee"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/132811","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Chen, Deming"]},{"key":"dc:creator","label":"Author","values":["Lee, Soyeon"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2025-12","2025-12-11"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["High-Level Synthesis","MLIR","LLM"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2025 Soyeon Lee"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/132811"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2027-12-01","The student, Soyeon Lee, accepted the attached license on 2025-12-10 at 13:06.","The student, Soyeon Lee, submitted this Thesis for approval on 2025-12-10 at 13:17.","This Thesis was approved for publication on 2025-12-11 at 07:28.","DSpace SAF Submission Ingestion Package generated from Vireo submission #23123 on 2026-02-19 at 20:10:10"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Dafny-HLS: verified and optimized high-level synthesis via MLIR with LLM-assisted bug repair"]}]}],"canonical_facts":{"dc:contributor":["Chen, Deming"],"dc:creator":["Lee, Soyeon"],"dc:date":["2025-12","2025-12-11"],"dc:description":["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.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2027-12-01","The student, Soyeon Lee, accepted the attached license on 2025-12-10 at 13:06.","The student, Soyeon Lee, submitted this Thesis for approval on 2025-12-10 at 13:17.","This Thesis was approved for publication on 2025-12-11 at 07:28.","DSpace SAF Submission Ingestion Package generated from Vireo submission #23123 on 2026-02-19 at 20:10:10"],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/132811"],"dc:language":["en"],"dc:rights":["Copyright 2025 Soyeon Lee"],"dc:subject":["High-Level Synthesis","MLIR","LLM"],"dc:title":["Dafny-HLS: verified and optimized high-level synthesis via MLIR with LLM-assisted bug repair"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:07Z"}