{"id":"f47c3ba0-f297-4f51-8f9e-058b5b19d7a4","arxiv_id":"2411.11036","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An equality-saturation-based mapper (Churchroad) decomposes large designs and auto-generates sketches, letting a synthesis tool map multi-DSP circuits it could not handle alone.","lead":"Churchroad combines equality saturation with an existing synthesis tool, Lakeroad, to map hardware designs onto FPGA DSP blocks without requiring users to write sketches. The paper shows a 16x32 multiplier compiled onto two DSP48E2 blocks in about four seconds, while the synthesis-only tool times out.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Unverified hand-written rewrite rules are the primary correctness risk: Churchroad's correctness depends on axioms that the paper itself defers to future work.","rationale":"The reader identified the soundness of the hand-written rewrite rules as the weakest assumption, and I agree. The paper's central claim is that Churchroad is a technology mapper that scales synthesis-based mapping to larger designs without user sketches. A technology mapper is only meaningful if it preserves semantics; if a rewriting axiom is unsound, the output can be wrong even though every Lakeroad subquery is correct. This is not a speculative, consensus-based concern: it is an explicit gap in the paper. The proof is absent, no formal verification is provided, and Section IV says generating correct rewrite rules is future work. The shown rule for eq. (4) is a specific identity that appears sound, but the paper relies on a database of such rules and on a variable-bitwidth generalization without proof. This makes the concern load-bearing rather than stylistic. I also note that the evaluation is limited to a single design, which is a real threat to the 'handles larger and more complex designs' generalization, but the correctness risk is the more foundational issue: if the rules are unsound, no amount of additional benchmarking would rescue the mapper. The conditional verdict remains appropriate: accepting the paper as a promising prototype contingent on rule verification and broader evaluation. I therefore recommend no change to the reader's verdict.","tokens_in":7848,"tokens_out":9096,"duration_ms":87356,"concrete_test":"Encode every rewrite rule in Churchroad's database as a universally quantified bit-vector identity over the rule's matched bitwidth range, and discharge each with an independent checked proof (e.g., a verified SMT solver, bit-blasting with a certified proof checker, or a proof assistant like Coq/Lean). Also instantiate the variable-bitwidth version of the eq. (4) rule for widths such as 8, 16, 32, and 64, and prove the identity before and after extraction. If any identity fails, Churchroad can emit incorrect hardware even when all Lakeroad calls succeed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim that Churchroad is a usable technology mapper depends on semantics preservation: every design it emits must be equivalent to the input spec. In Section II, Churchroad 'pre-applies equalities we know to be true' as egglog rules, e.g., the rule unioning a 16x32 Mul with the two-DSP decomposition corresponding to eq. (4). These rules are introduced as axioms and are not mechanically verified. The e-graph treats a union as semantic equivalence, so any unsound rule can equate the spec with an incorrect expansion; subsequent Lakeroad subqueries may all succeed because they only check the smaller generated specs, while the overall extracted design is wrong. The particular rule shown for eq. (4) is mathematically plausible for the stated unsigned truncated multiplication, but the paper does not prove the 'variable bitwidth' generalization it claims, and the rest of the rule database is neither enumerated nor validated. Section IV explicitly lists 'generating correct rewrite rules... rather than writing them manually' as future work, confirming that the present rules are manual and unproven. Since Churchroad's sketch-free workflow is precisely what routes the user through these rules, a single bad axiom breaks the correctness guarantee that a technology mapper must provide, even if every Lakeroad subquery is individually correct.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":8096,"tokens_out":4636,"duration_ms":51802,"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":[{"comment":"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).","section":"Section II, eq. (4) and the egglog rewrite rule"},{"comment":"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":"Sections I, II, and IV (evaluation evidence)"},{"comment":"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.","section":"Section II, DSP proposal rules"}],"minor_comments":[{"comment":"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":"Section II, e-graph figures"},{"comment":"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":"Section II, notation"},{"comment":"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":"Section II, runtime claim"},{"comment":"There is a grammatical error in the sentence 'egglog rules takes two arguments'; it should be 'egglog rules take two arguments.'","section":"Section II, text"},{"comment":"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.","section":"Section III, references"}],"recommendation":"major_revision","confidential_remarks":"The paper would be a solid workshop paper or a short progress report, but for a full archival venue the single-example evaluation and the unverified rewrite-rule database are substantial gaps. The authors should be encouraged to add a correctness proof or machine-checked validation for the rewrite rules and a broader benchmark suite. The central idea is novel and worth pursuing, so I would be willing to review a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"One thing to know: this paper does something genuinely useful—it uses equality saturation to split a synthesis-based technology mapping problem into subtasks, and it generates the sketches automatically from the e-graph. It's demonstrated on one 16x32 multiplier example, which is the whole evaluation. Be careful with the abstract's 'larger and more complex designs' claim; that's not yet backed by data.\n\nThe combination is new as far as I can tell. Prior work either requires user sketches (Lakeroad) or uses eqsat only as an SMT preprocessor (Haploid). Using the e-graph to propose DSP candidates and to synthesize both spec and sketch for each Lakeroad call is a solid, compact idea. The paper is clearly written and does not oversell; it labels itself early evidence.\n\nThe soft spots are real but mostly acknowledged. First, a single example is thin evidence for a technology mapper. Second, the rewrite rules are axioms. The stress-test note has this right: Churchroad's correctness depends on 'equalities we know to be true,' and the paper lists 'generating correct rewrite rules' as future work. For a hardware compiler that emits an FPGA design, an unsound rule could silently produce incorrect hardware. The specific rule shown for the truncated multiply is plausible, but the full rule database is neither listed nor verified. I don't think this is fatal for the research idea; it is a standard risk in eqsat-based tools, and the authors state it plainly. But it does cap the paper's current claim to 'prototype with unproven rules.'\n\nThe reader's CONDITIONAL verdict is about right. The paper is short, so the absence of benchmarks is not disqualifying for a workshop-style submission, but it limits generalizability. I'd want at least one different design and a broader rule set before trusting the scaling claim.\n\nWho it's for: eqsat folks, anyone working on synthesis-based hardware mapping, FPGA tooling people. It deserves a serious referee. I would send it to review with the expectation that the authors either add another benchmark or tighten the correctness story. I'd read the extended version.","headline":"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.","tokens_in":8593,"tokens_out":2363,"would_cite":false,"duration_ms":96546,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["equality saturation","technology mapping","FPGA","program synthesis","sketches","DSP","e-graph","SMT"],"falsifier":"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.","tokens_in":7664,"feed_emoji":"🔧","tokens_out":5133,"duration_ms":51744,"temperature":0.7,"pith_summary":"This paper claims that equality saturation can lift the two main limitations of sketch-guided program synthesis for FPGA technology mapping. It presents Churchroad, which combines the egglog equational-reasoning framework with the Lakeroad synthesis-based mapper, so that large designs are rewritten into smaller pieces and each piece is compiled by a separate Lakeroad query. This removes the need for users to write sketches, because the structure of the compiled output is inferred from the e-graph. As evidence, Churchroad compiles a 16-bit by 32-bit multiplier onto two DSP48E2 primitives, a design that Lakeroad alone cannot handle.","feed_headline":"Churchroad compiles a two-DSP multiplier Lakeroad can't","feed_subtitle":"Equality saturation splits wide multiplies into small SMT queries and generates sketches for free from the e-graph.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Provides the Lakeroad sketch-guided synthesis tool that Churchroad calls as a subroutine; it is the baseline that Churchroad must scale.","marker":"[2]"},{"why":"Supplies the egglog equality-saturation framework with its e-graph data structure and rule engine that Churchroad is built on.","marker":"[6]"},{"why":"Implements Rosette, the solver-aided language in which Lakeroad's synthesis queries are written and on which the bitwidth-scaling experiments run.","marker":"[10]"},{"why":"Documents the bit-blasting bottleneck for multiplication in SMT solvers, the scalability problem Churchroad's decomposition addresses.","marker":"[4]"},{"why":"Introduces equality saturation as the rewrite-based optimization technique that Churchroad adapts for technology mapping.","marker":"[9]"}],"fun_headline_variants":["Auto-sketches via equality saturation: Churchroad scales past Lakeroad","Equality saturation powers Churchroad to beat Lakeroad on DSP maps","Churchroad's eqsat auto-generates sketches for larger designs","Splitting multiplies with eqsat helps Churchroad out-map Lakeroad","No more hand sketches: Churchroad uses eqsat to scale synthesis"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The hand-written rewrite rules, such as the partial-product equality in equation (4), are sound and preserve semantics for every bitwidth they match.","fun_headline_variants_meta":{"raw":{"variants":["Auto-sketches via equality saturation: Churchroad scales past Lakeroad","Equality saturation powers Churchroad to beat Lakeroad on DSP maps","Churchroad's eqsat auto-generates sketches for larger designs","Splitting multiplies with eqsat helps Churchroad out-map Lakeroad","No more hand sketches: Churchroad uses eqsat to scale synthesis"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000979,"raw_usage":{"total_tokens":4122,"prompt_tokens":875,"completion_tokens":3247,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":491,"completion_tokens_details":{"reasoning_tokens":3151}},"tokens_in":491,"tokens_out":3247,"duration_ms":24287,"temperature":1.0,"reasoning_tokens":3151,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:59:21.319554+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Better together: Unifying datalog and equality saturation,","cited_arxiv_id":null,"evidence_quote":"Supplies the egglog equality-saturation framework with its e-graph data structure and rule engine that Churchroad is built on."},{"cited_title":"Growing solver-aided languages with rosette,","cited_arxiv_id":null,"evidence_quote":"Implements Rosette, the solver-aided language in which Lakeroad's synthesis queries are written and on which the bitwidth-scaling experiments run."},{"cited_title":"Further steps down the wrong path : Improving the bit- blasting of multiplication,","cited_arxiv_id":null,"evidence_quote":"Documents the bit-blasting bottleneck for multiplication in SMT solvers, the scalability problem Churchroad's decomposition addresses."},{"cited_title":"Equality saturation: a new approach to optimization,","cited_arxiv_id":null,"evidence_quote":"Introduces equality saturation as the rewrite-based optimization technique that Churchroad adapts for technology mapping."}],"review_version":1}