VeriQBench: A Benchmark for Multiple Types of Quantum Circuits

TL;DR

VeriQBench delivers a versatile, open-source benchmark for quantum circuits that spans combinational, dynamic, sequential, and variational types, with circuits described in OpenQASM and validated on Qiskit and QCOR. It provides generation scripts to scale circuits beyond small qubit counts and includes supporting benchmarks for qubit mapping (QUEKO) and metrics like Quantum Volume, alongside Clifford randomness and Supremacy-style circuits. The framework targets diverse verification activities—equivalence checking, testing, simulation, and model checking—while enabling easy integration into existing workflows. This benchmark aims to advance practical quantum software verification and benchmarking in the NISQ era by offering standardized, scalable, and interoperable circuit suites.

Abstract

In this paper, we introduce VeriQBench -- an open source benchmark for quantum circuits. It offers high-level quantum circuit abstractions of various circuit types, including 1) combinational, 2) dynamic, 3) sequential, and 4) variational quantum circuits, which cover almost all existing types of quantum circuits in the literature. Meanwhile, VeriQBench is a versatile benchmark which can be used in verifying quantum software for different applications, as is evidenced by the existing works including quantum circuit verification (e.g., equivalence checking [Hon+21a; WLY21] and model checking [Yin21]), simulation (e.g., fault simulation), testing (e.g., test pattern generation [CY22]) and debugging (e.g., runtime assertions [Li+20b]). All the circuits are described in OpenQASM and are validated on Qiskit and QCOR simulators. With the hope that it can be used by other researchers, VeriQBench is released at: https://github.com/Veri-Q/Benchmark.

Figures (14)

• Figure 1: Two examples of the Bernstein-Vazirani algorithm, where (a) $s=101$ and (b) $s=111$.
• Figure 2: Quantum circuit for Fourier Transform.
• Figure 3: Quantum circuit for phase estimation.
• Figure 4: An example of Grover's algorithm. Here, $f(x)$ is a 2-bit function and $f(x)=x_1 \cdot x_2$.
• Figure 5: Circuit of 3-bit adder

Theorems & Definitions (2)

• Definition 1
• Definition 2