Pith. sign in

REVIEW 5 major objections 5 minor 61 references

HEC: Equivalence Verification Checking for Code Transformation via Equality Saturation

T0 review · 5 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Hybrid e-graph rules verify MLIR rewrites and expose two optimizer bugs

desk verdict Hybrid static/dynamic e-graph rewriting is a real novelty, but the two 'identified' mlir-opt bugs rest on saturation failure rather than a proof of inequality, and the rule conditions are not formalized enough to support the soundness claims. read the letter →

arxiv 2506.02290 v2 pith:D2J4SJ66 submitted 2025-06-02 cs.AR cs.PL

Jiaqi Yin , Zhan Song , Nicolas Bohm Agostini , Antonino Tumeo , Cunxi Yu This is my paper
classification cs.ARcs.PL
keywords equivalencecheckinge-graphequalitysaturationMLIRloopunrollingtilingfusioncompilerbugdetection
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

HEC is a verification tool that checks whether a transformed MLIR program is functionally equivalent to its original by encoding both programs in an e-graph and saturating it with rewriting rules. The paper claims this covers datapath transformations through static algebraic rules and control-flow transformations such as unrolling, tiling, and fusion through rules generated dynamically for each input. On PolyBenchC benchmarks, HEC verifies these transformations in minutes and scales to more than 100,000 lines of MLIR in about 40 minutes. The practical payoff is that HEC caught two real mlir-opt bugs: an unrolling boundary error that executes iterations it should not, and a loop-fusion read-after-write violation that changes program results.

What carries the argument

The e-graph (equivalence graph) is the central object: a compact data structure whose nodes are expressions and whose equivalence classes are closed under congruence, allowing many equivalent program forms to be represented and unified simultaneously. HEC builds this graph from a custom MLIR graph representation that renames variables globally, decomposes each for loop into a loop-value component and an order-sensitive block, and tracks pseudo outputs for stores. The argument is carried by a hybrid ruleset: 62 static datapath rewrite rules, plus dynamic rules produced at runtime for control-flow patterns such as unrolling, tiling, fusion, and coalescing, with pattern conditions discharged by Z3. The machinery turns program equivalence into e-class membership after saturation, because any sequence of sound rewrites that unifies the two programs in one equivalence class witnesses their functional equivalence.

What would settle it

Instantiate Listing 9 and its unrolled Listing 10 with %0 = 5, execute both, and compare HEC's verdict with observed behavior: the original loop runs zero iterations while the unrolled version runs one, so any 'equivalent' verdict from HEC would refute its soundness guarantee.

Watch

Extended reading notes

Core claim

The central claim is that holistic equivalence checking of source-to-source transformations can be reduced to equality saturation over a graph representation of MLIR, provided the rule set is hybrid: static rewrite rules for datapath identities plus dynamic rules synthesized per input for loop transformations. The discovery HEC embodies is that control-flow transformations, normally hard to express as static term rewrites because their parameters and introduced variables are runtime-dependent, can be handled by a rule generator that inspects the input's graph representation, emits code-specific rewriting patterns, and checks the patterns' conditions with the Z3 SMT solver. On this basis, HEC reports functional equivalence when the original and transformed programs end up in the same e-class, and the paper demonstrates this on loop unrolling, tiling, and fusion over PolyBenchC, including nested unrolling. The paper further claims that this verification caught two genuine compiler bugs in mlir-opt: loop boundary errors in unrolling that cause unintended executions, and a loop-fusion read-after-write violation that alters memory state.

Load-bearing premise

The soundness of every loop-transformation verdict rests on the correctness of the dynamic rules in Table 2 and of the Z3 encoding of their conditions; those conditions are stated informally, and one tiling condition in the paper references an undefined variable.

Editorial extensions

If this is right

  • MLIR affine-dialect pass developers can use HEC as a regression oracle, since it checks whole transformations rather than single rewrites.
  • Equivalence checking no longer needs separate tools for control flow and datapath; one saturated e-graph can witness both at once.
  • The reported bugs mean mlir-opt's unrolling can add iterations when the loop start exceeds the end, and its fusion can reorder memory accesses illegally, so users of these default passes should guard those cases.
  • The dynamic-rule design makes the verifier extensible: adding a new loop transformation only requires formalizing its pattern and conditions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The informal dynamic-rule conditions in Table 2 are not a complete formal specification; in particular the tiling condition prints as "n2 = min(%1 + k1, %2)" with %2 undefined, so the soundness guarantee for loop transformations would need a repaired formalization before being relied on.
  • The same saturation machinery could be run in reverse as a synthesis engine: after equivalence is established, extracting the cheapest program from the saturated e-graph would yield an optimization, not just a verification.
  • The unrolling boundary bug suggests a cheap fuzzing strategy for MLIR: generate loops with symbolic bounds where the start can exceed the end and check that unrolled versions execute exactly the same trip count.
  • Since HEC's graph representation automatically normalizes loop-body-independent hoisting, it may already cover invariant-code-motion-style rewrites that the paper does not list as separate patterns.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 5 minor

