Abstract
We are at the dawn of a new “computing age” in which quantum computers will find their way into practical applications. Although quantum computers work differently than classical machines, the design flow for realizing applications is similar: first, the desired functionality/application is described on a high level. Then, it is compiled down to a description (usually called quantum circuit) that can be executed on an actual machine. During this process, lots of constraints have to be fulfilled, and optimizations are applied to reduce the circuit’s size and, hence, improve the actual performance on the quantum computer – all of which are highly nontrivial steps. As in conventional design, sooner or later, it is essential to check whether the resulting realization is correct – motivating verification. This chapter reviews and provides a summary of work in this regard. Considering the challenges currently seen in the verification of (comparatively simpler) classical systems, this may provide the basis for preventing the emergence of a verification gap in quantum computing.
Similar content being viewed by others
References
Amy M, Gheorghiu V (2019) Staq – a full-stack quantum processing toolkit. arXiv: 1912.06070
Amy M, Maslov D, Mosca M, Roetteler M (2013) A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits. IEEE Trans CAD Integr Circuits Syst 32(6):818–830
Barenco A et al (1995) Elementary gates for quantum computation. Phys Rev A, https://doi.org/10.1103/PhysRevA.52.3457
Bergeron J (2006) Writing testbenches using system verilog. Springer, New York
Biere A, Kunz W (2002) SAT and ATPG: boolean engines for formal hardware verification. In: International Conference on CAD, pp 782–785
Bookatz AD (2013) QMA-complete problems. arXiv: 1212.6312
Brandão FGSL, Harrow AW, Horodecki M (2016) Local random quantum circuits are approximate polynomial-designs. Commun Math Phys 346(2):397–434
Brennan J et al (2021) Tensor Network Circuit Simulation at Exascale. arXiv: 2110.09894
Burgholzer L, Wille R (2020a) Improved DD-based equivalence checking of quantum circuits. In: Asia and South Pacific Design Automation Conference
Burgholzer L, Wille R (2020b) The power of simulation for equivalence checking in quantum computing. In: Design Automation Conference
Burgholzer L, Wille R (2021a) Advanced equivalence checking for quantum circuits. IEEE Trans CAD Integr Circuits Syst, https://doi.org/10.1109/TCAD.2020.3032630
Burgholzer L, Wille R (2021b) QCEC: a JKQ tool for quantum circuit equivalence checking. Softw Impacts, https://doi.org/10.1016/j.simpa.2020.100051
Burgholzer L, Raymond R, Wille R (2020) Verifying results of the IBM Qiskit quantum circuit compilation flow. In: International Conference on Quantum Computing and Engineering
Burgholzer L, Raymond R, Sengupta I, Wille R (2021a) Efficient construction of functional representations for quantum algorithms. In: International Conference of Reversible Computation
Burgholzer L, Kueng R, Wille R (2021b) Random stimuli generation for the verification of quantum circuits. In: Asia and South Pacific Design Automation Conference
Burgholzer L, Bauer H, Wille R (2021c) Hybrid Schrödinger-Feynman simulation of quantum circuits with decision diagrams. In: International Conference on Quantum Computing and Engineering
Burgholzer L, Schneider S, Wille R (2022a) Limiting the search space in optimal quantum circuit mapping. In: Asia and South Pacific Design Automation Conference
Burgholzer L, Ploier A, Wille R (2022b) Exploiting arbitrary paths for the simulation of quantum circuits with decision diagrams. In: Design, Automation and Test in Europe
Chin-Yung L, Shiou-An W, Sy-Yen K (2011) An extended XQDD representation for multiple-valued quantum logic. IEEE Trans Comput 1377–1389, https://doi.org/10.1109/TC.2011.114
Cross AW et al (2021) OpenQASM 3: a broader and deeper quantum assembly language. arXiv: 2104.14722 [quant-ph]
Doi J, Takahashi H, Raymond R, Imamichi T, Horii H (2019) Quantum computing simulator on a heterogenous HPC system. In: International Conference on Computing Frontiers, pp 85–93
Drechsler R (2004) Advanced formal verification. Springer, https://doi.org/10.1007/b105236
Giles B, Selinger P (2013) Exact synthesis of multiqubit Clifford+T circuits. Phys Rev A 87(3):032332
Gottesman D (1997) Stabilizer codes and quantum error correction. Caltech
Green AS, Lumsdaine PL, Ross NJ, Selinger P, Valiron B (2013) Quipper: a scalable quantum programming language. SIGPLAN Not 48(6):333. arXiv: 1304.3390
Grover LK (1996) A fast quantum mechanical algorithm for database search. In: Proceedings of the ACM, pp 212–219
Guerreschi GG, Hogaboam J, Baruffa F, Sawaya NPD (2020) Intel Quantum Simulator: a cloud-ready high-performance simulator of quantum circuits. Quantum Sci Technol, https://doi.org/10.1088/2058-9565/ab8505
Hietala K, Rand R, Hung S-H, Wu X, Hicks M (2019) A verified optimizer for quantum circuits. arXiv: 1912.02250
Hunter-Jones N (2019) Unitary designs from statistical mechanics in random quantum circuits. arXiv: 1905.12053
Itoko T, Raymond R, Imamichi T, Matsuo A (2020) Optimization of quantum circuit mapping using gate transformation and commutation. Integration 70:43–50
Janzing D, Wocjan P, Beth T (2005) “Non-identity check” is QMA-complete. Int J Quantum Inform 03(03):463–473
Jones T, Brown A, Bush I, Benjamin SC (2018) QuEST and high performance simulation of quantum computers. Sci Rep, https://doi.org/10.1038/s41598-019-47174-9
Khatri S, LaRose R, Poremba A, Cincio L, Sornborger AT, Coles PJ (2019) Quantum-assisted quantum compiling. Quantum 3:140
Kitchen N, Kuehlmann A (2007) Stimulus generation for constrained random simulation. In: International Conference on CAD, pp 258–265
Klappenecker A, Rotteler M (2005) Mutually unbiased bases are complex projective 2-designs. In: International Symposium on Information Theory, pp 1740–1744
Kueng R, Gross D (2015) Qubit stabilizer states are complex projective 3-designs. arXiv: 1510.02767
Laeufer K, Koenig J, Kim D, Bachrach J, Sen K (2018) RFUZZ: coverage-directed fuzz testing of RTL on FPGAs. In: International Conference on CAD
Le HM, Große D, Bruns N, Drechsler R (2019) Detection of hardware trojans in SystemC HLS designs via coverage-guided fuzzing. In: Design, Automation and Test in Europe
Li G, Ding Y, Xie Y (2019) Tackling the qubit mapping problem for NISQ-era quantum devices. In: International Conference on Architectural Support for Programming Languages and Operating Systems
Maslov D (2016) On the advantages of using relative phase Toffolis with an application to multiple control Toffoli optimization. Phys Rev A 93(2):022311
Matsuo A, Hattori W, Yamashita S (2019) Reducing the overhead of mapping quantum circuits to IBM Q system. In: IEEE International Symposium on Circuits and Systems
Murali P, Baker JM, Javadi-Abhari A, Chong FT, Martonosi M (2019) Noise-adaptive compiler mappings for Noisy Intermediate-Scale Quantum computers. In: International Conference on Architectural Support for Programming Languages and Operating Systems
Nam Y, Ross NJ, Su Y, Childs AM, Maslov D (2018) Automated optimization of large quantum circuits with continuous parameters. npj Quantum Inf, https://doi.org/10.1038/s41534-018-0072-4
Nielsen MA, Chuang IL (2010) Quantum computation and quantum information. Cambridge University Press, Cambridge
Niemann P, Wille R, Miller DM, Thornton MA, Drechsler R (2016) QMDDs: efficient quantum function representation and manipulation. IEEE Trans CAD Integr Circuits Systems
Pednault E, Gunnels JA, Nannicini G, Horesh L, Wisnieff R (2019) Leveraging secondary storage to simulate deep 54-qubit Sycamore circuits. arXiv: 1910.09534
Schwinger J (1960) Unitary operator bases. In: Proc Natl Acad Sci 46(4):570–579
Seddon JR, Regula B, Pashayan H, Ouyang Y, Campbell ET (2020) Quantifying quantum speedups: improved classical simulation from tighter magic monotones. arXiv: 2002.06181
Siraichi MY, dos Santos VF, Collange S, Pereira FMQ (2018) Qubit allocation. In: International Symposium on Code Generation and Optimization
Smith KN, Thornton MA (2019) A quantum computational compiler and design tool for technology-specific targets. In: International Symposium on Computer Architecture, pp 579–588
Svore KM et al (2018) Q#: enabling scalable quantum computing and development with a high-level domain-specific language. In: Proceedings of RWDSL. arXiv:1803.00652
Viamontes GF, Markov IL, Hayes JP (2004) High-performance QuIDD-Based simulation of quantum circuits. In: Design, Automation and Test in Europe
Vidal G, Dawson CM (2004) Universal quantum circuit for two-qubit transformations with three controlled-NOT gates. Phys Rev A 69(1):010301
Villalonga B et al (2019) A flexible high-performance simulator for verifying and benchmarking quantum circuits implemented on real hardware. Npj Quantum Inf, https://doi.org/10.1038/s41534-019-0196-1
Vincent T et al (2021) Jet: fast quantum circuit simulations with parallel task-based tensor-network contraction. arXiv: 2107.09793 [quant-ph]
Watrous J (2018) The theory of quantum information. Cambridge University Press, Cambridge, 590pp
Wille R, Große D, Haedicke F, Drechsler R (2009) SMT-based stimuli generation in the SystemC Verification library. In: Forum on Specification and Design Languages
Wille R, Burgholzer L, Zulehner A (2019) Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations. In: Design Automation Conference
Wille R, Hillmich S, Burgholzer L (2020) JKQ: JKU tools for quantum computing. In: International Conference on CAD
Wille R, Burgholzer L, Artner M (2021) Visualizing decision diagrams for quantum computing. In: Design, Automation and Test in Europe
Yuan J, Pixley C, Aziz A (2006) Constraint-based verification. Springer
Zulehner A, Wille R (2018) One-pass design of reversible circuits: combining embedding and synthesis for reversible logic. IEEE Trans CAD Integr Circuits Syst 37(5):996–1008
Zulehner A, Wille R (2019a) Compiling SU(4) quantum circuits to IBM QX architectures. In: Asia and South Pacific Design Automation Conference, Tokyo, pp 185–190
Zulehner A, Wille R (2019b) Advanced simulation of quantum computations. IEEE Trans CAD Integr Circuits Syst, https://doi.org/10.1109/TCAD.2018.2834427
Zulehner A, Wille R (2019c) Matrix-Vector vs. Matrix-Matrix multiplication: potential in DD-based simulation of quantum computations. In: Design, Automation and Test in Europe
Zulehner A, Paler A, Wille R (2019d) An efficient methodology for mapping quantum circuits to the IBM QX architectures. IEEE Trans CAD Integr Circuits Syst, https://doi.org/10.1109/TCAD.2018.2846658
Zulehner A, Hillmich S, Wille R (2019e) How to efficiently handle complex values? Implementing decision diagrams for quantum computing. In: International Conference on CAD
Acknowledgements
This work received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement no. 101001318); was part of the Munich Quantum Valley, which is supported by the Bavarian state government with funds from the Hightech Agenda Bayern Plus; and has been supported by the BMK, BMDW, and the State of Upper Austria in the frame of the COMET program (managed by the FFG).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Section Editor information
Rights and permissions
Copyright information
© 2022 Springer Nature Singapore Pte Ltd.
About this entry
Cite this entry
Wille, R., Burgholzer, L. (2022). Verification of Quantum Circuits. In: Chattopadhyay, A. (eds) Handbook of Computer Architecture. Springer, Singapore. https://doi.org/10.1007/978-981-15-6401-7_43-1
Download citation
DOI: https://doi.org/10.1007/978-981-15-6401-7_43-1
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-15-6401-7
Online ISBN: 978-981-15-6401-7
eBook Packages: Springer Reference EngineeringReference Module Computer Science and Engineering