ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Efficient implementation of a BDD package
Full text PdfPdf (786 KB)
Source Annual ACM IEEE Design Automation Conference archive
Proceedings of the 27th ACM/IEEE conference on Design automation table of contents
Orlando, Florida, United States
Pages: 40 - 45  
Year of Publication: 1991
ISBN:0-89791-363-9
Authors
Karl S. Brace  Dept of ECE, Carnegie Mellon, Pittsburgh, PA
Richard L. Rudell  Synopsys, Inc., 1098 Alta Avenue, Mountain View, CA
Randal E. Bryant  School of Computer Science, Carnegie Mellon, Pittsburgh, PA
Sponsors
SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 41,   Downloads (12 Months): 198,   Citation Count: 175
Additional Information:

abstract   references   cited by   index terms   collaborative colleagues   peer to peer  

Tools and Actions: Review this Article  
Save this Article to a Binder    Display Formats: BibTex  EndNote ACM Ref   
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/123186.123222
What is a DOI?

ABSTRACT

Efficient manipulation of Boolean functions is an important component of many computer-aided design tasks. This paper describes a package for manipulating Boolean functions based on the reduced, ordered, binary decision diagram (ROBDD) representation. The package is based on an efficient implementation of the if-then-else (ITE) operator. A hash table is used to maintain a strong canonical form in the ROBDD, and memory use is improved by merging the hash table and the ROBDD into a hybrid data structure. A memory function for the recursive ITE algorithm is implemented using a hash-based cache to decrease memory use. Memory function efficiency is improved by using rules that detect when equivalent functions are computed. The usefulness of the package is enhanced by an automatic and low-cost scheme for recycling memory. Experimental results are given to demonstrate why various implementation trade-offs were made. These results indicate that the package described here is significantly faster and more memory-efficient than other ROBDD implementations described in the literature.


REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
S. Malik, A, Wang, R. Braytori, and A, Sangiovanni- Vincentelli, "Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment," in Proc. Int. Conf. CAD (ICCAD-88), Nov. 1988, pp. 6-9.
 
2
M. Fujita, H. Fujisawa, and N. Kawato, "Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams," in Proc. Int. Conf. CAD (ICCAD- 88), Nov. 1988, pp. 2-5.
 
3
O. Coudert, C. Berthet, andJ. Madre, "Verification of Sequential Machines using Boolean Function Vectors," in IMEC-IFIP ira. Workshop on Applied Formal Methods for Correct VLS! Design, 1989.
 
4
S. Muroga , Y. Kambayashi , H. C. Lai , J. N. Culliney, The Transduction Method-Design of Logic Networks Based on Permissible Functions, IEEE Transactions on Computers, v.38 n.10, p.1404-1424, October 1989  [doi>10.1109/12.35836 ]
 
5
M. A. Breuer and A. D. Friedman, Diagnosis and Reliable Design of Digitial Systems. Computer Science Press, 1976.
6
P. C. McGeer , R. K. Brayton, Efficient algorithms for computing the longest viable path in a combinational network, Proceedings of the 26th ACM/IEEE conference on Design automation, p.561-567, June 25-28, 1989, Las Vegas, Nevada, United States  [doi>10.1145/74382.74476]
 
7
K. Cho, Test Pattern Generation for Combinational and Sequential MOS Circuits by Symbolic Fault Siamlation. PhD thesis, Carnegie Mellon University, 1988.
 
8
M.R. Garey and D. S. Johnson, Computers and Inlractability. W. H. Freeman and Company, 1979.
 
9
Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
 
10
D. Bostick, G. D. Hachtcl, R. Jacoby, M. R, Lighmcr, E Moceyunas, C. R. Morrison, and D. Rav enscroft, "The Boulder Optimal Logic Design System," in Proc. Ira. Conf. CAD (ICCAD-87), Nov. 1987, pp. 62-65.
 
11
C. Y. Lee, "Representation of Switching Circuits by Binary- Decision Programs," Bell System Technical Journal, col. 38, pp. 985-999, July 1959.
 
12
Steven Fortune , John E. Hopcroft , Erik Meineche Schmidt, The Complexity of Equivalence and Containment for Free Single Variable Program Schemes, Proceedings of the Fifth Colloquium on Automata, Languages and Programming, p.227-240, July 17-21, 1978
 
13
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]
 
14
D.S. Reeves and M. J. irwin, "Fast Methods for Switch-Level Verification of MOS Circuits," ~ Trans. Elec. Comp., col. CAD-6, pp. 766-779, Sep. 1987.
 
15
Kevin Karplus, REPRESENTING BOOLEAN FUNCTIONS WITH IF-THEN-ELSE DAGs, University of California at Santa Cruz, Santa Cruz, CA, 1988
 
16
S. B. Akers, "Functional Testing with Binary Decision Diagrams," in Eighth Annual Conference on Fault-Tolerant Computing, 1978, pp. 75-82.
 