Summary. The manuscript proposes HEC, an equivalence checking framework for MLIR programs built on equality saturation. It converts input MLIR into a graph representation, constructs an e-graph, and applies a hybrid ruleset: 62 static datapath rewriting rules plus dynamic loop transformation rules generated at runtime for unrolling, tiling, fusion, and coalescing. Equivalence is established when the two program roots are united in one e-class after saturation. The paper evaluates HEC on PolyBenchC kernels, reports runtime and e-class scaling for various unrolling and tiling factors, and presents two case studies where mlir-opt transformations (loop unrolling and loop fusion) change program semantics; the paper claims HEC identified these compiler bugs.

Significance. Assuming the dynamic rules are sound and the graph representation faithfully models memory and control flow, HEC is a promising addition to the verification landscape: it targets MLIR directly, combines datapath and loop-level reasoning, and is evaluated on a nontrivial benchmark set and real mlir-opt failures. The two bug case studies are concrete and likely useful to the MLIR community. The main weaknesses are that the dynamic rule conditions and Z3 encoding are under-specified, the negative-verdict inference from saturation failure is not sound as a proof of inequality, and the memory-ordering semantics are not formalized; these issues directly affect the paper's soundness and bug-detection claims.

major comments (5)
  1. [Section 4.2, Table 2] The tiling pattern's second condition, 'n2 = min(%1 + k1, %2)', is ill-formed because %2 is introduced in the right-hand side as the inner loop induction variable, not as a bound of the transformed loop; as written, the condition cannot be evaluated by Z3 and does not express the usual tiling constraint n2 = min(%1 + k1, n1). Consequently, the manuscript does not contain a precise, checkable specification of the tiling dynamic rule. Please rewrite each condition in Table 2 with all variables explicitly quantified and show the corresponding SMT-LIB encoding, or state that this condition is not enforced and explain how tiling equivalence is checked without it.
  2. [Section 4.2 and Section 4.3] The soundness argument is incomplete. The paper states (Section 4.2) 'we assume that all integrated rewriting rules and transformation patterns are correct' and that Z3 checks whether the input code meets the pattern conditions, but it does not provide a formal semantics for the MLIR affine dialect subset, a definition of what 'k1/k2 times replication' means, or a proof that satisfaction of the pattern conditions implies semantic equivalence for arbitrary loop bodies. In particular, the unrolling and fusion conditions in Table 2 are partly syntactic statements about loop bodies, not arithmetic formulas, so the claim that Z3 verifies the conditions is not substantiated for those parts. Without this formalization, the paper's guarantee that HEC 'will never produce false positives' (Section 4.3) is not established.
  3. [Section 4.3] The negative direction is unsound as stated. The paper says that if saturation terminates with the two programs in different e-classes and no new dynamic rule can be created, 'HEC will conclude that the input MLIR codes are not equivalent.' In an e-graph, a saturation fixpoint only proves that the given rewrite rules cannot prove equivalence; without a completeness theorem or a produced counterexample, this is not a proof of semantic inequality. Section 4.3 itself acknowledges HEC is 'inherently incomplete,' which directly contradicts using saturation failure as a non-equivalence verdict.
  4. [Section 5.4] The two reported mlir-opt bugs are presented as detections by HEC, but the manuscript only shows manual counterexamples. For Case study 1, the counterexample %0 = 5 is not output by HEC; for Case study 2, the linearly increasing memory sequence is derived by the authors' reasoning about the two loops. In both cases, the tool's verdict appears to be a saturation failure or a failed dynamic-rule condition, which, per Major Comment 3, does not prove non-equivalence. To support the statement that 'HEC identified two critical compilation errors,' the paper should either augment HEC with a witness generator that produces a concrete distinguishing input along with the expected and observed outputs, or explicitly reframe the contribution as flagging transformations for human inspection rather than automatically identifying bugs.
  5. [Section 4.1] The paper does not explain how memory side effects are modeled in the e-graph. The graph representation records operation order inside a block, but the e-graph data structure represents expressions modulo congruence and does not natively preserve ordering; affine.store is given a 'pseudo output term' to maintain tracking, but the manuscript does not state how loads and stores are ordered or how read-after-write dependencies are detected when the e-graph runner unifies e-classes. Since Case study 2 in Section 5.4 is a memory-ordering bug, this missing formalization is load-bearing for the tool's ability to detect that bug.
