Quantum Logic Synthesis with Formal Verification
Kaitlin N. Smith, Mitchell Aaron Thornton · 2019
Quantum computers capable of practical information processing are emerging rapidly. As these devices become more advanced, tools will be needed for converting generalized quantum algorithms into formally-verified forms that are executable on real quantum machines. In this work, a prototype tool is presented that transforms quantum algorithms into executable specifications where optimization procedures yield 9-24 % cost improvement on a range of benchmarks. Additionally, the tool incorporates formal verification internally with Quantum Multiple-valued Decision Diagrams to confirm that the generated technology-dependent executable is functionally equivalent to the original, technology-independent algorithm. Experimental results are provided that target the Rigetti family of quantum processing units although the tool may also target other architectures.