FPGA Technology Mapping Using Sketch-Guided Program Synthesis

Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, Steven Lyubomirsky, Sorawee Porncharoenwase and 3 others

An FPGA is a reconfigurable chip whose modern building blocks — especially digital signal processors with nearly a hundred settings and a 75-page manual — are so complex that the tools meant to map a designer's circuit onto them are handwritten, buggy, and routinely fail, forcing engineers to configure the blocks by hand over hours or days; this work from the University of Washington builds Lakeroad, which reframes the mapping as a program-synthesis problem, automatically extracts each block's behavior from the vendor's own simulation model, and asks a solver to find a provably correct configuration, finding 2 to 44 times more optimal mappings than existing tools while guaranteeing correctness none of them offer.

The argument in one glance

Problem

Mapping circuits onto modern FPGA blocks is hard

An FPGA is a chip you reconfigure into custom hardware. Getting good performance means mapping a designer's high-level circuit onto the chip's low-level building blocks. Modern blocks are intricate — a single digital signal processor can have nearly a hundred settings and a 75-page manual of rules. Using them well is now essential and very hard.
What people did

Match circuits to blocks with handwritten rules

Today's mapping tools use handwritten, special-case pattern-matching rules: recognize a shape in the circuit, emit a specific block configuration. Simple blocks like lookup tables are handled well this way, and vendors add rules for the complex blocks too.
Why it fell short

Handwritten rules are incomplete, unsafe, and unextensible

The rules miss many mapping chances — a circuit that should fit one processor gets spread across several plus extra logic. They carry no correctness guarantee, and bugs are common across all major tools. And every new block demands hundreds of new rules and hand-written semantics. When mapping fails, the engineer configures the block by hand from the manual, which takes hours to days.
This paper's idea

Reframe mapping as solver-driven program synthesis

Lakeroad treats a block's configuration as a tiny programming language and asks a solver to write the right configuration. It extracts each block's exact behavior automatically from the vendor's own simulation model, uses architecture-independent sketch templates reusable across chips, and has the solver find a configuration provably equivalent to the design. It finds 2 to 44 times more optimal mappings than existing tools, with correctness guarantees none of them offer.

Why this problem is worth solving

The task sounds mechanical but has become genuinely hard.

An FPGA, a field-programmable gate array, is a chip whose logic you can reconfigure after manufacture to become almost any digital circuit. A designer writes a circuit in a high-level hardware description language, and a tool must implement it using the specific building blocks that particular FPGA provides. This implementation step is called technology mapping. For years the blocks were simple: lookup tables, which are tiny memories that can compute any small logic function, and carry chains for addition. Mapping to these is well understood — translate the circuit to basic gates and pack them into lookup tables. But to keep improving performance, FPGA makers now include large, specialized blocks, above all the digital signal processor, or DSP: a configurable arithmetic engine for multiply-and-add-heavy work. These are powerful but forbiddingly complex. One widely used DSP has nearly a hundred ports and parameters, and its manual runs 75 pages, much of it describing the intricate restrictions on how those settings may combine. Mapping a circuit onto such a block means searching an enormous space of configurations while respecting all those restrictions and getting the internal pipeline registers right. Using these blocks well is now essential to good FPGA performance, so a mapper that cannot handle them leaves a lot on the table.

The way tools handle these blocks is the root of the trouble.

Current technology mappers recognize circuit shapes and emit block configurations using handwritten, special-case pattern-matching rules, built up by hand for each block. This approach fails in three ways. First, it is incomplete: the rules only cover the shapes someone thought to write down, so they miss many legal mappings. The paper shows a small circuit — an add feeding a multiply feeding a bitwise operation — that the block’s own manual says fits on a single DSP, yet a leading tool spreads it across several DSPs plus extra lookup tables, wasting resources. Second, it gives no correctness guarantee. The rules are just code, and recent work has found significant numbers of bugs across all the major hardware synthesis tools, so a mapping might silently be wrong. Third, it is hard to extend. Each new block requires someone to understand its detailed semantics and add hundreds of new special-case rules, an enormous ongoing effort as FPGAs grow more diverse. When the automatic tools fail, the designer is left with bad options: accept lower performance, manually carve out the sub-circuit and re-run in hope, or, worst of all, configure the block by hand — reading the 75-page manual, setting dozens of ports, and getting the ten-plus pipeline registers right, which can take hours to days.

What people did before, and where it broke