minor comments (5)
  1. [Table 2 heading] The phrase 'interchangable' should be spelled 'interchangeable'.
  2. [Listing 7] The term 'a rit h_ co ns ta nt_ i1 1)' contains stray spaces and is difficult to read; please correct the formatting.
  3. [Section 4.2 and Figure 7] The terms 'pseudo combine node' and 'pseudocombine' are used inconsistently; please choose one spelling and apply it consistently.
  4. [Figure 6] The affine maps #map1 through #map3 are not explained in the caption or the body text; a brief description of how these maps implement nested unrolling by factors 2 and 3 would improve readability.
  5. [Section 5.4] The text says the case studies concern 'optimized HLS programs,' but the transformations in Listings 9-12 are produced by mlir-opt on MLIR kernels, not by an HLS tool; please rephrase to match the experimental setup.

Circularity Check

0 steps flagged · score 0.0 of 10

HEC's verification chain is rule-based but not circular: dynamic rules are input-specific yet their pattern conditions are stated as independent correctness checks, and the paper's negative-verdict unsoundness is a soundness gap, not a circular reduction.

full rationale

I find no circular step that reduces a claimed derivation or prediction to its own inputs. The dynamic rewriting rules in Table 2 are generated per input pair, but their application is gated by explicitly stated conditions (e.g., iteration-space equality, loop-body replication, memory-RAW absence), which the paper treats as independent correctness criteria checked with Z3. If those conditions are correct, matching them legitimately establishes equivalence; if they are incorrect or under-specified (the tiling condition contains an undefined '%2'), that is a correctness risk, not circularity. Static datapath rules come from standard algebraic identities. The graph representation unifies loop hoisting by dataflow equivalence, which is a defensible design choice rather than a renamed prediction. Self-citations to the authors' earlier e-graph work appear only as background and are not load-bearing. The paper's own incompleteness caveat does reveal an unsound inference in the negative direction: 'cannot determine equivalence' plus 'no new rules' is treated as a proof of non-equivalence, and the two bug reports rely on that inference. However, that is a soundness gap (absence of evidence treated as evidence of absence), not a by-construction circularity; the manual counterexamples supplied in Section 5.4 are independent evidence, and the bug-detection claim would need a witness or certificate to be fully justified. For this pass, the derivation chain is not circular.

Assumptions & free parameters 0 free parameters · 5 assumptions · 1 invented entities

The central claim rests on the soundness of the dynamic transformation patterns, the fidelity of the MLIR graph representation, and the behavior of concluding non-equivalence from saturation failure. None of these are independently machine-checked or shipped as an artifact.

assumptions (5)
  • standard math The e-graph operations and equality saturation implemented by the egg library are sound for the term rewriting performed.
    Background Section 3.3 relies on congruence closure from Nelson and Oppen and egg; standard result, but HEC's encoding of MLIR into e-graph terms is not formalized.
  • domain assumption The graph representation in Section 4.1 faithfully captures the semantics of the supported MLIR affine subset, including loop bounds, block ordering, and memory operations.
    If the representation misses memory dependence or scope information, equivalence verdicts can be wrong. Section 4.1 describes renaming and pseudo outputs but no formal semantics.
  • ad hoc to paper The dynamic transformation patterns in Table 2 are mathematically correct and their Z3 checks fully encode the conditions.
    Introduced by the authors without derivation. The paper asserts Z3 verification, but the printed conditions are informal and the tiling condition contains an undefined %2.
  • domain assumption The 62 static datapath rewriting rules are sound algebraic identities for all signedness and bitwidth cases they are applied to.
    Table 1 lists a few rules; the full rule set is not enumerated or proven, so correctness depends on the unlisted remainder.
  • ad hoc to paper When the e-graph runner cannot prove equivalence and no new dynamic rule can be generated, the input programs are reported as non-equivalent.
    Section 4.3 states this. It is not a valid proof of non-equivalence; the paper itself notes incompleteness, so this conclusion can be a false alarm. The bug reports in Section 5.4 rely on this behavior plus manual analysis.
