RTL Optimization Via Verified E-Graph Rewriting (Intel, Imperial College London)


A technical paper titled “ROVER: RTL Optimization via Verified E-Graph Rewriting” was published by researchers at Intel Corporation and Imperial College London.


“Manual RTL design and optimization remains prevalent across the semiconductor industry because commercial logic and high-level synthesis tools are unable to match human designs. Our experience in industrial datapath design demonstrates that manual optimization can typically be decomposed into a sequence of local equivalence preserving transformations. By formulating datapath optimization as a graph rewriting problem we automate design space exploration in a tool we call ROVER. We develop a set of mixed precision RTL rewrite rules inspired by designers at Intel and an accompanying automated validation framework. A particular challenge in datapath design is to determine a productive order in which to apply transformations as this can be design dependent. ROVER resolves this problem by building upon the e-graph data structure, which compactly represents a design space of equivalent implementations. By applying rewrites to this data structure, ROVER generates a set of efficient and functionally equivalent design options. From the ROVER generated e-graph we select an efficient implementation. To accurately model the circuit area we develop a theoretical cost metric and then an integer linear programming model to extract the optimal implementation. To build trust in the generated design ROVER also produces a back-end verification certificate that can be checked using industrial tools. We apply ROVER to both Intel-provided and open-source benchmarks, and see up to a 63% reduction in circuit area. ROVER is also able to generate a customized library of distinct implementations from a given parameterizable RTL design, improving circuit area across the range of possible instantiations.”

Find the technical paper here. Published June 2024 (preprint).

Coward, Samuel, Theo Drane, and George A. Constantinides. “ROVER: RTL Optimization via Verified E-Graph Rewriting.” arXiv preprint arXiv:2406.12421 (2024).

Related Reading
Merging Power And Arithmetic Optimization Via Datapath Rewriting (Intel, Imperial College London)
A technical paper titled “Combining Power and Arithmetic Optimization via Datapath Rewriting” was published by researchers at Intel Corporation and Imperial College London.
Verification Tools Straining To Keep Up
Widening gap in the verification flow will require improvements in tools. AI may play a bigger role.

Leave a Reply

(Note: This name will be displayed publicly)