ROVER: RTL Optimization via Verified E-Graph Rewriting

TL;DR

A set of mixed precision RTL rewrite rules inspired by designers at Intel are developed and an accompanying automated validation framework is developed, which is able to generate a customized library of distinct implementations from a given parameterizable RTL design.

Abstract

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.

Figures (11)

• Figure 1: Progression of design cost throughout RTL rewriting for the Weight Calculation benchmark (described in Section \ref{['sect:results']}). We plot the percentage change in the circuit area metric compared to the original design at every point in the rewrite chain. The area metric may converge non-monotonically.
• Figure 2: Flow diagram describing the operation of ROVER. The intermediate RTL designs are formally verified to be functionally equivalent using a commercial equivalence checker (EC) forming a chain of reasoning. The orange boxes denote the novel contributions.
• Figure 3: E-graph rewriting for standard integer arithmetic. Dashed boxes represent e-classes of equivalent expressions. Green nodes represent newly added nodes. Red dashed boxes highlight which e-class has been modified.
• Figure 4: Edge labels show the operand's index and bitwidth in square brackets.
• Figure 5: Verilog associativity rewriting example. Signals left1 and right are functionally distinct, because the carry-out is discarded in computing add_8bit, therefore left1$\not\rightarrow$right. The signals left2 and right are functionally equivalently, therefore it is valid to rewrite left2$\rightarrow$right.