Skip to main content
SpringerLink
Log in

Biconditional Logic

  • Chapter
  • First Online:
New Data Structures and Algorithms for Logic Synthesis and Verification

  • 1095 Accesses

Abstract

In this chapter, we present Biconditional Binary Decision Diagrams (BBDDs), a novel canonical representation form for Boolean functions. BBDDs are binary decision diagrams where the branching condition, and its associated logic expansion, is biconditional on two variables. Empowered by reduction and ordering rules, BBDDs are remarkably compact and unique for a Boolean function. The interest of such representation form in modern Electronic Design Automation (EDA) is twofold. On the one hand, BBDDs improve the efficiency of traditional EDA tasks based on decision diagrams, especially for arithmetic intensive designs. On the other hand, BBDDs represent the natural and native design abstraction for emerging technologies where the circuit primitive is a comparator, rather than a simple switch. We provide, in this chapter, a solid ground for BBDDs by studying their underlying theory and manipulation properties. Thanks to an efficient BBDD software package implementation, we validate (i) runtime reduction in traditional decision diagrams applications with respect to other DDs, and (ii) improved synthesis of circuits in standard and emerging technologies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 54.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    A strong canonical form is a form of data pre-conditioning to reduce the complexity of equivalence test [46].

References

  1. C.Y. Lee2, Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38(4), 985–999 (1959)

    Google Scholar 

  2. S.B. Akers2, Binary decision diagrams. IEEE Trans. Comp. 100(6), 509–516 (1978)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  4. C. Yang, M. Ciesielski, BDS: A BDD-based logic optimization system. IEEE Trans. CAD IC Syst. 21(7): 866–876 (2002)

    Google Scholar 

  5. S. Malik et al., Logic verification using binary decision diagrams in a logic synthesis environment in IEEE International Conference on CAD (1988), pp. 6–9

    Google Scholar 

  6. M.S. Abadir et al., Functional test generation for digital circuits using binary decision diagrams. IEEE Trans. Comput. 100(4), 375–379 (1986)

    Article  Google Scholar 

  7. C. Scholl, R. Drechsler, B. Becker, Functional simulation using binary decision diagrams in IEEE International Conference on CAD (1997), pp. 8–12

    Google Scholar 

  8. U. Kebschull, W. Rosenstiel, E. Schubert, Multilevel logic synthesis based on functional decision diagrams, in IEEE European Conference Design Automation (1992), pp. 43–47

    Google Scholar 

  9. R. Drechsler et al., Ordered Kronecker functional decision diagrams-a data structure for representation and manipulation of Boolean functions. IEEE Trans. CAD IC Syst. 17(10), 965–973 (1998)

    Google Scholar 

  10. CUDD: CU Decision Diagram Package Release 2.5.0. http://vlsi.colorado.edu/fabio/CUDD/cuddIntro.html

  11. Decision Diagram-Package PUMA. http://ira.informatik.uni-freiburg.de/software/puma/pumamain.html

  12. M. De Marchi et al., Polarity control in double-gate (gate-all-around vertically stacked silicon nanowire FETs, in IEEE Electron Devices Meeting (2012), pp. 8–14

    Google Scholar 

  13. Y. Lin et al., High-performance carbon nanotube field-effect transistor with tunable polarities. IEEE Trans. Nanotech. 4(5), 481–489 (2005)

    Article  Google Scholar 

  14. N. Harada et al., A polarity-controllable graphene inverter. Appl. Phys. Lett. 96(1), 012102 (2010)

    Article  Google Scholar 

  15. D. Lee2 et al., Combinational logic design using six-terminal NEM relays. IEEE Trans. CAD IC Syst. 32(5), 653–666 (2013)

    Google Scholar 

  16. L. Amaru, P.-E. Gaillardon, S. Mitra, G. DeMicheli, New logic synthesis as nanotechnology enabler, in Proceedings of the IEEE (2015)

    Google Scholar 

  17. L. Amaru, P.-E. Gaillardon, G. De Micheli, Biconditional BDD: a novel canonical representation form targeting the synthesis of XOR-rich circuits, in Design Automation and Test in Europe (2013), pp. 1014–1017

    Google Scholar 

  18. L. Amaru, P.-E. Gaillardon, G. De Micheli, An efficient manipulation package for biconditional binary decision diagrams, in Design Automation and Test in Europe (2014), pp. 296–301

    Google Scholar 

  19. BBDD package. http://lsi.epfl.ch/BBDD

  20. L. Kathleen, Logic and Boolean Algebra, Barrons Educational Series (1979)

    Google Scholar 

  21. G. De Micheli, Synthesis and Optimization of Digital Circuits (McGraw-Hill, New York, 1994)

    Google Scholar 

  22. I. Wegener, Branching Programs and Binary Decision Diagrams: Theory and Applications, vol. 4 (SIAM, Philadelphia, 2000)

    Google Scholar 

  23. M. Kreuzer, L. Robbiano, Computational Commutative Algebra, vol. 1 (Springer, Berlin, 2005)

    MATH  Google Scholar 

  24. R.E. Bryant, On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205–213 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  25. J. Gergov, C. Meinel, Mod-2-OBDDs A data structure that generalizes EXOR-sum-of-products and ordered binary decision diagrams. Form. Methods Syst. Des. 8(3), 273–282 (1996)

    Article  Google Scholar 

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

    Article  MATH  Google Scholar 

  27. T. Koshy, Discrete Mathematics with Applications (Academic Press, Cambridge, 2004)

    Google Scholar 

  28. T.S. Czajkowski, S.D. Brown, Functionally linear decomposition and synthesis of logic circuits for FPGAs. IIEEE Trans. CAD IC Syst. 27(12), 2236–2249 (2008)

    Google Scholar 

  29. J.F. Groote, J. Van de Pol, Equational Binary Decision Diagrams, Logic for programming and automated reasoning (Springer, Heidelberg, 2000)

    Book  MATH  Google Scholar 

  30. S. Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, in IEEE Conference on Design Automation (DAC) (1993), pp. 272–277

    Google Scholar 

  31. C. Meinel, F. Somenzi, T. Theobald, Linear sifting of decision diagrams, in IEEE Conference on Design Automation (DAC) (1997), pp. 202–207

    Google Scholar 

  32. W. Gunther, R. Drechsler, BDD minimization by linear transformations. Adv. Comput. Syst. 525–532 (1998)

    Google Scholar 

  33. M. Fujita, Y. Kukimoto, R. Brayton, BDD minimization by truth table permutation, in IEEE International Symposium on CAS (1996), pp. 596–599

    Google Scholar 

  34. E.M. Clarke, M. Fujita, X. Zhao, Hybrid decision diagrams, in IEEE International Conference on CAD (1995), pp. 159–163

    Google Scholar 

  35. E.I. Goldberg, Y. Kukimoto, R.K. Brayton, Canonical TBDD’s and their application to combinational verification, in ACM/IEEE International Workshop on Logic Synthesis (1997)

    Google Scholar 

  36. U. Kebschull, W. Rosenstiel, Efficient graph-based computation and manipulation of functional decision diagrams, in IEEE Euro Conference on Design Automation (1993), pp. 278–282

    Google Scholar 

  37. J.E. Rice, Making a choice between BDDs and FDDs, in ACM/IEEE International Workshop on Logic Synthesis (2005)

    Google Scholar 

  38. R. Drechsler, Ordered Kronecker Functional Decision Diagrams und ihre Anwndung, Ph.D. Thesis, 1996

    Google Scholar 

  39. S. Grygiel, M.A. Perkowski, New compact representation of multiple-valued functions, relations, and non-deterministic state machines, in IEEE International Conference on Computer Design (1998), pp. 168–174

    Google Scholar 

  40. A. Srinivasan, T. Kam, S. Malik, R. Brayton, Algorithms for Discrete Function Manipulation, in IEEE International Conference on CAD (1990), pp. 92–95

    Google Scholar 

  41. S. Minato et al., Shared BDD with attributed edges for efficient boolean function manipulation, in IEEE Conference on Design Automation (DAC) (1990), pp. 52–57

    Google Scholar 

  42. B. Becker, R. Drechsler, How many decomposition types do we need?, in IEEE Euro Conference on Design Automation (1995), pp. 438–442

    Google Scholar 

  43. B. Becker, R. Drechsler, M. Theobald, On the expressive power of OKFDDs. Form. Methods Syst. Des. 11(1), 5–21 (1997)

    Article  Google Scholar 

  44. R. Drechsler, B. Becker, Binary Decision Diagrams: Theory and Implementation (Kluwer Academic Publisher, The Netherlands, 1998)

    Google Scholar 

  45. P. Tarau, Pairing Functions, Boolean Evaluation and Binary Decision Diagrams, arxiv preprint arXiv:0808.0555 (2008)

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

    Google Scholar 

  47. R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, in IEEE International Conference on CAD (1993), pp. 42–47

    Google Scholar 

  48. An iterative decoder for Product Code—from Open Cores: http://opencores.org/project,product_code_iterative_decoder

  49. S. Panda, F. Somenzi, Who are the variables in your neighborhood, in IEEE International Conference on CAD (1995), pp. 74–77

    Google Scholar 

  50. B. Bollig et al., Simulated annealing to improve variable orderings for OBDDs, in ACM/IEEE International Workshop on Logic Synthesis (1995)

    Google Scholar 

  51. R. Drechsler et al., A genetic algorithm for variable ordering of OBDDs, in ACM/IEEE International Workshop on Logic Synthesis (1995)

    Google Scholar 

  52. ABC synthesis tool - available online

    Google Scholar 

  53. J. Hagenauer, E. Offer, L. Papke, Iterative decoding of binary block and convolutional codes. IEEE Trans. Inf. Theory 42(2), 429–445 (1996)

    Article  MATH  Google Scholar 

  54. A. Picart, R. Pyndiah, Adapted iterative decoding of product codes, in Global Telecommunications Conference, 1999. GLOBECOM’99, vol. 5 (IEEE, New York, 1999)

    Google Scholar 

  55. A. Chattopadyay, et al., Reversible logic synthesis via biconditional binary decision diagrams, in Proceedings of the ISMVL 15

    Google Scholar 

  56. RevLib is an online resource for benchmarks within the domain of reversible and quantum circuit design. http://www.revlib.org

  57. C.H. Bennett, Logical reversibility of computation. IBM J. Res. Dev. 17(6), 525532 (1973)

    Article  MathSciNet  Google Scholar 

  58. M. Nielsen, I. Chuang, Quantum Computation and Quantum Information (Cambridge University Press, Cambridge, 2000)

    MATH  Google Scholar 

  59. R. Cuykendall, D.R. Andersen, Reversible optical computing circuits. Opt. Lett. 12(7), 542544 (1987)

    Article  Google Scholar 

  60. R.C. Merkle, Reversible electronic logic using switches, in Nanotechnology, vol. 4 (1993), p. 2140

    Google Scholar 

  61. A. Barenco et al., Elementary gates for quantum computation, in Physical Review (1995)

    Google Scholar 

  62. O. Loh, H. Espinosa, Nanoelectromechanical contact switches. Nat. Nanotechnol. 7(5), 283–295 (2012)

    Article  Google Scholar 

  63. Nano-Electro-Mechanical Switches, ITRS, white paper (2008)

    Google Scholar 

  64. V. Pott et al., Mechanical computing redux: relays for integrated circuit applications. Proc. IEEE 98(12), 2076–2094 (2010)

    Article  Google Scholar 

  65. Sharma, P., Perruisseau-Carrier, J., Moldovan, C., Ionescu, A. Electromagnetic performance of RF NEMS graphene capacitive switches. IEEE Trans. Nanotech. (2014)

    Google Scholar 

  66. Dana Weinstein, Sunil A. Bhave, The resonant body transistor. Nano Lett. 10(4), 1234–1237 (2010)

    Article  Google Scholar 

  67. D. Lee et al., Combinational logic design using six-terminal NEM relays. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(5), 653–666 (2013)

    Article  Google Scholar 

  68. M. Spencer et al., Demonstration of integrated micro-electro-mechanical relay circuits for VLSI applications. IEEE J. Solid State Circuits 46(1), 308–320 (2011)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Synopsys Inc., Santa Clara, CA, USA

    Luca Gaetano Amaru

Authors
  1. Luca Gaetano Amaru
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Gaetano Amaru .

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Amaru, L.G. (2017). Biconditional Logic. In: New Data Structures and Algorithms for Logic Synthesis and Verification. Springer, Cham. https://doi.org/10.1007/978-3-319-43174-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-43174-1_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-43173-4

  • Online ISBN: 978-3-319-43174-1

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation