Synthesizing Instruction Selection Rewrite Rules from RTL using SMT

“Synthesizing Instruction Selection Rewrite Rules from RTL using SMT” by Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett, and Pat Hanrahan. In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 139-150.

Abstract

Creating a compiler for an instruction set architecture (ISA) requires a set of rewrite rules describing how to translate from the compiler's intermediate representation (IR) to the ISA. We address this challenge by synthesizing rewrite rules from a register-transfer level (RTL) description of the target architecture (with minimal annotations about its state and the ISA format), together with formal IR semantics, by constructing SMT queries where solutions represent valid rewrite rules. We evaluate our approach on multiple architectures, supporting both integer and floating-point operations. We synthesize both integer and floating-point rewrite rules from an intermediate representation to various reconfigurable array architectures in under 1.2 seconds per rule. We also synthesize integer rewrite rules from WebAssembly to RISC-V with both standard and custom extensions in under 4 seconds per rule, and we synthesize floating-point rewrite rules in under 8 seconds per rule.

BibTeX entry:

@inproceedings{DDM+22,
   author = {Ross Daly and Caleb Donovick and Jackson Melchert and
	Rajsekhar Setaluri and Nestan Tsiskaridze and Priyanka Raina and
	Clark Barrett and Pat Hanrahan},
   editor = {Alberto Griggio and Neha Rungta},
   title = {Synthesizing Instruction Selection Rewrite Rules from {RTL}
	using {SMT}},
   booktitle = {Proceedings of the {\it 22^{nd}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '22)},
   pages = {139--150},
   publisher = {TU Wien Academic Press},
   month = oct,
   year = {2022},
   doi = {10.34727/2022/isbn.978-3-85448-053-2_20},
   url = {http://theory.stanford.edu/~barrett/pubs/DDM+22.pdf}
}

(This webpage was created with bibtex2web.)