Formal Verification of an ASML EUV Wafer Stepper

Extreme Ultraviolet Lithography (EUV) wafer steppers are among the most complex machines in manufacturing. Their throughput depends on parallel behaviors—robots moving wafers, doors cycling, and chambers pumping down. But concurrency is dangerous: if a door opens under a pressure differential, catastrophic damage can result.

This post shows how formal methods help verify such systems. Starting with Milner’s CCS for modeling concurrency, touching LTL for linear-time properties, and culminating in the modal µ-calculus, we express and check safety-critical requirements on a wafer stepper controller. The project models a simplified ASML wafer stepper and extracts three core requirements that guard vacuum integrity.

Background: CCS, LTL, and why µ-Calculus

CCS (Calculus of Communicating Systems, Milner).
A process algebra for describing concurrent systems via atomic actions and composition. Key operators:

• Parallel composition to run processes concurrently.
• Hiding to make internal actions invisible (τ).
• Renaming to refactor action labels for composition.

LTL (Linear Temporal Logic).
Expresses properties along a single execution trace:

• $G\,p$ (“always”)
• $F\,p$ (“eventually”)
• $p\,U\,q$ (“until”)

Powerful for liveness and invariants on linear paths, but not inherently branching.

Modal µ-Calculus.
A highly expressive branching-time logic that subsumes CTL and can encode many LTL/CTL properties. It adds:

• Fixpoints: least ($\mu$) for eventualities, greatest ($\nu$) for invariants.
• Modalities: $[a]\varphi$ and $\langle a\rangle\varphi$ (for all/exists next via action $a$).
• Abstraction: naturally pairs with CCS operators like hiding/renaming.
• Branching bisimulation: two systems are equivalent if they satisfy the same µ-calculus formulae (under appropriate modalities), supporting compositional reasoning.

Motivation and modeling assumptions

EUV steppers integrate sluices, low-vacuum and high-vacuum chambers, doors (gates), and robots. Errors are costly: damaged hardware, contaminated chambers, or hours of downtime. To make the model analyzable we adopt standard assumptions:

1. Atomic actions for door operations and robot moves.
2. Pressure domains: ambient ($p_A$), low ($p_L$), high ($p_H$); each chamber has an allowed set.
3. Instant communications for control signals (no delays in the model).

With these, a CCS/mCRL2-style model captures concurrency; a µ-calculus property set checks the safety envelope.

Figure: Wafer-stepper schematic

The system of interest is:

High-level requirements

• Doors must respect pressure discipline.
• Airlocks (sluices) behave as true airlocks.
• The low-vacuum chamber isolates from both sides except in controlled transitions.
• Robots only move wafers through permitted door/chamber configurations.
• No configuration simultaneously compromises low-vac and high-vac boundaries.

From the full set, the three most important formal requirements for safety and correctness are:

1) Pressure equalization before opening any door
“Any door can open only if the pressures on both sides are equal.”

2) Sluice door interlocks
“Any sluice may have at most one door open at a time.”

3) Low-vacuum chamber exclusivity
“The low-vac chamber may be open either to high-vac or to the sluices, but never both.”

These invariants prevent catastrophic pressure breaks and enforce proper chamber isolation.

µ-Calculus crash course (just enough to read the specs)

• State predicates: Boolean conditions over the current state (e.g., a door is open, a chamber has pressure $p_L$).
• Actions / modalities: $[a]\varphi$ means “after all $a$ transitions, $\varphi$ holds”; $\langle a\rangle\varphi$ means “there exists an $a$ transition to a state where $\varphi$ holds.”
• Fixpoints:
  • Greatest fixpoint $\nu X.\,\Phi(X)$ captures “always”/invariants (closed under future behavior).
  • Least fixpoint $\mu X.\,\Phi(X)$ captures “eventually”/reachability.

For safety properties like ours, we’ll mostly use $\nu$ (greatest fixpoint) to assert invariants are maintained on all paths.

Operators you’ll see (abstraction tools)

• Hiding ($\tau$): internalizes an action so environment cannot observe it (useful to ignore robot micro-steps).
• Renaming: maps action labels so multiple sub-components can be composed under a shared interface.
• Synchronization (in CCS parallel composition): combines complementary actions (e.g., door command + door sensor) into a single visible step, often then hidden.

These let us state properties over a clean interface while abstracting away internal chatter.

The three core invariants in modal µ-Calculus

The following are the three most important requirements from the wafer stepper specification, stated exactly as in the source and expressed in modal µ-calculus.

R1 — Pressure Equalization

Requirement:
“Any door can only open if the pressure on both sides is equal.”

µ-calculus formula:

1
2
3
4
5
6
7
8
9
νX (PcI:Pressure = pA, PcL:Pressure = pL, PcO:Pressure = pA) . (
  (∀p:Pressure . [set_pressure(cI, p)] X(p, PcL, PcO)) ∧
  (∀p:Pressure . [set_pressure(cL, p)] X(PcI, p, PcO)) ∧
  (∀p:Pressure . [set_pressure(cO, p)] X(PcI, PcL, p)) ∧
  [¬∃p:Pressure, c:Chamber . set_pressure(c, p)] X(PcI, PcL, PcO) ∧
  [instruct_door(dLI, sO)] (PcI = PcL) ∧
  [instruct_door(dLO, sO)] (PcO = PcL) ∧
  [instruct_door(dH,  sO)] (pH  = PcL)
)

