Improving Equality Saturation for EDA via Semantic E-Graphs
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change
13:40 - 15:20 | |||
13:40 20mTalk | Versioned E-Graphs PLDI Research Papers Jahrim Gabriele Cesario University of St. Gallen, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen DOI | ||
14:00 20mTalk | Improving Equality Saturation for EDA via Semantic E-Graphs PLDI Research Papers Sijie Kong University of California at Santa Barbara, Jingtao Xia University of California at Santa Barbara, Daniel Ruelas-Petrisko University of Washington, Zachary D. Sisco Chinese University of Hong Kong, Jonathan Balkind University of California at Santa Barbara, Gus Henry Smith Southmountain Research DOI | ||
14:20 20mTalk | Equality Saturation for Quantum Circuit Optimization PLDI Research Papers Ganxiang Yang Columbia University, Paige Raun University of Maryland, Runzhou Tao University of Maryland, Ronghui Gu Columbia University; CertiK DOI | ||
14:40 20mTalk | Fungible Memories for Automated Technology Mapping and Retargeting PLDI Research Papers Zachary D. Sisco Chinese University of Hong Kong, Sijie Kong University of California at Santa Barbara, Daniel Ruelas-Petrisko University of Washington, Jingtao Xia University of California at Santa Barbara, Julian Springer TU Berlin, Varun Rao University of California at Berkeley, Spencer Wang University of California at Santa Barbara, Gus Henry Smith Southmountain Research, Ben Hardekopf University of California at Santa Barbara, Jonathan Balkind University of California at Santa Barbara DOI | ||
15:00 20mTalk | Redundant Array Computation Elimination PLDI Research Papers Zixuan Wang Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Liang Yuan Institute of Computing Technology at Chinese Academy of Sciences, Xianmeng Jiang Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Kun Li Institute of Computing Technology at Chinese Academy of Sciences, Junmin Xiao Institute of Computing Technology at Chinese Academy of Sciences, Yunquan Zhang Institute of Computing Technology at Chinese Academy of Sciences DOI | ||