Map simple blocks with logic packing (tools like ABC). Translate the circuit to basic gates and pack them into lookup tables. Where it broke. This works beautifully for simple blocks, but says nothing about how to use the large, configurable blocks like DSPs where modern performance now lives.
Handwritten pattern-matching rules for complex blocks. For each block, hand-write rules that recognize circuit shapes and emit configurations. Where it broke. The rules are incomplete (they miss legal mappings), carry no correctness guarantee (bugs are common across all major tools), and demand hundreds of new rules per block, making them laborious and error-prone.
Fall back to manual work. When mapping fails, the engineer isolates the sub-circuit and re-runs, or hand-configures the block from its manual. Where it broke. Partial re-runs often still fail, and manual configuration of a hundred-setting block with a deep pipeline is expert work that takes hours to days per block.
The gap. No mapper could use complex FPGA blocks completely, with a correctness guarantee, and be easy to extend to new blocks and architectures. Achieving all three by turning mapping into solver-driven program synthesis, fed by automatically extracted semantics and reusable templates, is what Lakeroad does.

How Lakeroad works

From handwritten rules to solver-found, provably-correct configurations

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Reframe an ad-hoc matching problem as a solver-driven search. The pivot is to stop writing rules that guess which configuration fits a circuit shape, and instead observe that a block’s settings form a tiny programming language, so the question “which configuration implements this design” is a program-synthesis problem. Lakeroad hands that question to an SMT solver, a tool that can search a huge space of possibilities and prove when one satisfies a specification. Turning a hand-tuned, pattern-based engineering task into a template whose blanks a solver fills by search is the same move the traversal-synthesis work covered elsewhere on this site makes, filling in a template with a solver by encoding the requirements as a constraint problem rather than writing the answer out by hand.

Mine the semantics from an artifact that already exists. Synthesis needs an exact model of what each block does, and hand-writing that for a hundred-setting block is precisely the laborious, error-prone work Lakeroad wants to avoid. Its insight is that the chip vendor already ships such a model — the simulation model used to validate designs — and Lakeroad automatically extracts the block’s semantics from it, repurposing an artifact that was only ever used after mapping to now drive mapping. Recovering the precise meaning a tool needs from a lower-level artifact that was never packaged to provide it is the same recovery the lifted-binary analysis work covered elsewhere on this site performs, reconstructing the program’s intended variables from how the low-level code actually uses its pointers.

Factor out what is common so each new target is nearly free. The high-level blueprints for arranging blocks — a single DSP with holes for its settings, or a bank of lookup tables with holes for their memories, or a mix — look much the same across FPGA families. Lakeroad captures these as architecture-independent sketch templates, so supporting a new block or a new chip usually requires no new template at all, only a short description and the vendor model. Separating the architecture-independent structure from the per-chip details so that retargeting is cheap is the same layering the shared-intermediate-representation compiler work covered elsewhere on this site relies on, lifting programs into one common representation and then lowering it to each chip rather than rebuilding the whole path per target.

Following a circuit onto a single DSP

Mapping an add-multiply-and module the tools get wrong

Tracing one mapping shows why synthesis beats pattern matching.

Step 1 of 5

A small circuit that should fit one block

A designer has a module that adds two numbers, multiplies by a third, and applies a bitwise operation. The block's manual says this fits on a single digital signal processor, but a leading proprietary tool spreads it across several processors plus extra lookup tables.

That waste is multiplied every time the module is reused across a large design.

Why it works

A block’s configuration is a tiny language. Because each setting of a block’s hundred ports and parameters defines a different computation → the space of configurations is exactly a small programming language → so finding a configuration that matches the design is a program-synthesis problem a solver can search.
The vendor already wrote the semantics. Because chip makers publish a simulation model that precisely describes each block’s behavior → extracting that model yields the exact semantics synthesis needs → so no one must hand-write and debug hundreds of pattern-matching rules per block.
Templates factor out what is common. Because the blueprints for how blocks combine are similar across FPGA families → one architecture-independent sketch template serves many chips → so adding a new block or architecture usually needs no new template at all.
The solver proves equivalence. Because Lakeroad asks the solver for a configuration equivalent to the design on all inputs → a returned answer is correct by construction rather than by trusting a hand-written rule → so it carries a correctness guarantee no existing tool provides.
Completeness saves real resources. Because the solver explores configurations the pattern matchers miss → it packs a design into fewer processors and lookup tables → so each small module uses fewer resources, multiplied across the hundreds of times it appears in a full design.

