Compiler Verification and Equivalence Testing — Operating Quantum Computers

Quantum compilation is not a cosmetic rewrite. It changes gate sets, inserts routing operations, rewrites timing, maps logical to physical qubits, and may transform dynamic behavior. A compiler bug can produce a plausible distribution that is wrong enough to mislead and noisy enough to evade casual detection.

OpenQASM 3 is designed as a language for near-term algorithms with timing, pulse, and control-flow features [R138]. MQT QCEC provides quantum circuit equivalence checking and compilation-flow verification methods, while also noting that general quantum circuit equivalence is hard and cannot be treated as a trivial matrix comparison at scale [R139]. The operating lesson is clear: verification must be layered.

80.1 Compilation risk surface

Diagram loads as you read

80.1 Compilation risk surface · Figure 1

View diagram source

flowchart TB
    Compile[Compilation] --> Parse[Parsing and lowering]
    Compile --> Rewrite[Algebraic rewrite]
    Compile --> Layout[Qubit layout]
    Compile --> Routing[Routing and swaps]
    Compile --> Scheduling[Timing and scheduling]
    Compile --> Dynamic[Dynamic-control lowering]
    Compile --> Pulse[Pulse binding]

Each stage needs checks appropriate to the transformation it performs.

80.2 Equivalence is contextual

Diagram loads as you read

80.2 Equivalence is contextual · Figure 2

View diagram source

flowchart LR
    Source[Source program] --> Semantics[Declared semantics]
    Compiled[Compiled program] --> Target[Target semantics]
    Semantics --> Compare[Equivalence check]
    Target --> Compare
    Compare --> Verdict[Equivalent, bounded, or rejected]

A circuit can be equivalent under ideal unitary semantics and still fail under timing, noise, dynamic-control, or measurement semantics. The verification claim must say what it covers.

80.3 Verification layers

Diagram loads as you read

80.3 Verification layers · Figure 3

View diagram source

flowchart TB
    Verification[Verification layers] --> Syntax[Syntax and schema checks]
    Verification --> Type[Type and register checks]
    Verification --> Structural[Structural invariants]
    Verification --> Equiv[Equivalence checking]
    Verification --> Simulation[Simulation regression]
    Verification --> Hardware[Hardware canary]
    Verification --> Evidence[Evidence review]

No single layer is sufficient. Structural checks are cheap. Equivalence checks are stronger but may be limited. Hardware canaries are expensive but catch target-specific failures.

80.4 Compiler release gate

Diagram loads as you read

80.4 Compiler release gate · Figure 4

View diagram source

sequenceDiagram
    participant Dev as Compiler developer
    participant CI as Compiler CI
    participant Verify as Equivalence engine
    participant Sim as Simulator
    participant Canary as Hardware canary
    participant Registry as Compiler registry
    Dev->>CI: submit compiler change
    CI->>Verify: run equivalence suite
    CI->>Sim: run regression suite
    CI->>Canary: run selected hardware probes
    Canary-->>CI: target-specific signal
    CI->>Registry: publish approved compiler version

A compiler version should be a first-class artifact in every evidence package.

80.5 Invariant catalog

Diagram loads as you read

80.5 Invariant catalog · Figure 5

View diagram source

flowchart TB
    Invariant[Invariant catalog] --> Width[qubit and bit counts]
    Invariant --> Measurement[measurement mapping]
    Invariant --> Observable[observable mapping]
    Invariant --> Parameter[parameter binding]
    Invariant --> Control[control-flow semantics]
    Invariant --> Timing[timing constraints]
    Invariant --> Metadata[metadata preservation]

Many bugs are not deep quantum bugs. They are mapping, labeling, and metadata bugs. These are preventable.

80.6 Failure triage

Diagram loads as you read

80.6 Failure triage · Figure 6

View diagram source

flowchart LR
    Failure[Verification failure] --> SourceBug[Source bug]
    Failure --> CompilerBug[Compiler bug]
    Failure --> Unsupported[Unsupported target feature]
    Failure --> SpecGap[Spec ambiguity]
    Failure --> ToolBug[Verifier or simulator bug]
    Failure --> HardwareDrift[Hardware drift]

The triage path should preserve failing artifacts. Quantum compiler bugs are often difficult to reproduce once target profiles and dependencies change.

80.7 Certificate of compilation

Diagram loads as you read

80.7 Certificate of compilation · Figure 7

View diagram source

flowchart TB
    Certificate[Compilation certificate] --> SourceHash[Source hash]
    Certificate --> Compiler[Compiler version]
    Certificate --> Target[Target profile]
    Certificate --> Passes[Pass list]
    Certificate --> Checks[Verification checks]
    Certificate --> Limits[Known limits]
    Certificate --> Signature[Signature]

A compilation certificate records the claimed process, checks, and results. Its assurance depends on the trusted producer, verified signature, artifact binding, and validity of the checks; the certificate alone proves neither semantic equivalence nor physical result correctness.

80.8 Operating rule

Do not promote a compiler as “better” because it reduces depth. Promote it when it improves the workload under verified semantics, target constraints, and evidence requirements.

Diagram loads as you read

80.8 Operating rule · Figure 8

View diagram source

flowchart LR
    Improvement[Compiler improvement] --> Depth[Depth]
    Improvement --> Fidelity[Expected fidelity]
    Improvement --> Cost[Cost]
    Improvement --> Verified[Verified semantics]
    Verified --> Release[Release decision]

Additional technical sources: [R266].