17
Jean-Christophe Madre , Jean-Paul Billon, Proving circuit correctness using formal comparison between expected and extracted behaviour, Proceedings of the 25th ACM/IEEE conference on Design automation, p.205-210, June 12-15, 1988, Atlantic City, New Jersey, United States
 
18
R. Lisanke, "Logic Synthesis Benchmarks," in Proc. Int. Workshop on Logic Synthesis (}WLS-89), May 1989.
 
19
Leonard Berman , Louise Trevillyan, A global approach to circuit size reduction, Proceedings of the fifth MIT conference on Advanced research in VLSI, p.203-214, January 1988, Cambridge, Massachusetts, United States

CITED BY  175
 
Yirng-An Chen , Randal E. Bryant, PHDD: an efficient graph representation for floating point circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.2-7, November 09-13, 1997, San Jose, California, United States
Kwang-Ting Cheng , A. S. Krishnakumar, Automatic generation of functional vectors using the extended finite state machine model, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.1 n.1, p.57-79, Jan. 1996
 
Pranav Ashar , Matthew Cheong, Efficient breadth-first manipulation of binary decision diagrams, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.622-627, November 06-10, 1994, San Jose, California, United States
 
Kiyoharu Hamaguchi , Akihito Morita , Shuzo Yajima, Efficient construction of binary moment diagrams for verifying arithmetic circuits, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.78-82, November 05-09, 1995, San Jose, California, United States
Timothy Kam , Tiziano Villa , Robert Brayton , Alberto Sangiovanni-Vincentelli, A fully implicit algorithm for exact state minimization, Proceedings of the 31st annual conference on Design automation, p.684-690, June 06-10, 1994, San Diego, California, United States
 
Ruchir Puri , Jun Gu, A divide-and-conquer approach for asynchronous interface synthesis, Proceedings of the 7th international symposium on High-level synthesis, p.118-125, May 18-20, 1994, Niagra-on-the-Lake, Ontario, Canada
 
Wolfgang Günther , Rolf Drechsler, Efficient manipulation algorithms for linearly transformed BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.50-54, November 07-11, 1999, San Jose, California, United States
 
Dirk Möller , Janett Mohnke , Michael Weber, Detection of symmetry of Boolean functions represented by ROBDDs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.680-684, November 07-11, 1993, Santa Clara, California, United States
 
Yuji Kukimoto , Masahiro Fujita, Rectification method for lookup-table type FPGA's, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.54-61, November 1992, Santa Clara, California, United States
Thomas R. Shiple , Ramin Hojati , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Heuristic minimization of BDDs using don't cares, Proceedings of the 31st annual conference on Design automation, p.225-231, June 06-10, 1994, San Diego, California, United States
 
Y.-T. Lai , S. Sastry, Edge-valued binary decision diagrams for multi-level hierarchical verification, Proceedings of the 29th ACM/IEEE conference on Design automation, p.608-613, June 08-12, 1992, Anaheim, California, United States
 
Ronald Herrmann , Hergen Pargmann, Computing binary decision diagrams for VHDL data types, Proceedings of the conference on European design automation, p.578-583, September 19-23, 1994, Grenoble, France
 
E. Pastor , J. Cortadella, Efficient encoding schemes for symbolic analysis of petri nets, Proceedings of the conference on Design, automation and test in Europe, p.790-795, February 23-26, 1998, Le Palais des Congrés de Paris, France
 
Jerry R. Burch , David E. Long, Efficient Boolean function matching, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.408-411, November 1992, Santa Clara, California, United States
 
Jérôme Amilhastre , Hélène Fargier , Pierre Marquis, Consistency restoriation and explanations in dynamic CSPs----application to configuration, Artificial Intelligence, v.135 n.1-2, p.199-234, 02/01/2002
 
Seh-Woong Jeong , Fabio Somenzi, A new algorithm for the binate covering problem and its application to the minimization of Boolean relations, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.417-420, November 1992, Santa Clara, California, United States
Andreas Hett , Christoph Scholl , Bernd Becker, Distance driven finite state machine traversal, Proceedings of the 37th conference on Design automation, p.39-42, June 05-09, 2000, Los Angeles, California, United States
 
O. Coudert , J. C. Madre, Implicit and incremental computation of primes and essential primes of Boolean functions, Proceedings of the 29th ACM/IEEE conference on Design automation, p.36-39, June 08-12, 1992, Anaheim, California, United States
 
Janett Mohnke , Paul Molitor , Sharad Malik, Limits of Using Signatures for Permutation Independent Boolean Comparison, Formal Methods in System Design, v.21 n.2, p.167-191, September 2002
 
Giampiero Cabodi , Paolo Camurati , Fulvio Corno , Paolo Prinetto , Matteo Sonza Reorda, The General Product Machine: a New Model for Symbolic FSM Traversal, Formal Methods in System Design, v.12 n.3, p.267-289, April 1, 1998
Daniel Große , Rüdiger Ebendt , Rolf Drechsler, Improvements for constraint solving in the systemc verification library, Proceedings of the 17th great lakes symposium on Great lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy
 