invented entities (1)
  • Pseudo combine node
    purpose: Binds multiple candidate loop operations into one parent e-node so dynamic rules can merge their e-classes during multi-step verification.
    Section 4.3 and Figure 7 introduce pseudocombine nodes. They are an internal graph construction with no external falsifiable handle, and their semantics are not formally specified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of HEC: Equivalence Verification Checking for Code Transformation via Equality Saturation." pith.science (2026). https://pith.science/paper/D2J4SJ66

@misc{pith2026250602290,
  author       = {Pith},
  title        = {Pith review of: HEC: Equivalence Verification Checking for Code Transformation via Equality Saturation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/D2J4SJ66}},
  note         = {Machine review of arXiv:2506.02290}
}
read the original abstract

In modern computing systems, compilation employs numerous optimization techniques to enhance code performance. Source-to-source code transformations, which include control flow and datapath transformations, have been widely used in High-Level Synthesis (HLS) and compiler optimization. While researchers actively investigate methods to improve performance with source-to-source code transformations, they often overlook the significance of verifying their correctness. Current tools cannot provide a holistic verification of these transformations. This paper introduces HEC, a framework for equivalence checking that leverages the e-graph data structure to comprehensively verify functional equivalence between programs. HEC utilizes the MLIR as its frontend and integrates MLIR into the e-graph framework. Through the combination of dynamic and static e-graph rewriting, HEC facilitates the validation of comprehensive code transformations. We demonstrate effectiveness of HEC on PolyBenchC benchmarks, successfully verifying loop unrolling, tiling, and fusion transformations. HEC processes over 100,000 lines of MLIR code in 40 minutes with predictable runtime scaling. Importantly, HEC identified two critical compilation errors in mlir-opt: loop boundary check errors causing unintended executions during unrolling, and memory read-after-write violations in loop fusion that alter program semantics. These findings demonstrate HEC practical value in detecting real-world compiler bugs and highlight the importance of formal verification in optimization pipelines.

Figures

Figures reproduced from arXiv: 2506.02290 by the authors.

