REVIEW 3 major objections 5 minor 25 references
Scaling Program Synthesis Based Technology Mapping with Equality Saturation
T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash
Pith's one-line read Churchroad, a new technology mapper, combines equality saturation with the Lakeroad synthesizer to compile a two-DSP design that Lakeroad alone cannot handle, without any user-provided sketch.
desk verdict Neat eqsat-plus-synthesis combination on one compelling example; the unverified rewrite rules and single-example evaluation keep it a prototype, but it deserves reviewer time. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the e-graph built by the egglog equality-saturation framework, a data structure that stores all equivalent expressions from applying rewrite rules as nodes in shared equivalence classes. Churchroad uses egglog rules in two ways: rewrite rules that encode known arithmetic identities (such as the partial-product decomposition of a multiply) to expand the spec, and DSP proposal rules that mark eclasses as potentially implementable by a DSP. The DSP? proposal nodes become the interface to Lakeroad: each one becomes a generated sketch, and the eclass's expression becomes the generated spec for a small synthesis query. The query decomposition is what keeps the underlying SMT solvers tractable, because multiplication only appears at small bitwidths in each subquery.
What would settle it
Check the rewrite rule from equation (4) at a bitwidth outside the demonstrated range, for example a 17-bit by 31-bit multiply, with a small bounded exhaustive search or an SMT query; if any operand pair violates the equality, Churchroad can emit a wrong design even when every Lakeroad subquery is correct.
Extended reading notes
Core claim
The central claim is that a program-synthesis-based technology mapper like Lakeroad can be treated as a specialized subroutine whose queries are orchestrated by an equality-saturation engine. Churchroad pre-applies arithmetic equalities, such as the identity that splits a wide product into shifted partial products, to rewrite the specification into a form where each subexpression is small enough for an SMT solver to verify. The e-graph also supplies the sketch: DSP proposal rules insert 'DSP?' nodes that mark eclasses as candidates, and Churchroad generates both the spec and the sketch for each candidate directly from e-graph contents. The paper demonstrates this on a 16 x 32 multiplier, where a single two-DSP Lakeroad query times out but the decomposed Churchroad queries each return a DSP48E2 configuration, yielding a complete mapping that Lakeroad could not produce.
Load-bearing premise
The hand-written rewrite rules, such as the partial-product equality in equation (4), are sound and preserve semantics for every bitwidth they match.
Editorial extensions
If this is right
- Churchroad compiles multi-DSP designs that a single Lakeroad query times out on, without any hand-written sketch.
- Users no longer need to know Lakeroad's sketching DSL or the target primitive's internals to map a design.
- Breaking a synthesis query into pieces changes the scaling behavior: SMT solvers only need to handle small-bitwidth multiplication.
- The combination suggests a general pattern: equality saturation as an orchestrator for specialized, high-powered synthesis subroutines.
Reading between the lines
- The paper's evidence is one design; whether Churchroad's decomposition scales to arbitrary graphs of multiply-add-shift operations remains untested.
- The hand-written rewrite-rule database is likely the next bottleneck; automatically generating and proving these equalities would make the approach more robust, and the paper names this as future work.
- The e-graph-generated sketches are only as good as the DSP proposal rules, so extending Churchroad to other primitives would apparently require writing new proposal rules for each.
- Churchroad's four-second compile on the example suggests the eqsat overhead is modest, so the practical limit on larger designs will be e-graph growth and the number of Lakeroad queries.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper presents Churchroad, a technology mapper that combines equality saturation (via the egglog framework) with the existing sketch-guided synthesis tool Lakeroad. The core idea is to use semantics-preserving rewrite rules to decompose a large design in an e-graph, then use DSP proposal rules to identify subexpressions that may be implementable on Xilinx UltraScale+ DSP48E2 primitives, and finally call Lakeroad only on those smaller subexpressions. By doing so, the paper argues, Churchroad both avoids the user burden of providing sketches and mitigates the SMT scalability problems that arise when Lakeroad is asked to map a multi-DSP design monolithically. The approach is demonstrated end-to-end on a 16-bit x 32-bit unsigned multiplier that is mapped to two DSP48E2 blocks, with Churchroad reportedly taking about 4 seconds to compile the design whereas a single Lakeroad query on the full design times out.
Significance. The composition of equality saturation with a synthesis-based mapper is a sensible and potentially valuable architecture: it replaces a monolithic SMT query by several smaller queries and automatically generates the sketch from the e-graph. The paper also contains a concrete, reproducible demonstration of the SMT bit-blasting wall for multiplication (Fig. 1), and the implementation is open source. However, the current evidence is limited to a single end-to-end example, and the rewrite rules that are load-bearing for correctness are introduced as axioms rather than verified; the paper itself lists automatic rule generation as future work. If the rules and the evaluation are strengthened, the approach could be a meaningful step toward practical synthesis-based technology mapping for complex FPGA primitives.
major comments (3)
- [Section II, eq. (4) and the egglog rewrite rule] The correctness of every design emitted by Churchroad depends on the rewrite rules being semantics-preserving for all matched bitwidths. The paper states that Churchroad 'pre-applies equalities we know to be true' and encodes eq. (4) as an axiom in egglog, but it does not provide a proof of the variable-bitwidth generalization that the text claims (the displayed rule is hardcoded to 16- and 32-bit arguments), nor does it enumerate or validate the rest of the rule database. Section IV explicitly lists 'generating correct rewrite rules... rather than writing them manually' as future work, which confirms that the current rules are manual and unverified. Since an unsound rule would union the spec with an incorrect expansion while every Lakeroad subquery could still succeed on the smaller generated specs, this is a load-bearing correctness gap for a technology mapper. Please add a machine-checked or SMT-verified correctness argument for the rule set, or at minimum provide a formal statement and proof for the variable-bitwidth form of eq. (4).
- [Sections I, II, and IV (evaluation evidence)] The paper's central claim is that Churchroad 'handles larger and more complex designs than the program-synthesis-based tool alone,' but the only end-to-end demonstration is the single 16x32 multiplier example in Section II. There is no benchmark suite, no comparison against other mappers (e.g., Yosys or Lakeroad without Churchroad), and no scaling study of Churchroad itself; Figure 1 measures only the underlying SMT solvers' timeout on a monolithic proof of eq. (4), not Churchroad's own behavior across designs. Section IV appropriately calls the work 'early evidence,' but the abstract and introduction state the broader claim as a result. Please either expand the evaluation to several designs with varying bitwidths and DSP patterns, or adjust the claims to describe a proof-of-concept case study.
- [Section II, DSP proposal rules] The DSP proposal rules use hardcoded thresholds (e.g., 'bw e <= 48', 'bw arg0 <= 17', 'bw arg1 <= 17', and a similar rule for multiply-add) that are asserted to identify expressions implementable on UltraScale+ DSP48E2 blocks, but the paper does not justify these thresholds or report their precision and recall. An overly permissive proposal is harmless because Lakeroad will reject invalid mappings, but an overly restrictive proposal silently loses mapping opportunities, which undermines the claim of more optimal mappings. Please document the source of these thresholds and, if possible, evaluate the proposal rules against a set of known DSP-legal and DSP-illegal expressions to demonstrate that they do not systematically exclude feasible mappings.
minor comments (5)
- [Section II, e-graph figures] The e-graph figures are difficult to read in the PDF; the dotted eclass boxes are not consistently labeled with the numbers used in the text (e.g., 'eclass labeled 1' and 'eclass labeled 2' are mentioned after the figures are introduced). Please add explicit labels or captions that tie the figures to the prose.
- [Section II, notation] The notation 'b = b1 + + b0' is used without definition; please define it explicitly as concatenation (or use a standard symbol such as '::' or '||') and keep it consistent with the later use of '++' in eqs. (1) and (2).
- [Section II, runtime claim] The sentence 'Churchroad currently takes about 4 seconds to compile this example' lacks experimental context; please report the machine, operating system, and versions of egglog, Rosette, and the SMT solvers used.
- [Section II, text] There is a grammatical error in the sentence 'egglog rules takes two arguments'; it should be 'egglog rules take two arguments.'
- [Section III, references] References [23] and [24] are cited in a way that suggests they are companion tools or techniques for using axioms to simplify SMT queries, but the exact relationship to Churchroad is not made clear; please expand the related-work discussion to explain how Haploid and Dafny's axiom support differ from Churchroad's use of rewrite rules.
Circularity Check
No significant circularity: Churchroad's derivation is self-contained; hand-written rewrite rules are an acknowledged correctness risk, not a circular input.
full rationale
The paper's derivation chain is transparent: (1) a spec is given; (2) Churchroad applies an explicitly stated arithmetic equality (eq. (4)) as an egglog rule, unioning the spec's Mul node with a two-DSP decomposition; (3) DSP-proposal rules mark eclasses and Lakeroad is invoked as a subroutine; (4) Lakeroad's SMT-backed queries verify each DSP configuration; (5) the final design is extracted from the e-graph. No step reduces to a fitted parameter, a self-definition, or a renamed empirical pattern. The equality in eq. (4) is a true unsigned truncated-multiplication identity, not an empirical fit, and the concrete DSP parameters are produced and verified by Lakeroad's independent synthesis queries. Lakeroad is prior work by the same group, but it was peer-reviewed and externally evaluated (ASPLOS '24), so citing it is not load-bearing circularity. The only substantive caveats are limitations, not circularity: the rewrite rules are manual axioms, so their soundness is an unverified assumption, and the paper itself says in Section IV, 'We also plan to generate correct rewrite rules for Churchroad, rather than writing them manually.' Likewise, the 'no sketches' claim is somewhat generous because the structural decomposition is encoded in the manually written rule database, but the paper openly acknowledges the manual-rule limitation and the example is a legitimate deductive demonstration from a stated axiom. No self-citation chain forces the result, and no uniqueness theorem is imported from the authors.
Assumptions & free parameters
assumptions (5)
- domain assumption The equality a*b = concat((a*b1 + (a*b0)>>16)[15:0], (a*b0)[15:0]) for 16-bit by 32-bit unsigned multiplication is true in general and is sound as an e-graph rewrite rule.
- standard math The egglog equality saturation computation preserves the semantics of the design through unions.
- ad hoc to paper The DSP proposal patterns (e.g., bitwidth <= 48 and <=17 for operands) correctly identify expressions implementable on UltraScale+ DSP48E2 blocks.
- domain assumption Lakeroad's synthesis subqueries are sound, i.e., a returned DSP configuration is equivalent to the eclass spec.
- domain assumption Extracting a legal structural Verilog node from each eclass preserves the semantics of the design.
Cite this review
Pith. "Pith review of Scaling Program Synthesis Based Technology Mapping with Equality Saturation." pith.science (2026). https://pith.science/paper/RE2IKUWA
@misc{pith2026241111036,
author = {Pith},
title = {Pith review of: Scaling Program Synthesis Based Technology Mapping with Equality Saturation},
year = {2026},
howpublished = {\url{https://pith.science/paper/RE2IKUWA}},
note = {Machine review of arXiv:2411.11036}
}
read the original abstract
State-of-the-art hardware compilers for FPGAs often fail to find efficient mappings of high-level designs to low-level primitives, especially complex programmable primitives like digital signal processors (DSPs). New approaches apply sketch-guided program synthesis to more optimally map designs. However, this approach has two primary drawbacks. First, sketch-guided program synthesis requires the user to provide sketches, which are challenging to write and require domain expertise. Second, the open-source SMT solvers which power sketch-guided program synthesis struggle with the sorts of operations common in hardware -- namely multiplication. In this paper, we address both of these challenges using an equality saturation (eqsat) framework. By combining eqsat and an existing state-of-the-art program-synthesis-based tool, we produce Churchroad, a technology mapper which handles larger and more complex designs than the program-synthesis-based tool alone, while eliminating the need for a user to provide sketches.
Figures
Reference graph
Works this paper leans on
-
[1]
Yosys-a free verilog synthesis suite,
C. Wolf, J. Glaser, and J. Kepler, “Yosys-a free verilog synthesis suite,” in Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip), vol. 97, 2013
2013
-
[2]
Fpga technology mapping using sketch-guided program synthesis,
G. H. Smith, B. Kushigian, V . Canumalla, A. Cheung, S. Lyubomirsky, S. Porncharoenwase, R. Just, G. L. Bernstein, and Z. Tatlock, “Fpga technology mapping using sketch-guided program synthesis,” in Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 , ser. ASPLOS ’24. New...
arXiv 2024
-
[3]
Program synthesis by sketching,
A. Solar-Lezama, “Program synthesis by sketching,” Ph.D. dissertation, USA, 2008, aAI3353225
work page 2008
-
[4]
Further steps down the wrong path : Improving the bit- blasting of multiplication,
M. Brain, “Further steps down the wrong path : Improving the bit- blasting of multiplication,” in SMT’21: 19th International Workshop on Satisfiability Modulo Theories , 2021
work page 2021
-
[5]
egg: Fast and extensible equality saturation,
M. Willsey, C. Nandi, Y . R. Wang, O. Flatt, Z. Tatlock, and P. Panchekha, “egg: Fast and extensible equality saturation,” Proc. ACM Program. Lang., vol. 5, no. POPL, jan 2021. [Online]. Available: https://doi.org/10.1145/3434304
doi:10.1145/3434304 2021
-
[6]
Better together: Unifying datalog and equality saturation,
Y . Zhang, Y . R. Wang, O. Flatt, D. Cao, P. Zucker, E. Rosenthal, Z. Tatlock, and M. Willsey, “Better together: Unifying datalog and equality saturation,” Proc. ACM Program. Lang. , vol. 7, no. PLDI, jun
-
[7]
There and back again: A netlist’s tale with much egraphin’,
G. H. Smith, Z. D. Sisco, T. Techaumnuaiwit, J. Xia, V . Canumalla, A. Cheung, Z. Tatlock, C. Nandi, and J. Balkind, “There and back again: A netlist’s tale with much egraphin’,” arXiv preprint arXiv:2404.00786, 2024
arXiv 2024
-
[8]
Techniques for program verification,
C. G. Nelson, “Techniques for program verification,” Ph.D. dissertation, Stanford, CA, USA, 1980, aAI8011683
work page 1980
Show all 25 references
-
[9]
Equality saturation: a new approach to optimization,
R. Tate, M. Stepp, Z. Tatlock, and S. Lerner, “Equality saturation: a new approach to optimization,” SIGPLAN Not. , vol. 44, no. 1, p. 264–276, jan 2009. [Online]. Available: https://doi.org/10.1145/1594834.1480915
2009
-
[10]
Growing solver-aided languages with rosette,
E. Torlak and R. Bodik, “Growing solver-aided languages with rosette,” in Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software , 2013, pp. 135–152
2013
-
[11]
Kroening and O
D. Kroening and O. Strichman, Decision Procedures - An Algorithmic Point of View. Springer Berlin, Heidelberg, 2016
2016
-
[12]
Kami: a platform for high-level parametric hardware specification and its modular verification,
J. Choi, M. Vijayaraghavan, B. Sherman, A. Chlipala, and Arvind, “Kami: a platform for high-level parametric hardware specification and its modular verification,” Proc. ACM Program. Lang., vol. 1, no. ICFP, Aug. 2017. [Online]. Available: https://doi.org/10.1145/3110268
2017 doi
-
[13]
The essence of bluespec: a core language for rule-based hardware design,
T. Bourgeat, C. Pit-Claudel, A. Chlipala, and Arvind, “The essence of bluespec: a core language for rule-based hardware design,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI 2020. New York, NY , USA: Associatio...
2020
-
[14]
Bluespec system verilog: efficient, correct rtl from high level specifications,
R. S. Nikhil, “Bluespec system verilog: efficient, correct rtl from high level specifications,” Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co- Design, 2004. MEMOCODE ’04. , pp. 69–70, 2004. [Online]. Available: https://api.semant...
2004
-
[15]
Loop rerolling for hardware decompilation,
Z. D. Sisco, J. Balkind, T. Sherwood, and B. Hardekopf, “Loop rerolling for hardware decompilation,” Proc. ACM Program. Lang. , vol. 7, no. PLDI, Jun. 2023. [Online]. Available: https://doi.org/10.1145/3591237
2023 doi
-
[16]
Verisketch: Synthesizing secure hardware designs with timing-sensitive information flow properties,
A. Ardeshiricham, Y . Takashima, S. Gao, and R. Kastner, “Verisketch: Synthesizing secure hardware designs with timing-sensitive information flow properties,” in Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security , ser. CCS ’19. New York, NY ...
2019
-
[17]
Sketchilog: Sketching combinational circuits,
A. Becker, D. Novo, and P. Ienne, “Sketchilog: Sketching combinational circuits,” 01 2014, pp. 1–4
2014
-
[18]
A verilog rtl synthesis tool for heterogeneous fpgas,
P. Jamieson and J. Rose, “A verilog rtl synthesis tool for heterogeneous fpgas,” in International Conference on Field Programmable Logic and Applications, 2005., 2005, pp. 305–310
2005
-
[19]
Odin ii - an open-source verilog hdl synthesis tool for cad research,
P. Jamieson, K. B. Kent, F. Gharibian, and L. Shannon, “Odin ii - an open-source verilog hdl synthesis tool for cad research,” in Proceedings of the 2010 18th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines , ser. FCCM ’10. USA: IEEE Compute...
2010 doi
-
[20]
Polysat: Word-level bit-vector reasoning in z3,
J. Rath, C. Eisenhofer, D. Kaufmann, N. Bjørner, and L. Kov ´acs, “Polysat: Word-level bit-vector reasoning in z3,” 2024. [Online]. Available: https://arxiv.org/abs/2406.04696
2024 arXiv
-
[21]
Formal verifi- cation of arithmetic circuits by function extraction,
C. Yu, W. Brown, D. Liu, A. Rossi, and M. Ciesielski, “Formal verifi- cation of arithmetic circuits by function extraction,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , vol. 35, no. 12, pp. 2131–2142, 2016
2016
-
[22]
Efficient parallel verification of galois field multipliers,
C. Yu and M. Ciesielski, “Efficient parallel verification of galois field multipliers,” in 2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC), 2017, pp. 238–243
2017
-
[23]
dafny-lang community, Dafny Reference Manual , 2024
T. dafny-lang community, Dafny Reference Manual , 2024
2024
-
[24]
Haploid: Speed up smt via preprocessing using egg,
“Haploid: Speed up smt via preprocessing using egg,” 2024. [Online]. Available: https://github.com/IanBriggs/haploid
2024
- [2023]
Reviewed August 12, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.