Control Logic Synthesis: Drawing the Rest of the OWL

Zachary D. Sisco, Andrew David Alex, Zechen Ma, Yeganeh Aghamohammadi, Boming Kong, Benjamin Darnell and 3 others

Designing a small chip means writing both the datapath (the parts that move and crunch data) and the control logic (the wires and signals that steer them in the right order) — and the control logic is the fiddly, error-prone half that eats about half of all verification effort; this paper (UC Santa Barbara) lets the designer draw only the datapath and leave the control as holes, then adapts program synthesis to fill those holes with provably correct control logic derived from a formal spec, generating a whole RISC-V core's control in seconds instead of by hand.

The argument in one glance

Problem

Control logic is the fiddly, dangerous half of designing a chip

A processor or accelerator splits into two parts. The datapath is the machinery that actually moves and transforms data — register files, adders, the ALU, pipeline registers. The control logic is everything that steers that machinery: the signals that decode an instruction, pick which functional unit runs, select which value flows down which wire, and advance a state machine from one step to the next. The datapath is where a designer starts, because it captures the intent; the control logic is the tangle that makes it actually obey the specification, cycle by cycle, and it is the part where subtle bugs hide. Studies find roughly half of all hardware development time goes to verification, much of it chasing control bugs. In an embedded root-of-trust chip, one such bug can be catastrophic.
What people did

Write the control logic by hand, then verify it

The traditional flow has an engineer reason through every behavior the instruction set can produce, down through the microarchitecture and its optimizations like pipelining, and hand-write the control signals to match. Then a separate, expensive verification effort tries to prove that what was written actually meets the specification.
Why it fell short

Every design iteration means re-deriving and re-verifying the control by hand

Agile hardware means iterating: add a custom instruction, deepen the pipeline, swap a functional unit. Each change ripples into the control logic, which must be rewritten and re-verified from scratch. The control-datapath split is also leaky — pipelining and hazards couple them — so the reasoning is genuinely hard. Doing it by hand is exactly where correctness is lost and where agility grinds to a halt.
This paper's idea

Draw only the datapath, leave the control as holes, and synthesize the rest

The designer writes a datapath sketch with the control logic left as "holes", plus a formal specification of the intended behavior. A program-synthesis engine then searches for control logic that fills the holes so the completed design provably matches the spec — correct-by-construction. To keep the search tractable it is done independently per instruction and the pieces are unioned. The title is a joke on the "how to draw an owl" meme: the datapath is the two circles, and synthesis draws the rest of the owl.

Why this problem is worth solving

The split at the heart of this paper is the oldest idea in computer architecture, and its awkwardness is what makes the paper necessary.

Every synchronous digital design is conventionally divided into a datapath and control logic. The datapath is the collection of functional units and stateful elements that operate on data — adders, shifters, multiplexers, register files, memories, and the pipeline registers between them. The control logic is the surrounding web of signals that orchestrates the datapath: it decodes the current instruction or opcode, decides which units fire, selects which wire feeds which input, enables or stalls registers, and drives state machines through their steps. Designers naturally start with the datapath because it embodies what the machine computes; the control is the harder, later, bug-prone job of making the datapath do it in the right order. The division is convenient but leaky — pipelining, hazards, and stalls make control and datapath depend on each other bidirectionally — which is precisely why hand-writing the control against a moving datapath is so error-prone.

The technique that makes automation possible is borrowed from software, not hardware.

Program synthesis is the use of a search engine that, given a specification of what a piece of code must do and a space of candidate programs to consider, automatically finds a concrete program that provably satisfies the specification. Here the “program” being synthesized is hardware control logic, the specification is a formal description of the instruction set, and the space of candidates is the set of ways to fill the holes in the datapath sketch. The power of synthesis is that it searches over all designs that meet the spec rather than following fixed templates, so it can discover control that a human might miss — but that same search grows explosively with design size, which is why the paper works so hard to pose each synthesis question in a small, tractable form.

What people did before, and where it broke

