Verifying Circuit Correctness

Every pass in this suite rewrites your quantum circuit in some way — decomposing gates, cancelling redundant operations, mapping qubits to a device. These transformations are meant to preserve exactly what your circuit does; only its representation should change. Verification is a built-in safety net that checks this automatically: it compares the circuit before a transformation to the circuit after, and tells you whether they are still equivalent.

You don’t need to write any extra code to use it — it’s a single flag you add to the mqss-opt command.

Why this matters

Compiler passes are ordinary code, and ordinary code can have bugs. A decomposition pass might use a slightly wrong rotation angle; a mapping pass might drop a gate while rewiring qubits. Without verification, a bug like this can silently produce a circuit that looks fine (it still parses and compiles) but no longer computes the same thing. Verification catches this class of bug automatically by checking equivalence rather than just checking that the output is well-formed.

Methods Used

We use the Checking methods from the MQT-QCEC library to perform Equivalence Checking. Specifically, we use the following methods:

• Alternating Equivalence Checker (using Decision Diagrams)

• Simulation Equivalence Checker

• ZX-Calculus Equivalence

Enabling verification

Add the --mqssci-verify flag to your mqss-opt invocation:

mqss-opt bell-state.qke --BasisConversionPass=gates=phased_rx,cz --mqssci-verify

It’s a plain on/off switch — pass --mqssci-verify to enable it, or leave it out for the default (off). When enabled, equivalence is checked after every pass in whatever you ran, so if you pass several passes at once, each one gets its own check.

Reading the output

When verification runs, it prints one line per quantum kernel (function) in your circuit, telling you whether the before-and-after circuits are equivalent:

[verify] __nvqpp__mlirgen__bellILm2EE: Equivalent

If a transformation changed what the circuit computes, this will instead say the circuit is NOT equivalent — that’s a signal that something in the pass pipeline you ran needs investigating. If a pass itself fails to complete (unrelated to equivalence — a crash, an illegal rewrite, etc.), verification is skipped for that pass and a message is printed instead explaining that the pass didn’t finish, so equivalence couldn’t be checked.

Where this fits

Verification works with any pass or pipeline you invoke on mqss-opt — a single pass, one of the preset pipelines, or an explicit -pass-pipeline=... string. See Passes for the full list of passes you can combine it with, and Running test circuits for more examples of invoking mqss-opt.

Note: --mqssci-verify is currently only available when invoking mqss-opt directly. The mqss-cc front-end wrapper does not yet expose it as a first-class flag.