More Web Proxy on the site http://driver.im/

research-article

Random Stimuli Generation for the Verification of Quantum Circuits

Authors:

Lukas Burgholzer,

Robert WilleAuthors Info & Claims

ASPDAC '21: Proceedings of the 26th Asia and South Pacific Design Automation Conference

Pages 767 - 772

https://doi.org/10.1145/3394885.3431590

Published: 29 January 2021 Publication History

Abstract

Verification of quantum circuits is essential for guaranteeing correctness of quantum algorithms and/or quantum descriptions across various levels of abstraction. In this work, we show that there are promising ways to check the correctness of quantum circuits using simulative verification and random stimuli. To this end, we investigate how to properly generate stimuli for efficiently checking the correctness of a quantum circuit. More precisely, we introduce, illustrate, and analyze three schemes for quantum stimuli generation---offering a trade-off between the error detection rate (as well as the required number of stimuli) and efficiency. In contrast to the verification in the classical realm, we show (both, theoretically and empirically) that even if only a few randomly-chosen stimuli (generated from the proposed schemes) are considered, high error detection rates can be achieved for quantum circuits. The results of these conceptual and theoretical considerations have also been empirically confirmed---with a grand total of approximately 106 simulations conducted across 50 000 benchmark instances.

References

[1]

A. Biere and W. Kunz, "SAT and ATPG: Boolean engines for formal hardware verification," in Int'l Conf. on CAD, 2002, pp. 782--785.

[2]

R. Drechsler, Ed., Advanced Formal Verification. Boston, MA: Springer, 2004.

[3]

J. Yuan, C. Pixley, and A. Aziz, Constraint-based verification. New York, NY: Springer, 2006, 253 pp.

Digital Library

[4]

J. Bergeron, Writing Testbenches using System Verilog. Boston, MA: Springer, 2006.

[5]

N. Kitchen and A. Kuehlmann, "Stimulus generation for constrained random simulation," in Int'l Conf. on CAD, 2007, pp. 258--265.

[6]

R. Wille et al., "SMT-based stimuli generation in the SystemC verification library," in Forum on Specification and Design Languages, 2009, pp. 1--6.

[7]

H. M. Le et al., "Detection of hardware trojans in SystemC HLS designs via coverage-guided fuzzing," in Design, Automation and Test in Europe, 2019, pp. 602--605.

[8]

K. Laeufer et al., "RFUZZ: Coverage-directed fuzz testing of RTL on FPGAs," in Int'l Conf. on CAD, 2018.

Digital Library

[9]

M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information. Cambridge University Press, 2010.

Digital Library

[10]

L. Burgholzer and R. Wille, "Advanced equivalence checking of quantum circuits," IEEE Trans. on CAD of Integrated Circuits and Systems, 2021.

[11]

L. Burgholzer, R. Raymond, and R. Wille, "Verifying results of the IBM Qiskit quantum circuit compilation flow," in Int'l Conf. on Quantum Computing and Engineering, 2020.

[12]

R. Duncan et al. (2019). "Graph-theoretic simplification of quantum circuits with the ZX-calculus." arXiv: 1902.03178.

[13]

S. Yamashita and I. L. Markov, "Fast equivalence-checking for quantum circuits," in Int'l Symp. on Nanoscale Architectures, 2010.

[14]

E. Ardeshir-Larijani, S. J. Gay, and R. Nagarajan, "Automated equivalence checking of concurrent quantum systems," ACM Trans. Comput. Logic, vol. 19, no. 4, pp. 1--32, 2018.

Digital Library

[15]

G. G. Guerreschi et al., "Intel Quantum Simulator: A cloud-ready high-performance simulator of quantum circuits," Quantum Sci. Technol., vol. 5, p. 034 007, 2020.

[16]

T.Jones et al., "QuEST and high performance simulation of quantum computers," in Scientific Reports, 2018.

[17]

B. Villalonga et al., "A flexible high-performance simulator for verifying and benchmarking quantum circuits implemented on real hardware," Npj Quantum Inf., vol. 5, no. 1, pp. 1--16, 2019.

[18]

E. Pednault et al. (2019). "Leveraging secondary storage to simulate deep 54-qubit Sycamore circuits." arXiv: 1910.09534.

[19]

J. R. Seddon et al. (2020). "Quantifying quantum speedups: Improved classical simulation from tighter magic monotones." arXiv: 2002.06181.

