TLA+ for Hardware: Proving the Protocol Before the RTL Exists

A companion to the verification steps in the ASIC design flow. That article covers simulation, formal property checking and emulation — everything that acts on RTL. This one is about the level above: the protocol and the global state machine, which are decided months before any RTL exists and are where the expensive mistakes are made.

There is a specific kind of bug that survives every gate in a modern flow. It passes lint, because the code is clean. It passes formal property checking, because each module satisfies its own assertions. It passes constrained-random simulation with full functional coverage, because the testbench exercises every scenario anyone thought to define. It reaches silicon, and then a rare interleaving of three independent agents puts the system in a state the architecture never anticipated.

It survives because every one of those tools reasons about the implementation, and the error is in the design. The RTL faithfully implements a protocol that was wrong.

TLA+ is a notation and a model checker for the level above RTL: the protocol, the global state machine, the interaction between agents. It is not a hardware tool — it comes from distributed systems, and its best-known users are cloud infrastructure teams — but a cache coherence protocol, a power-domain sequence and a multi-master arbiter are distributed-systems problems wearing a different hat. The state space is concurrent, the interleavings are adversarial, and the failures are exactly the ones a simulation is least likely to find.

1. What it actually is

TLA+ is a specification language. You describe a system as a state machine: what the variables are, what the initial states are, and what steps are allowed. Then you state properties that must hold, and a tool checks them.

Three pieces, and it is worth keeping them distinct:

For hardware use, the realistic combination is PlusCal or TLA+ for the model, TLC for the checking. TLAPS is a research-grade commitment and almost never what a chip project needs.

The important property: TLC is exhaustive over the instance you give it. Not random, not sampled, not directed. If you tell it there are three requesters and two credits, it visits every reachable configuration of that system and every interleaving of the steps. When it says an invariant holds, it holds — for that instance.

That last clause is the whole discipline, and section 6 is about it.

2. The two kinds of property

Everything you will want to state falls into one of two categories, and they behave very differently.

Safety — “nothing bad happens.” An invariant: a predicate true in every reachable state. A counterexample is a finite trace ending in a state where it is false. These are the properties you will write most of, and TLC finds violations of them quickly.

$$\Box\, \mathrm{Inv} \qquad\text{— in every reachable state, } \mathrm{Inv} \text{ holds}$$

Liveness — “something good eventually happens.” A temporal property: every request is eventually granted, every powered-down domain is eventually restored. A counterexample is an infinite trace — a cycle in which the good thing never occurs.

$$\mathrm{Request} \rightsquigarrow \mathrm{Grant} \qquad\text{— every request LEADS TO a grant}$$

Liveness is where the interesting hardware bugs live, because starvation and deadlock are liveness failures, not safety failures. An arbiter that never grants anything satisfies every safety property you can write about it: it certainly never grants two masters at once. Checking liveness costs considerably more than checking safety, and it requires you to state your fairness assumptions explicitly — which is itself a useful exercise, because it forces you to say out loud what you are assuming about scheduling.

3. A worked example: power-domain sequencing

This is a good first hardware use of TLA+ because the failure is real, the state space is small, and the bug is one that RTL verification structurally struggles to find.

From the silicon power article: a power domain cannot simply be switched off. Its outputs must be isolated first, or its floating outputs corrupt the live domain next to it; state that must survive must be retained first; and on the way back up the order reverses. The legal combinations are the power state table, and UPF describes the intent. What UPF does not do is prove that your controller respects it under every interleaving of software requests, interrupts and hardware wake events.

The specification

---------------------------- MODULE PowerSequence ----------------------------
EXTENDS Naturals, FiniteSets

CONSTANTS Domains                  \* e.g. {"cpu", "gpu", "npu"}

VARIABLES phase,                   \* per domain: ON, ISO, SAVED, OFF
          isolated,                \* isolation clamps asserted?
          retained                 \* state saved to the always-on supply?

vars == <<phase, isolated, retained>>

Phases == {"ON", "ISO", "SAVED", "OFF"}

