Towards Equivalence Checking of Classical Circuits Using Quantum Computing

TL;DR

This paper explores how quantum computing, specifically Grover's algorithm, can be applied to classical circuit equivalence checking, highlighting challenges and proposing a foundational methodology for future solutions.

Contribution

It introduces a quantum computing approach for classical circuit equivalence checking and discusses potential pitfalls and foundational concepts for future development.

Findings

Identifies challenges in applying Grover's algorithm to equivalence checking

Proposes a foundational quantum methodology for circuit verification

Highlights the need for careful adaptation of quantum algorithms

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.