I. Radivojevic , F. Brewer, On applicability of symbolic techniques to larger scheduling problems, Proceedings of the 1995 European conference on Design and Test, p.48, March 06-09, 1995
Yusuke Matsunaga , Patrick C. McGeer , Robert K. Brayton, On computing the transitive closure of a state transition relation, Proceedings of the 30th international conference on Design automation, p.260-265, June 14-18, 1993, Dallas, Texas, United States
Yun-Cheng Ju , Resve A. Saleh, Incremental techniques for the identification of statically sensitizable critical paths, Proceedings of the 28th conference on ACM/IEEE design automation, p.541-546, June 17-22, 1991, San Francisco, California, United States
 
Takashi Horiyama , Toshihide Ibaraki, Ordered binary decision diagrams as knowledge-bases, Artificial Intelligence, v.136 n.2, p.189-213, April 2002
 
Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
Jagesh V. Sanghavi , Rajeev K. Ranjan , Robert K. Brayton , Alberto Sangiovanni-Vincentelli, High performance BDD package by exploiting memory hierarchy, Proceedings of the 33rd annual conference on Design automation, p.635-640, June 03-07, 1996, Las Vegas, Nevada, United States
Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States
Xiahua Kong , Radu Negulescu, Formal verification of pulse-mode asynchronous circuits, Proceedings of the 2001 conference on Asia South Pacific design automation, p.347-352, January 2001, Yokohama, Japan
Ted Stanion , Carl Sechen, A method for finding good Ashenhurst decompositions and its application to FPGA synthesis, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.60-64, June 12-16, 1995, San Francisco, California, United States
 
Gary D. Hachtel , Fabio Somenzi, A symbolic algorithm for maximum flow in 0-1 networks, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.403-406, November 07-11, 1993, Santa Clara, California, United States
 
Debashis Bhattacharya , Prathima Agrawal, Boolean algebraic test generation using a distributed system, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.440-443, November 07-11, 1993, Santa Clara, California, United States
 
G. Cabodi , P. Camurati , F. Corno , S. Gai , P. Prinetto , M. Sonza Reorda, A new model for improving symbolic product machine traversal, Proceedings of the 29th ACM/IEEE conference on Design automation, p.614-619, June 08-12, 1992, Anaheim, California, United States
Hui Xu , Rob A. Rutenbar , Karem Sakallah, sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing, Proceedings of the 2002 international symposium on Physical design, April 07-10, 2002, San Diego, CA, USA
Christoph Meinel , Fabio Somenzi , Thorsten Theobald, Linear sifting of decision diagrams, Proceedings of the 34th annual conference on Design automation, p.202-207, June 09-13, 1997, Anaheim, California, United States
Larry G. Jones, Accelerating switch-level simulation by function caching, Proceedings of the 28th conference on ACM/IEEE design automation, p.211-214, June 17-22, 1991, San Francisco, California, United States
 
Shipra Panda , Fabio Somenzi , Bernard F. Plessier, Symmetry detection and dynamic variable ordering of decision diagrams, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.628-631, November 06-10, 1994, San Jose, California, United States
Andrew Seawright , Forrest Brewer, High-level symbolic construction technique for high performance sequential synthesis, Proceedings of the 30th international conference on Design automation, p.424-428, June 14-18, 1993, Dallas, Texas, United States
David E. Long, The design of a cache-friendly BDD library, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.639-645, November 08-12, 1998, San Jose, California, United States
Jeffery P. Hansen , Masatoshi Sekine, Synthesis by spectral translation using Boolean decision diagrams, Proceedings of the 33rd annual conference on Design automation, p.248-253, June 03-07, 1996, Las Vegas, Nevada, United States
Luca Benini , Giovanni De Micheli, A survey of Boolean matching techniques for library binding, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.2 n.3, p.193-226, July 1997
 
G. D. Hachtel , F. Somenzi, A Symbolic Algorithms for Maximum Flow in 0-1 Networks, Formal Methods in System Design, v.10 n.2-3, p.207-219, April -May 1997
Alan J. Hu , Gary York , David L. Dill, New techniques for efficient verification with implicitly conjoined BDDs, Proceedings of the 31st annual conference on Design automation, p.276-282, June 06-10, 1994, San Diego, California, United States
 
A. Hett , B. Becker , R. Drechsler, MORE: an alternative implementation of BDD packages by multi-operand synthesis, Proceedings of the conference on European design automation, p.164-169, September 1996, Geneva, Switzerland
 
Rüdiger Ebendt , Wolfgang Günther , Rolf Drechsler, Combining ordered best-first search with branch and bound for exact BDD minimization, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.875-878, January 27-30, 2004, Yokohama, Japan
 
Franco Fummi , Donatella Sciuto, A Hierarchical Test Generation Approach for Large Controllers, IEEE Transactions on Computers, v.49 n.4, p.289-302, April 2000
 
