Quantum logic synthesis by symbolic reachability analysis

ABSTRACT

Reversible quantum logic plays an important role in quantum computing. In this paper, we propose an approach to optimally synthesize quantum circuits by symbolic reachability analysis where the primary inputs are purely binary. we use symbolic reachability analysis, a technique most commonly used in model checking (a way of formal verification), to synthesize the optimum quantum circuits. We present an exact synthesis method with optimal quantum cost and a speedup method with non-optimal quantum cost. Both our methods guarantee the synthesizeability of all reversible circuits. Unlike previous works which use permutative reversible gates, we use a lower level library which includes non-permutative quantum gates. For the first time, problems in quantum logic synthesis have been reduced to those of multiple-valued logic synthesis thus reducing the search space and algorithm complexity. We synthesized quantum circuits for gate, half-adder, full-adder, etc. with the smallest cost.. Our approach obtains the minimum cost quantum circuits for Miller's gate, half-adder, and full-adder, which are better than previous results. In addition, we prove the minimum quantum cost (using our elementary quantum gates) for Fredkin, Peres, and Toffoli gates. Our work constitutes the first successful experience of applying satisfiability with formal methods to quantum logic synthesis.

REFERENCES

• 1: A. Barenco et al. Elementary gates for quantum computation. Physical Review A, 52(5):3457--3467, 1995.
• 2: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 3: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 4: Fady Copty , Limor Fix , Ranan Fraer , Enrico Giunchiglia , Gila Kamhi , Armando Tacchella , Moshe Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting, Proceedings of the 13th International Conference on Computer Aided Verification, p.436-453, July 18-22, 2001
• 5: D. Deutsch. Quantum computational networks. Royal Society of London Series A, 425:73--90, 1989.
• 6: A. Ekert et al. Basic concepts in quantum computation. In Coherent atomic matter waves, volume 72 of Lectures Notes in Les Houches Physics School. Springer, August 1999.
• 7: E. Fredkin and T. Toffoli. Conservative logic. Int. Journal of Theoretical Physics, 21:219--253, 1982.
• 8: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 9: J. Gruska. Quantum Computing. Osborne McGraw-Hill, April 1999.
• 10: W. N. N. Hung et al. BDD Minimization by Scatter Search. IEEE Trans. CAD, 21(8), August 2002.
• 11: W. N. N. Hung et al. Segmented Channel Routability via Satisfiability. ACM Trans. Design Automation, July 2004.
• 12: Kazuo Iwama , Yahiko Kambayashi , Shigeru Yamashita, Transformation rules for designing CNOT-based quantum circuits, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514026]
• 13: A. Khlopotine et al. Reversible logic synthesis by iterative compositions. In Int. Workshop on Logic Synthesis, 2002.
• 14: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 15: D. M. Miller. Spectral and two-place decomposition techniques in reversible logic. In Proc. IEEE Midwest Symp. Circuits and Systems, August 2002.
• 16: D. Michael Miller , Dmitri Maslov , Gerhard W. Dueck, A transformation based algorithm for reversible logic synthesis, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775915]
• 17: Quantum computation and quantum information, Cambridge University Press, New York, NY, 2000
• 18: A. Peres. Reversible logic and quantum computers. Physical Review A, 32:3266--3276, 1985.
• 19: Vivek V. Shende , Aditya K. Prasad , Igor L. Markov , John P. Hayes, Reversible logic circuit synthesis, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.353-360, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774625]
• 20: T. Sleator and H. Weinfurter. Realizable universal quantum logic gates. Physical Review Letters, 74(20):4087--4090, 1995.
• 21: J. A. Smolin and D. P. DiVincenzo. Five two-bit quantum gates are sufficient to implement the quantum Fredkin gate. Physical Review A, 53:2855--2856, 1996.
• 22: Xiaoyu Song , William N. N. Hung , Alan Mishchenko , Malgorzata Chrzanowska-Jeske , Andrew Kennings , Alan Coppola, Board-level multiterminal net assignment for the partial cross-bar architecture, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.3, p.511-514, June 2003 [doi>10.1109/TVLSI.2003.812322]
• 23: X. Song et al. Algebraic characteristics of reversible gates. Theory of Computing Systems, 2004.
• 24: L. M. K. Vandersypen et al. Experimental realization of Shor's quantum factoring algorithm using nuclear magnetic resonance. Nature, 414:883--887, Dec 2001.
• 25: G. Yang et al. Majority-Based Reversible Logic Gate. In Proc. Int. Symp. Representations and Methodology of Future Computing Technologies (RM2003), March 2003.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

General Terms:
Algorithms, Design

Keywords:
formal verification, model checking, quantum computing, reversible logic, satisfiability