Towards Equivalence Checking of Classical Circuits Using Quantum Computing

TL;DR

The paper addresses the verification gap in classical circuit equivalence by framing the problem as a Grover search. It analyzes pitfalls of naive Grover deployment and proposes an iterative, threshold-driven workflow that handles an unknown number of counterexamples, implemented and evaluated on 6–9 bit instances using simulators. The approach demonstrates correct classification of equivalence vs non-equivalence and yields a practical, quantum-ready concept for near-term quantum verification. This work offers a concrete pathway to integrate quantum computing into classical verification, potentially accelerating verification in the quantum era.

Abstract

Quantum computers and quantum algorithms have made great strides in the last few years and promise improvements over classical computing for specific tasks. Although the current hardware is not yet ready to make real impacts at the time of writing, this will change over the coming years. To be ready for this, it is important to share knowledge of quantum computing in application domains where it is not yet represented. One such application is the verification of classical circuits, specifically, equivalence checking. Although this problem has been investigated over decades in an effort to overcome the verification gap, how it can potentially be solved using quantum computing has hardly been investigated yet. In this work, we address this question by considering a presumably straightforward approach: Using Grover's algorithm. However, we also show that, although this might be an obvious choice, there are several pitfalls to avoid in order to get meaningful results. This leads to the proposal of a working concept of a quantum computing methodology for equivalent checking providing the foundation for corresponding solutions in the (near) future.

Figures (5)

• Figure 1: State vector evolution in the $S$-Basis with the corresponding state amplitudes.
• Figure 2: Probability of measuring a desired state in dependence of the number of iterations when $1$ respectively $15$ out of $64$ basis states represent desired states.
• Figure 3: Miter configuration with two non-equivalent circuits.
• Figure 4: Probability distributions of 32 states for different numbers of iterations with the four counter examples "11011", "11101", "11110", and "11111".
• Figure 5: Distribution of number of measurements when executed with 256 shots.

Theorems & Definitions (8)

• Example 1
• Example 2
• Example 3
• Example 4
• Example 5
• Example 6
• Example 7
• Example 8