Arlindo L. Oliveira , Luca P. Carloni , Tiziano Villa , Alberto L. Sangiovanni-Vincentelli, Exact Minimization of Binary Decision Diagrams Using Implicit Techniques, IEEE Transactions on Computers, v.47 n.11, p.1282-1296, November 1998
M. M. Vaseekar Kumar , S. Tragoudas, Low power test generation for path delay faults using stability functions, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
 
Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, v.10 n.1, p.47-71, February 1997
 
Ingo Wegener, The Size of Reduced OBDD's and Optimal Read-Once Branching Programs for Almost all Boolean Functions, IEEE Transactions on Computers, v.43 n.11, p.1262-1269, November 1994
 
Brian Herlihy , Peter Schachte , Harald Søndergaard, Boolean equation solving as graph traversal, Proceedings of the 12th Computing: The Australasian Theroy Symposium, p.123-132, January 16-19, 2006, Hobart, Australia
Cheng-Hsing Yang , Chia-Chun Tsai , Jan-Ming Ho , Sao-Jie Chen, Hmap: a fast mapper for EPGAs using extended GBDD hash tables, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.2 n.2, p.135-150, April 1997
 
Hong-Yu Xie , Sarma B. K. Vrudhula, A Technique for Estimating Signal Activity in Logic Circuits, Integrated Computer-Aided Engineering, v.5 n.2, p.141-152, April 1998
S. Tragoudas , M. Michael, ATPG tools for delay faults at the functional level, Proceedings of the conference on Design, automation and test in Europe, p.124-es, January 1999, Munich, Germany
 
F. Corno , M. Cusinato , M. Ferrero , P. Prinetto, Proving testing preorders for process algebra descriptions, Proceedings of the 1995 European conference on Design and Test, p.333, March 06-09, 1995
 
S. Minato , S. Ishihara, Streaming BDD manipulation for large-scale combinatorial problems, Proceedings of the conference on Design, automation and test in Europe, p.702-707, March 2001, Munich, Germany
 
M. R. Mercer , R. Kapur , D. E. Ross, Functional approaches to generating orderings for efficient symbolic representations, Proceedings of the 29th ACM/IEEE conference on Design automation, p.624-627, June 08-12, 1992, Anaheim, California, United States
M. Michael , S. Tragoudas, ATPG tools for delay faults at the functional level, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.7 n.1, p.33-57, January 2002
Per Lindgren , Mikael Kerttu , Mitch Thornton , Rolf Drechsler, Low power optimization technique for BDD mapped circuits, Proceedings of the 2001 conference on Asia South Pacific design automation, p.615-621, January 2001, Yokohama, Japan
 
D. Bhattacharya , P. Agrawal , V. D. Agrawal, Delay fault test generation for scan/hold circuits using Boolean expressions, Proceedings of the 29th ACM/IEEE conference on Design automation, p.159-164, June 08-12, 1992, Anaheim, California, United States
Tony Stornetta , Forrest Brewer, Implementation of an efficient parallel BDD package, Proceedings of the 33rd annual conference on Design automation, p.641-644, June 03-07, 1996, Las Vegas, Nevada, United States
Bwolen Yang , David R. O'Hallaron, Parallel breadth-first BDD construction, ACM SIGPLAN Notices, v.32 n.7, p.145-156, July 1997
 
Aarti Gupta , Allan L. Fisher, Representation and symbolic manipulation of linearly inductive Boolean functions, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.192-199, November 07-11, 1993, Santa Clara, California, United States
 
Shipra Panda , Fabio Somenzi, Who are the variables in your neighborhood, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.74-77, November 05-09, 1995, San Jose, California, United States
 
Y. Liu , K. Wang , T. Hwang , C. Liu, Binary decision diagram with minimum expected path length, Proceedings of the conference on Design, automation and test in Europe, p.708-712, March 2001, Munich, Germany
Subdodh M. Reddy , Wolfgang Kunz , Dhiraj K. Pradhan, Novel verification framework combining structural and OBDD methods in a synthesis environment, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.414-419, June 12-16, 1995, San Francisco, California, United States
R. Drechsler , A. Sarabi , M. Theobald , B. Becker , M. A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Proceedings of the 31st annual conference on Design automation, p.415-419, June 06-10, 1994, San Diego, California, United States
 
Debashis Bhattacharya , Prathima Agrawal, Boolean algebraic test generation using a distributed system, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.440-443, November 07-11, 1993, Santa Clara, California, United States
Jochen Bern , Christoph Meinel , Anna Slobodová, Efficient OBDD-based boolean manipulation in CAD beyond current limits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.408-413, June 12-16, 1995, San Francisco, California, United States
Jörg Köller , Markus Mohnen, Efficient abstract interpretation using component-wise homomorphisms, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.226-234, September 20-23, 2000, Montreal, Quebec, Canada
 
Hiroshige Fujii , Goichi Ootomo , Chikahiro Hori, Interleaving based variable ordering methods for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.38-41, November 07-11, 1993, Santa Clara, California, United States
 