TypeOK ==
  /\ phase    \in [Domains -> Phases]
  /\ isolated \in [Domains -> BOOLEAN]
  /\ retained \in [Domains -> BOOLEAN]

Init ==
  /\ phase    = [d \in Domains |-> "ON"]
  /\ isolated = [d \in Domains |-> FALSE]
  /\ retained = [d \in Domains |-> FALSE]

Isolate(d) ==
  /\ phase[d] = "ON"
  /\ phase'    = [phase    EXCEPT ![d] = "ISO"]
  /\ isolated' = [isolated EXCEPT ![d] = TRUE]
  /\ UNCHANGED retained

Save(d) ==
  /\ phase[d] = "ISO"
  /\ phase'    = [phase    EXCEPT ![d] = "SAVED"]
  /\ retained' = [retained EXCEPT ![d] = TRUE]
  /\ UNCHANGED isolated

PowerDown(d) ==
  /\ phase[d] = "SAVED"
  /\ phase' = [phase EXCEPT ![d] = "OFF"]
  /\ UNCHANGED <<isolated, retained>>

PowerUp(d) ==
  /\ phase[d] = "OFF"
  /\ phase' = [phase EXCEPT ![d] = "SAVED"]
  /\ UNCHANGED <<isolated, retained>>

Restore(d) ==
  /\ phase[d] = "SAVED"
  /\ phase'    = [phase    EXCEPT ![d] = "ISO"]
  /\ retained' = [retained EXCEPT ![d] = FALSE]
  /\ UNCHANGED isolated

Release(d) ==
  /\ phase[d] = "ISO"
  /\ phase'    = [phase    EXCEPT ![d] = "ON"]
  /\ isolated' = [isolated EXCEPT ![d] = FALSE]
  /\ UNCHANGED retained

Next == \E d \in Domains :
          Isolate(d) \/ Save(d) \/ PowerDown(d)
       \/ PowerUp(d) \/ Restore(d) \/ Release(d)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
==============================================================================

Note what Next says: any domain may take any legal step at any time. Nothing sequences the domains relative to one another. That is deliberate — it is the adversary, and it is what a real system looks like when software, interrupts and a power controller are all running.

The properties

NeverOffWithoutIsolation ==
  \A d \in Domains : phase[d] = "OFF" => isolated[d]

NeverOffWithoutRetention ==
  \A d \in Domains : phase[d] = "OFF" => retained[d]

IsolationReleasedOnlyWhenOn ==
  \A d \in Domains : ~isolated[d] => phase[d] = "ON"

EventuallyRestored ==
  \A d \in Domains : (phase[d] = "OFF") ~> (phase[d] = "ON")

Run TLC on three domains and all three hold — 64 reachable states, explored exhaustively. Which is the point: the model is now a thing you can break on purpose. Delete the phase[d] = "ISO" guard from Save, as a tired engineer might when an unrelated bug seems to need a shortcut, and TLC returns a three-state trace — initial state, Save, PowerDown — ending in a domain at OFF with isolated[d] = FALSE. Two steps, and that trace is a directed test.

It breaks IsolationReleasedOnlyWhenOn as well, one state earlier, which is the more useful signal: the shortest counterexample points at the earliest place the reasoning went wrong, not at the invariant you happened to care about most.

The version that actually finds something

The specification above is too kind, because it assumes isolation and power-down are atomic. Real hardware has the isolation enable and the power switch on different control paths, with independent delays. Model that:

VARIABLES phase, isoReq, isoAck, powerSw

IsolateRequest(d) ==
  /\ phase[d] = "ON"
  /\ isoReq' = [isoReq EXCEPT ![d] = TRUE]
  /\ UNCHANGED <<phase, isoAck, powerSw>>

IsolateComplete(d) ==                  \* the clamps have actually closed
  /\ isoReq[d]
  /\ isoAck' = [isoAck EXCEPT ![d] = TRUE]
  /\ UNCHANGED <<phase, isoReq, powerSw>>

