Control Logic Synthesis: Drawing the Rest of the OWL

System-on-chip (SoC) design requires complex reasoning about the interactions between an architectural specification, the microarchitectural datapath (e.g., functional units), and the control logic (which coordinates the datapath) to facilitate the critical computing tasks on which we all depend. Hardware specialization is now the expectation rather than the exception, meaning we need new hardware design tools to bring ideas to reality with both agility and correctness.

We introduce a new technique, "control logic synthesis", which automatically generates control logic given a datapath description and an architectural specification. This enables an entirely new hardware design process where the designer only needs to write a datapath sketch, leaving the control logic as "holes." Then, guided by an architectural specification, we adapt program synthesis techniques to automatically generate a correct hardware implementation of the control logic, filling the holes and completing the design.

We evaluate control logic synthesis over two classes of control (state machines and instruction decoders) and different architectures (embedded-class RISC-V cores and hardware accelerators for cryptography). We demonstrate how agileoriented SoC developers can iterate over designs without writing control logic by hand yet still retain formal assurances with only minimal microarchitectural information.