qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking

This paper proposes an efficient quantum SAT solver (qSAT) for hardware equivalence checking that utilizes Grover's algorithm and an Exclusive-Sum-of-Product based CNF generation to reduce qubit requirements and circuit depth, with experimental validation performed on the Qiskit platform and IBM quantum computers.

The Gist

The Big Problem: Finding a Needle in a Haystack

Imagine you are a quality inspector at a toy factory. You have two versions of a complex toy robot:

1. The Golden Model ($G_R$): The perfect, original design.
2. The Test Model ($G_I$): The new one coming off the assembly line.

Your job is to check if they work exactly the same. If they are different, you need to find the specific button press or switch setting that makes the new robot do something the old one doesn't.

In the world of computer chips, this is called Equivalence Checking. Traditionally, we use a "classical" computer to solve this. The paper explains that for complex toys (circuits), the classical computer has to check every single possibility one by one. If the toy has just a few more buttons, the time it takes to check grows exponentially—like trying to count every grain of sand on a beach by picking them up one at a time. For a 12-bit multiplier (a specific math chip), the paper shows that adding just one extra bit can make the check take hours instead of seconds.

The Solution: The Quantum "Super-Scanner"

The authors propose a new tool called qSAT. Instead of checking possibilities one by one, they use a Quantum Computer.

Think of a classical computer as a detective walking through a dark maze, checking one path at a time. A quantum computer is like a detective who can magically split into thousands of clones, walking down every path in the maze simultaneously.

The paper uses a famous quantum trick called Grover's Algorithm. Imagine you are looking for a specific name in a phone book.