Figure 1
Figure 1. Variants B, C, and D achieve equivalence with the baseline (Listing [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. Overview of the HEC Framework: Initially, the input MLIR code is converted into a graph-based representation through dataflow analysis (step ⃝1 ). This graph representa￾tion serves as a foundation for constructing the e-graph. The dynamic rules (step ⃝2 ) are specifically designed to handle complex loop transformations that are not suitable for static rewriting. Finally, the e-graph runner (step ⃝3 ) employs a hy￾br… view at source ↗
Figure 2
Figure 2. The e-graph rewriting for the expression [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: The dataflow graph for Listing 1 Task 2 – The second challenge involves accurately repre￾senting for loop constructs within our graph representation. To address this, we decompose each for loop into two primary components: a loopvalue component and a block operation. A…
Figure 5
Figure 5. Figure 5: Loop unrolling transformation pattern: the code [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: MLIR Nested Unrolling Case Study: The bottom [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: E-graph verification for the motivating example provided in Figure [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 8
Figure 8. Figure 8: Heatmap of Runtime for Different Nested Unrolling Configurations. The x-axis and y-axis represent the unrolling [PITH_FULL_IMAGE:figures/full_fig_p010_8.png]
Figure 9
Figure 9. Figure 9: Runtime and e-graph complexity w.r.t nested unrolling complexity under the same unrolling factors. [PITH_FULL_IMAGE:figures/full_fig_p012_9.png]
Figure 10
Figure 10. Figure 10: Runtime and e-nodes number for HEC across repre￾sentative problem sizes ranging from 15,000 to 90,000 LOC. HEC is designed to manage both static and dynamic trans￾formations. In this section, we focus on the datapath trans￾formation capabilities of HEC. Specifically, …

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

61 extracted references · 59 canonical work pages

  1. [1]

    IREE, September 2019

    work page 2019

  2. [2]

    https://repo.or.cz/w/isa.git, 2024

    ISA. https://repo.or.cz/w/isa.git, 2024

    work page 2024

  3. [3]

    Soda-opt an mlir based flow for co-design and high-level synthesis

    Nicolas Bohm Agostini, Serena Curzel, David Kaeli, and Antonino Tumeo. Soda-opt an mlir based flow for co-design and high-level synthesis. In Proceedings of the 19th ACM International Conference on Computing Frontiers, pages 201–202, 2022

    work page 2022

  4. [4]

    Rewrite-based equational theorem proving with selection and simpli- fication

    Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simpli- fication. Journal of Logic and Computation, 4(3):217– 247, 1994

    work page 1994

  5. [5]

    Equational rea- soning in saturation-based theorem proving

    Leo Bachmair and Harald Ganzinger. Equational rea- soning in saturation-based theorem proving. Automated deduction—a basis for applications, 1:353–397, 1998

    work page 1998

  6. [6]

    Smt-based trans- lation validation for machine learning compiler

    Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, and Juneyoung Lee. Smt-based trans- lation validation for machine learning compiler. In In- ternational Conference on Computer Aided Verification, pages 386–407. Springer, 2022

    work page 2022

  7. [7]

    Polycheck: Dynamic verification of iteration space transformations on affine programs

    Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, and Ponnuswamy Sadayap- pan. Polycheck: Dynamic verification of iteration space transformations on affine programs. ACM SIGPLAN Notices, 51(1):539–554, 2016

    work page 2016

  8. [8]

    Bab- ble: Learning better abstractions with e-graphs and anti- unification

    David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova. Bab- ble: Learning better abstractions with e-graphs and anti- unification. Proceedings of the ACM on Programming Languages, 7(POPL):396–424, 2023

    work page 2023

Show all 61 references
  1. [9]

    E-morphic: Scalable equality saturation for structural exploration in logic˜ synthesis

    Chen Chen, Guangyu HU, Cunxi Yu, Yuzhe Ma, and Hongce Zhang. E-morphic: Scalable equality saturation for structural exploration in logic˜ synthesis. Design Automation Conference (DAC), 2025

    2025

  2. [10]

    E-syn: E-graph rewriting with technology-aware cost functions for logic synthesis

    Chen Chen, Guangyu Hu, Dongsheng Zuo, Cunxi Yu, Yuzhe Ma, and Hongce Zhang. E-syn: E-graph rewriting with technology-aware cost functions for logic synthesis. pages 1–6, 2024

    2024

  3. [11]

    Seer: Super-optimization explorer for hls using e-graph rewriting with mlir

    Jianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho, and Theo Drane. Seer: Super-optimization explorer for hls using e-graph rewriting with mlir. arXiv preprint arXiv:2308.07654, 2023

    2023 arXiv

  4. [12]

    Seer: Super-optimization explorer for high-level synthesis using e-graph rewriting

    Jianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho, and Theo Drane. Seer: Super-optimization explorer for high-level synthesis using e-graph rewriting. In Proceedings of the 29th ACM International Confer- ence on Architectural Support for Programming Lan- guages and...

    2024

  5. [13]

    Circuit ir compilers and tools (CIRCT)., 2024

    2024

  6. [14]

    Fpga hls today: successes, challenges, and opportunities

    Jason Cong, Jason Lau, Gai Liu, Stephen Neuendorffer, Peichen Pan, Kees Vissers, and Zhiru Zhang. Fpga hls today: successes, challenges, and opportunities. ACM Transactions on Reconfigurable Technology and Systems (TRETS), 15(4):1–42, 2022

    2022

  7. [15]

    High-level synthesis for fpgas: From prototyping to deployment

    Jason Cong, Bin Liu, Stephen Neuendorffer, Juanjo Noguera, Kees Vissers, and Zhiru Zhang. High-level synthesis for fpgas: From prototyping to deployment. IEEE Transactions on Computer-Aided Design of Inte- grated Circuits and Systems, 30(4):473–491, 2011

    2011

  8. [16]

    Automatic datapath optimization using e-graphs

    Samuel Coward, George A Constantinides, and Theo Drane. Automatic datapath optimization using e-graphs. In 2022 IEEE 29th Symposium on Computer Arithmetic (ARITH), pages 43–50. IEEE, 2022

    2022

  9. [17]

    Automating constraint-aware datapath optimiza- tion using e-graphs

    Samuel Coward, George A Constantinides, and Theo Drane. Automating constraint-aware datapath optimiza- tion using e-graphs. In 2023 60th ACM/IEEE Design Automation Conference (DAC), pages 1–6. IEEE, 2023

    2023

  10. [18]

    Datapath verifica- tion via word-level e-graph rewriting

    Samuel Coward, Emiliano Morini, Bryan Tan, Theo Drane, and George A Constantinides. Datapath verifica- tion via word-level e-graph rewriting. In 2023 Formal Methods in Computer-Aided Design (FMCAD), pages 92–100. IEEE, 2023

    2023

  11. [19]

    Dmazerunner: Exe- cuting perfectly nested loops on dataflow accelerators

    Shail Dave, Youngbin Kim, Sasikanth Avancha, Kyoung- woo Lee, and Aviral Shrivastava. Dmazerunner: Exe- cuting perfectly nested loops on dataflow accelerators. ACM Transactions on Embedded Computing Systems (TECS), 18(5s):1–27, 2019

    2019

  12. [20]

    Efficient e-matching for smt solvers

    Leonardo De Moura and Nikolaj Bjørner. Efficient e-matching for smt solvers. In Automated Deduction– CADE-21: 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceed- ings 21, pages 183–198. Springer, 2007

    2007

  13. [21]

    Z3: An effi- cient smt solver

    Leonardo De Moura and Nikolaj Bjørner. Z3: An effi- cient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008

    2008

  14. [22]

    A taste of rewrite systems

    Nachum Dershowitz. A taste of rewrite systems. Func- tional Programming, Concurrency, Simulation and Au- tomated Reasoning: International Lecture Series 1991– 1992 McMaster University, Hamilton, Ontario, Canada, pages 199–228, 2005

    1991

  15. [23]

    Sim- plify: a theorem prover for program checking

    David Detlefs, Greg Nelson, and James B Saxe. Sim- plify: a theorem prover for program checking. Journal of the ACM (JACM), 52(3):365–473, 2005

    2005

  16. [24]

    Taso: optimizing deep learning computation with automatic generation of graph substitutions

    Zhihao Jia, Oded Padon, James Thomas, Todd Warsza- wski, Matei Zaharia, and Alex Aiken. Taso: optimizing deep learning computation with automatic generation of graph substitutions. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, pages 47– 62, 2019

    2019

  17. [25]

    Verification of loop and arithmetic transformations of array-intensive behaviors

    Chandan Karfa, Kunal Banerjee, Dipankar Sarkar, and Chittaranjan Mandal. Verification of loop and arithmetic transformations of array-intensive behaviors. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(11):1787–1800, 2013

    2013

  18. [26]

    Heterocl: A multi-paradigm programming infrastructure for software-defined reconfigurable computing

    Yi-Hsiang Lai, Yuze Chi, Yuwei Hu, Jie Wang, Cody Hao Yu, Yuan Zhou, Jason Cong, and Zhiru Zhang. Heterocl: A multi-paradigm programming infrastructure for software-defined reconfigurable computing. In Pro- ceedings of the 2019 ACM/SIGDA International Sympo- sium on Field-Prog...

    2019

  19. [27]

    Programming and synthesis for software-defined fpga acceleration: sta- tus and future prospects

    Yi-Hsiang Lai, Ecenur Ustun, Shaojie Xiang, Zhenman Fang, Hongbo Rong, and Zhiru Zhang. Programming and synthesis for software-defined fpga acceleration: sta- tus and future prospects. ACM Transactions on Recon- figurable Technology and Systems (TRETS), 14(4):1–39, 2021

    2021

  20. [28]

    LLVM: A compilation framework for lifelong program analysis & transforma- tion

    Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transforma- tion. In International symposium on code generation and optimization, 2004. CGO 2004., pages 75–86. IEEE, 2004

    2004

  21. [29]

    Mlir: Scaling compiler infrastructure for do- main specific computation

    Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Ta- tiana Shpeisman, Nicolas Vasilache, and Oleksandr Zi- nenko. Mlir: Scaling compiler infrastructure for do- main specific computation. In 2021 IEEE/ACM Inter- national Symp...

    2021

  22. [30]

    Formal verification of a realistic compiler

    Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009

    2009

  23. [31]

    Compcert-a formally verified optimizing compiler

    Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bern- hard Schommer, Markus Pister, and Christian Ferdinand. Compcert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016

    2016

  24. [32]

    An overview of the production quality compiler-compiler project

    Bruce W Leverett, Roderic Geoffrey Galton Cattell, Steven O Hobbs, Joseph M Newcomer, Andrew Henry Reiner, Bruce R Schatz, and William A Wulf. An overview of the production quality compiler-compiler project. Computer, 13(8):38–49, 1980

    1980

  25. [33]

    Alive2: bounded translation validation for llvm

    Nuno P Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. Alive2: bounded translation validation for llvm. In Proceedings of the 42nd ACM SIGPLAN International Conference on Pro- gramming Language Design and Implementation, pages 65–79, 2021

    2021

  26. [34]

    Provably correct peephole optimiza- tions with alive

    Nuno P Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Provably correct peephole optimiza- tions with alive. In Proceedings of the 36th ACM SIG- PLAN Conference on Programming Language Design and Implementation, pages 22–32, 2015

    2015

  27. [35]

    Polygeist: Raising c to polyhedral mlir

    William S Moses, Lorenzo Chelini, Ruizhe Zhao, and Oleksandr Zinenko. Polygeist: Raising c to polyhedral mlir. In 2021 30th International Conference on Paral- lel Architectures and Compilation Techniques (PACT), pages 45–59. IEEE, 2021

    2021

  28. [36]

    Techniques for program verifi- cation

    Charles Gregory Nelson. Techniques for program verifi- cation. Stanford University, 1980

    1980

  29. [37]

    Fast decision proce- dures based on congruence closure

    Greg Nelson and Derek C Oppen. Fast decision proce- dures based on congruence closure. Journal of the ACM (JACM), 27(2):356–364, 1980

    1980

  30. [38]

    Proof- producing congruence closure

    Robert Nieuwenhuis and Albert Oliveras. Proof- producing congruence closure. In International Confer- ence on Rewriting Techniques and Applications, pages 453–468. Springer, 2005

    2005

  31. [39]

    Automatically improving accuracy for floating point expressions

    Pavel Panchekha, Alex Sanchez-Stern, James R Wilcox, and Zachary Tatlock. Automatically improving accuracy for floating point expressions. Acm Sigplan Notices , 50(6):1–11, 2015

    2015

  32. [40]

    Polybench: The poly- hedral benchmark suite

    Louis-Noël Pouchet et al. Polybench: The poly- hedral benchmark suite. https://github.com/ MatthiasJReisinger/PolyBenchC-4.2.1, 437:1–1, 2012

    2012

  33. [41]

    Formal verification of source-to-source transformations for hls

    Louis-Noël Pouchet, Emily Tucker, Niansong Zhang, Hongzheng Chen, Debjit Pal, Gabriel Rodríguez, and Zhiru Zhang. Formal verification of source-to-source transformations for hls. In Proceedings of the 2024 ACM/SIGDA International Symposium on Field Pro- grammable Gate Arrays, ...

    2024

  34. [42]

    Halide: a language and compiler for optimiz- ing parallelism, locality, and recomputation in image processing pipelines

    Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, and Saman Ama- rasinghe. Halide: a language and compiler for optimiz- ing parallelism, locality, and recomputation in image processing pipelines. Acm Sigplan Notices, 48(6):519– 530, 2013

    2013

  35. [43]

    Verification of source code transfor- mations by program equivalence checking

    KC Shashidhar, Maurice Bruynooghe, Francky Catthoor, and Gerda Janssens. Verification of source code transfor- mations by program equivalence checking. In Compiler Construction: 14th International Conference, CC 2005, Held as Part of the Joint European Conferences on The- ory ...

    2005

  36. [44]

    Pure tensor program rewrit- ing via access patterns (representation pearl)

    Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael Taylor, Luis Ceze, and Zachary Tatlock. Pure tensor program rewrit- ing via access patterns (representation pearl). In Pro- ceedings of the 5th ACM SIGPLAN International Sympo- sium on Mac...

    2021

  37. [45]

    Autodse: Enabling software programmers to design efficient fpga accelerators

    Atefeh Sohrabizadeh, Cody Hao Yu, Min Gao, and Jason Cong. Autodse: Enabling software programmers to design efficient fpga accelerators. ACM Transactions on Design Automation of Electronic Systems (TODAES), 27(4):1–27, 2022

    2022

  38. [46]

    Equality saturation: a new approach to optimiza- tion

    Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: a new approach to optimiza- tion. In Proceedings of the 36th annual ACM SIGPLAN- SIGACT symposium on Principles of programming lan- guages, pages 264–276, 2009

    2009

  39. [47]

    Triton: an intermediate language and compiler for tiled neural network computations

    Philippe Tillet, Hsiang-Tsung Kung, and David Cox. Triton: an intermediate language and compiler for tiled neural network computations. In Proceedings of the 3rd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pages 10–19, 2019

    2019

  40. [48]

    Impress: Large integer multiplication expres- sion rewriting for fpga hls

    Ecenur Ustun, Ismail San, Jiaqi Yin, Cunxi Yu, and Zhiru Zhang. Impress: Large integer multiplication expres- sion rewriting for fpga hls. In 2022 IEEE 30th Annual International Symposium on Field-Programmable Cus- tom Computing Machines (FCCM), pages 1–10. IEEE, 2022

    2022

  41. [49]

    Equality saturation for datapath synthesis: A pathway to pareto optimality

    Ecenur Ustun, Cunxi Yu, and Zhiru Zhang. Equality saturation for datapath synthesis: A pathway to pareto optimality. In 2023 60th ACM/IEEE Design Automation Conference (DAC), pages 1–2. IEEE, 2023

    2023

  42. [50]

    Polybench-nn

    Hrishikesh Vaidya, Akilesh B, Abhishek Patwardhan, and Ramakrishna Upadrasta. Polybench-nn. https:// github.com/IITH-Compilers/PolyBench-NN, 2018

    2018

  43. [51]

    Vectorization for dig- ital signal processors via equality saturation

    Alexa VanHattum, Rachit Nigam, Vincent T Lee, James Bornholt, and Adrian Sampson. Vectorization for dig- ital signal processors via equality saturation. In Pro- ceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating S...

    2021

  44. [52]

    Equivalence checking of static affine pro- grams using widening to handle recurrences

    Sven Verdoolaege, Gerda Janssens, and Maurice Bruynooghe. Equivalence checking of static affine pro- grams using widening to handle recurrences. ACM Transactions on Programming Languages and Systems (TOPLAS), 34(3):1–35, 2012

    2012

  45. [53]

    Egg: Fast and extensible equality saturation

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. Egg: Fast and extensible equality saturation. Proceedings of the ACM on Programming Languages, 5(POPL):1–29, 2021

    2021

  46. [54]

    Rewriting history: Repurposing domain- specific cgras

    Jackson Woodruff, Thomas Koehler, Alexander Brauck- mann, Chris Cummins, Sam Ainsworth, and Michael FP O’Boyle. Rewriting history: Repurposing domain- specific cgras. arXiv preprint arXiv:2309.09112, 2023

    2023 arXiv

  47. [55]

    Ironman: Gnn- assisted design space exploration in high-level synthesis via reinforcement learning

    Nan Wu, Yuan Xie, and Cong Hao. Ironman: Gnn- assisted design space exploration in high-level synthesis via reinforcement learning. In Proceedings of the 2021 on Great Lakes Symposium on VLSI, pages 39–44, 2021

    2021

  48. [56]

    Equal- ity saturation for tensor graph superoptimization

    Yichen Yang, Phitchaya Phothilimthana, Yisu Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. Equal- ity saturation for tensor graph superoptimization. Pro- ceedings of Machine Learning and Systems, 3:255–268, 2021

    2021

  49. [57]

    Scalehls: A new scalable high-level synthesis framework on multi-level intermediate representation

    Hanchen Ye, Cong Hao, Jianyi Cheng, Hyunmin Jeong, Jack Huang, Stephen Neuendorffer, and Deming Chen. Scalehls: A new scalable high-level synthesis framework on multi-level intermediate representation. In 2022 IEEE International Symposium on High-Performance Computer Architect...

    2022

  50. [58]

    Boole: Exact symbolic reasoning via boolean equal- ity saturation

    Jiaqi Yin, Zhan Song, Chen Chen, Qihao Hu, and Cunxi Yu. Boole: Exact symbolic reasoning via boolean equal- ity saturation. Design Automation Conference (DAC), 2025

    2025

  51. [59]

    Advanced datapath synthesis using graph isomorphism

    Cunxi Yu, Mihir Choudhury, Andrew Sullivan, and Ma- ciej Ciesielski. Advanced datapath synthesis using graph isomorphism. In 2017 IEEE/ACM International Confer- ence on Computer-Aided Design (ICCAD), pages 424–

    2017

  52. [60]

    Better together: Unifying datalog and equality saturation

    Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. Better together: Unifying datalog and equality saturation. Proc. ACM Program. Lang., 7(PLDI), jun 2023

    2023

  53. [61]

    Polsca: Polyhedral high-level synthesis with compiler transformations

    Ruizhe Zhao, Jianyi Cheng, Wayne Luk, and George A Constantinides. Polsca: Polyhedral high-level synthesis with compiler transformations. In 2022 32nd Interna- tional Conference on Field-Programmable Logic and Applications (FPL), pages 235–242. IEEE, 2022

    2022

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.