qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking
Abhoy Kole, Mohammed Elkacem Djeridane, Lennart Weingarten, Kamalika Datta, Rolf Drechsler · ACM Journal on Emerging Technologies in Computing Systems · 2025
The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential runtime 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 (ESOP)-based generation of the Conjunctive Normal Form (CNF) equivalent clauses demands 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.