PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency

To formally prove a processor gets its memory-ordering rules right, engineers must first hand-write a precise mathematical model of those rules — tedious, error-prone work that most hardware architects lack the formal-methods training to do, and existing tools that automate it only work once the chip's detailed design is finished, too late to catch bugs cheaply; this work from Berkeley and Michigan builds PipeSynth, which instead generates the formal ordering rules automatically, before any implementation exists, from small test programs and simulator traces an engineer already understands, letting a solver synthesize most of a processor's memory-ordering specification for them.

The argument in one glance

Problem

Formal verification needs a formal spec nobody wants to write

Proving a processor gets its memory-ordering rules right requires first writing a formal specification — a precise mathematical model of those rules. For memory ordering this is a memory consistency model, which is notoriously hard to get right, and today these specs are mostly hand-written by engineers who usually lack formal-methods training. That makes them tedious, error-prone, and a barrier to using formal verification at all.
What people did

Auto-synthesize the spec from the finished design

Existing tools can synthesize a formal microarchitecture specification automatically, sparing engineers the hand-writing. They do it by reading the processor's completed low-level implementation code.
Why it fell short

Using the finished implementation is too late

Because those tools need the finished implementation, the formal spec only appears after the design is built. By then any design bugs are already baked into an implementation that took real effort to create, so that effort is wasted, and the whole point of formal verification — catching bugs early and cheaply — is lost.
This paper's idea

Synthesize ordering axioms before implementation (PipeSynth)

PipeSynth automatically synthesizes formal microarchitectural ordering axioms before any implementation exists, from inputs engineers already understand: small test programs (litmus tests) and simulator execution traces. It encodes the task as syntax-guided synthesis with a novel template, and lets a solver fill in the missing axioms so the spec forbids the forbidden behaviors and allows the required ones. It synthesizes 42 of 46 axioms across four microarchitectures.

Why this problem is worth solving

Verifying a processor is only possible if you first describe it formally, and that description is the bottleneck.

Formal verification uses mathematics to prove a system obeys a property, and it is increasingly important for processors, where verification now dominates the cost of hardware design. But every formal verification approach needs a formal specification: a precise mathematical model of the design being checked. For the behavior of memory in a parallel processor, that specification is a memory consistency model. A memory consistency model states the ordering rules governing memory and synchronization operations across cores — concretely, which values a load instruction is allowed to return. The simplest is sequential consistency, where all memory operations appear to happen in one total order that respects each core’s program order. Real processors relax this for speed, and their memory consistency models are notoriously difficult to specify, because the complexity of a modern pipeline creates a great many corner cases that the rules must account for. Today these specifications are mostly written by hand, which is tedious and error-prone, and the situation is worse because most architects and hardware engineers do not have formal-methods training, so writing a correct formal specification is a serious barrier for them. And a specification that is wrong in the unsafe direction is dangerous: if it is weaker than the real design, verification can pass while the actual hardware is buggy.

There is a working way to verify such models, but the automation for building the spec comes too late.

A line of tools called Check established how to formally verify memory ordering at the microarchitectural level. They represent an execution of a small test program as a graph of happens-before relationships — call it an ordering graph. Each node is a sub-event, one instruction at one pipeline stage, such as an instruction being fetched, or decoded-and-executed, or written back. Each edge means one event must happen before another. Because an edge is a happens-before relation, a cycle in the graph would mean some event has to happen before itself, which is impossible — so a cyclic graph represents an execution the hardware can never produce, and an acyclic graph represents one it can. The microarchitecture is described by a specification made of axioms: each axiom is one small ordering rule saying when edges must be added to the graph — for example, that if one instruction is fetched before another, it must also be decoded-and-executed before that other. To verify a test, the tool instantiates the axioms and uses a solver to search for an acyclic graph satisfying all of them; if a test that should be impossible turns out to have such a graph, the design is buggy. This works well, but it still needs the axioms. Existing automation that synthesizes those axioms reads the finished implementation, so the formal model only exists after the design is built, and any design bugs are already there and expensive to fix.

What people did before, and where it broke