• Classical way: You read page 1, page 2, page 3... until you find it.
• Quantum way (Grover's): You use a special "quantum magnifying glass" that highlights the right page much faster. It doesn't just look twice as fast; it looks quadratically faster. If there are a million pages, a classical computer might need 500,000 tries, but the quantum one might only need 1,000.

The Secret Sauce: ESOP (The "Efficient Packing" Method)

The paper's biggest innovation isn't just using quantum computers; it's how they translate the problem for the quantum machine.

Usually, translating a complex logic puzzle into a format a quantum computer understands is like trying to fit a giant, awkward sofa into a tiny elevator. You need a lot of extra space (qubits) and a lot of complex maneuvers (gates) to get it in.

The authors developed a method called ESOP (Exclusive Sum-of-Products).

• The Analogy: Imagine you are packing a suitcase. The old way (standard logic) is like throwing clothes in randomly, requiring a huge suitcase and lots of folding. The ESOP method is like using a vacuum-seal bag. It compresses the logic tightly.
• The Result: This method requires fewer qubits (the quantum equivalent of suitcase space) and fewer gates (the steps needed to pack). The paper claims this makes the quantum circuit "linear," meaning it scales much more smoothly as the problem gets bigger.

The "Miter" Circuit: The Comparison Machine

To check if the two robots are the same, the authors build a special "comparison machine" called a Miter Circuit.

• They feed the same inputs into both the Golden Model and the Test Model.
• They then ask the machine: "Do these two outputs match?"
• If the machine finds a difference, it outputs a "Counter-Example" (CEX)—a specific set of inputs that proves the robots are different.

The authors optimized this comparison machine. They showed that by using their "vacuum-seal" (ESOP) method, they can build a smaller, faster comparison machine that uses fewer resources.

The Case Study: The Multiplexer and the Full-Adder

To prove their idea works, they tested it on two common building blocks of computer chips:

1. The Multiplexer (MUX): A switch that chooses between two inputs.
2. The Full-Adder: A circuit that adds three numbers together.

They compared two ways of building the "Golden Model" for these circuits:

• Method A (Standard): Uses a lot of extra variables (like using 4 extra suitcases).
• Method B (Their ESOP method): Uses fewer extra variables (like using only 2 suitcases).

The Results:

• Fewer Resources: Method B used significantly fewer qubits and gates. For the Full-Adder, they reduced the number of "Grover iterations" (the number of times the quantum computer has to scan) by a factor of roughly $\sqrt{8}$ (about 2.8 times faster).
• Accuracy: When they ran these tests on a simulator and a real IBM quantum computer, the "Method B" circuits were more reliable (higher fidelity) and still found the correct answers (Counter-Examples) with high probability (over 75%).

Summary

The paper presents a new way to check if computer chips are built correctly using quantum computers.

1. The Problem: Classical computers are too slow for checking complex chips.
2. The Fix: Use a quantum computer with Grover's algorithm to search for errors much faster.
3. The Innovation: They invented a new "packing" method (ESOP) to translate the chip logic into quantum instructions. This makes the quantum circuit smaller, shallower, and less expensive to run.
4. The Proof: They tested this on real chip components and showed it uses fewer resources and works reliably on current quantum hardware.

Essentially, they figured out how to shrink the "suitcase" so the quantum detective can fit into the elevator and solve the mystery much faster than before.

Technical Summary

Technical Summary: qSAT – Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking

Problem Statement
Hardware verification, particularly equivalence checking of Boolean circuits, frequently encounters exponential run-time complexities when solved using classical Boolean Satisfiability (SAT) solvers. While modern solvers like Z3 (using SMT and CDCL algorithms) are effective, they struggle with circuits of asymmetric structures, leading to massive increases in verification time and memory requirements as bit-widths increase. This paper addresses the need for a more efficient approach by leveraging quantum computing to achieve substantial speed-ups over classical searching algorithms.

Methodology
The authors propose qSAT, a quantum SAT solver designed for hardware equivalence checking that utilizes Grover's search algorithm. The methodology is built upon three core technical pillars:

1. ESOP-Based Clause Generation: Instead of translating Boolean gates directly into Conjunctive Normal Form (CNF) clauses—which often introduces expensive auxiliary variables and high resource overhead—the authors employ an Exclusive-Sum-of-Product (ESOP) based generation method. By redefining logical equivalences (e.g., $p \Leftrightarrow (q \lor r)$) into ESOP forms (e.g., $p \oplus (\neg q \land \neg r)$), the quantum circuit interpretation requires fewer qubits, gates, and circuit depth.
2. Quantum Miter Circuit Realization: The verification problem is formulated as a "miter" circuit, which computes the XOR difference between a circuit-under-assessment ($G_I$) and a reference model ($G_R$). The paper details two quantum interpretations of this miter:
   • $V_F$: An economical version that retains the outcomes of operations on auxiliary variables.
   • $U_F$: A version that "uncomputes" auxiliary variables to associate the miter outcome strictly with the input state, essential for the oracle in Grover's algorithm.
     The number of qubits required is estimated as $|X| + 2|A| + 1$, where $|X|$ is the number of input variables and $|A|$ is the number of auxiliary variables.
3. qSAT Architecture and Optimization: The solver uses the $U_F$ miter as the oracle for Grover's algorithm to amplify the probability of finding counter-examples (CEXs). A key optimization strategy involves selecting reference models ($G_R$) that minimize the number of auxiliary variables. The paper presents case studies on Multiplexers and 1-bit Full-Adders, demonstrating that using ESOP-optimized reference models (denoted as $\hat{G}_R$) significantly reduces the number of required Grover iterations (by a factor of $\sqrt{2^{-3}}$ in specific cases) compared to standard CNF-based reference models.

Key Contributions
The paper outlines the following specific contributions:

• Architecture Development: The design of a comprehensive qSAT solver architecture that leverages Grover's search algorithm for finding solutions to constructed miter circuits.
• Search Space Optimization: The utilization of ESOP-based clause generation and miter circuit implementation to optimize the search space, reducing the overhead of qubits and gates.
• Resource Assessment: An evaluation of the qSAT solver based on gate overhead, solution probability, and operational fidelity across selected benchmarks with specific faults.
• Reference Model Analysis: A case study demonstrating how the choice of reference circuit (standard vs. ESOP-optimized) directly impacts Grover's iterations and quantum resource requirements.

Experimental Results
Experiments were conducted using the open-source Qiskit platform and an IBM quantum computer (specifically ibm_brisbane for fidelity analysis). The study evaluated various Boolean functions (AND, NAND, OR, NOR, XOR, XNOR, MUX, CARRY, and Full-Adder) with injected faults.

• Resource Efficiency: The ESOP-optimized approach ($G_F \oplus \hat{G}_R$) consistently required fewer resources than the standard approach ($G_F \oplus G_R$). For example, in the Full-Adder (FA) benchmark, the optimized version reduced the number of qubits from 30 to 24, CNOT gates (#CX) from 16,413 to 4,941, and circuit depth (#D) from 26,741 to 7,742.
• Accuracy: In ideal simulation environments (Qiskit Aer), the qSAT solver achieved a probability of SAT outcomes ($P(SAT) \geq 75\%$) for the optimized miters, comparable to the standard approach but with significantly lower resource consumption.
• Fidelity: Operational fidelity analysis on real quantum hardware showed that the $\hat{G}_R$ type reference models exhibited higher operational fidelity for almost all tested Boolean functions compared to the standard $G_R$ models.

Significance and Claims
The paper claims that the proposed qSAT architecture offers a viable path toward efficient hardware equivalence checking by reducing the quantum resource overhead (qubits, gates, and depth) associated with SAT solving. The authors state that this work represents "a first attempt towards design of a complete qSAT solver." They emphasize that the approach is linear in terms of the number of gates present in the circuits considered for verification and that the use of ESOP-based generation minimizes the quantum circuit interpretation overhead. The results suggest that optimizing the reference model is a critical factor in making quantum SAT solvers practical for current and near-future quantum hardware.