🐛 equivalence verification crashed for a transpiled circuit

Co1lin commented 1 year ago

Environment information

OS: Ubuntu 22.04.3 LTS
mqt.qcec 2.4.1

Description

For the given circuit, equivalence verification crashed for the transpiled circuit. The error log is [1] 3989380 IOT instruction (core dumped) python bug.py . After mapping physical qubits back to logical qubits, the verification could run, but gave False, which was unexpected.

Expected behavior

No response

How to Reproduce

from qiskit import QuantumCircuit
from qiskit import transpile
from qiskit import QuantumCircuit
from qiskit.providers.fake_provider import FakeAuckland

def num_gates(qc: QuantumCircuit) -> int:
    return sum(qc.count_ops().values())

def check_qcec(qc_x: QuantumCircuit, qc_y: QuantumCircuit) -> bool:
    from mqt import qcec

    result = qcec.verify(qc_x, qc_y)
    # ic(result.equivalence)
    return result.considered_equivalent()

backend = FakeAuckland()

qc = QuantumCircuit.from_qasm_str('''OPENQASM 2.0;
include "qelib1.inc";
qreg q[5];
h q[4];
cx q[3],q[4];
tdg q[4];
cx q[2],q[4];
t q[4];
cx q[3],q[4];
tdg q[4];
cx q[2],q[4];
cx q[2],q[3];
t q[4];
tdg q[3];
cx q[2],q[3];
t q[2];
t q[3];
h q[3];
cx q[1],q[3];
tdg q[3];''')
qc.draw('mpl', filename='test.png')
print(num_gates(qc))

qc_basis = transpile(qc, backend, optimization_level=3)
qc_basis.draw(output='mpl', filename='test_basis.png')
print(qc_basis.qasm())
'''
OPENQASM 2.0;
include "qelib1.inc";
qreg q[27];
rz(pi/2) q[13];
sx q[13];
rz(pi/2) q[13];
cx q[14],q[13];
rz(-pi/4) q[13];
cx q[12],q[13];
sx q[12];
rz(-pi) q[12];
rz(pi/4) q[13];
cx q[14],q[13];
rz(-pi/4) q[13];
sx q[13];
rz(-3*pi/2) q[13];
cx q[13],q[12];
rz(pi/2) q[12];
sx q[13];
cx q[13],q[12];
rz(-pi/4) q[12];
sx q[13];
rz(-pi/4) q[13];
cx q[13],q[14];
rz(-pi/4) q[14];
cx q[13],q[14];
rz(3*pi/4) q[14];
sx q[14];
rz(pi/2) q[14];
cx q[16],q[14];
rz(-pi/4) q[14];
'''
# print(qc_basis.layout.initial_layout.get_physical_bits())
print(num_gates(qc_basis))
# print(check_qcec(qc, qc_basis)) # CRASHED: [1]    3989380 IOT instruction (core dumped)  python bug.py

'''map physical qubit in qc_basis back to logical qubit in qc
13 -> 4
14 -> 3
12 -> 2
16 -> 1
21 -> 0
'''

qc_match = QuantumCircuit.from_qasm_str('''OPENQASM 2.0;
include "qelib1.inc";
qreg q[27];
rz(pi/2) q[4];
sx q[4];
rz(pi/2) q[4];
cx q[3],q[4];
rz(-pi/4) q[4];
cx q[2],q[4];
sx q[2];
rz(-pi) q[2];
rz(pi/4) q[4];
cx q[3],q[4];
rz(-pi/4) q[4];
sx q[4];
rz(-3*pi/2) q[4];
cx q[4],q[2];
rz(pi/2) q[2];
sx q[4];
cx q[4],q[2];
rz(-pi/4) q[2];
sx q[4];
rz(-pi/4) q[4];
cx q[4],q[3];
rz(-pi/4) q[3];
cx q[4],q[3];
rz(3*pi/4) q[3];
sx q[3];
rz(pi/2) q[3];
cx q[1],q[3];
rz(-pi/4) q[3];''')

print(check_qcec(qc, qc_match)) # False???

burgholzer commented 1 year ago

Hi 👋🏼

Thanks for raising this issue. I can confirm that I can reproduce the error locally.

One thing that caught my attention right away is that your original circuit is missing measurements at the end of the circuit. As stated in https://mqt.readthedocs.io/projects/qcec/en/latest/CompilationFlowVerification.html#Using-QCEC-to-Verify-Compilation-Flow-Results, this is essential for keeping track of the qubit permutation introduced by routing during transpilation. (Note that QCEC will soon also support a different way of extracting the output permutation when given a Qiskit circuit; via the final_layout member exposed through Qiskit). Simply adding a classical register and measurements to the original circuit:

  OPENQASM 2.0;
  include "qelib1.inc";
  qreg q[5];
  creg c[5];  // <---
  h q[4];
  cx q[3],q[4];
  tdg q[4];
  cx q[2],q[4];
  t q[4];
  cx q[3],q[4];
  tdg q[4];
  cx q[2],q[4];
  cx q[2],q[3];
  t q[4];
  tdg q[3];
  cx q[2],q[3];
  t q[2];
  t q[3];
  h q[3];
  cx q[1],q[3];
  tdg q[3];
  measure q -> c; // <---