Hand-write the ordering axioms. Have an engineer write the formal memory-ordering specification directly. Where it broke. It is tedious and error-prone for complex pipelines, and most architects lack the formal-methods training to do it, so few specifications get written at all.
Synthesize instruction-set-level specs (MemSynth). Automatically synthesize the memory consistency model at the instruction-set level. Where it broke. It produces the higher-level, architecture-level model, not the detailed microarchitectural ordering specification needed to verify a specific pipeline design.
Synthesize microarchitectural specs from the implementation (RTL-based tools). Read the finished low-level hardware description to derive a microarchitectural spec. Where it broke. The spec appears only after implementation, so it cannot catch design bugs early; the engineers have already spent effort building a design that may be wrong.
The gap. No tool synthesized microarchitectural memory-ordering axioms before implementation, from examples an engineer can produce during design. Doing exactly that, from litmus tests and simulator traces via syntax-guided synthesis, is what PipeSynth provides.

How PipeSynth works

From hand-written or too-late axioms to pre-implementation synthesis

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

The idea

Generate the formal spec with a solver instead of writing it by hand. The heart of PipeSynth is to treat writing the ordering axioms not as a manual chore but as a synthesis problem: describe the space of possible axioms with a grammar, state the correctness conditions, and let a solver find axioms that satisfy them. This is syntax-guided synthesis, and it turns an expert-only task into one an engineer can drive with examples. Replacing a laborious, error-prone hand-written artifact with one a solver produces from a grammar and a specification is the same move the sketch-guided hardware-mapping work covered elsewhere on this site makes, describing the space with a template and asking a solver to fill it rather than writing the mapping rules by hand.

Let a solver fill a carefully-shaped template. A solver cannot synthesize these ordering axioms from a naive description — the axioms have a structure that generic synthesis cannot express. PipeSynth’s contribution is a novel conjunct-based encoding, with reusable templates for common axiom types, that places solver-fillable holes in the right shape so the solver can complete them. Casting the job as filling the blanks of a well-designed template with a solver, rather than searching an unstructured space, is the same technique the solver-driven traversal-synthesis work covered elsewhere on this site relies on, encoding the problem as a template whose holes a constraint solver completes.

Catch the bug before the design is built. The reason to synthesize the spec pre-implementation is timing: a formal model that only exists after the low-level design is finished can only find bugs once the buggy design has already been built, wasting the effort spent on it. PipeSynth produces the specification from simulator traces during design, so verification can flag ordering bugs before implementation begins. Moving bug-finding earlier in the hardware timeline, so flaws are caught before they are cast into a costly artifact, is the same shift-left instinct the pre-silicon processor-fuzzing work covered elsewhere on this site pursues, hunting bugs at the design stage precisely because a flaw fixed before manufacture is far cheaper than one found after.

Following an axiom being synthesized

Synthesizing the missing ordering axiom for a message-passing test

Tracing one synthesis shows how examples become a formal axiom.

Step 1 of 5

A missing axiom in a partial spec

An engineer has a formal ordering spec for a simple in-order pipeline but has not written the axiom that keeps the decode-and-execute stage in order. They leave a placeholder for it.

The other axioms are present; only this one is a hole to fill.

Why it works

Formal verification needs a spec nobody wants to write. Because verifying a processor requires a formal ordering model, and those are hand-written by engineers who often lack formal-methods training → the specs are tedious, error-prone, and a barrier to verification → so automating their creation widens the use of formal methods.
Waiting for the implementation wastes effort. Because existing synthesis reads the finished low-level design → it can only produce a spec after the design is built, too late to catch design bugs cheaply → so synthesizing before implementation, from simulator traces, catches bugs before effort is spent building them.
Examples are the language engineers speak. Because litmus tests and execution traces are formats architects already use → PipeSynth takes those as input and produces the formal axioms from them → so an engineer specifies allowed and forbidden behavior without writing formal logic.
Forbidden tests alone are not enough. Because an axiom that forbids every execution trivially satisfies the forbidden tests → required tests with execution traces are needed as a witness of how a legal run should execute → so the synthesized axioms reflect real orderings rather than a nonsensical rule forbidding everything.
A tailored encoding makes the solver succeed. Because naive syntax-guided synthesis cannot express these ordering axioms → a novel conjunct-based encoding with templates lets the solver fill the placeholders → so PipeSynth synthesizes 42 of 46 axioms and a whole in-order specification in under an hour.