Shin-ichi Minato, Streaming BDD Manipulation, IEEE Transactions on Computers, v.51 n.5, p.474-485, May 2002
Sunil P. Khatri , Amit Narayan , Sriram C. Krisnan , Kenneth L. McMillan , Robert K. Brayton , A. Sangiovanni-Vincentelli, Engineering change in a non-deterministic FSM setting, Proceedings of the 33rd annual conference on Design automation, p.451-456, June 03-07, 1996, Las Vegas, Nevada, United States
 
Yung-Te Lai , Massoud Pedram , Sarma B. K. Vrudhula, Formal Verification Using Edge-Valued Binary Decision Diagrams, IEEE Transactions on Computers, v.45 n.2, p.247-255, February 1996
 
Takashi Horiyama , Toshihide Ibaraki, Translation among CNFs, characteristic models and ordered binary decision diagrams, Information Processing Letters, v.85 n.4, p.191-198, 28 February 2003
Kenneth M. Butler , Don E. Ross , Rohit Kapur , M. Ray Mercer, Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagrams, Proceedings of the 28th conference on ACM/IEEE design automation, p.417-420, June 17-22, 1991, San Francisco, California, United States
 
Yasushi Koseko , Takuji Ogihara , Shinichi Murai, Tri-state bus conflict checking method for ATPG using BDD, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.512-515, November 07-11, 1993, Santa Clara, California, United States
J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States
 
R. I. Bahar , E. A. Frohm , C. M. Gaona , G. D. Hachtel , E. Macii , A. Pardo , F. Somenzi, Algebric Decision Diagrams and Their Applications, Formal Methods in System Design, v.10 n.2-3, p.171-206, April -May 1997
 
Xinyu Zang , Dazhi Wang , Hairong Sun , Kishor S. Trivedi, A BDD-Based Algorithm for Analysis of Multistate Systems with Multistate Components, IEEE Transactions on Computers, v.52 n.12, p.1608-1618, December 2003
 
Yanbin Jiang , Sachin S. Sapatnekar , Cyrus Bamji, Technology mapping for high-performance static CMOS and pass transistor logic designs, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.9 n.5, p.577-589, October 2001
 
Shin-Ichi Minato , F. Somenzi, Arithmetic Boolean Expression Manipulator Using BDDs, Formal Methods in System Design, v.10 n.2-3, p.221-242, April -May 1997
 
F. Bréant , J.-M. Couvreur , F. Gilliers , F. Kordon , I. Mounier , E. Paviot-Adet , D. Poitrenaud , D. Regep , G. Sutre, Modeling and verifying behavioral aspects, Formal methods for embedded distributed systems: how to master the complexity, Kluwer Academic Publishers, Norwell, MA, 2004
Christoph Csallner , Nikolai Tillmann , Yannis Smaragdakis, DySy: dynamic symbolic execution for invariant inference, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
 
Olaf Schröer , Ingo Wegener, The Theory of Zero-Suppressed BDDs and the Number of Knight‘s Tours, Formal Methods in System Design, v.13 n.3, p.235-253, Nov. 1998
 
C. Cayrol , M.-C. Lagasquie-Schiex , T. Schiex, Nonmonotonic reasoning: from complexity to algorithms, Annals of Mathematics and Artificial Intelligence, v.22 n.3-4, p.207-236, 1998
 
A. Hett , R. Drechsler , B. Becker, Fast and Efficient Construction of BDDs by Reordering Based Synthesis, Proceedings of the 1997 European conference on Design and Test, p.168, March 17-20, 1997
 
J.-K. Rho , F. Somenzi, Inductive verification of iterative systems, Proceedings of the 29th ACM/IEEE conference on Design automation, p.628-633, June 08-12, 1992, Anaheim, California, United States
Hiroyuki Ochi , Nagisa Ishiura , Shuzo Yajima, Breadth-first manipulation of SBDD of Boolean functions for vector processing, Proceedings of the 28th conference on ACM/IEEE design automation, p.413-416, June 17-22, 1991, San Francisco, California, United States
Jerry R. Burch, Using BDDs to verify multipliers, Proceedings of the 28th conference on ACM/IEEE design automation, p.408-412, June 17-22, 1991, San Francisco, California, United States
 
S. Höreth, Compilation of optimized OBDD-algorithms, Proceedings of the conference on European design automation, p.152-157, September 1996, Geneva, Switzerland
 
Markus Mohnen, An open framework for data-flow analysis in Java: extended abstract, Proceedings of the inaugural conference on the Principles and Practice of programming, 2002 and Proceedings of the second workshop on Intermediate representation engineering for virtual machines, 2002, June 13-14, 2002, Dublin, Ireland
 
Hiroyuki Ochi , Koichi Yasuoka , Shuzo Yajima, Breadth-first manipulation of very large binary-decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.48-55, November 07-11, 1993, Santa Clara, California, United States
R. Glenn Wood , Rob A. Rutenbar, FPGA routing and routability estimation via Boolean satisfiability, Proceedings of the 1997 ACM fifth international symposium on Field-programmable gate arrays, p.119-125, February 09-11, 1997, Monterey, California, United States
 
