Equivalence checking with a certain restriction

[ritu-thombre99]

Environment information

OS: MacOS
MQT version: 2.6.0
Compiler: C++

Description

I'm trying to compile circuits with a certain restriction that measurements can only be performed using certain qubits.

For example, in the following coupling map, measurement can only be performed using physical qubit 2

The input circuit is a GHZ state preparation:

After compiling:
Initial mapping (logical->physical) : 0->2, 1->1, 2->0

Logical qubit 0 is already mapped to physical qubit 2, so it is measured

But to measure logical qubit 1, it needs to be swapped with logical qubit 0 so that it is mapped to physical qubit 2

Hence, a SWAP is inserted between logical qubits 1 and 0 after measuring logical qubit 0

And the compiled circuit looks like below:

Is it possible to check equivalence of this compiling?

I tried with the following code:

from mqt import qcec
result = qcec.verify(circ, circ_comp, transform_dynamic_circuit=True,)

# print the result
print(result.equivalence)

Output: not_equivalent

I also tried running the equivalence with combinations of backpropagate_output_permutation=True and fix_output_permutation_mismatch=True, but the output is not_equivalent.

Sometimes it is equivalent

In a very particular case where logical qubit is mapped to physical qubit 0 (mapping of logical qubit 1 and 2 doesn't matter),
the circuits before and after compiling are equivalent

Expected behavior

Circuits should be equivalent in both the cases, not just when logical qubit 0 is mapped to physical qubit 0.

How to Reproduce

Import qiskit, mqt.qcec and the run the code/circuit blocks mentioned above.

[burgholzer]

I am fairly sure that QCEC cannot handle this special case at the moment.
What you are describing here is a dynamic circuit that contains mid-circuit measurements. So it needs some kind of transformation before being able to be checked.
I am fairly sure that QCEC currently messes up the initial layout or the output permutation when it tries to transform the circuits above.

I think this could be fixable in principle for cases like these with a combination of the optimization passes we have in place already.
I'll see what I can do once I am back from vacation.

[ritu-thombre99]

@glassnotes to keep you in loop