About SemanticVeriferPass

[IsolatedMy]

Hello, I'm a student from USTC. Recently I used your Enfield compiler, it's great and I learned a lot. But when I tried to implement CODAR algorithm in arxiv/2002.10915, I found the compiled result of my allocator cannot pass the SemanticVerifierPass. According to my debugging, I guess your project cannot handle the algorithm with commutativity detection. I sincerely wait your reply.

[ysiraichi]

Yes. You are right. The SemanticVerifierPass was mostly a "sanity checker" for messing with qubit mappings. So, in summary, it verifies that two circuits are semantically the same iff:

given a mapping M (from logical to physical qubits), and two qubits a and u, such that a maps to u, any operation applied to a should also be applied to u in the same order.

Note that mapping M could change as operations are applied. So it takes into account the compiler intrinsics, namely: swap, reversal, and bridge operations.