  FPGA technology mapping is the process of implementing a hardware design
expressed in high-level HDL (hardware design language) code using the
low-level, architecture-specific primitives of the target FPGA. As FPGAs become
increasingly heterogeneous, achieving high performance requires hardware
synthesis tools that better support mapping to complex, highly configurable
primitives like digital signal processors (DSPs). Current tools support DSP
mapping via handwritten special-case mapping rules, which are laborious to
write, error-prone, and often overlook mapping opportunities. We introduce
Lakeroad, a principled approach to technology mapping via sketch-guided program
synthesis. Lakeroad leverages two techniques -- architecture-independent sketch
templates and semantics extraction from HDL -- to provide extensible technology
mapping with stronger correctness guarantees and higher coverage of mapping
opportunities than state-of-the-art tools. Across representative
microbenchmarks, Lakeroad produces 2--3.5$\times$ the number of optimal
mappings compared to proprietary state-of-the-art tools and 6--44$\times$ the
number of optimal mappings compared to popular open-source tools, while also
providing correctness guarantees not given by any other tool.
