一句话：提出语义 e-graph 与 Nextmap 引擎，以等式饱和跨高层和低层硬件表示优化 EDA，缓解阶段顺序问题。
等式饱和（eqsat）能同时探索多种优化，缓解 EDA 中的阶段顺序问题。已有 EDA 应用多局限于单个工具阶段，难以跨阶段优化，原因是缺少同时适用于高层算术优化与低层逻辑综合的高效硬件表示，并需维护高低层表达式间的语义等价；仅用语法重写效率低下。为此，本文提出语义 e-graph，增强 e-graph 对一类基于语义等价关系的处理性能；并实现 Nextmap，一个基于 eqsat 的硬件优化引擎，用语义 e-graph 桥接高低层硬件表达式。结果表明，Nextmap 可同时运行比先前工作更多的 EDA 阶段，更有效缓解阶段顺序问题并达到此前难以获得的优化，在多种设计上相对开源和商业工具具有竞争力。
Equality saturation (eqsat) is a program optimization technique that uses syntax-based term rewriting to simultaneously explore many possible optimizations of a program, storing equivalent programs efficiently in a data structure called an e-graph. By exploring optimizations simultaneously, eqsat mitigates the phase ordering problem, where the order of optimizations significantly affects quality of results. Eqsat is especially promising for Electronics Design Automation (EDA), whose tools suffer from phase ordering. Previous eqsat-for-EDA efforts have focused on single tool stages; while they demonstrate significant benefits within a stage, they do not address phase ordering between stages. When we investigated the reason for their limited scope, we found that previous works struggle to implement an efficient hardware representation useful in both high-level (e.g. arithmetic optimization) and low-level (e.g. logic synthesis) tasks. The root issue is that such a representation must maintain equivalences between the high- and low-level portions of the language. While these equalities are conceptually simple—e.g., two high-level bitvectors are equal if they contain the same low-level bits—maintaining them using syntax-based rewrites alone proves inefficient in modern eqsat engines. In response, this paper makes two contributions. First, we introduce semantic e-graphs, an enhancement to e-graphs that improves performance of a narrow but highly useful class of semantics-based equalities. Second, we present Nextmap, a new eqsat-based hardware optimization engine whose representation uses semantic e-graphs to efficiently bridge high- and low-level hardware expressions. As a result, Nextmap simultaneously runs more EDA stages than previous eqsat-based works, more effectively mitigating phase ordering and reaching previously inaccessible optimizations. Compared with open-source and commercial tools, Nextmap provides competitive quality of results on a range of designs.
@article{KongXRSBS26,
title = {Improving Equality Saturation for EDA via Semantic E-Graphs},
author = {Sijie Kong and Jingtao Xia and Daniel Ruelas-Petrisko and Zachary D. Sisco and Jonathan Balkind and Gus Henry Smith},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808299}
}