Paul Tafertshofer , Massoud Pedram, Factored Edge-Valued Binary Decision Diagrams, Formal Methods in System Design, v.10 n.2-3, p.243-270, April -May 1997
Congguang Yang , Maciej Ciesielski , Vigyan Singhal, BDS: a BDD-based logic optimization system, Proceedings of the 37th conference on Design automation, p.92-97, June 05-09, 2000, Los Angeles, California, United States
Christoph Scholl , Bernd Becker, On the generation of multiplexer circuits for pass transistor logic, Proceedings of the conference on Design, automation and test in Europe, p.372-379, March 27-30, 2000, Paris, France
 
Rüdiger Ebendt , Wolfgang Günther , Rolf Drechsler, Minimization of the expected path length in BDDs based on local changes, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.865-870, January 27-30, 2004, Yokohama, Japan
 
Tsung-Hsi Chiang , Lan-Rong Dung, Verification method of dataflow algorithms in high-level synthesis, Journal of Systems and Software, v.80 n.8, p.1256-1270, August, 2007
 
F. Corno , P. Prinetto , M. Sonza Reorda, Using symbolic techniques to find the maximum clique in very large sparse graphs, Proceedings of the 1995 European conference on Design and Test, p.320, March 06-09, 1995
 
B. Becker , R. Drechsler, How many decomposition types do we need? [decision diagrams], Proceedings of the 1995 European conference on Design and Test, p.438, March 06-09, 1995
 
S. Chiusano , F. Corno , P. Prinetto , M. Sonza Reorda, Hybrid symbolic-explicit techniques for the graph coloring problem, Proceedings of the 1997 European conference on Design and Test, p.422, March 17-20, 1997
 
Amit Narayan , Jawahar Jain , M. Fujita , A. Sangiovanni-Vincentelli, Partitioned ROBDDs—a compact, canonical and efficiently manipulable representation for Boolean functions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.547-554, November 10-14, 1996, San Jose, California, United States
Christoph Scholl , Bernd Becker , Andreas Brogle, The multiple variable order problem for binary decision diagrams: theory and practical application, Proceedings of the 2001 conference on Asia South Pacific design automation, p.85-90, January 2001, Yokohama, Japan
 
Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.236-243, November 05-09, 1995, San Jose, California, United States
 
G. Cabodi , P. Camurati , F. Corno , P. Prinetto , M. Sonza Reorda, Cross-fertilizing FSM verification techniques and sequential diagnosis, Proceedings of the conference on European design automation, p.306-311, November 1992, Congress Centrum Hamburg, Hamburg, Germany
 
Andrew S. Miner, Implicit GSPN reachability set generation using decision diagrams, Performance Evaluation, v.56 n.1-4, p.145-165, March 2004
M.M Vaseekar Kumar , S. Padmanaban , S. Tragoudas, Low power ATPG for path delay faults, Proceedings of the 14th ACM Great Lakes symposium on VLSI, April 26-28, 2004, Boston, MA, USA
 
Detlef Sieling, The nonapproximability of OBDD minimization, Information and Computation, v.172 n.2, p.103-138, January 29, 2002
Kaviraj Chopra , Sarma B. K. Vrudhula, Implicit pseudo boolean enumeration algorithms for input vector control, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
 
Andrew Seawright , Forrest Brewer, Clairvoyant: a synthesis system for production-based specification, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
 
David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
Rolf Drechsler , Nicole Drechsler , Wolfgang Günther, Fast exact minimization of BDDs, Proceedings of the 35th annual conference on Design automation, p.200-205, June 15-19, 1998, San Francisco, California, United States
 
Enrico Macii , Massimo Poncino, Predicting the functional complexity of combinational circuits by symbolic spectral analysis of Boolean functions, Proceedings of the conference on European design automation, p.294-299, September 18-22, 1995, Brighton, England
 
W. Baker , A. Newton, The maximal VHDL subset with a cycle-level abstraction, Proceedings of the conference on European design automation, p.470-475, September 1996, Geneva, Switzerland
Felice Balarin, Automatic abstraciton for worst-case analysis of discrete systems, Proceedings of the conference on Design, automation and test in Europe, p.494-501, March 27-30, 2000, Paris, France
Peter F. A. Middelhoek , Sreeranga P. Rajan, From VHDL to efficient and first-time-right designs: a formal approach, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.1 n.2, p.205-250, April 1996
 
Don E. Ross , Kenneth M. Butler , Rohit Kapur , M. Ray Mercer, Fast functional evaluation of candidate OBDD variable orderings, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
 
Marc-Michel Corsini , Antoine Rauzy, Toupie: The µ-calculus over Finite Domains as a Constraint Language, Journal of Automated Reasoning, v.19 n.2, p.143-171, October 1997
Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Bernard Plessier , Fabio Somenzi, Algorithms for approximate FSM traversal, Proceedings of the 30th international conference on Design automation, p.25-30, June 14-18, 1993, Dallas, Texas, United States
 