OpenSwitch(d) ==                       \* the controller cuts the supply
  /\ isoReq[d]                         \* <-- it waits for the REQUEST
  /\ powerSw' = [powerSw EXCEPT ![d] = FALSE]
  /\ UNCHANGED <<phase, isoReq, isoAck>>

The controller waits for the isolation request rather than the acknowledge. This is an extremely common real bug, it looks completely reasonable in RTL, and every module-level assertion about the isolation cell and about the power switch passes, because neither module is wrong. TLC finds it immediately:

State 1: isoReq = FALSE, isoAck = FALSE, powerSw = TRUE
State 2: IsolateRequest("cpu")   isoReq = TRUE
State 3: OpenSwitch("cpu")       powerSw = FALSE
         -- isoAck still FALSE: the clamps have not closed
Invariant NeverOffWithoutIsolation violated.

Three states. A simulation finds this only if the testbench happens to delay the isolation acknowledge past the switch decision — which is precisely the corner a directed test writer, who knows how the design is supposed to work, is least likely to write.

4. Where else it earns its keep on a chip

Cache coherence. The canonical application, and the one with the most published precedent. MSI, MESI and MOESI are small enough to specify in a page and have state spaces that no human reliably reasons about. Invariant: no two caches hold the same line in a writable state. Invariant: a line in Modified is absent or Invalid everywhere else. These are one-liners in TLA+ and are miserable to establish by simulation.

Credit-based flow control. Credits issued, credits consumed, credits returned, over a link with latency. Invariant: outstanding transactions never exceed buffer depth. Liveness: a sender with data eventually sends. The classic bug is a credit-return race that loses a credit under a specific interleaving, and the system then works perfectly but slightly slowly, for ever.

Arbitration and QoS. Safety is easy: never grant two masters. Liveness is the whole problem — a priority scheme with no ageing starves the lowest requester under sustained load, and the fairness property makes it visible in seconds.

Reset and clock-domain handoff. Which blocks may be reset independently, what happens if a reset arrives while a transaction is in flight, whether a domain can be released before its clock is stable. Sequencing questions, and the state space is small.

Safety-mechanism interaction. For an ISO 26262 item: does a fault detected in one channel drive the system to a safe state under every interleaving with a concurrent fault in the detector itself? This is a protocol question, and the answer belongs in the safety case as an argument rather than as a simulation count.

Boot and firmware handshakes. Secure boot, lifecycle state transitions, debug unlock. Here the adversary is not a scheduler but an attacker, and an exhaustive check over the protocol states is a genuinely different kind of evidence.

5. What it does not do, stated plainly

This is the section that matters most, because TLA+’s failure mode is over-claiming.

• It says nothing about your RTL. TLA+ proves the protocol is sound. Whether your Verilog implements that protocol is an entirely separate question and is what SVA, formal property checking and simulation are for. There is no automatic refinement path from a TLA+ model to RTL, and anyone who implies otherwise is selling something.
• There is no time. TLA+ has ordering, not duration. It cannot express a setup constraint, a clock frequency, or a timeout measured in nanoseconds. You can model a timeout as a state transition, but you are modelling the logic of the timeout, not its duration.
• There is no X, no metastability, no analog. A synchroniser is not a TLA+ problem. Neither is a reset that glitches.
• It proves the instance, not the design. Three domains checked exhaustively is not four domains checked. Section 6.
• The model can be wrong. The specification is written by the same people who wrote the spec, and it can faithfully encode the same misunderstanding. A model check proves internal consistency between your model and your properties — not that either matches reality.

Someone will ask why not simply use SystemVerilog Assertions and a formal property checker for all of this. The honest answer is that for module-level properties you should — they are better tools for that job, and they act on the real implementation. The gap is that they need RTL to exist, they work best within a module rather than across a whole system’s global state, and their state-space handling on a system-wide property usually does not converge. TLA+ fills the window before RTL and above the module.

6. State-space explosion, and how to live with it

The state space is the product of every variable’s domain across every agent. It grows brutally. Four techniques, in the order you should reach for them:

