khieta
commented
2 years ago Here is an (in-progress) list of ideas on how to improve VOQC’s circuit mapping:
- [ ] Add a function to split a SQIR circuit into "layers" of disjoint 2-qubit gates (related: write a function to count circuit depth).
- [X] Add a better heuristic layout (mapping) function. At present, all we have is
trivial_layoutin Layouts.v. DONE - [ ] Implement a circuit mapping routine that works by layer instead of by gate (as is currently done in
simple_mapin SimpleMapping.v).- For example: the algorithm in Sec 2.2.3 of Eddie’s paper, which is parameterized by a choice of mapper (=layout algorithm) and permuter (=routing algorithm). In particular, I think we should try to implement his "greedy swap" algorithm.
- [X] Use a "higher-level" language for circuit mapping that distinguishes SWAP gates from other gates. DONE
- [ ] SWAP-specific optimizations (a few ideas: SWAPs at the end of the beginning/end of a circuit can be deleted; SWAPs around single-qubit gates can be removed; SWAPs between qubits with the same value can be deleted)
- [x] Verified translation validation (per the original comment in this thread). DONE
- [ ] Implement & verify an interesting (and realistic) circuit mapping algorithm
- Eddie's paper provides examples of mappers & permuters. It may be tricky to implement these for general graphs in Coq because we need subroutines to solve graph matching and min/max problems.
- See Qiskit's layout and routing algorithms.
- Zulehner et al. use A* search.
- Also look at what tket does.
Sophisticated mapping routines (e.g. that use error-aware heuristics to find the best path through a graph) are likely tricky to implement and verify in Coq, so we may want to use existing unverified mappers. We can still provide some correctness guarantees in this case by using verified translation validation functions. For example: we could define a function that compares two programs (along with initial and final qubit layouts) and checks that one is a permutation of the other via inserted SWAPs. We could then prove that if this function returns true, then the mapping routine preserves semantics for that input.