What it costs (trade-offs and scope)

The engineer still supplies inputs and structure. PipeSynth needs a partial specification with placeholders, a set of forbidden litmus tests, and execution traces. This is far easier than writing axioms in formal logic, but it is not zero effort, and it asks the engineer to choose or design the axiom templates.
It is not fully complete. PipeSynth synthesized 42 of the 46 evaluated axioms; some axioms fall outside its built-in templates and require custom templates, and some could not be synthesized under the parameters used, so it augments rather than entirely replaces human expertise.
Synthesis can be slow. Single-axiom synthesis took up to about two hours per axiom, and synthesizing many axioms at once is harder. The approach trades human effort for solver time, which is bounded but real.
Quality depends on the tests and traces. The synthesized axioms only reflect the behaviors the provided litmus tests and traces exercise; gaps in the test set can leave the specification under-constrained, so good coverage of orderings matters.
It targets ordering axioms in one formalism. PipeSynth synthesizes axioms in a specific microarchitectural-ordering language, over happens-before graphs. It addresses memory-ordering specification, not every kind of correctness property a processor must satisfy.
A synthesized spec must still be trusted appropriately. The output is only as sound as the forbidden tests and required traces that define correctness; if those inputs are wrong, the synthesized specification can be wrong in the same way.

The evaluation

Three ways to get a formal microarchitectural ordering spec

Property	Hand-written	Synthesis from implementation
Who writes the axioms		Tool, from the design
Needs formal-methods expertise		Less
Available before implementation	Yes but manual
Catches design bugs early	If the spec is right
Demonstrated coverage	Depends on effort	Not applicable

Three ways to obtain a formal microarchitectural memory-ordering specification, evaluated on four microarchitectures including an out-of-order processor and one with a non-traditional coherence protocol. Hand-writing the axioms is tedious, error-prone, and needs formal-methods skill most architects lack. Existing automated synthesis reads the finished low-level implementation, so the specification arrives too late to catch design bugs cheaply. PipeSynth instead synthesizes the ordering axioms before implementation, from forbidden litmus tests and allowed simulator execution traces, by encoding the task as syntax-guided synthesis with a novel conjunct-based template that a solver fills. In single-axiom synthesis it produced replacement axioms for 42 of the 46 evaluated axioms in under two hours each, and in multi-axiom synthesis it produced an entire specification for the in-order Multi-V-scale processor in under an hour and at least four nontrivial axioms at once for the others. The tool is open-source.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

PipeSynth is a well-targeted formal-methods contribution: it attacks the real bottleneck in verifying processor memory ordering, which is not the verification algorithm but the formal specification someone has to write first. Its idea is to synthesize that specification with a solver, framing the problem as syntax-guided synthesis, and its technical contribution is a novel encoding and templates that make such synthesis feasible for microarchitectural ordering axioms, which naive synthesis cannot handle. Two things make it practical. It works before implementation, from litmus tests and simulator traces rather than finished design code, so it can catch ordering bugs while they are cheap to fix. And it takes inputs architects already understand, lowering the barrier for engineers without formal-methods training. The results are solid: across four microarchitectures, including an out-of-order processor and one with a non-traditional coherence protocol, it synthesized 42 of 46 axioms, and an entire in-order specification in under an hour. Read it with its scope. It is not fully complete — a few axioms needed custom templates or could not be synthesized, so it augments rather than replaces human effort. Synthesis can take up to a couple of hours per axiom, the engineer still supplies partial specs, tests, and traces, and the quality of the result depends on the coverage of those inputs. And it targets memory-ordering axioms in one formalism, not every processor property. The durable idea is that when the hard part of verification is writing the specification, turning that into a synthesis problem driven by familiar examples can make formal verification accessible far earlier and to far more engineers.

Background

Why turning specification into synthesis keeps unlocking verification

