Table of Contents
Table of Contents
Preface
Chapter 1. Introduction to Binary Decision Diagrams
Chapter 2. Boolean Algebras and Boolean Functions
Chapter 3. BDD: Data Structure and Algorithms for Operation with Boolean Functions
Chapter 4. BDD Efficient Implementation
Chapter 5. Series-Parallel BDD: Theory and Applications
Chapter 6. Simple Logic Implications (SLI) and False-Noise Analysis
Chapter 7. Detecting False Paths in Static Timing Analysis Basing on Logic Implications
Chapter 8. Obfuscation of Digital Circuits Based on Use of Logic Implications
Chapter 9. Simulation of Digital CMOS Circuits Using Ternary Decision Diagrams and Simple Logic Implications
Index
References
[1] Garey M. R., Johnson D. S. Computers and Intractability
W. H. Freeman and Co., 1979.[2] Karchmer M. Communication Complexity: A New Approach to Circuit Depth MIT Press, 1989.[3] Brayton R., Hachtel G., McMullen C., Sangiovanni-Vincentelli A. Logic Minimization Algorithms for VLSI Synthesis Kluwer Academic Publishers, 1984.[4] De Micheli G. Synthesis and Optimization of Digital Circuits McGraw Hill, 1994.[5] Cormen T. H., Leiserson C. E., Rivest R. H., Stein C. Introduction to Algorithms MIT Press, 2001.[6] Sipser M. Introduction to the Theory of Computation, edn Course Technology, 2005.[7] Schoning U., Pruim R. Gems of Theoretical Computer Science Springer, 1998.[8] Bryant R. Graph-Based Algorithms for Boolean Function Manipulation IEEE Trans. on Computers, 1986, v. C-35, pp. 677-691.[9] Aziz A., Tasiran S., Brayton R. BDD Variable Ordering for Interacting Finite State Machines DAC-94, pp. 283-288.[10] Berman C. L. Ordered Binary Decision Diagrams and Circuit Structure ICCD-89.[11] Malik S., Wang A. R., Brayton R. K., Sangiovanni-Vincentelli A. Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment ICCAD-88, pp. 6-9.[12] Wegener L. Branching Programs and Binary Decision Diagrams SIAM, 2000.[13] Glebov A. L., Blaauw D., Jones L.G. Transistor Reordering for Low Power CMOS Gates Using SP-BDD Representation Intern. Symp. On Low Power Design. Dana Point, 1995, p.161.[14] Gavrilov S. V., Glebov A. L., Stempkovsky A. L. Fast algorithm of power calculation for digital CMOS circuits Electronics: NTB. 2002, №4, p. 42 (in Russian).[15] Glebov A. L., Gurary M. M., Zharov M. M. et al. Latest problems in CAD simulation Moscow: Nauka, 2003, 430 pp. (in Russian).[16] Gupta A. Formal Hardware Verification Methods: A Survey Formal Method Syst. Des., 1993, v. 1, pp. 151-238.[17] Kuehlmann A., Krohm F. Equivalence Checking Using Cuts and Heaps DAC-97.[18] McMillan K. L. Symbolic Model Checking Kluwer Academic Publishers, 1993.[19] Yuan J., Pixley, C., Aziz A. Constraint-Based Verification Springer, 2006.[20] Brace K., Rudell R., Bryant R. Efficient Implementation of a BDD Package DAC-90.[21] Somenzi F. Colorado University Decision Diagram Package http://vlsi.colorado.edu/~fabio/.Chapter 2[1] Stempkovsky A., Gavrilov S., Glebov A. Methods of logical and logical-timing anslysis of digital CMOS VLSI Moscow, 2007, 220 pp.[2] Boole G. The Mathematical Analysis of Logic London: G. Bell, 1847.[3] Boole G. An Investigation of the Laws of Thought London: Walton, 1854.[4] Jevons W. S. Pure Logic, or the Logic of Quality Apart from Quantity London: Stanford, 1864.[5] Poretsky P. Sept lois fondamentales de la theorie des egalites logiques Bull. De la Soc. Physico-Mathematique de Kasan, 1898, ser. 2, vol. 8, pp. 33-103, 129-181, 183-216.[6] Schroder E. Vorlesungen uber die Algebra der Logik Leipzig: Vol. 1, 1890; Vol. 2, 1891; Vol. 3, 1895; Vol. 2, Part 2, 1905.[7] Venn J. Symbolic Logic, edition London: Macmillan, 1894.[8] Whitehead A. N. A Treatise on Universal Algebra, with Applications Cambridge: The University Press, 1898.[9] Whitehead A. N. Memoir on the algebra of symbolic logic, Part 1 Am.J. of Math. vol. 23, 1901, pp. 139-165, 297-316.[10] Ehrenfest P. Review of L. Couturat, The Algebra of Logic Journ. Russian Phys. & Chem. Soc. 1910, sec. 2, vol. 42, no. 10, p. 382.[11] Couturat L. L’algebre de la Logique Paris: Scientia, 1905.[12] Shestakov V. Some mathematical methods of constructing and simplifying two-terminal electrical networks of class A Moscow, 1938.[13] Shannon C. E. A symbolic analysis of relay and switching circuits Trans. Amer. Inst. Elec. Engrs, 1938, vol. 57, pp. 713-723.[14] Nakasima A. Algebraic expressions relative to simple partial paths in the relay circuits (in Japanese) J. Inst. Electrical Communication Engineers of Japan, August 1937, no. 173.[15] Akers S. B. On a theory of Boolean functions J. Soc. Indust. Appl.Math. 1959, vol. 7, no. 4, pp. 487-498.[16] Ashenhurst R.L. Simultaneous equations in switching theory, Report BL-5 Harvard Computation Lab. Harvard University, 1954, pp. 1-8.[17] Ledley R. S. A digitalization, systematization, and formulation of the theory and methods of the propositional calculus, NBS Report 3363 Nat’l. Bureau of Standards, U.S. Dep’t. of Commerce, 1 Feb 1954.[18] Stone M. H. The theory of representations for Boolean algebras Trans. Amer. Math. Soc. 1936, vol. 40, pp. 37-111.[19] Phister M. Logical Design of Digital Computers New York: John Wiley, 1958.[20] Brown F. M. Boolean Reasoning London: Kluwer, 1990.[21] Lowenheim L. Uber die Auflosung von Gleichungen im logischen Gebietekalkul Math. Ann. vol. 68, 1910, pp. 169-207.[22] Muller E. Abriss der Algebra der Logik 1909-10.Chapter 3[1] R. E. Bryant. “Graph-based algorithms for Boolean function manipulation,” IEEE Trans. on Computers, v. C-35, 1986, pp. 677-691[2] C. Y. Lee. “Representation of switching circuits by binary-decision programs,” Bell Syst. Tech. J. v.38, 1959, pp. 985-999.[3] S. B. Akers. “Binary decision diagrams,” IEEE Trans. on Computers, v. C-27, 1978, pp. 509-516.[4] M.R.Garey, D.S.Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. New York: Freeman, 1979.[5] F. J. Hill, G. R. Peterson. Introduction to Switching Theory and Logical Design. New York: Wiley, 1974.[6] J. P. Roth. Computer Logic, Testing, and Verification. Rockville, MD:Computer Science Press, 1980.[7] R. Brayton et al. “Fast recursive Boolean function manipulation,” Proc. Int. Symp. Circuits and Syst., IEEE Rome, Italy, 1982, pp. 58-62.[8] B. M. E. Moret. “Decision trees and diagrams,” Ass. Comput. Mach.Comput. Surv. v. 14, 1982, pp. 593-623.[9] S. Fortune, J. Hopcroft, E. M. Schmidt. “The complexity of equivalence and containment for free single variable program schemes,” Automata, Languages and Programming, Lecture Notes in Computer Science, v. 62, 1978, pp. 227-240.[10] R. W. Payne. “Reticulation and other methods of reducing the size of printed diagnostic keys,”J. Gen. Microbiol. v. 98, 1977, pp. 595-597.[11] R. Brayton et al. Logic Minimization Algorithm for VLSI Synthesis. Hingham, MA: Kluwer, 1984.[12] C. E. Shannon. “A symbolic analysis of relay and switching circuits,” Trans. AIEE v.57, 1938, pp.713-723.[13] C. S. Wallace. “A suggestion for a fast multiplier,” IEEE Trans. Electron. Comput. v. EC-13, 1964, pp.14-17.[14] A. V. Aho, J. E. Hopcroft, J. D. Ullman. The Design and Analysis of Computer Algorithms. Reading, MA: Addison-Wesley, 1974.[15] J. S. Jephson, R. P. McQuarrie, R. E. Vogelsberg. “A three-level design verification system,” IBM Syst. J. v. 8, 1969, pp. 178-188.[16] TTL Data Book, Texas Instruments, Dallas, TX, 1976.[17] M. Rowan-Robinson. Cosmology. London: Oxford University Press, 1977.[18] S. B. Akers. “Functional testing with binary decision diagrams,” Proc. 8 IEEE Conf. Fault-Tolerant Comput. 1978, pp.75-82.[19] R. P. Brent, H. T. Kung. “The area-time complexity of binary multiplication,” J. Ass. Comput. Mach. v. 28, 1981, pp. 521-534.[20] H. Abelson, P. Andreae. “Information transfer and area-time trade-offs for VLSI multiplication,” Commun. Ass. Comput. Mach. v. 23, 1980, pp.20-23.Chapter 4[1] Brace K. S., Rudell R. L., Bryant R. E. Efficient Implementation of a BDD Package DAC-1990, pp. 40-45.[2] Meinel C., Theobald T. Algorithms and Data Structures in VLSI Design Berlin: Springer-Verlag, 1998.Chapter 5[1] R. E. Bryant. “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans on Computers, 1986, v. 35, n. 8, p. 677.[2] S. Devadas, S. Malik. “A Survey of Optimization Techniques Targeting Low Power VLSI Circuits,” DAC-95, p. 242.[3] S. Iman, M. Pedram. “Logic Extraction and Factorization for Low Power,” DAC-95, p. 248.[4] C. Y. Tsui, M. Pedram, A. M. Despain. “Technology Decomposition and Mapping Targeting Low Power Dissipation,” DAC-93, p. 68.[5] J. P. Fishburn. “A Depth-Decreasing Heuristic for Combinational Logic; or How to Convert a Ripple-Carry Adder into a Carry-Lookahead Adder or Anything In-Between,” DAC-90, p. 361.[6] V. Tivari, P. Ashar, S. Malik. “Technology Mapping for Low Power,” DAC-93, p.74.[7] B. S. Carlson, S. J. Lee. “Delay Optimization of Digital CMOS VLSI Circuits by Transistor Reordering,” IEEE Trans. on CAD, 1995, v. 14, n. 10, p. 1183.[8] A. L. Glebov, D. Blaauw, L. G. Jones. “Transistor Reordering for Low Power CMOS Gates Using SP-BDD Representation,” Intern. Symp. on Low Power Design, 1995, p. 161.[9] A. Glebov, S. Gavrilov, D. Blaauw, G. Vijayan, S. Pullela, S. Moore. “Library-Less Synthesis for Static CMOS Circuits,” accepted for ICCAD-97.[10] K. D. Boese, A. B. Kahng, C. W. A. Tsao. “Best-So-Far vs. Where-You-Are: New Perspectives on Simulated Annealing for CAD,” Euro-DAC’93, p. 78.<br>[11] T. Sakurai, A. R. Newton. “MOSFET Model Parameter Extraction Based on Fast Simulated Diffusion,” Memorandum UCB/ERL M90/20, 16 March 1990, Univ. of California, Berkeley.[12] J. P. Caisso, E. Cerny, N. S. Rumin. “A Recursive Technique for Computing Delays in Series-Parallel MOS Transistor Circuits,” IEEE Trans. on CAD, 1991, v. 10, n. 5, p. 589.[13] S. Gavrilov, A. Glebov, S. Rusakov, D. Blaauw, L. Jones, G. Vijayan. “Fast Power Loss Calculation for Digital Static CMOS Circuits,” European Design & Test Conf., 1997, p. 411.[14] C. H. Tan, J. Allen. “Minimization of Power in VLSI Circuits Using Transistor Sizing, Input Ordering, and Statistical Power Estimation,” Proc. of Int. Workshop on Low Power Design, 1994, p. 75.[15] M. Boehner. “LOGEX – An Automatic Logic Extractor from Transistor to Gate Level for CMOS Technology,” DAC-88, p. 517.Chapter 6 Bahar, R. I., Burns, M., Hachtel, G. D., et al. 1996. Symbolic computation of logic implications for technology-dependent low-power synthesis. In Proceedings of the International Symposium on Low Power Electronics and Design.Bobba, S. and Hajj, I. N. 1998. Estimation of maximum current envelope for power bus analysis and design. In Proceedings of the International Symposium on Physical Design.Brglez, F. and Fujiwara, H. 1985. A neutral netlist of 10 combinatorial benchmark circuits. In Proceedings of the IEEE ISCAS, IEEE Press, Piscataway, N. J., 695–698 BROWN, F. M. 1990. Boolean Reasoning. Kluwer Academic, Hingham, Mass.Bryant, R. E. 1986. Graph-based algorithms for Boolean function manipulation.IEEE Trans. Comput. 35. 677–691.Chen, P. and Keutzer, K. 1999. Towards tyrue crosstalk noise analysis. In ACM/IEEE Proceed- ings of the International Conference on Computer-Aided Design, 132–137.Garey, M. R. and Johnson, D. S. 1979. Computers and Intractability, A Guide to the Theory of NP-Completeness, Freeman, San Francisco.<br>Hachtel, G., Jacoby, R., Moceyunas, P., and Morrison, C. 1998. Performance enhancements in BOLD using implications. In ACM/IEEE Proceedings of the International Conference on Computer-Aided Design, 94–97.Kirkpatrick, D. A. and Sangiovanni-Vincentelli, A. L. 1996. Digital sensitivity: Predicting signal interaction using functional analysis. In ACM/IEEE Proceedings of the International Conference on Computer-Aided Design, 536–541.Kunz, W. and Menon, P. R. 1994. Multi-level logic optimization by implication analysis. In ACM/IEEE Proceedings of the International Conference on Computer-Aided Design, 6–13. Levy, R., Blaauw, D., Braca, G., Dasgupta, A., Grinshpon, A., Oh, C., Orchav, B., Sirichotiyakul, S., and Zolotov, V. 2000. Clarinet: A noise analysis tool for deep submicron design. In Proceedings of the IEEE/ACM Design Automation Conference (June), 233–238.Long, W., Wu, Y. L., and Bian, J. 2000. IBAW: An implication-tree based alternative-wiring logic transformation algorithm. In Proceedings of the Asian Pacific Design Automation Conference, 415–422.Loukakis, E. and Tsouros, C. 1983. An algorithm for the maximum internally stable set in a weighted graph. Int. J. Comput. Math. 13, 117–129.Meinel, C. and Teobald, T. 1998.Algorithms and Data Structures in VLSI Design, Springer- Verlag, New York.Rubio, A., Itazaki, N., Xu, X., and Kinoshita, K. 1997. An approach to the analysis and detection of crosstalk faults in digital VLSI circuits.IEEE Trans. Comput. Aid. Des. 13, 3.Shepard, K. L. 1998. Design methodologies for noise in digital integrated circuits. In Proceedings of the ACM/IEEE Design Automation Conference Shepard, K. L., Narayanan, V., Elemendorf, P. C., and Zheng, G. 1997. Global harmony: Coupled noise analysis for full-chip RC interconnect networks. In ACM/IEEE Proceedings of the Interna- tional Conference on Computer-Aided Design, 139–146.Tohr, T. S., Alt, H., Hetzel, A., and Koehl, K. 1998. Analysis, reduction and avoidance of crosstalk on VLSI chips. In Proceedings of the International Symposium on Physical Design, 211–218. Vittal, A. and Marek-Sadowska, M. 1997. Crosstalk reduction for VLSI. IEEE Trans. Comput. Aid. Des. 16, 3 (March), 290–298.Vittal, A., Chen, L. H., Marek-Sadowska, M., Wang, K.-P., and Yang, S. 1999. Crosstalk in VLSI Interconnections. IEEE Trans. Comput. Aid. Des. Integ. Circ. Syst. 18, 12 (Dec.), 1817–1824.Wroblewski, A., Schimpfle, C. V., and Nossek, J. A. 2000. Automated transistor sizing algorithm for minimizing spurious switching activities in CMOS circuits. In Proceedings of the ISCAS, 291–294.Xue, T., Kuh, E. S., and Wang, D. 1994. Post global routing crosstalk risk estimation and re- duction. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 616–619.<br>Zhou, H. and Wong, D. F. 1998. Global routing with crosstalk contraints. In Proceedings of the IEEE/ACM Design Automation Conference, 374–377.Zurada, J. M., Joo, Y. S., and Bell, S. V. 1989. Dynamic noise margins of MOS logic gates. In Proceedings of IEEE ISCAS, 1153–1156.Chapter 7[1] Amon T., Borriello G. An approach to symbolic timing verification. DAC, 1992. – P. 410-412.[2] Gladstone B. Accurate timing analysis holds the key to performance in today’s system designs. EDA. – 1993.[3] Overhauser D. Fast timing simulation of MOS VLSI circuits. Ph.D. thesis. – University of Illinois at Urbana-Champaign. – 1989.<br>[4] Dharchoudhury A., Kang S. M., Kim K. H., Lee S. H. Fast and accurate timing simulation with regionwise quadratic models of MOS I-V characteristics. ICCAD, 1994. – P. 190-194.[5] Hitchcock R. B. Timing verification and the Timing analysis Program. DAC, 1982. – P. 594-604.[6] Reddi R., Chen C. Hierarchical Timing Verification System. Computer Aided Design. – Vol. 18. – 9, November. – P. 467-477.[7] Yen S., Du D., Ghanta S. Efficient Algorithms for Extracting the K Most Critical Paths in Timing Analysis. DAC, 1989. – P. 649-654.[8] REFERENCE OMITTED FOR BLIND REVIEW.[9] REFERENCE OMITTED FOR BLIND REVIEW.[10] Robinson J.A. A Machine-Oriented Logic Based on the Resolution Principle. J. of the ACM. – 1965. – 12(1). – P. 23-41.Chapter 8[1] Lynn B., Prabhakaran M., Sahai A., “Positive results and techniques for obfuscation,” Lecture Notes in Computer Science, v. 3027, 2004, pp. 20-39.[2] Barak B. et al. “On the (Im)possibility of obfuscating programs,” Electronic Colloquium on Computational Complexity, 8(57), 2001, pp. 1-41.[3] Norman K. T., “Algorithms for white-box obfuscation using randomized subcircuit selection and replacement,” Thesis, Air Force Institute of Technology, Ohio, 2008, 99 pp.[4] REFERENCE OMITTED FOR BLIND REVIEW[5] Riedel M. D., Bruck J., “The synthesis of cyclic combinational circuits,” DAC-2003, pp.163-168.[6] Riedel M. D. “Cyclic combinational circuits,” PhD Dissertation, California Institute of Technology, 2004.Chapter 9[1] Glebov A. L. Mindeeva A. A., Petrosyan V. S., Gevorgyan A. M. Simulation of digital CMOS circuits using ternary decision diagrams. Modern problems of science and education. 2013. №4. (in Russian).[2] Bryant R. E. Graph-based algorithms for Boolean function manipulation IEEE Trans. on Computers, v. C-35, 1986, pp. 677-691.[3] Glebov A. L., Stempkovsky A. L., and others. Actual problems of modeling in circuit design automation systems. Moscow: Science, 2003 (in Russian).
Audience: Mathematicians and software developers, primarily working in microelectronics CAD