[20]

P. Niemann et al., "QMDDs: Efficient quantum function representation and manipulation," IEEE Trans. on CAD of Integrated Circuits and Systems, vol. 35, no. 1, pp. 86--99, 2016.

Digital Library

[21]

A. Zulehner and R. Wille, "Advanced simulation of quantum computations," IEEE Trans. on CAD of Integrated Circuits and Systems, vol. 38, no. 5, pp. 848--859, 2019.

[22]

A. Zulehner and R. Wille, "Matrix-vector vs. matrix-matrix multiplication: Potential in DD-based simulation of quantum computations," in Design, Automation and Test in Europe, 2019.

[23]

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

[24]

S. Khatri et al., "Quantum-assisted quantum compiling," Quantum, vol. 3, p. 140, 2019.

[25]

L. Burgholzer and R. Wille, "The power of simulation for equivalence checking in quantum computing," in Design Automation Conf., 2020.

[26]

J. Schwinger, "Unitary operator bases," Proceedings of the National Academy of Sciences, vol. 46, no. 4, pp. 570--579, 1960.

[27]

A. Klappenecker and M. Rotteler, "Mutually unbiased bases are complex projective 2-designs," in Int'l Symp. on Information Theory, 2005, pp. 1740--1744.

[28]

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

[29]

D. Gottesman, "Stabilizer codes and quantum error correction.," Caltech, 1997.

[30]

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

[31]

F. G. S. L. Brandão, A. W. Harrow, and M. Horodecki, "Local random quantum circuits are approximate polynomial-designs," Commun. Math. Phys., vol. 346, no. 2, pp. 397--434, 2016.

[32]

E. Magesan, J. M. Gambetta, and J. Emerson, "Characterizing quantum gates via randomized benchmarking," Phys. Rev. A, vol. 85, no. 4, p. 042 311, 2012.

[33]

R. Kueng et al., "Comparing experiments to the fault-tolerance threshold," Phys. Rev. Lett., vol. 117, no. 17, p. 170 502, 2016.

[34]

B. Schumacher, "Sending entanglement through noisy quantum channels," Phys. Rev. A, vol. 54, no. 4, pp. 2614--2628, 1996.

[35]

A. Y. Kitaev, "Quantum computations: Algorithms and error correction," Russ. Math. Surv., vol. 52, no. 6, pp. 1191--1249, 1997.

[36]

R. Wille, S. Hillmich, and L. Burgholzer, "JKQ: JKU tools for quantum computing," in Int'l Conf. on CAD, 2020.

Digital Library

[37]

G. Aleksandrowicz et al., "Qiskit: An open-source framework for quantum computing," 2019.

Cited By

Wille RBerent LForster TKunasaikaran JMato KPeham TQuetschlich NRovara DSander ASchmid LSchönberger DStade YBurgholzer L(2024)The MQT Handbook : A Summary of Design Automation Tools and Software for Quantum Computing2024 IEEE International Conference on Quantum Software (QSW)10.1109/QSW62656.2024.00013(1-8)Online publication date: 7-Jul-2024
https://doi.org/10.1109/QSW62656.2024.00013
Witharana HVolya DMishra PKim T(2024)QcAssert: Quantum Device Testing with Concurrent AssertionsProceedings of the 29th Asia and South Pacific Design Automation Conference10.1109/ASP-DAC58780.2024.10473900(491-496)Online publication date: 22-Jan-2024
https://dl.acm.org/doi/10.1109/ASP-DAC58780.2024.10473900
Wille RBurgholzer L(2024)Verification of Quantum CircuitsHandbook of Computer Architecture10.1007/978-981-97-9314-3_43(1413-1440)Online publication date: 21-Dec-2024
https://doi.org/10.1007/978-981-97-9314-3_43
Show More Cited By

Recommendations

Model Checking for Verification of Quantum Circuits
Formal Methods
Abstract
In this survey paper, we describe a framework for assertion-based verification of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which:
- Noiseless and noisy quantum circuits are modelled ...
Rotational abstractions for verification of quantum Fourier transform circuits
Abstract
With the race to build large‐scale quantum computers and efforts to exploit quantum algorithms for efficient problem solving in science and engineering disciplines, the requirement to have efficient and scalable verification methods are of vital ...