Write and verify control logic by hand. The dominant industrial flow: engineers author the control signals in an HDL like SystemVerilog or Chisel, then verify against the spec. Where it broke. Verification eats about half of development time, and every datapath change forces the control to be rewritten and re-verified, so hand-authoring is both the slowest step and the one where correctness is most often lost.
High-level synthesis (HLS) from a behavioral description. Tools compile a high-level, often C-like description of what the hardware should do into RTL, generating datapath and control together. Where it broke. HLS asks the designer to give up control over the microarchitecture and trust the tool’s schedule; it targets throughput-oriented accelerators, not the bespoke, cycle-exact embedded cores with custom instruction sets that this work aims at, where the designer wants to own the datapath precisely.
Formal verification and equivalence checking. Prove an already-written design matches a golden model or an ISA specification. Where it broke. These tools check a design a human already wrote; they find bugs but do not remove the burden of writing correct control in the first place, and a failed check sends the engineer back to hand-editing.
Push-button processor generators and templated cores. Parameterized generators emit a core from a fixed template. Where it broke. They produce only the designs the template anticipated; step outside it — a custom crypto instruction, a bespoke constant-time core, an unusual pipeline — and you are back to hand-writing control.
General program synthesis over the whole design at once. Hand the entire datapath and specification to a synthesizer and ask it to produce all the control. Where it broke. The search space explodes; synthesizing control for even a small design in one shot times out, because the constraints sent to the solver grow with every instruction and every time step at once.
The gap. No flow let a designer keep full control of a small, bespoke datapath, leave only the control logic unwritten, and have it filled in automatically and provably correctly — while staying tractable enough to finish in seconds rather than timing out.

How control logic synthesis is put together

From a datapath sketch and a spec to correct-by-construction control

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

The idea

Leave holes where the control goes, and let a solver draw them in. The central move is to invert the usual order of work. Instead of writing the datapath and then laboring over the control that steers it, the designer writes only the datapath — the solid lines of the design diagram — and marks every place a control signal is needed with a hole. A hole in Oyster is literally an unknown bitvector the solver is free to choose. The synthesis engine then asks: is there an assignment to all these holes such that, for this instruction, whenever the precondition holds the design ends in the state the specification demands? If the solver says yes, the values it returns are the control logic, and because they were found by satisfying the specification itself, the result is correct by construction rather than correct-if-verified-later. Starting from a partial design riddled with holes and asking a search engine to complete it against a specification is the same sketch-driven discipline the sketch-guided program-synthesis work covered elsewhere on this site uses to map a circuit onto an FPGA, where the human fixes the shape and the solver supplies the details that make it correct.

Do not synthesize the whole design at once — cut it per instruction. Handing a solver the entire datapath and every instruction together is what makes naive synthesis hopeless: the constraints multiply across all instructions and all time steps, and the search times out even on tiny cores. The paper’s key tractability idea is that, absent feedback in the control logic, the control for one instruction can be synthesized in isolation and the separate answers combined with a union operator. So the tool poses one small synthesis query per instruction — each a modest satisfiability problem the solver dispatches in a fraction of a second — and assembles the pieces afterward. The payoff is dramatic: synthesizing control for the whole base RISC-V integer instruction set in one shot exceeds a three-hour timeout, while the per-instruction strategy finishes the same design in about six and a half seconds. Taming an intractable synthesis problem by decomposing it into solver-sized subproblems whose local answers compose into the whole is the same discipline the solver-aided compiler work covered elsewhere on this site relies on, handing each phase of an NP-hard job to the solver engine best suited to it rather than presenting one monolith.

Describe the hardware once, concretely, and get the symbolic machinery for free. The engine underneath is Rosette, which turns an ordinary interpreter into a symbolic one automatically: the authors write Oyster as a plain cycle-accurate simulator, and Rosette lifts it so the same code runs on symbolic bitvectors and produces SMT constraints. That means the effort of building a bespoke symbolic reasoner for hardware — normally a research project in itself — collapses into writing a normal simulator and letting the solver framework do the rest. An abstraction function ties the sketch’s concrete state and timing back to the abstract specification, so pipelining and hazards can be expressed as which time step each read and write happens. Building the hard analysis by writing a straightforward concrete interpreter and letting a solver-aided framework lift it to symbolic reasoning is exactly the symbolic-compilation approach the tree-traversal synthesis work covered elsewhere on this site takes, where a domain-specific interpreter is compiled into symbolic form so a solver can search over its behaviors.

Following one instruction through synthesis

Synthesizing control for an ALU add on a pipelined core

An illustrative trace of how the tool generates the control logic for one instruction — an ADD on a small ALU core the designer wants to pipeline. The datapath is drawn; the control is holes.

Step 1 of 5

The designer draws the datapath and marks the holes

The datapath sketch has a register file, an ALU, and two pipeline registers the designer inserted — one after reading the two source registers, one holding the ALU result. Where a control signal is needed — which ALU operation to select from the opcode, which value to route into each pipeline register — the designer writes a hole instead of a concrete signal.