Shrink the instance. Three cache lines, not 1024. Two credits, not 64. Almost every protocol bug that exists at N exists at 2 or 3 — this is the small scope hypothesis, and it is empirical rather than proved, but it holds up remarkably well. A model that needs large numbers to show its bug is rare.

Exploit symmetry. If your domains are interchangeable, tell TLC so with a symmetry set and it will collapse permutations that differ only by naming. On a model with $n$ identical agents this is close to an $n!$ reduction, and it is usually the single biggest win available.

Constrain the state. A StateConstraint bounds exploration — no more than k outstanding transactions, counters below some limit. This is the dangerous one: you are telling the checker not to look somewhere, so anything you constrain away is unchecked. Write down what you excluded, and put it in the RTL coverage plan, which is why “state constraint” maps to “coverage point” in the handoff below.

Check safety first, liveness later. Safety checking is far cheaper. Get the invariants clean on a larger instance, then check liveness on a smaller one.

A practical scale: a protocol model that runs in under a minute is one you will iterate on and therefore one that will find bugs. A model that takes six hours is one you will run twice and abandon. Optimise for iteration speed over instance size — a small model you actually explore beats a large one you run once.

7. The handoff to RTL

A TLA+ model is not a deliverable. Its value is realised when each thing it produces becomes something in the RTL verification plan.

• Every invariant that survived becomes an SVA assertion bound to the RTL. You now know it is the right property, which is the part that is usually guesswork.
• Every temporal property becomes a liveness or cover property, and usually a watchdog in the testbench.
• Every counterexample trace becomes a directed test. This is the highest-value output of the whole exercise: a sequence that breaks the design, found by a tool, that no test writer would have composed.
• Every state constraint becomes a coverage point, because it marks a region the model check deliberately did not examine.

There is also a documentation benefit that is easy to undersell. A TLA+ specification is executable and unambiguous, which makes it a far better handover artifact than a protocol description in prose — particularly between an IP supplier and an integrator, where the assumptions of use are exactly the kind of thing that gets misread.

8. A method that fits a real project

1. Pick a target where the cost of being wrong is high and the state is global. Coherence, power sequencing, arbitration, a security handshake. Do not start with a datapath — TLA+ is poor at arithmetic and it is not what the tool is for.
2. Write the model before the RTL. The entire value proposition is finding the error while it is still a paragraph in a document.
3. Model the adversary, not the happy path. Let every agent take any legal step at any time. If you find yourself sequencing things to make the model behave, you are encoding the assumption you were trying to test.
4. State safety invariants first, and make sure they fail when you break the model on purpose. An invariant that passes against a deliberately broken model is checking nothing — the same two-sided discipline a safety mechanism needs in an FMEDA.
5. Then state liveness, with explicit fairness. Expect this to be where the real bugs are.
6. Shrink until it runs in under a minute. Iterate.
7. Hand off: invariants to SVA, traces to directed tests, constraints to the coverage plan.
8. Keep the model alive. When the protocol changes, change the model first. A specification that has diverged from the design is worse than none, because it is still being believed.

9. Tooling, briefly

All of it is free, which matters in a domain where the alternative costs per token. The real cost of TLA+ is the week it takes an engineer to become fluent, and that is the number to put in a plan — not the licence, which is zero, and not the runtime, which is minutes.

10. The pitfalls

• Modelling the happy path, then reporting that the protocol is correct.
• Constraining the state space until the bug is outside it, and not writing down what was excluded.
• Checking safety only, and missing the starvation that was the actual risk.
• Believing a green model check says something about the RTL.
• Writing a specification so detailed it is a second implementation — with its own bugs, and no faster to review than the first.
• Building the model after the RTL, when the answer can no longer change anything cheaply.
• Letting the model rot after the first protocol change.
• Using it on a datapath, where a formal property checker on the actual RTL is the better tool.

Glossary

Action — A relation between a state and its successor, written with primed variables: x' = x + 1. TLA+’s whole notion of “a step” is an action, which is why the language has no statements and no control flow in the programming sense.