What it costs (trade-offs and scope)

Synthesis can be slow, and solvers can time out. Asking a solver to search a large configuration space takes real time, and hard queries may not finish. Lakeroad runs several solvers in parallel and uses the first to answer, but this is heavier than a quick pattern match, and some mappings will exceed the time budget.
It targets small fragments, not whole designs directly. Lakeroad maps the module-sized fragments that should fit onto a block, the pieces a designer would try to map to a DSP. Composing these into full-design mapping is future work, though such fragments recur many times so the wins multiply.
It depends on the vendor model being available and faithful. The semantics come from the vendor’s simulation model, so a block with no published model, or an inaccurate one, limits what Lakeroad can do. Its guarantee is relative to that model and the trusted extraction toolchain.
The guarantee is equivalence, not physical timing. The solver proves the configuration computes the same function with the right pipeline latency; it does not by itself guarantee the placed-and-routed design meets a clock frequency, which remains a downstream concern.
It is a research tool with a defined footprint. Lakeroad is about 13,000 lines and supports several blocks across four FPGA architectures. It demonstrates the approach convincingly, but is not a drop-in replacement for a full commercial toolchain’s breadth.
Extending still needs some inputs. Although new blocks usually need no new sketch templates, they do need a short architecture description and the vendor model, and occasionally a new template for a genuinely novel arrangement.

The evaluation

Three ways to map circuits onto complex FPGA blocks

Property	Proprietary tools	Open-source (Yosys)
How it maps to complex blocks
Correctness guarantee		No
Adding a new block		Hundreds of rules
Optimal mappings found	Baseline
Resources per module	More blocks and logic	Most

Three ways to map circuits onto complex FPGA blocks, evaluated on microbenchmarks of designs that should each fit a single digital signal processor, across the Xilinx UltraScale+, Lattice ECP5, and Intel Cyclone 10 LP architectures (plus the open-source SOFA for the simpler blocks). Proprietary and open-source tools both use handwritten pattern-matching rules that miss many legal mappings, offer no correctness guarantee, and need hundreds of new rules per block. Lakeroad instead asks an SMT solver to fill architecture-independent sketch templates using semantics extracted automatically from the vendor's simulation model. It finds 2 to 3.5 times more optimal mappings than the proprietary state-of-the-art tools and 6 to 44 times more than the popular open-source Yosys, uses on average several fewer logic elements and registers per module (for example about 4 fewer logic elements and 8 fewer registers than the Xilinx tool, and 33 fewer logic elements than Yosys), and is correct by construction, further validated by simulating thousands of cycles.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

Lakeroad is a clean application of programming-languages ideas to a real hardware problem, with a satisfying payoff: it maps circuits onto complex FPGA blocks more completely than the tools engineers use today, and it is the only one that guarantees its mappings are correct. The three ideas fit together well. Reframing mapping as program synthesis lets a solver search configurations that hand-written rules never enumerate; extracting semantics from the vendor’s own simulation model removes the laborious, bug-prone step of hand-writing each block’s behavior; and architecture-independent sketch templates make supporting a new block or chip nearly free. The measured gains are large — 2 to 3.5 times more optimal mappings than proprietary tools, up to 44 times more than the open-source one, with fewer resources per module — and the correctness comes from the solver proving equivalence on all inputs, not from testing. Read it with its scope. Synthesis is heavier than pattern matching and can time out, so it is run per module rather than across a whole design, and composing module mappings into full designs is future work. The guarantee is equivalence relative to the vendor model and the trusted extraction toolchain, and it concerns function and pipeline latency, not final placed-and-routed timing. Lakeroad supports several blocks across four architectures in about thirteen thousand lines; it proves the approach rather than replacing a commercial toolchain wholesale. The durable lesson is that when a compiler component has grown into a sprawl of hand-written special cases, reframing it as search against extracted semantics can make it at once more complete, more correct, and easier to extend.

Background

Why replacing hand-written rules with a solver is a recurring win

It helps to see Lakeroad as one more case of a pattern that keeps paying off: a piece of a compiler or system that has accreted into a pile of hand-written special cases is often better expressed as a search over a precise specification. Hand-written rules are where completeness leaks away and bugs creep in, because no person can enumerate every case a real design will present. The copy-on-write correctness work covered elsewhere on this site tells a kindred story in the operating-system kernel, where years of ad-hoc, bug-prone patches to a subtle interaction were finally replaced by one principled rule that a system could enforce with a guarantee. In both, the win comes from stepping back from case-by-case engineering to a stated specification — an equivalence the solver must satisfy, an invariant the kernel must preserve — and letting a principled mechanism handle the cases automatically. The broad point is that completeness and correctness are hard to bolt onto a heuristic after the fact, but they can fall out naturally when the problem is posed as satisfying a specification. As hardware and systems grow more complex, the components most worth rebuilding this way are exactly the ones that have become unmanageable heaps of special cases.