It helps to see PipeSynth within a broader movement in hardware correctness: the barrier to formal verification is usually not the proving but the specifying, and the way past it is often to generate the formal artifact with a solver from something people can more easily provide. Here the artifact is a set of memory-ordering axioms, and the easier input is litmus tests and traces. The formal graphics-processor memory-model work covered elsewhere on this site works the same seam from the other side, giving memory consistency a precise, checkable form so that real code can be verified against it — in both cases the leverage comes from making the elusive, corner-case-ridden rules of memory ordering into something a machine can reason about rather than something only an expert can hand-write. The common thread is that memory consistency is one of the hardest things in computing to get right, riddled with subtle orderings, and progress comes from tools that either construct or check the formal rules automatically. The general lesson is that as designs grow more complex, the value of verification is gated by how cheaply and how early a trustworthy specification can be produced, and that reframing specification as synthesis — from examples, before implementation — pushes both the cost down and the timeline earlier, which is exactly where catching a bug is worth the most.

If you remember only three things

1. Formally verifying a processor's memory ordering requires a formal specification — a memory consistency model, the rules governing what values a load may return in a parallel program — which is notoriously hard to get right because of countless corner cases. Today these are mostly hand-written, which is tedious and error-prone, and most hardware architects lack the formal-methods training to write them. Existing tools that synthesize such specifications automatically read the processor's finished implementation, so the spec arrives too late to catch design bugs cheaply, after effort has already been spent building a possibly-buggy design.
2. PipeSynth automatically synthesizes formal microarchitectural ordering axioms before implementation, from inputs engineers already understand: a partial specification with placeholders, forbidden litmus tests (small programs that must be impossible), and allowed execution traces from a pre-implementation simulator. It encodes the task as syntax-guided synthesis — a grammar bounds the possible ordering rules and a solver searches for ones satisfying the constraints — using a novel conjunct-based encoding with templates, because naive synthesis cannot express these axioms. Required traces are essential: without them, an axiom that forbids everything would trivially pass, so traces witness how a legal run should execute.
3. Across four microarchitectures (including an out-of-order processor and one with a non-traditional coherence protocol), PipeSynth synthesized replacement axioms for 42 of 46 axioms in under two hours each, and synthesized an entire specification for the in-order Multi-V-scale processor in under an hour, plus at least four nontrivial axioms at once for the others; it is open-source. Its scope: it is not fully complete (a few axioms needed custom templates or could not be synthesized), synthesis can be slow, the engineer still supplies partial specs and tests, result quality depends on test and trace coverage, and it targets memory-ordering axioms in one formalism rather than every processor property.

Check yourself

Check your understanding

1. Why is writing the formal specification, rather than running the verifier, the main bottleneck for verifying processor memory ordering?
2. Why is synthesizing the spec from the finished implementation (as prior tools do) too late?
3. PipeSynth is given forbidden litmus tests. Why does it also need allowed execution traces?
4. PipeSynth synthesized 42 of 46 axioms, not all of them. How should this be read?

Sources

The paper is “PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency” by Chase Norman, Adwait Godbole, and Yatin A. Manerkar, published at ASPLOS 2023, DOI 10.1145/3582016.3582056. The authors are at the University of California, Berkeley, and the University of Michigan. The tool is open-source.

This explainer is written from the full text of the paper, obtained from the last author’s University of Michigan copy, which matches the ASPLOS 2023 proceedings. Everything above comes from the paper’s own sections: the introduction and motivation on the difficulty of hand-writing formal specifications (memory consistency models being notoriously hard to specify and the lack of formal-methods training among architects) and on the limitation of existing synthesis tools that require a completed implementation; the background on microarchitectural memory-consistency verification (litmus tests, the happens-before graphs whose acyclicity determines observability, and the ordering axioms of the microarchitectural-ordering language that dictate when edges are added, with the message-passing test and sequential consistency as examples) and on syntax-guided synthesis with a grammar and a satisfiability-modulo-theories solver; the PipeSynth design (its three required inputs of a partial specification with placeholder functions, forbidden litmus tests, and observable execution traces from a pre-implementation simulator, the need for required tests and traces to avoid the trivial forbid-everything axiom, the litmus-test generation of boundary tests, and the novel conjunct-based encoding with reusable and custom templates that makes microarchitectural-ordering-axiom synthesis feasible); and the evaluation across four microarchitectures including an out-of-order processor and one with a non-traditional coherence protocol, reporting single-axiom synthesis of replacement axioms for 42 of 46 axioms in under two hours each, and multi-axiom synthesis of an entire specification for the in-order Multi-V-scale processor in under an hour and at least four nontrivial axioms at once for the others.