Automated Translation Validation of a Compiler for Statically Scheduled Accelerators

“Automated Translation Validation of a Compiler for Statically Scheduled Accelerators” by Jackson Melchert, Caleb Terrill, Áron Ricardo Perez-Lopez, Clark Barrett, and Priyanka Raina. In Proceedings of the 25^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '25), (Ahmed Irfan and Daniela Kaufmann, eds.), Oct. 2025, pp. 198-208. Menlo Park, CA, USA.

Abstract

Compilers for programmable hardware accelerators are complex and involve progressively lowering an application down to the hardware. Bugs can be introduced at many different stages, but simulation does not provide full bug coverage and has poor bug localization. We propose a methodology for automated formal translation validation of compilers for statically scheduled accelerators. This includes generating symbolic representations of every stage in the application compiler and the hardware, leveraging scheduling information for automatically generating translation validation queries, and implementing performance enhancements for effective formal verification. This work provides a blueprint for rigorous verification of compilers and generators for hardware accelerators.

BibTeX entry:

@inproceedings{MTP+25,
   author = {Jackson Melchert and Caleb Terrill and {\'A}ron Ricardo
	Perez-Lopez and Clark Barrett and Priyanka Raina},
   editor = {Ahmed Irfan and Daniela Kaufmann},
   title = {Automated Translation Validation of a Compiler for Statically
	Scheduled Accelerators},
   booktitle = {Proceedings of the {\it 25^{th}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '25)},
   pages = {198--208},
   publisher = {TU Wien Academic Press},
   month = oct,
   year = {2025},
   doi = {10.34727/2025/isbn.978-3-85448-084-6_26},
   note = {Menlo Park, CA, USA},
   url = {https://repositum.tuwien.at/handle/20.500.12708/219556}
}

(This webpage was created with bibtex2web.)