R2 — Sluice Door Interlock

Requirement:
“Any sluice can have at most one door open at a time.”

µ-calculus formula:

1
2
3
4
5
6
7
8
9
10
11
νX (SdAI:DoorState = sC, SdAO:DoorState = sC,
    SdLI:DoorState = sC, SdLO:DoorState = sC) . (
  (∀ds:DoorState . [instruct_door(dAI, ds)] X(ds, SdAO, SdLI, SdLO)) ∧
  (∀ds:DoorState . [instruct_door(dAO, ds)] X(SdAI, ds, SdLI, SdLO)) ∧
  (∀ds:DoorState . [instruct_door(dLI, ds)] X(SdAI, SdAO, ds, SdLO)) ∧
  (∀ds:DoorState . [instruct_door(dLO, ds)] X(SdAI, SdAO, SdLI, ds)) ∧
  [instruct_door(dAI, sO)] (SdAO = sC) ∧
  [instruct_door(dAO, sO)] (SdAI = sC) ∧
  [instruct_door(dLI, sO)] (SdLO = sC) ∧
  [instruct_door(dLO, sO)] (SdLI = sC)
)

R3 — Low-Vacuum Chamber Exclusivity

Requirement:
“The low-vacuum chamber can either have the door to the high-vacuum chamber open or the door(s) to the sluice(s).”

µ-calculus formula:

1
2
3
4
5
6
7
8
νX (SdLI:DoorState = sC, SdLO:DoorState = sC, SdH:DoorState = sC) . (
  (∀ds:DoorState . [instruct_door(dLI, ds)] X(ds, SdLO, SdH)) ∧
  (∀ds:DoorState . [instruct_door(dLO, ds)] X(SdLI, ds, SdH)) ∧
  (∀ds:DoorState . [instruct_door(dH,  ds)] X(SdLI, SdLO, ds)) ∧
  [instruct_door(dH,  sO)] (SdLO = sC ∧ SdLI = sC) ∧
  [instruct_door(dLI, sO)] (SdH = sC) ∧
  [instruct_door(dLO, sO)] (SdH = sC)
)

Where CCS and abstraction help

• Use renaming to align door actions across subsystems (controller vs actuator), then synchronize and hide the internal handshake so your µ-calculus properties quantify only over the external event (e.g., instruct_door(..., sO)).
• Use hiding to abstract robot micro-motions so they do not pollute the property alphabet. Your safety invariants remain focused on door/chamber relations.

This keeps the property set stable even if you refactor internal implementation.

Practical notes for model checking

• State predicates like press(c)=p and open(d) should be modeled as part of the system state (e.g., booleans/enums) and updated by transitions.
• Enable conditions: You can enforce R1 by guarding door-open transitions with pressure equality. Then R1 becomes both a property and an implicit design contract (transition is disabled otherwise).
• Compositionality: Verify each requirement on the composed, abstracted system; also check on components with assume/guarantee contracts if your tool supports it.

Why µ-Calculus is the right tool here

• Branching safety: We need properties to hold across all possible interleavings of concurrent actions. Greatest fixpoints naturally express “always safe.”
• Abstraction friendliness: Hiding/renaming keep specs stable as internals evolve.
• Expressiveness: Airlock discipline and exclusivity constraints are succinct invariants; liveness (e.g., “eventually pump-down completes”) can be added with $\mu$ fixpoints.

Extensions (beyond the big three)

• Robot-aware guards: e.g., wafers must not cross an open boundary unless chamber pressures match.

• Pumpdown sequencing: eventually reach $p_H$ in $cH$ from $p_L$ in $cL$ when commanded:

  \[\mu Y.\ \langle pump\_step \rangle (press(cH)=p_H \lor Y)\]
• Bisimulation checks: show a refactored controller is branching-bisimilar to the original by constructing a relation and proving it satisfies the transfer conditions (or by using a tool’s equivalence checker).

Conclusion

By encoding (R1) pressure equalization, (R2) sluice interlock, and (R3) low-vac exclusivity in modal µ-calculus, we prove that dangerous states are unreachable under all concurrent interleavings. CCS gives us a disciplined modeling vocabulary; µ-calculus gives us the right proof language. The result is a controller that’s not just tested to work—it’s proven to uphold its safety envelope.

Exercise for readers

1. What if both sluice doors could be open together (while $dH$ is closed)?
   Update R3 accordingly. What additional guards would you add to maintain vacuum discipline?

2. Hiding and renaming:
   Hide the actuator-side events and rename controller commands so properties quantify only over instruct_door (interface-level). Show that your properties are unaffected by the change (invariance under abstraction).

3. From invariant to guard:
   Implement R1 as a transition guard in the model, re-check the property, and compare state-space size and verification time.

• Previous
  Petri-nets, SDFs, and Markov Chains
• Next
  Automata Theory — From Finite Machines to Complexity