In an effort to continue to drive computing efficiency to new heights, the traditional lines between hardware and software are becoming increasingly blurry. Unfortunately, any changes made to the most ubiquitous form of hardware, the processor, are stymied by the complex and non-intuitive interactions between the datapath and control. New design languages that help hardware engineers navigate these interactions through a co-analysis of the concrete implementation (e.g. a digital design) and the higher-level abstractions they intend to embody (e.g. the ISA) can unlock a creative, new, energy-efficient system by freeing them to worry more about the structure of the computation than the details of its cycle-level coordination. Specifically, in our ongoing work we introduce a solver-aided hardware-description language IR which supports program sketching for program synthesis. Our program synthesis tool takes the datapath of a processor in HDL code along with instruction semantics extracted from a formal ISA specification, then generates HDL code that implements the control logic for that processor. We evaluate our control logic synthesis tool on an HDL code implementation for a 2-stage pipelined processor for the RISC-V RV32I ISA, automatically generating the HDL code for the control logic in 9 minutes.