Prathima Agrawal , Debashis Bhattacharya , Vishwani D. Agrawal, Test Generation for Path Delay Faults Using Binary Decision Diagrams, IEEE Transactions on Computers, v.44 n.3, p.434-447, March 1995
 
A. Cimatti , M. Roveri , P. Bertoli, Conformant planning via symbolic model checking and heuristic search, Artificial Intelligence, v.159 n.1-2, p.127-206, November 2004
 
Bernd Becker , Rolf Drechsler , Michael Theobald, On the Expressive Power of OKFDDs, Formal Methods in System Design, v.11 n.1, p.5-21, July 1997
 
C. Pixley , S.-W. Jeong , G. D. Hachtel, Exact calculation of synchronization sequences based on binary decision diagrams, Proceedings of the 29th ACM/IEEE conference on Design automation, p.620-623, June 08-12, 1992, Anaheim, California, United States
Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992
 
Christophe Lohou , Gilles Bertrand, A 3D 12-subiteration thinning algorithm based on P-simple points, Discrete Applied Mathematics, v.139 n.1-3, p.171-195, 30 April 2004
Rüdiger Ebendt , Rolf Drechsler, Lower bounds for dynamic BDD reordering, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
 
Elena Dubrova , Luca Macchiarulo, A Comment on 'Graph-Based Algorithm for Boolean Function Manipulation', IEEE Transactions on Computers, v.49 n.11, p.1290-1292, November 2000
Madhav P. Desai, A systematic technique for verifying critical path delays in a 300MHz Alpha CPU design using circuit simulation, Proceedings of the 33rd annual conference on Design automation, p.125-130, June 03-07, 1996, Las Vegas, Nevada, United States
 
A. Crews , F. Brewer, Controller optimization for protocol intensive applications, Proceedings of the conference on European design automation, p.140-145, September 1996, Geneva, Switzerland
 
Julian F. Miller , Dominic Job , Vesselin K. Vassilev, Principles in the Evolutionary Design of Digital Circuits—Part I, Genetic Programming and Evolvable Machines, v.1 n.1-2, p.7-35, April 2000
Bhanu Kapoor, Improving the accuracy of circuit activity measurement, Proceedings of the 31st annual conference on Design automation, p.734-739, June 06-10, 1994, San Diego, California, United States
 
K. Kubiak , S. Parkes , W. K. Fuchs , R. Saleh, Exact evaluation of diagnostic test resolution, Proceedings of the 29th ACM/IEEE conference on Design automation, p.347-352, June 08-12, 1992, Anaheim, California, United States
Farid N. Najm, Transition density, a stochastic measure of activity in digital circuits, Proceedings of the 28th conference on ACM/IEEE design automation, p.644-649, June 17-22, 1991, San Francisco, California, United States
 
Scott Woods , Giorgio Casinovi, Efficient solution of systems of Boolean equations, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.542-546, November 10-14, 1996, San Jose, California, United States
Jason Cong , Yuzheng Ding, Combinational logic synthesis for LUT based field programmable gate arrays, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.1 n.2, p.145-204, April 1996
 
Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
 
Z. Zeng , P. Kalla , M. Ciesielski, LPSAT: a unified approach to RTL satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.398-402, March 2001, Munich, Germany
 
A. Bogliolo , L. Benini , G. De Micheli, Characterization-free behavioral power modeling, Proceedings of the conference on Design, automation and test in Europe, p.767-773, February 23-26, 1998, Le Palais des Congrés de Paris, France
 
R. Leupers , P. Marwedel, A BDD-based frontend for retargetable compilers, Proceedings of the 1995 European conference on Design and Test, p.239, March 06-09, 1995
 
R. Mukherjee , J. Jain , M. Fujita, VERIFUL: VERIfication using FUnctional Learning, Proceedings of the 1995 European conference on Design and Test, p.444, March 06-09, 1995
 
A. Bogliolo , M. Damiani, Synthesis of multilevel fault-tolerant combinational circuits, Proceedings of the 1995 European conference on Design and Test, p.80, March 06-09, 1995
 
Christophe Lohou , Gilles Bertrand, A 3D 6-subiteration curve thinning algorithm based on P-simple points, Discrete Applied Mathematics, v.151 n.1-3, p.198-228, 1 October 2005
 
J. Gergov , C. Meinel, Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's, IEEE Transactions on Computers, v.43 n.10, p.1197-1209, October 1994
 
S. Chakravarty, A Characterization of Binary Decision Diagrams, IEEE Transactions on Computers, v.42 n.2, p.129-137, February 1993
 
Rolf Drechsler, Verifying integrity of decision diagrams, Integration, the VLSI Journal, v.32 n.1-3, p.61-75, November 2002
 
