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.