Skip to main content
SpringerLink
Log in

Verification of Quantum Circuits

  • Living reference work entry
  • First Online:
Handbook of Computer Architecture

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

References

  • Amy M, Gheorghiu V (2019) Staq – a full-stack quantum processing toolkit. arXiv: 1912.06070

    Google Scholar 

  • 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

    Article  Google Scholar 

  • Barenco A et al (1995) Elementary gates for quantum computation. Phys Rev A, https://doi.org/10.1103/PhysRevA.52.3457

    Book  MATH  Google Scholar 

  • Bergeron J (2006) Writing testbenches using system verilog. Springer, New York

    Book  Google Scholar 

  • Biere A, Kunz W (2002) SAT and ATPG: boolean engines for formal hardware verification. In: International Conference on CAD, pp 782–785

    Google Scholar 

  • Bookatz AD (2013) QMA-complete problems. arXiv: 1212.6312

    Google Scholar 

  • Brandão FGSL, Harrow AW, Horodecki M (2016) Local random quantum circuits are approximate polynomial-designs. Commun Math Phys 346(2):397–434

    Article  MathSciNet  MATH  Google Scholar 

  • Brennan J et al (2021) Tensor Network Circuit Simulation at Exascale. arXiv: 2110.09894

    Google Scholar 

  • Burgholzer L, Wille R (2020a) Improved DD-based equivalence checking of quantum circuits. In: Asia and South Pacific Design Automation Conference

    Book  Google Scholar 

  • Burgholzer L, Wille R (2020b) The power of simulation for equivalence checking in quantum computing. In: Design Automation Conference

    Book  Google Scholar 

  • 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

    Book  Google Scholar 

  • 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

    Google Scholar 

  • 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

    Book  Google Scholar 

  • Burgholzer L, Raymond R, Sengupta I, Wille R (2021a) Efficient construction of functional representations for quantum algorithms. In: International Conference of Reversible Computation

    Book  MATH  Google Scholar 

  • Burgholzer L, Kueng R, Wille R (2021b) Random stimuli generation for the verification of quantum circuits. In: Asia and South Pacific Design Automation Conference

    Book  Google Scholar 

  • 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

    Book  Google Scholar 

  • Burgholzer L, Schneider S, Wille R (2022a) Limiting the search space in optimal quantum circuit mapping. In: Asia and South Pacific Design Automation Conference

    Book  Google Scholar 

  • 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

    Book  Google Scholar 

  • 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]

    Google Scholar 

  • 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

    Google Scholar 

  • Drechsler R (2004) Advanced formal verification. Springer, https://doi.org/10.1007/b105236

    Book  MATH  Google Scholar 

  • Giles B, Selinger P (2013) Exact synthesis of multiqubit Clifford+T circuits. Phys Rev A 87(3):032332

    Article  Google Scholar 

  • Gottesman D (1997) Stabilizer codes and quantum error correction. Caltech

    Google Scholar 

  • 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

    Google Scholar 

  • Grover LK (1996) A fast quantum mechanical algorithm for database search. In: Proceedings of the ACM, pp 212–219

    MATH  Google Scholar 

  • 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

    Google Scholar 

  • Hietala K, Rand R, Hung S-H, Wu X, Hicks M (2019) A verified optimizer for quantum circuits. arXiv: 1912.02250

    Google Scholar 

  • Hunter-Jones N (2019) Unitary designs from statistical mechanics in random quantum circuits. arXiv: 1905.12053

    Google Scholar 

  • Itoko T, Raymond R, Imamichi T, Matsuo A (2020) Optimization of quantum circuit mapping using gate transformation and commutation. Integration 70:43–50

    Article  Google Scholar 

  • Janzing D, Wocjan P, Beth T (2005) “Non-identity check” is QMA-complete. Int J Quantum Inform 03(03):463–473

    Article  MATH  Google Scholar 

  • 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

    Google Scholar 

  • Khatri S, LaRose R, Poremba A, Cincio L, Sornborger AT, Coles PJ (2019) Quantum-assisted quantum compiling. Quantum 3:140

    Article  Google Scholar 

  • Kitchen N, Kuehlmann A (2007) Stimulus generation for constrained random simulation. In: International Conference on CAD, pp 258–265

    Google Scholar 

  • Klappenecker A, Rotteler M (2005) Mutually unbiased bases are complex projective 2-designs. In: International Symposium on Information Theory, pp 1740–1744

    Google Scholar 

  • Kueng R, Gross D (2015) Qubit stabilizer states are complex projective 3-designs. arXiv: 1510.02767

    Google Scholar 

  • 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

    Book  Google Scholar 

  • 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

    Book  Google Scholar 

  • 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

    Book  Google Scholar 

  • 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

    Article  Google Scholar 

  • 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

    Book  Google Scholar 

  • 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

    Book  Google Scholar 

  • 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

    MATH  Google Scholar 

  • Niemann P, Wille R, Miller DM, Thornton MA, Drechsler R (2016) QMDDs: efficient quantum function representation and manipulation. IEEE Trans CAD Integr Circuits Systems

    Google Scholar 

  • Pednault E, Gunnels JA, Nannicini G, Horesh L, Wisnieff R (2019) Leveraging secondary storage to simulate deep 54-qubit Sycamore circuits. arXiv: 1910.09534

    Google Scholar 

  • Schwinger J (1960) Unitary operator bases. In: Proc Natl Acad Sci 46(4):570–579

    Google Scholar 

  • Seddon JR, Regula B, Pashayan H, Ouyang Y, Campbell ET (2020) Quantifying quantum speedups: improved classical simulation from tighter magic monotones. arXiv: 2002.06181

    Google Scholar 

  • Siraichi MY, dos Santos VF, Collange S, Pereira FMQ (2018) Qubit allocation. In: International Symposium on Code Generation and Optimization

    Google Scholar 

  • 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

    Google Scholar 

  • 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

    Google Scholar 

  • Viamontes GF, Markov IL, Hayes JP (2004) High-performance QuIDD-Based simulation of quantum circuits. In: Design, Automation and Test in Europe

    Book  Google Scholar 

  • Vidal G, Dawson CM (2004) Universal quantum circuit for two-qubit transformations with three controlled-NOT gates. Phys Rev A 69(1):010301

    Article  Google Scholar 

  • 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

    Book  Google Scholar 

  • Vincent T et al (2021) Jet: fast quantum circuit simulations with parallel task-based tensor-network contraction. arXiv: 2107.09793 [quant-ph]

    Google Scholar 

  • Watrous J (2018) The theory of quantum information. Cambridge University Press, Cambridge, 590pp

    Book  MATH  Google Scholar 

  • 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

    Google Scholar 

  • 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

    Book  Google Scholar 

  • Wille R, Hillmich S, Burgholzer L (2020) JKQ: JKU tools for quantum computing. In: International Conference on CAD

    Book  Google Scholar 

  • Wille R, Burgholzer L, Artner M (2021) Visualizing decision diagrams for quantum computing. In: Design, Automation and Test in Europe

    Google Scholar 

  • Yuan J, Pixley C, Aziz A (2006) Constraint-based verification. Springer

    MATH  Google Scholar 

  • 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

    Google Scholar 

  • 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

    Google Scholar 

  • Zulehner A, Wille R (2019b) Advanced simulation of quantum computations. IEEE Trans CAD Integr Circuits Syst, https://doi.org/10.1109/TCAD.2018.2834427

    Book  Google Scholar 

  • 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

    Google Scholar 

  • 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

    Book  Google Scholar 

  • Zulehner A, Hillmich S, Wille R (2019e) How to efficiently handle complex values? Implementing decision diagrams for quantum computing. In: International Conference on CAD

    Book  Google Scholar 

Download references

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

  1. Chair for Design Automation, Technical University of Munich, Munich, Germany

    Robert Wille

  2. Software Competence Center Hagenberg GmbH (SCCH), Hagenberg im Mühlkreis, Austria

    Robert Wille

  3. Institute for Integrated Circuits, Johannes Kepler University Linz, Linz, Austria

    Lukas Burgholzer

Authors
  1. Robert Wille
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lukas Burgholzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Robert Wille .

Editor information

Editors and Affiliations

  1. Sch of Computer Science & Engineering, Nanyang Technological University, Singapore, Singapore

    Anupam Chattopadhyay

Section Editor information

  1. Intel, 6250 Santa Teresa Blvd., Apt 121, 95119, San Jose, California, USA

    Ray Sayak

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Singapore Pte Ltd.

About this entry

Check for updates. Verify currency and authenticity via CrossMark

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

Publish with us

Policies and ethics

Search

Navigation