qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909047876222976 |
|---|---|
| author | Kole, Abhoy Djeridane, Mohammed E. Weingarten, Lennart Datta, Kamalika Drechsler, Rolf |
| author_facet | Kole, Abhoy Djeridane, Mohammed E. Weingarten, Lennart Datta, Kamalika Drechsler, Rolf |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_03917 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking Kole, Abhoy Djeridane, Mohammed E. Weingarten, Lennart Datta, Kamalika Drechsler, Rolf Quantum Physics Emerging Technologies 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. |
| title | qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking |
| topic | Quantum Physics Emerging Technologies |
| url | https://arxiv.org/abs/2409.03917 |