nach oben

Erschienen in:

2010 | OriginalPaper | Buchkapitel

2. Preliminaries

verfasst von : Robert Wille, Rolf Drechsler

Erschienen in: Towards a Design Flow for Reversible Logic

Verlag: Springer Netherlands

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This chapter provides the basic definitions and notations to keep the remaining book self-contained. The chapter is divided into three parts. In the first section, Boolean functions, reversible functions, and the respective circuit descriptions are introduced. This builds the basis for all approaches described in this book. Since many of the proposed techniques exploit decision diagrams and satisfiability solvers, respectively, the basic concepts of these core techniques are also introduced in the last two sections. All descriptions are thereby kept brief, but references for a more in-depth treatment are provided.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Introduction

Nächstes Kapitel Synthesis of Reversible Logic

The controlled-NOT gate is also known as CNOT or Feynman gate.

SWORD has been co-developed by the authors of this book. Even if SWORD is focused on problem-specific knowledge, it can also be used as an SMT solver and already participated in the respective SMT competitions in 2008 [WSD08] and 2009 [JSWD09], respectively.

[BB09]

R. Brummayer, A. Biere, Boolector: An efficient SMT solver for bit-vectors and arrays, in Tools and Algorithms for the Construction and Analysis of Systems (2009), pp. 174–177

[BBC+95]

A. Barenco, C.H. Bennett, R. Cleve, D.P. DiVinchenzo, N. Margolus, P. Shor, T. Sleator, J.A. Smolin, H. Weinfurter, Elementary gates for quantum computation. Am. Phys. Soc. 52, 3457–3467 (1995)

[BBC+05]

M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. Rossum, S. Schulz, R. Sebastiani, The MathSAT 3 system, in Int. Conf. on Automated Deduction (2005), pp. 315–321

[BCCZ99]

A. Biere, A. Cimatti, E. Clarke, Y. Zhu, Symbolic model checking without BDDs, in Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1579 (Springer, Berlin, 1999), pp. 193–207 CrossRef

[Ben05]

M. Benedetti, sKizzo: a suite to evaluate and certify QBFs, in Int’l Conf. on Automated Deduction (2005), pp. 369–376

[Bie05]

A. Biere, Resolve and expand, in Theory and Applications of Satisfiability Testing. LNCS, vol. 3542 (Springer, Berlin, 2005), pp. 59–70 CrossRef

[BRB90]

K.S. Brace, R.L. Rudell, R.E. Bryant, Efficient implementation of a BDD package, in Design Automation Conf. (1990), pp. 40–45

[Bry86]

R.E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986) MATHCrossRef

[BW96]

B. Bollig, I. Wegener, Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996) MATHCrossRef

[CBRZ01]

E.M. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001) MATHCrossRef

[Coo71]

S.A. Cook, The complexity of theorem proving procedures, in Symposium on Theory of Computing (1971), pp. 151–158

[DB98]

R. Drechsler, B. Becker, Binary Decision Diagrams—Theory and Implementation (Kluwer Academic, Dordrecht, 1998)

[DBW+07]

S. Deng, J. Bian, W. Wu, X. Yang, Y. Zhao, EHSAT: An efficient RTL satisfiability solver using an extended DPLL procedure, in Design Automation Conf. (2007), pp. 588–593

[DEF+08]

R. Drechsler, S. Eggersglüß, G. Fey, A. Glowatz, F. Hapke, J. Schloeffel, D. Tille, On acceleration of SAT-based ATPG for industrial designs. IEEE Trans. CAD 27, 1329–1333 (2008)

[DLL62]

M. Davis, G. Logeman, D. Loveland, A machine program for theorem proving. Commun. ACM 5, 394–397 (1962) MATHCrossRef

[DM06a]

B. Dutertre, L. Moura, A fast linear-arithmetic solver for DPLL(T), in Computer Aided Verification. LNCS, vol. 4114 (Springer, Berlin, 2006), pp. 81–94 CrossRef

[DM06b]

B. Dutertre, L. Moura, The YICES SMT solver (2006). Available at http://yices.csl.sri.com/

[DP60]

M. Davis, H. Putnam, A computing procedure for quantification theory. J. ACM 7, 506–521 (1960) MathSciNetCrossRef

[EFD05]

R. Ebendt, G. Fey, R. Drechsler, Advanced BDD Optimization (Springer, Berlin, 2005)

[ES04]

N. Eén, N. Sörensson, An extensible SAT solver, in SAT 2003. LNCS, vol. 2919 (Springer, Berlin, 2004), pp. 502–518

[FT82]

E.F. Fredkin, T. Toffoli, Conservative logic. Int. J. Theor. Phys. 21(3/4), 219–253 (1982) MathSciNetMATHCrossRef

[GD07]

V. Ganesh, D.L. Dill, A decision procedure for bit-vectors and arrays, in Computer Aided Verification (2007), pp. 519–531

[GN02]

E. Goldberg, Y. Novikov, BerkMin: a fast and robust SAT-solver, in Design, Automation and Test in Europe (2002), pp. 142–149

[HSY+06]

W.N.N. Hung, X. Song, G. Yang, J. Yang, M. Perkowski, Optimal synthesis of multiple output Boolean functions using a set of quantum gates by symbolic reachability analysis. IEEE Trans. CAD 25(9), 1652–1663 (2006)

[JSWD09]

J.C. Jung, A. Sülflow, R. Wille, R. Drechsler, SWORD v1.0, Satisfiability Modulo Theories Competition (2009)

