Equivalence Checker for Dynamic Circuit fails🐛

[gideonuchehara]

Environment information

mqt-qcec version: 2.2.3 qiskit version: 0.25.1 C++ compiler: g++ (Ubuntu 11.4.0-1ubuntu1~22.04) 11.4.0 OS: DISTRIB_DESCRIPTION="Ubuntu 22.04.3 LTS"

Description

The following circuits, one static and the other dynamic, are supposed to be equivalent. But your equivalent check returned not_equivalent which is wrong. Why is this so? I guess the problem could be from the relabelling of the circuits when your equivalent checker converts from dynamic to static circuits before checking for equivalence. Could you please fix this? Copying @glassnotes.

from mqt import qcec
from qiskit import QuantumCircuit
import os

quantinuum_circ = QuantumCircuit(5)

quantinuum_circ.cx(1,2)
quantinuum_circ.cx(0,3)

quantinuum_circ.cx(1,4)

quantinuum_circ.cx(2,4)
quantinuum_circ.cx(3,4)

quantinuum_circ.measure_all()

quantinuum_circ.draw('mpl')

from qiskit import QuantumCircuit
quantinuum_dynamic_circ = QuantumCircuit(3, 5)

quantinuum_dynamic_circ.cx(0,1)
quantinuum_dynamic_circ.cx(0,2)
quantinuum_dynamic_circ.measure(0, 1)
quantinuum_dynamic_circ.reset(0)

quantinuum_dynamic_circ.cx(1,2)
quantinuum_dynamic_circ.measure(1, 2)
quantinuum_dynamic_circ.reset(1)

quantinuum_dynamic_circ.cx(0,1)
quantinuum_dynamic_circ.measure(0, 0)

quantinuum_dynamic_circ.cx(1,2)
quantinuum_dynamic_circ.measure(1, 3)
quantinuum_dynamic_circ.measure(2, 4)

quantinuum_dynamic_circ.draw('mpl')

config = qcec.Configuration()
config.optimizations.transform_dynamic_circuit = True
result = qcec.verify(quantinuum_circ, quantinuum_dynamic_circ, configuration=config)

# print the result
print(result.equivalence)

Below are two bv circuits as written in qiskit qasm that are supposed to be equivalent but failed the test. Note that I couldn't attach them as qasm file hence, I pasted them here.

First static circuit:

OPENQASM 2.0;
include "qelib1.inc";
qreg q[9];
creg meas[9];
h q[0];
h q[1];
h q[2];
h q[3];
h q[4];
h q[5];
h q[6];
h q[7];
h q[8];
z q[8];
cx q[0],q[8];
cx q[1],q[8];
cx q[3],q[8];
cx q[5],q[8];
cx q[6],q[8];
cx q[7],q[8];
h q[0];
h q[1];
h q[2];
h q[3];
h q[4];
h q[5];
h q[6];
h q[7];
barrier q[0],q[1],q[2],q[3],q[4],q[5],q[6],q[7],q[8];
measure q[0] -> meas[0];
measure q[1] -> meas[1];
measure q[2] -> meas[2];
measure q[3] -> meas[3];
measure q[4] -> meas[4];
measure q[5] -> meas[5];
measure q[6] -> meas[6];
measure q[7] -> meas[7];
measure q[8] -> meas[8];

The second dynamic circuit equivalent:

OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
creg c6[9];
h q[0];
h q[0];
measure q[0] -> c6[2];
reset q[0];
h q[0];
h q[0];
measure q[0] -> c6[4];
reset q[0];
h q[0];
h q[1];
z q[1];
cx q[0],q[1];
h q[0];
measure q[0] -> c6[0];
reset q[0];
h q[0];
cx q[0],q[1];
h q[0];
measure q[0] -> c6[1];
reset q[0];
h q[0];
cx q[0],q[1];
h q[0];
measure q[0] -> c6[3];
reset q[0];
h q[0];
cx q[0],q[1];
h q[0];
measure q[0] -> c6[5];
reset q[0];
h q[0];
cx q[0],q[1];
h q[0];
measure q[0] -> c6[6];
reset q[0];
h q[0];
cx q[0],q[1];
measure q[1] -> c6[8];
h q[0];
measure q[0] -> c6[7];

Expected behavior

No response

How to Reproduce

from mqt import qcec
from qiskit import QuantumCircuit
import os

config = qcec.Configuration() config.optimizations.transform_dynamic_circuit = True result = qcec.verify(quantinuum_circ, quantinuum_dynamic_circ, configuration=config)

I have included other qasm files to reproduce the error for dynamic circuits equivalence checking. Here is the result I got:

[burgholzer]

Many thanks for opening this issue. That seems like a big to me. I would guess it has to do something with the way the qubits are ordered after the transformation. I remember it wasn't really straight forward to decide how this should be done best. I'll come back to you once I know more 👍🏻

[gideonuchehara]

that's exactly what we suspected as well!

[burgholzer]

The primary underlying cause was really the initial layout of the transformed dynamic circuit. It turns out that it's not so easy to correctly guess the intended initial layout of the qubits at the beginning of the circuit.

346 introduces a new optimization pass that tries to derive a good guess for the initial layout by backpropagating the output permutation described by the measurements.

I added both instances from above as regression tests and added some further dynamic circuit tests on the C++ side using MQT Core's algorithm implementations of BV, QFT, QPE (and their dynamic variant). All of these can be successfully verified now (given the new backpropagate_output_permutation option).

I will probably add a couple more convenience features to QCEC over the next couple days and release a new version afterwards. Please let me know if you should encounter any further issues and feel free to re-open this one in case some new failures pop up.