In PyRTL the holes appear as the dotted-line boxes of the design diagram; everything solid is the datapath the human fully controls.

Why it works

Holes turn “write the control” into “search for the control”. Marking each control point as an unknown bitvector hands the hard creative step to a solver → and satisfying the specification directly means the returned values are correct by construction, not correct-pending-verification → so the most bug-prone, verification-heavy part of design is produced already proven against the spec.
Per-instruction decomposition is what makes synthesis finish. Synthesizing all control at once multiplies constraints across every instruction and time step until the solver times out → but with no feedback in the control, each instruction can be synthesized alone and the pieces unioned → which is why the whole RISC-V integer ISA drops from a three-hour timeout to about 6.6 seconds.
An abstraction function makes pipelining expressible. A pipelined design reads and writes state across different cycles, so naive pre/postconditions do not match → but recording, per state element, which time step it is touched lets the spec align with a multi-cycle datapath → so the same technique generates control for single-cycle, two-stage, and three-stage versions of a core just by editing the timing map.
Rosette gives symbolic reasoning for free. Building a bespoke symbolic evaluator for an HDL is normally a project of its own → but writing Oyster as a plain concrete interpreter and letting Rosette lift it produces the symbolic interpreter automatically → so the team could focus on posing the right synthesis questions instead of engineering a solver.
Owning the datapath keeps the tool honest about microarchitecture. Letting the designer fully specify the datapath, including pipeline registers and functional units, means the tool never guesses the microarchitecture → and the generated control is forced to match that exact structure and the ISA spec → so agile iteration — add an instruction, deepen the pipeline — becomes re-synthesis rather than a hand rewrite.

What it costs (trade-offs and scope)

Big designs still blow up the solver. The synthesis constraints grow with design size and the number of time steps evaluated, and for large designs solving times increase dramatically. Exploding solve times are a known program-synthesis problem; this work inherits it, and only small embedded-class cores are demonstrated.
The per-instruction trick assumes no feedback in the control. The independence optimization that delivers the speedup is valid only for the class of machines with no feedback between instructions in the control logic. Features like out-of-order execution violate the assumption and are explicitly out of scope, left to future work on how to lift and generalize the technique.
The generated logic is bigger than a human’s. The synthesized HDL is larger than a hand-written reference, and the resulting circuit uses about ten percent more gates; running a logic-optimization pass in Yosys still leaves roughly three percent more gates than the reference. The tool guarantees correctness, not minimality of area, power, or code size.
The output is a netlist, not readable HDL. The generated control essentially is a netlist and is not optimized for a human to read or maintain. Making it readable would require a further decompilation step to lift it back to high-level HDL.
The designer must still supply three formal artifacts. The flow needs an ILA specification, a PyRTL datapath sketch, and a hand-written abstraction function that must be kept in sync as the design changes. The burden of writing control moves to the burden of writing and maintaining a correct spec and abstraction.
Evaluation is on small, bespoke targets. The case studies are an embedded RISC-V core (with crypto extensions), a bespoke constant-time cryptography core, and an AES-128 accelerator — a strong demonstration of generality and correctness, but not a study of large, production-scale processors.

The evaluation

Three ways to get correct control logic for a bespoke embedded core

Property	Hand-write and verify	Synthesize the whole design at once	Control logic synthesis (per-instruction)
Who writes the control logic
Correctness guarantee
Time for the full RISC-V integer ISA
Circuit size versus a hand-written reference		n/a (does not finish)
Iterating the design (new instruction, deeper pipeline)		Re-run, still times out

How the three approaches compare on the paper's embedded-class targets. The per-instruction synthesis times and the roughly 10-percent (about 3-percent after optimization) gate overhead are from the paper's RISC-V case study; the whole-design timeout is the reported over-3-hour result the per-instruction optimization avoids.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The headline is real and clean: a designer draws only the datapath, and correct control logic for a whole embedded RISC-V core — base integer instructions plus cryptography extensions — is generated in seconds, correct-by-construction against a formal specification, with the constant-time cryptography core verified to spend the same number of cycles regardless of input length (a genuine security property) and to match a hand-written reference cycle for cycle. Read that against the limits. The per-instruction speedup that makes it practical depends on the control having no feedback between instructions, so out-of-order execution is out of scope. Solve times still explode on large designs, so only small embedded cores are shown. The generated circuit uses about ten percent more gates than a human’s (three percent after optimization) and is an unreadable netlist. And the designer still must write and maintain an ILA specification, a PyRTL sketch, and an abstraction function. The contribution is a compelling proof that program synthesis can own the most bug-prone half of small, trusted hardware designs — not a claim that it replaces hand design at scale.

