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

TL;DR

This paper introduces qSAT, a quantum SAT solver designed for hardware equivalence checking that leverages Grover's algorithm to achieve a quadratic speed-up over classical search. It advances ESOP-based clause generation to minimize qubits and circuit depth, and presents a quantum miter circuit architecture with two realizations to optimize resource use. Through theoretical analysis and experiments on Qiskit and IBM hardware, it demonstrates reduced qubit counts, gate counts, and circuit depth, as well as improved fidelity when using a reduced reference model. The approach offers a practical pathway for deploying quantum-assisted hardware verification on NISQ devices, marking a notable step toward a complete qSAT solver.

Abstract

The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential run-time in several instances. In this work we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover's algorithm. The Exclusive-Sum-of-Product based generation of the Conjunctive Normal Form equivalent clauses demand less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover's iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open-source Qiskit platform and IBM quantum computer.

Figures (10)

• Figure 1: Time and memory requirements of SAT based verification of multipliers.
• Figure 2: Quantum circuit interpretation of a Boolean function, $\mathcal{F}(a,b) = a \Rightarrow b$.
• Figure 3: Miter circuit for hardware verification of Boolean circuits.
• Figure 4: An illustration of a quantum miter circuit realization; (a) classical miter circuit $\mathcal{F}$ for doing equivalence checking of Boolean circuits $\mathcal{G_I}$ and $\mathcal{G_R}$; (b) quantum circuit interpretation of $\mathcal{F}$ additionally realizing operations inferred on auxiliary variables $a_1$, $a_2$ and $a_3$; (c) uncomputing the inferences on $a_1$, $a_2$ and $a_3$ applying respective operations in reverse order.
• Figure 5: (a) A miter network for verifying the implementation of a $3$-input NAND operation using a pair of $2$-input AND and NAND operations; (b) quantum circuit interpretation of the miter network.