A significant component of a processor design is the control logic, which dictates how data flows through the circuit. We propose a method for using program synthesis to automatically generate control logic for datapath sketches, leveraging formal specifications to extract ISA semantics. We create a parser and symbolic executor for Sail specifications that automatically constructs synthesis goals for a given ISA. Synthesizing control logic from a formal specification lets hardware developers use less effort to produce more efficient, correct-by-construction designs.