If you remember only three things

1. An FPGA is a reconfigurable chip, and technology mapping implements a designer's high-level circuit using the chip's low-level building blocks. Modern blocks like digital signal processors are intricate — nearly a hundred settings and a 75-page manual of rules — and using them well is essential to performance. Today's tools map onto them with handwritten pattern-matching rules that are incomplete (they miss legal mappings, sometimes spreading a circuit that fits one block across several), carry no correctness guarantee (bugs are common across all major tools), and need hundreds of new rules per block. When they fail, engineers configure blocks by hand over hours to days.
2. Lakeroad reframes mapping as sketch-guided program synthesis. It observes that a block's configuration space is a tiny programming language and asks an SMT solver to find a configuration provably equivalent to the design on all inputs. Two techniques make this practical: it automatically extracts each block's exact semantics from the vendor's own published simulation model (rather than hand-writing them), and it uses architecture-independent sketch templates — reusable blueprints of blocks with holes — so supporting a new block or FPGA family usually needs no new template. The result is correct by construction and further validated by simulation.
3. Across microbenchmarks that should each fit a single digital signal processor, on the Xilinx UltraScale+, Lattice ECP5, and Intel Cyclone 10 LP architectures, Lakeroad finds 2 to 3.5 times more optimal mappings than proprietary state-of-the-art tools and 6 to 44 times more than the open-source Yosys, using on average several fewer logic elements and registers per module, with correctness guarantees no other tool offers. Its limits: synthesis is heavier than pattern matching and can time out, it maps module-sized fragments rather than whole designs directly, it depends on a faithful vendor model, and its guarantee is functional equivalence rather than final physical timing.

Check yourself

Check your understanding

1. Why has FPGA technology mapping become so much harder in recent years?
2. What is Lakeroad's central reframing of the mapping problem?
3. Lakeroad needs an exact model of each block's behavior. How does it get one without hand-writing it?
4. A team wants Lakeroad to guarantee their entire large design meets a target clock frequency after being placed on the chip. Can it, based on the paper?

Sources

The paper is “FPGA Technology Mapping Using Sketch-Guided Program Synthesis” by Gus Henry Smith, Ben Kushigian, Vishal Canumalla, Andrew Cheung, Steven Lyubomirsky, Sorawee Porncharoenwase, Rene Just, Gilbert Louis Bernstein, and Zachary Tatlock, published at ASPLOS 2024, DOI 10.1145/3620665.3640387. Most authors are at the University of Washington. The tool is named Lakeroad.

This explainer is written from the full text of the paper, obtained from the authors’ arXiv preprint (2401.16526), which matches the ASPLOS 2024 proceedings and is distributed under a Creative Commons Attribution license. Everything above comes from the paper’s own sections: the introduction and background on FPGA technology mapping (lookup tables, carry chains, and the shift to complex digital signal processors such as the DSP48E2 with its nearly hundred ports and parameters and 75-page manual), the three shortcomings of handwritten pattern-matching rules (incompleteness, lack of correctness guarantees with bugs found across all major tools, and difficulty of extension), and the fallback to partial design mapping and manual instantiation; the key observation that a block’s configuration space is a small programming language and mapping is therefore program synthesis, adapted as sketch-guided synthesis on the Rosette framework; the two enabling techniques of semantics extraction from vendor HDL simulation models (using Yosys passes to produce solver-ready semantics) and architecture-independent sketch templates; the formalization of the Lakeroad function synthesizing a program equivalent to the design at a given clock cycle, the SMT equivalence query, the portfolio of solvers (Bitwuzla, cvc5, Yices2, and STP), and validation via Verilator; and the evaluation across the Xilinx UltraScale+, Lattice ECP5, Intel Cyclone 10 LP, and open-source SOFA architectures, with the microbenchmark counts (1320 for Xilinx, 396 for Lattice, 66 for Intel), the completeness results (2 to 3.5 times more optimal mappings than proprietary tools and 6 to 44 times more than Yosys), and the average resource reductions in logic elements and registers.