Improving Equality Saturation for EDA via Semantic E-Graphs

An equality-saturation and hardware-synthesis paper with two coupled contributions. At the data-structure level, semantic e-graphs replace opaque e-class identifiers with user-defined semantic values, so domain equivalence can cause merging directly and equality between composite values can propagate to their components. At the tool level, Nextmap instantiates those ideas for RTL and keeps word-level arithmetic, bit-level logic, technology-independent optimization, and technology mapping in one equality-saturation search. The paper’s strongest evidence is not that one optimizer beats every alternative, but that extracting a single design between stages discards variants that a later mapper could have exploited.

The phase boundary, not one pass, is the optimization target

Earlier equality-saturation tools for EDA usually optimize within one stage: word-level datapaths, Boolean logic, or mapping to LUTs and DSPs. They avoid phase ordering locally but must still select one representative before handing the design to the next tool. Figure 1 makes the loss concrete. Algebraic rewriting may retain both a*(b+c) and (b+c)*a, yet an intermediate extraction commits to one syntax before a brittle DSP matcher sees it.

Nextmap instead saturates optimization and mapping rules in the same structure. This reframes phase ordering as an information-retention problem: the benefit does not come merely from running more rewrites, but from delaying the point at which equivalent implementations collapse to one selected circuit. The idea is broader than any particular FPGA primitive, although the implementation and most experiments are centered on FPGA synthesis.

Semantic identifiers bridge representation levels

A conventional e-graph uses an opaque identifier for each equivalence class. Semantic e-graphs use identifiers from a domain supplied by the application. A constructor interprets a node when enough of its children are known and otherwise falls back to a symbolic value. Terms that compute the same semantic identifier join the same class without an explicit pairwise rewrite.

Composite identifiers add the reverse direction. If two vectors become equal, their aligned component wires must also become equal; a user-defined decomposition exposes those obligations directly. Deferred rebuild then propagates the canonical component identifiers upward. This replaces the quadratic joins and loop-like rules needed to express the same bidirectional relationship in vanilla egglog.

For RTL, the paper gives separate semantic domains to single wires, wire vectors, and registers. A wire vector is identified by its ordered component wires. Consequently, a word-level adder and its bit-blasted realization can coexist while sharing corresponding output bits, and an extract–concat roundtrip recovers the original vector through its semantics rather than a family of syntactic rewrites. Registers are composite too, but extraction distinguishes valid sequential feedback from forbidden combinational cycles.

The formal results are deliberately conditional. The paper proves that the algorithm maintains only the congruence generated by its syntactic and semantic relations, and that rebuild terminates under monotone constructors and finite ascending chains of semantic precision. Semantic soundness follows only when the supplied rewrite relation, constructors, and decomposition equalities are themselves sound. The theorem therefore validates the propagation machinery; it does not independently certify a technology library or Nextmap’s hardware rewrite set.

Nextmap is a mixed symbolic and optimization pipeline

Nextmap imports Yosys RTLIL into a SQLite-backed semantic e-graph. Users apply built-in or custom arithmetic, retiming, bit-blasting, and logic rules, then describe target cells through JSON or Python technology libraries. DSP mapping anchors on multipliers and grows matches into surrounding datapaths; regular accelerator blocks are matched hierarchically. An integer linear program selects a type-consistent, technology-constrained implementation, using Gurobi or CBC, and exports RTLIL. Unmapped cells continue through downstream Yosys.

That composition matters when reading the results. Nextmap directly maps DSPs, but LUT, mux, and flip-flop mapping remains a downstream Yosys task. The reported FPGA resource vector is therefore produced by a Nextmap-plus-Yosys flow, while the Yosys baseline omits Nextmap’s retained alternatives and richer DSP rules.

The ablations support delayed extraction

The evaluation spans small hand-challenging designs and larger systolic-array, FIR, FFT, and RISC-V designs, ranging from 1,082 to 345,238 wires before optimization. On the reported resource vectors, Nextmap largely dominates the open-source Yosys baseline and is often competitive with an unnamed proprietary tool. The result is not a universal PPA ordering: FPGA tables report resource counts rather than timing, individual resources trade off, and the commercial tool and its configuration are not disclosed.

The cleaner causal test compares ordinary Nextmap with a phase-ordered variant using the same rewrites but extracting and repopulating an e-graph between stages. The phase-ordered variant never dominates ordinary Nextmap on the reported resource vectors, while ordinary Nextmap dominates it on multiple designs. This supports the paper’s central information-loss account more directly than the cross-tool comparison.

The semantic-e-graph efficiency experiment is similarly targeted. A specialized egglog implementation completes construction for sixteen 32-bit ALUs and an AES S-box in under a second where the vanilla relational encoding times out after 600 seconds. End-to-end scaling is less uniform: larger-design runtimes range from 0.3 to 1,938 seconds, with the two largest systolic arrays taking 145 and 1,938 seconds and most time spent in ILP extraction. Semantic equality addresses one representation bottleneck; it does not eliminate the extraction problem.

This is adjacent to, not an instance of, symbolic execution

Nextmap symbolically retains many hardware implementations and performs equality reasoning over expressions, but it does not execute a design over symbolic inputs, accumulate path conditions, or characterize reachable behaviors. Its alternatives are implementations intended to be semantically equivalent, not execution paths or input-partitioned states. It is therefore a useful boundary case for Symbolic execution and for the Symbolic Execution of Digital Hardware Designs: A Systematic Map of Path-Conditioned Design Execution survey: symbolic representation and solver use alone do not make a hardware method symbolic execution.

Assessment

• Durable: Intermediate extraction is a lossy architectural decision. Keeping optimization and mapping alternatives together can expose solutions that no independently tuned phase can recover after committing to one representative.
• Durable: Semantic identifiers plus structural decomposition are a general pattern for combining congruence closure with domain knowledge without enumerating every derived equality as a rewrite.
• Strong evidence: The phase-ordering and vanilla-egglog ablations isolate the paper’s two central mechanisms better than the headline comparison with other synthesis tools.
• Caveat: Formal soundness is relative to user-supplied relations; the paper does not turn rewrite libraries or technology descriptions into independently checked proofs.
• Caveat: FPGA quality is evaluated mainly through resource counts on one target family, with downstream Yosys in the flow and an unidentified proprietary baseline. “Competitive QoR” should not be generalized to timing, power, other technologies, or other tool configurations.
• Caveat: The SQLite backend is chosen for simplicity, and ILP extraction dominates the longest runs. The representation result and the end-to-end scalability result should be kept separate.

Nextmap’s lasting contribution is a representation boundary: domain semantics can participate in e-class identity without converting every semantic fact into a rewrite, and retaining those equalities across synthesis stages can be more valuable than optimizing any one stage in isolation.