makes the crash go away.

Nevertheless, the result is still shown as non-equivalent. I need to dig a little deeper into why this might be happening, but I am fairly sure that this has something to do with q[0] being completely unused in the original circuit and the way we try to strip idle qubits in circuits to reduce the complexity for QCEC. Two possible workarounds for now:

Explicitly add a barrier statement on all qubits in front of the measurement, i.e.,

OPENQASM 2.0;
include "qelib1.inc";
qreg q[5];
creg c[5];
h q[4];
cx q[3],q[4];
tdg q[4];
cx q[2],q[4];
t q[4];
cx q[3],q[4];
tdg q[4];
cx q[2],q[4];
cx q[2],q[3];
t q[4];
tdg q[3];
cx q[2],q[3];
t q[2];
t q[3];
h q[3];
cx q[1],q[3];
tdg q[3];
barrier q;
measure q -> c;

This essentially forces the idle qubit to be included.

Instead of adding the classical register, measurements and barrier to the QASM file, call qc.measure_all() after loading the QASM string.

In both cases, this allows QCEC to verify the circuit correctly. I'll come back to you in a few days once I find some time to dig deeper into why the above workarounds are necessary at the moment.

burgholzer commented 1 year ago

Ok. Wasn't that hard to drill down to the underlying issue. The crash you experienced was due to https://github.com/cda-tum/mqt-core/pull/437. I just updated QCEC with the fix in #313. Waiting for one more PR to go through before I'll create a new patch release.

The following test file now works properly with the changes noted above.

from __future__ import annotations

import pytest
from qiskit import QuantumCircuit, transpile
from qiskit.providers.fake_provider import FakeAuckland

from mqt import qcec

@pytest.fixture()
def qc() -> QuantumCircuit:
    """Fixture for a simple circuit."""
    return QuantumCircuit.from_qasm_str(
        """
        OPENQASM 2.0;
        include "qelib1.inc";
        qreg q[5];
        h q[4];
        cx q[3],q[4];
        tdg q[4];
        cx q[2],q[4];
        t q[4];
        cx q[3],q[4];
        tdg q[4];
        cx q[2],q[4];
        cx q[2],q[3];
        t q[4];
        tdg q[3];
        cx q[2],q[3];
        t q[2];
        t q[3];
        h q[3];
        cx q[1],q[3];
        tdg q[3];
        """
    )

def test_works(qc: QuantumCircuit) -> None:
    """Adding barriers + measurements works."""
    qc.measure_all()  # <--- either add this statement here
    qc2 = transpile(qc, backend=FakeAuckland(), optimization_level=3, seed_transpiler=12345)
    result = qcec.verify(qc, qc2, parallel=False)
    print(result)
    assert result.considered_equivalent()

def test_works_without_measurements(qc: QuantumCircuit) -> None:
    """Without measurements, the circuits are non-equivalent since their output permutation does not match."""
    qc2 = transpile(qc, backend=FakeAuckland(), optimization_level=3, seed_transpiler=12345)
    qc2.swap(12, 13)  # <--- or correct for the output permutation
    print(qc2.draw(fold=-1))
    result = qcec.verify(qc, qc2, parallel=True)
    print(result)
    assert result.considered_equivalent()

Note that, without the information from measurements, both circuits are not equivalent if you do not manually correct the output permutation as shown in the above example (even if you relabel the qubits to the original logical indices). The main reason for that is that transpilation introduces a SWAP operation and, thus, permutes the logical qubits. This will go away, once we support the final_layout member of Qiskit. However, it is important to recall: these circuits do not implement the same unitary. So QCEC is technically correct here.

burgholzer commented 1 year ago

V2.4.2 is out on PyPI https://pypi.org/project/mqt.qcec/

Please let me know if it fixes your issues!

Co1lin commented 1 year ago

Hi, thank you so much for your instant reply! Just one question/confirmation:

This will go away, once we support the final_layout member of Qiskit.

Does this mean, after this support, you will consider circuits that do not implement the same unitary but are functionally equivalent after qubit swapping as equivalent circuits?

burgholzer commented 1 year ago

Per default: yes. I am not yet sure how fine granular the control should be on what is considered equivalent and what not. I could imagine at least:

A strict mode that assumes both circuits act on the same number of qubits with the same initial layout and the same output permutation
A lax mode that tries to make everything work with the information available (close to what QCEC does now)

But also anything in between, like allowing initial layouts, allowing output permutations, etc.

burgholzer commented 11 months ago

Closing this for now. Feel free to re-open if you are still experiencing issues!

cda-tum / mqt-qcec