Background

Why bother automating control for tiny embedded chips

It is worth asking why so much machinery targets small cores rather than big server CPUs. The answer is where the stakes are. Embedded systems-on-chip sit at the foundation of critical infrastructure — remote surgical equipment, telecommunications satellites, the root-of-trust chips that gate access to larger compute and storage. In those settings a single control bug is not a slowdown but a potential catastrophe, and the designs are often bespoke: a custom instruction for a cryptographic routine, a constant-time core built to leak nothing through timing, an accelerator for one algorithm. These are exactly the designs no push-button generator anticipates, so they are hand-built, and hand-built control is where correctness slips. That world — small, sophisticated, security-critical processors whose value is that a team can tailor the microarchitecture and still trust it — is the same world the open programmable RISC-V hardware work covered elsewhere on this site inhabits, where owning and modifying the core down to the microarchitecture is the whole point. Making the trusted half of such a design correct-by-construction, and fast to re-derive on every iteration, is what turns agile hardware from an aspiration into a workable process precisely where the cost of a mistake is highest.

If you remember only three things

1. A chip splits into a datapath (the machinery that moves and crunches data) and control logic (the signals that steer it cycle by cycle), and the control is the bug-prone half that eats roughly half of all verification time and must be re-derived by hand on every design iteration; this paper introduces control logic synthesis, where the designer writes only the datapath sketch and leaves the control as holes.
2. A program-synthesis engine fills those holes with control logic that provably satisfies a formal ILA specification, making it correct-by-construction: the datapath sketch is lowered to an IR called Oyster, Rosette automatically lifts its concrete interpreter to a symbolic one, an abstraction function records read/write timing so pipelining is expressible, and an SMT solver finds hole values that meet each instructions pre- and postconditions.
3. The key to tractability is synthesizing control independently per instruction and unioning the pieces, valid because the control has no feedback between instructions — which cuts the whole RISC-V integer ISA from an over-three-hour timeout to about 6.6 seconds; it is demonstrated on an embedded RISC-V core with crypto extensions, a constant-time cryptography core, and an AES accelerator, though the generated circuit runs about ten percent larger, solve times still explode on big designs, and out-of-order execution is out of scope.

Check yourself

Check your understanding

1. What does the designer write, and what does control logic synthesis generate?
2. Why does the tool synthesize control logic independently for each instruction instead of all at once?
3. What role does Rosette play in the toolchain?
4. Which qualification most affects how the results should be read?

Sources

The paper is “Control Logic Synthesis: Drawing the Rest of the OWL” by Zachary D. Sisco, Andrew David Alex, Zechen Ma, Yeganeh Aghamohammadi, Boming Kong, Benjamin Darnell, Timothy Sherwood, Ben Hardekopf, and Jonathan Balkind, published at ASPLOS 2024 (Volume 4), DOI 10.1145/3622781.3674170. Most authors are at the University of California, Santa Barbara; Benjamin Darnell is at the University of Illinois Urbana-Champaign. The work is licensed CC-BY-NC-SA.

This explainer is written from the full 16-page text. Everything above comes from the paper’s own sections: the introduction framing the control-datapath split, the verification burden, and the goal of correct-by-construction control for embedded root-of-trust SoCs; the background defining datapath versus control logic and the two control classes (instruction decoders and finite state machines) with the ALU decode and accumulator FSM examples; Section 3’s toolchain (the ILA specification, the PyRTL datapath sketch with holes, the abstraction function, the Oyster IR and its grammar, and Rosette lifting the interpreter to symbolic form) and the per-instruction synthesis with the union operator and its correctness argument; Section 4’s three case studies (the single-, two-, and three-stage embedded RISC-V core with the Zbkb/Zbkc crypto extensions, the constant-time cryptography core with CMOV and the SHA-256 constant-cycle result, and the AES-128 FSM accelerator with its lookup tables modeled as immutable vectors); and Section 5’s results and limitations, including the over-three-hour whole-ISA timeout versus about 6.6 seconds per-instruction, the roughly ten-percent (about three-percent after Yosys) gate overhead against a hand-written reference, and the discussion of solve-time explosion, the instruction-independence assumption, and the netlist-like unreadable output.