[Lar92]

T. Larrabee, Test pattern generation using Boolean satisfiability. IEEE Trans. CAD 11, 4–15 (1992)

[MD04a]

D. Maslov, G.W. Dueck, Improved quantum cost for n-bit Toffoli gates. IEE Electron. Lett. 39, 1790 (2004) CrossRef

[MD04b]

D. Maslov, G.W. Dueck, Reversible cascades with minimal garbage. IEEE Trans. CAD 23(11), 1497–1509 (2004)

[Mer07]

N.D. Mermin, Quantum Computer Science: An Introduction (Cambridge University Press, Cambridge, 2007) MATHCrossRef

[MK04]

M.M. Mano, C.R. Kime, Logic and Computer Design Fundamentals (Pearson Education, Upper Saddle River, 2004)

[MMZ+01]

M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in Design Automation Conf. (2001), pp. 530–535

[MS99]

J.P. Marques-Silva, K.A. Sakallah, GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999) MathSciNetCrossRef

[MT06]

D.M. Miller, M.A. Thornton, QMDD: A decision diagram structure for reversible and quantum circuits, in Int’l Symp. on Multi-Valued Logic (2006), p. 6

[MT08]

D.M. Miller, M.A. Thornton, Multiple-Valued Logic: Concepts and Representations (Morgan and Claypool, San Rafael, 2008)

[MYDM05]

D. Maslov, C. Young, G.W. Dueck, D.M. Miller, Quantum circuit simplification using templates, in Design, Automation and Test in Europe (2005), pp. 1208–1213

[NC00]

M. Nielsen, I. Chuang, Quantum Computation and Quantum Information (Cambridge Univ. Press, Cambridge, 2000) MATH

[Pap93]

C.H. Papadimitriou, Computational Complexity (Addison Wesley, Reading, 1993)

[PBG05]

M.R. Prasad, A. Biere, A. Gupta, A survey of recent advances in SAT-based formal verification. Softw. Tools Technol. Transf. 7(2), 156–173 (2005) CrossRef

[Per85]

A. Peres, Reversible logic and quantum computers. Phys. Rev. A 32, 3266–3276 (1985) MathSciNetCrossRef

[Pit99]

A.O. Pittenger, An Introduction to Quantum Computing Algorithms (Birkhauser, Basel, 1999)

[PMH08]

K. Patel, I. Markov, J. Hayes, Optimal synthesis of linear reversible circuits. Quantum Inf. Comput. 8(3–4), 282–294 (2008) MathSciNetMATH

[Rud93]

R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, in Int’l Conf. on CAD (1993), pp. 42–47

[SD96]

J.A. Smolin, D.P. DiVincenzo, Five two-bit quantum gates are sufficient to implement the quantum fredkin gate. Phys. Rev. A 53(4), 2855–2856 (1996) MathSciNetCrossRef

[Sha38]

C.E. Shannon, A symbolic analysis of relay and switching circuits. Trans. AIEE 57, 713–723 (1938)

[Som01]

F. Somenzi, CUDD: Cu Decision Diagram Package Release 2.3.1 (University of Colorado at Boulder, Boulder, 2001)

[SPMH03]

V.V. Shende, A.K. Prasad, I.L. Markov, J.P. Hayes, Synthesis of reversible logic circuits. IEEE Trans. CAD 22(6), 710–722 (2003)

[SVAV05]

A. Smith, A.G. Veneris, M.F. Ali, A. Viglas, Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. CAD 24(10), 1606–1621 (2005)

[TG08]

M.K. Thomson, R. Glück, Optimized reversible binary-coded decimal adders. J. Syst. Archit. 54, 697–706 (2008) CrossRef

[Tof80]

T. Toffoli, Reversible computing, in Automata, Languages and Programming, ed. by W. de Bakker, J. van Leeuwen (Springer, Berlin, 1980), p. 632. Technical Memo MIT/LCS/TM-151, MIT Lab. for Comput. Sci. CrossRef

[WFG+07]

R. Wille, G. Fey, D. Große, S. Eggersglüß, R. Drechsler, SWORD: A SAT like prover using word level information, in VLSI of System-on-Chip (2007), pp. 88–93

[WFG+09]

R. Wille, G. Fey, D. Große, S. Eggersglüß, R. Drechsler, SWORD: A SAT like prover using word level information, in VLSI-SoC: Advanced Topics on Systems on a Chip: A Selection of Extended Versions of the Best Papers of the Fourteenth International Conference on Very Large Scale Integration of System on Chip, ed. by R. Reis, V. Mooney, P. Hasler (Springer, Berlin, 2009), pp. 175–192

[WSD08]

R. Wille, A. Sülflow, R. Drechsler, SWORD v0.2—Module-based SAT Solving, Satisfiability Modulo Theories Competition (2008)

[ZSM+05]

J. Zhang, S. Sinha, A. Mishchenko, R. Brayton, M. Chrzanowska-Jeske, Simulation and satisfiability in logic synthesis, in Int’l Workshop on Logic Synth. (2005), pp. 161–168

Titel: Preliminaries
verfasst von: Robert Wille
Rolf Drechsler
Verlag: Springer Netherlands
Buch: Towards a Design Flow for Reversible Logic
Print ISBN: 978-90-481-9578-7

Electronic ISBN: 978-90-481-9579-4

Copyright-Jahr: 2010
DOI: https://doi.org/10.1007/978-90-481-9579-4_2