Quantum Equivalence Checking. Innovation in Verification

Can quantum computing have any relevance to EDA? This month’s paper suggests it might have a role someday, in accelerating one of the most fundamental of EDA algorithms: SAT. Paul Cunningham (GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and lecturer at Stanford, EE292A) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking. The authors are from Cyber-Physical Systems, Siemens EDA, and University of Bremen, all in Germany. The paper (2024) has been published in the ACM Journal on Emerging Technologies in Computing Systems and has 6 citations.

SAT is foundational in multiple EDA algorithms, in verification and synthesis, and is the standard benchmark for algorithm complexity. What better challenge then for quantum computing which aims to deliver (at least in some cases) exponential speedup over classical computing methods?

Logic circuit examples considered in this paper are very elementary – multiplexers and 1-bit full adders for example, testing first basic viability of the method. Tests have been run on IBM quantum computers with an initial focus on resources – how many qubits are required and quantum circuit depth, rather than on performance.

Paul’s view

Back to quantum computing this month. Last time we blogged on building a quantum simulator, this time it’s on building a quantum formal equivalence checker. At its heart, formal equivalence is a Boolean satisfiability (SAT) problem: XOR the spec with the implementation and any solution must be a situation where the spec and implementation differ.

Commercial SAT on a classical computer begins by converting a circuit or spec into Conjunctive Normal Form (CNF), which can be done quickly and efficiently using the Tseytin method. Many fast, parallelizable algorithms exist to search heuristically over a CNF to find a variable assignment that satisfies it, for example Kissat.

To implement a Boolean expression in a quantum circuit, it is best to represent the expression with XOR and AND functions, since the fundamental building block of Boolean expressions in a quantum circuit is the Toffoli gate, which implements the expression “a XOR (b AND c)”.

The main contribution in this paper is set of expression rewriting rules that improve the efficiency of mapping a Tseytin CNF into Toffoli gates, while still being fast and memory efficient to apply. On some very small 3-input circuits (like a mux or adder) these rules reduce the total number of quantum gates in the authors’ quantum SAT solver by over 2x.

The actual solving part of the authors’ method uses Grover’s Algorithm. This algorithm is beyond our blog but is seriously innovative and cool. Executive summary: a SAT solver on a classical computer is O(2^n) for n boolean variables.  Grover’s algorithm on a quantum computer is O(2^(n/2)), so a quadratic factor more efficient.

But don’t get too excited yet – modern SAT solvers routinely solve expressions with millions of variables in only minutes. Current quantum computers can SAT solve less than 100 variables.

Raúl’s view

SAT was the first problem proven to be NP-complete: every problem in NP can be reduced to SAT. It also has numerous applications in digital circuit design, including optimization and verification. Quantum computing does not make SAT fundamentally easier, SAT remains an NP-complete problem, but it can speed up the search for solutions. For example, Grover’s algorithm provides a quadratic speedup, reducing a brute-force search over (2ⁿ) assignments from (O(2ⁿ)) to (O(2^n/2)). This paper introduces qSAT, a quantum SAT solver based on Grover search, and develops an end-to-end framework for applying it to Boolean equivalence checking in hardware verification. The authors describe it, “to the best of our knowledge,” as a first attempt toward a complete qSAT solver on a quantum computer.

Notes: 1) Other approaches to implementing SAT on quantum computers include Quantum Annealing, the Quantum Approximate Optimization Algorithm (QAOA), etc.

2) This paper’s “qSAT” should not be confused with QSAT / Quantum Satisfiability, the QMA-complete quantum analogue of SAT (QMA, Quantum Merlin-Arthur, is the quantum analogue of classical NP).

In their approach, a Boolean formula is rewritten in ESOP form (Exclusive Sum Of Products), because ESOP expressions map efficiently into reversible quantum circuits using controlled-X/Toffoli-type gates. These circuits are assembled into a quantum miter (the XOR of the outputs of the two circuits to be checked); the miter is then used as the oracle in Grover’s algorithm, marking input assignments that are counterexamples to equivalence.

The improvement is mainly in quantum resource usage. By utilizing compact ESOP representations and eliminating auxiliary variables, the authors reduce qubit counts, Grover iterations, gates, and circuit depth. For their larger examples, MUX and CARRY show about 27% fewer qubits and roughly 70% fewer gates and depth; the Full Adder shows about 20% fewer qubits and a 70% reduction in gates and depth. However, these metrics only compare their optimized formulation against their own less-optimized baseline. The paper does not provide a quantitative comparison against a prior independent quantum SAT solver.

The paper is difficult to read because of non-standard English and a somewhat confusing organization. For example, it introduces the final quantum miter architecture before explaining the core ESOP mathematics needed to build it. The paper is also not very careful with notation. In Eq. (25), U= ϕ∧(ϕ⇔GR) is a Boolean expression. In Fig. 10, however, U is used for the measured probability of the expected outcome of the quantum implementation of U. The authors use “fidelity” loosely for the probability that the implemented circuit produces the expected output. They reuse ϕ, previously the output of the miter, and restrict the test to the case ϕ =1. They conclude that in almost all examples their smaller implementation also produces the expected output more reliably (Fig. 10). That is their “fidelity”.

As for what an actual IBM quantum computer can handle, even these examples are large: MUX requires about 1,000–3,400 CX gates and the full adder about 5,000–16,000. The IBM Grover tutorial notes that the number of sequential layers of two-qubit gates “grows extremely rapidly with the number of qubits — roughly exponentially, making Grover impractical on current noisy quantum hardware beyond very small problem sizes”. On today’s IBM hardware, the theoretical quadratic algorithmic speedup is overwhelmed by circuit depth and noise. Indeed, the complete qSAT/Grover circuits in the paper are evaluated on the ideal Aer simulator; the experiments on the actual IBM quantum computer are limited to the much smaller reference-model circuits used for the fidelity comparison.

Nevertheless, the paper makes a useful contribution to quantum formal verification: it shows how logic representation, specifically ESOP-based encoding, can substantially reduce the quantum resources required to implement a Grover-based equivalence checker.

Share this post via:

• 
• 
• 
•