Natarajan Shankar, Automated verification using deduction, exploration, and abstraction, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
Priyank Kalla , Zhihong Zeng , Maciej J. Ciesielski , Chilai Huang, A BDD-based satisfiability infrastructure using the unate recursive paradigm, Proceedings of the conference on Design, automation and test in Europe, p.232-236, March 27-30, 2000, Paris, France
Silvia Ercolani , Giovanni De Micheli, Technology mapping for electrically programmable gate arrays, Proceedings of the 28th conference on ACM/IEEE design automation, p.234-239, June 17-22, 1991, San Francisco, California, United States
 
Chih-Chang Lin , Mike Tien-Chien Lee , Malgorzata Marek-Sadowska , Kuang-Chien Chen, Cost-free scan: a low-overhead scan path design methodology, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.528-533, November 05-09, 1995, San Jose, California, United States
 
John Lafferty , Alexander Vardy, Ordered Binary Decision Diagrams and Minimal Trellises, IEEE Transactions on Computers, v.48 n.9, p.971-986, September 1999
 
Scott Woods , Giorgio Casinovi, Gate-level simulation of digital circuits using multi-valued Boolean algebras, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.413-419, November 05-09, 1995, San Jose, California, United States
 
Valeria Bertacco , Maurizio Damiani, The disjunctive decomposition of logic functions, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.78-82, November 09-13, 1997, San Jose, California, United States
Pi-Yu Chung , Yi-Min Wang , Ibrahim N. Hajj, Diagnosis and correction of logic design errors in digital circuits, Proceedings of the 30th international conference on Design automation, p.503-508, June 14-18, 1993, Dallas, Texas, United States
 
Stephen A. Edwards , Edward A. Lee, The semantics and execution of a synchronous block-diagram language, Science of Computer Programming, v.48 n.1, p.21-42, July 2003
 
A. Cimatti , M. Pistore , M. Roveri , P. Traverso, Weak, strong, and strong cyclic planning via symbolic model checking, Artificial Intelligence, v.147 n.1-2, p.35-84, July 2003
Chih-Chang Lin , Kuang-Chien Chen , Shih-Chieh Chang , Malgorzata Marek-Sadowska , Kwang-Ting Cheng, Logic synthesis for engineering change, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.647-652, June 12-16, 1995, San Francisco, California, United States
 
Afshin Abdollahi, Probabilistic decision diagrams for exact probabilistic analysis, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Lluís Ribas-Xirgo , Jordi Carrabina-Bordoll, Analysis of switch-level faults by symbolic simulation, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.352-357, June 12-16, 1995, San Francisco, California, United States
John W. Sias , Wen-Mei W. Hwu , David I. August, Accurate and efficient predicate analysis with binary decision diagrams, Proceedings of the 33rd annual ACM/IEEE international symposium on Microarchitecture, p.112-123, December 2000, Monterey, California, United States
Kwang Ting Cheng , A. S. Krishnakumar, Automatic functional test generation using the extended finite state machine model, Proceedings of the 30th international conference on Design automation, p.86-91, June 14-18, 1993, Dallas, Texas, United States
 
Wolfgang Günther , Rolf Drechsler, Minimization of free BDDs, Integration, the VLSI Journal, v.32 n.1-3, p.41-59, November 2002
Pejman Lotfi-Kamran , Mohammad Hosseinabady , Hamid Shojaei , Mehran Massoumi , Zainalabedin Navabi, TED+: a data structure for microprocessor verification, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
 
Yuke Wang , Carl McCrosky, Solving Boolean Equations Using ROSOP Forms, IEEE Transactions on Computers, v.47 n.2, p.171-177, February 1998
 
Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Automatic Vector Generation Using Constraints and Biasing, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.107-120, Feb/April 2000
 
Brock J. LaMeres , Sunil P. Khatri, Bus stuttering: an encoding technique to reduce inductive noise in off-chip data transmission, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
 
Wolfgang Günther , Rolf Drechsler, Efficient Minimization and Manipulation of Linearly Transformed Binary Decision Diagrams, IEEE Transactions on Computers, v.52 n.9, p.1196-1209, September 2003
 
Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Strong planning under partial observability, Artificial Intelligence, v.170 n.4, p.337-384, April 2006
 
Afshin Abdollahi , Massoud Pedram, Analysis and synthesis of quantum circuits by using quantum decision diagrams, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
 
Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
 
Rolf Drechsler , Wolfgang Günther , Stefan Höreth, Minimization of word-level decision diagrams, Integration, the VLSI Journal, v.33 n.1, p.39-70, December 2002
 
Farid N. Najm, Power estimation techniques for integrated circuits, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.492-499, November 05-09, 1995, San Jose, California, United States
 
Franco Fummi , Donatella Sciuto , Micaela Serra, Synthesis for Testability of Highly Complex Controllers by Functional Redundancy Removal, IEEE Transactions on Computers, v.48 n.12, p.1305-1323, December 1999
 
Dirk Beyer , Andreas Noack , Claus Lewerentz, Efficient Relational Calculation for Software Analysis, IEEE Transactions on Software Engineering, v.31 n.2, p.137-149, February 2005

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)