Apalache — A symbolic model checker for TLA+ built on an SMT solver. Where TLC enumerates states explicitly, Apalache reasons about them symbolically, which makes some large-domain models tractable — at the cost of type annotations and more setup.

Fairness (weak / strong) — The assumption that an action which stays enabled will eventually be taken (weak), or that one enabled infinitely often will be (strong). Liveness properties are meaningless without a fairness assumption, and stating yours forces you to be explicit about what you assume the scheduler does.

Invariant — A predicate true in every reachable state: the safety half of a specification. Cheap to check and where most of the practical value sits.

Leads-to (~>) — The temporal operator for “whenever P becomes true, Q eventually becomes true”. The natural way to say “every request is granted” and therefore the natural way to state the absence of starvation.

Liveness — “Something good eventually happens.” Deadlock and starvation are liveness failures, not safety failures, which is why a design can satisfy every assertion you wrote and still hang.

Model checking — Exhaustive exploration of the reachable states of a finite instance. Exhaustive is the operative word: not sampled, not random, not directed — every reachable state of the instance you specified.

PlusCal — An algorithm-like syntax that compiles into TLA+. Easier to write for anyone with a programming background, with identical semantics, and it keeps the generated TLA+ in the same file so the translation stays visible.

Refinement — Proving that one specification implements another more abstract one. Powerful and expensive; in hardware practice the refinement step from TLA+ to RTL is done by SVA and simulation, not by proof.

Safety — “Nothing bad happens.” Violations have finite counterexamples, which is why they are found quickly and why you should write these first.

Small scope hypothesis — The empirical observation that most protocol bugs appear in very small instances. It is the justification for checking three agents rather than thirty, and it is empirical rather than proved — worth knowing which of those it is.

State constraint — A bound that tells the checker where not to look, used to keep a model tractable. The one mechanism here that can silently hide a bug, so anything you constrain away belongs in the RTL coverage plan.

Symmetry set — A declaration that certain model values are interchangeable, letting the checker collapse permutations that differ only by naming. Usually the single largest state-space reduction available.

TLC — The explicit-state model checker that ships with TLA+. The workhorse: it explores states, reports invariant violations with a trace, and finds liveness violations as cycles.

Temporal logic — Logic with operators about time-ordering — always ([]), eventually (<>), leads-to (~>). What lets a specification talk about sequences of states rather than single ones.

Related reading

• TLA+ for ISO 26262 functional safety — the same tool aimed at a safety argument rather than a protocol: a dual-channel redundancy spec, the two architectural bugs a model checker finds in it, and where that evidence sits in the V-cycle
• The ASIC design flow — where simulation, formal and emulation sit, and what each one can prove
• Silicon power usage — UPF, power state tables, and the sequencing the worked example above is checking
• The FMEDA work package — where a protocol argument lands in a safety case
• On-die signal integrity — the layer below, where timing and noise live

Further reading

Book links below are Amazon affiliate links: if you buy through one we earn a small commission at no extra cost to you. It does not influence what is recommended — the same books were on this list before the links were.

• Leslie Lamport, Specifying Systems — the definitive text, by the language’s author, and free from his own site. Dense; read it second.
• Hillel Wayne, Practical TLA+ — read it first. Engineer-facing, example-driven, and honest about where the tool does not help.
• Lamport’s Learn TLA+ video course and the TLA+ examples repository — the fastest route to a first working model, and the examples include several protocols worth reading before writing your own.
• Newcombe et al., “How Amazon Web Services Uses Formal Methods”, CACM 58(4), 2015 — the industrial case study that made the argument credible, with honest numbers on cost and on what it caught.
• Clarke, Grumberg and Peled, Model Checking — the theory underneath, if you want to know why state-space reduction works rather than just that it does.
• Erik Seligman, Tom Schubert and M V Achutha Kiran Kumar, Formal Verification: An Essential Toolkit for Modern VLSI Design — the RTL-level companion, and the right book for the handoff in section 7.

Have a protocol that works until three things happen at once, or a safety argument that needs to be an argument rather than a simulation count? That’s what we do. Reach us at circuit-design.space.