A scalable and efficient formal verification method for quantum Fourier transform circuits, capable of verifying unto 10,000 qubits QFT circuit in less than an hour time is proposed. The work uses rotational abstractions to achieve the verification and ...
Commuting quantum circuits: efficient classical simulations versus hardness results

The study of quantum circuits composed of commuting gates is particularly useful to understand the delicate boundary between quantum and classical computation. Indeed, while being a restricted class, commuting circuits exhibit genuine quantum effects ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPDAC '21: Proceedings of the 26th Asia and South Pacific Design Automation Conference

January 2021

930 pages

ISBN:9781450379991

DOI:10.1145/3394885

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE CAS
IEEE CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 January 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed limited

Conference

ASPDAC '21

Sponsor:

SIGDA

ASPDAC '21: 26th Asia and South Pacific Design Automation Conference

January 18 - 21, 2021

Tokyo, Japan

Acceptance Rates

ASPDAC '21 Paper Acceptance Rate 111 of 368 submissions, 30%;

Overall Acceptance Rate 466 of 1,454 submissions, 32%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
150
Total Downloads

Downloads (Last 12 months)47
Downloads (Last 6 weeks)1

Reflects downloads up to 18 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wille RBerent LForster TKunasaikaran JMato KPeham TQuetschlich NRovara DSander ASchmid LSchönberger DStade YBurgholzer L(2024)The MQT Handbook : A Summary of Design Automation Tools and Software for Quantum Computing2024 IEEE International Conference on Quantum Software (QSW)10.1109/QSW62656.2024.00013(1-8)Online publication date: 7-Jul-2024
https://doi.org/10.1109/QSW62656.2024.00013
Witharana HVolya DMishra PKim T(2024)QcAssert: Quantum Device Testing with Concurrent AssertionsProceedings of the 29th Asia and South Pacific Design Automation Conference10.1109/ASP-DAC58780.2024.10473900(491-496)Online publication date: 22-Jan-2024
https://dl.acm.org/doi/10.1109/ASP-DAC58780.2024.10473900
Wille RBurgholzer L(2024)Verification of Quantum CircuitsHandbook of Computer Architecture10.1007/978-981-97-9314-3_43(1413-1440)Online publication date: 21-Dec-2024
https://doi.org/10.1007/978-981-97-9314-3_43
Thanos DVilloria ABrand SQuist AMei JCoopmans TLaarman A(2024)Automated Reasoning in Quantum Circuit CompilationModel Checking Software10.1007/978-3-031-66149-5_6(106-134)Online publication date: 13-Oct-2024
https://doi.org/10.1007/978-3-031-66149-5_6
Vinkhuijzen LCoopmans TElkouss DDunjko VLaarman A(2023)LIMDD: A Decision Diagram for Simulation of Quantum Computing Including Stabilizer StatesQuantum10.22331/q-2023-09-11-11087(1108)Online publication date: 11-Sep-2023
https://doi.org/10.22331/q-2023-09-11-1108
Quetschlich NBurgholzer LWille R(2023)MQT Bench: Benchmarking Software and Design Automation Tools for Quantum ComputingQuantum10.22331/q-2023-07-20-10627(1062)Online publication date: 20-Jul-2023
https://doi.org/10.22331/q-2023-07-20-1062
Chen YChung KLengál OLin JTsai WYen D(2023)An Automata-Based Framework for Verification and Bug Hunting in Quantum CircuitsProceedings of the ACM on Programming Languages10.1145/35912707:PLDI(1218-1243)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591270
Peham TBrandl NKueng RWille RBurgholzer L(2023)Depth-Optimal Synthesis of Clifford Circuits with SAT Solvers2023 IEEE International Conference on Quantum Computing and Engineering (QCE)10.1109/QCE57702.2023.00095(802-813)Online publication date: 17-Sep-2023
https://doi.org/10.1109/QCE57702.2023.00095
Thanos DCoopmans TLaarman A(2023)Fast Equivalence Checking of Quantum Circuits of Clifford GatesAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_10(199-216)Online publication date: 19-Oct-2023
https://doi.org/10.1007/978-3-031-45332-8_10
Vinkhuijzen LGrurl THillmich SBrand SWille RLaarman A(2023)Efficient Implementation of LIMDDs for Quantum Circuit SimulationModel Checking Software10.1007/978-3-031-32157-3_1(3-21)Online publication date: 2-May-2023
https://doi.org/10.1007/978-3-031-32157-3_1
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents