Dynamic variable ordering for ordered binary decision diagrams

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Dynamic variable ordering for ordered binary decision diagrams

Full text

Pdf (744 KB)

Source

International Conference on Computer Aided Design archive
Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design table of contents

Santa Clara, California, United States

Pages: 42 - 47

Year of Publication: 1993

ISBN:0-8186-4490-7

Author

Richard Rudell

Synopsys, Inc., 700 E. Middlefield Road, Mountain View, California

Sponsors

IEEE-CS : Computer Society
SIGDA: ACM Special Interest Group on Design Automation

Publisher

IEEE Computer Society Press Los Alamitos, CA, USA

Bibliometrics

Downloads (6 Weeks): 18, Downloads (12 Months): 114, Citation Count: 151

Additional Information:

references cited by collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

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	K. Brace. Personal Communication, June 1989.
	2	Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
	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	J. Butch. Personal Communication, June 1992.
	5	M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams. In Proceedings International Conference on Computer-Aided Design, pages 2-5, November 1988.
	6	Masahiro Fujita , Yusuke Matsunaga , Taeko Kakuda, On variable ordering of binary decision diagrams for the application of multi-level logic synthesis, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
	7	N. Ishiura, H. Sawada, and S. Yajima. Minimization of Binary Decision Diagrams Based on Exchanges of Variables. In Proceedings International Conference on Computer.Aided Design, pages 472-475, November 1991.
	8	Kevin Karplus, REPRESENTING BOOLEAN FUNCTIONS WITH IF-THEN-ELSE DAGs, University of California at Santa Cruz, Santa Cruz, CA, 1988
	9	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
	10	S. Malik, A. Wang, R. Brayton, and A. Sangiovanni- Vincentelli. Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment. In Proceedings International Conference on Computer- Aided Design, pages 6-9, November 1988.
	11	Shin-ichi Minato , Nagisa Ishiura , Shuzo Yajima, Shared binary decision diagram with attributed edges for efficient Boolean function manipulation, Proceedings of the 27th ACM/IEEE conference on Design automation, p.52-57, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123225]
	12	R.. Rudell. Dynamic Variable Ordering for Ordered Binary Decision Diagrams. Technical Report, Synopsys, Inc., 700 E. Middlefield Road, Mountain View, CA 94043~ January 1993.

CITED BY 151

	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
	Pranav Ashar , Aarti Gupta , Sharad Malik, Using complete-1-distinguishability for FSM equivalence checking, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.6 n.4, p.569-590, October 2001
	Chunghee Kim , Luciano Lavagno , Alberto Sangiovanni-Vincentelli, Free MDD-based software optimization techniques for embedded systems, Proceedings of the conference on Design, automation and test in Europe, p.14-19, March 27-30, 2000, Paris, France
	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
	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
	Adnan Aziz , Serdar Taşiran , Robert K. Brayton, BDD variable ordering for interacting finite state machines, Proceedings of the 31st annual conference on Design automation, p.283-288, June 06-10, 1994, San Diego, California, United States
	Gila Kamhi , Limor Fix, Adaptive variable reordering for symbolic model checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.359-365, November 08-12, 1998, San Jose, California, United States
	Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States
	Rolf Drechsler, BiTeS: a BDD based test pattern generator for strong robust path delay faults, Proceedings of the conference on European design automation, p.322-327, September 19-23, 1994, Grenoble, France
	Pranav Ashar , Sharad Malik, Fast functional simulation using branching programs, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.408-412, November 05-09, 1995, San Jose, California, United States
	S. Höreth , R. Drechsler, Dynamic minimization of word-level decision diagrams, Proceedings of the conference on Design, automation and test in Europe, p.612-617, February 23-26, 1998, Le Palais des Congrés de Paris, France
	Bwolen Yang , David R. O'Hallaron, Parallel breadth-first BDD construction, ACM SIGPLAN Notices, v.32 n.7, p.145-156, July 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
	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
	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
	Youpyo Hong , Peter A. Beerel , Luciano Lavagno , Ellen M. Sentovich, Don't care-based BDD minimization for embedded software, Proceedings of the 35th annual conference on Design automation, p.506-509, June 15-19, 1998, San Francisco, California, United States
	Ilan Beer , Shoham Ben-David , Cindy Eisner , Avner Landver, RuleBase: an industry-oriented formal verification tool, Proceedings of the 33rd annual conference on Design automation, p.655-660, June 03-07, 1996, Las Vegas, Nevada, 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
	D. Ghosh , N. Kapur , J. Harlow, III , F. Brglez, Synthesis of wiring signature-invariant equivalence class circuit mutants and applications to benchmarking, Proceedings of the conference on Design, automation and test in Europe, p.656-663, February 23-26, 1998, Le Palais des Congrés de Paris, France
	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
	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
	Rolf Drechsler , Wolfgang Günther, Using lower bounds during dynamic BDD minimization, Proceedings of the 36th ACM/IEEE conference on Design automation, p.29-32, June 21-25, 1999, New Orleans, Louisiana, United States
	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Jacob A. Abraham , Donald S. Fussell , Masahiro Fujita, Efficient Combinational Verification Using Overlapping Local BDDs and a Hash Table, Formal Methods in System Design, v.21 n.1, p.95-101, July 2002
	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
	Jawahar Jain , Rajarshi Mukherjee , Masahiro Fujita, Advanced verification techniques based on learning, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.420-426, June 12-16, 1995, San Francisco, California, United States
	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
	Massimiliano Chiodo , Paolo Guisto , Attila Jurecska , Luciano Lavagno , Ellen Sentovich , Harry Hsieh , Kei Suzuki , Alberto Sangiovanni-Vincentelli, Synthesis of software programs for embedded control application, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.587-592, 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
	S. Höreth, Compilation of optimized OBDD-algorithms, Proceedings of the conference on European design automation, p.152-157, September 1996, Geneva, Switzerland
	Yuan Lu , Jawahar Jain , Edmund Clarke , Masahiro Fujita, Efficient variable ordering using aBDD based sampling, Proceedings of the 37th conference on Design automation, p.687-692, June 05-09, 2000, Los Angeles, California, United States
	Youpyo Hong , Peter A. Beerel , Jerry R. Burch , Kenneth L. McMillan, Safe BDD minimization using don't cares, Proceedings of the 34th annual conference on Design automation, p.208-213, June 09-13, 1997, Anaheim, California, United States
	Yi Feng , Eduard Cerny, Term ordering problem on MDG, Proceedings of the 12th ACM Great Lakes symposium on VLSI, April 18-19, 2002, New York, New York, USA
	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
	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
	Pranav Ashar , Aarti Gupta , Sharad Malik, Using complete-1-distinguishability for FSM equivalence checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.346-353, November 10-14, 1996, San Jose, California, United States
	Malay K. Ganai , Adnan Aziz , Andreas Kuehlmann, Enhancing simulation with BDDs and ATPG, Proceedings of the 36th ACM/IEEE conference on Design automation, p.385-390, June 21-25, 1999, New Orleans, Louisiana, United States
	Randal E. Bryant , Christoph Meinel, Ordered binary decision diagrams, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Christoph Scholl , Rolf Drechsler , Bernd Becker, Functional simulation using binary decision diagrams, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.8-12, November 09-13, 1997, San Jose, 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
	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
	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
	Riccardo Forth , Paul Molitor, An efficient heuristic for state encoding minimizing the BDD representations of the transistion relations of finite state machines, Proceedings of the 2000 conference on Asia South Pacific design automation, p.61-66, January 2000, Yokohama, Japan
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, 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
	Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists, Formal Methods in System Design, v.23 n.1, p.39-65, July 2003
	Christoph Meinel , Christian Stangier, Speeding up symbolic model checking by accelerating dynamic variable reordering, Proceedings of the 10th Great Lakes symposium on VLSI, p.39-42, March 02-04, 2000, Chicago, Illinois, 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
	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
	Hiroyuki Higuchi , Fabio Somenzi, Lazy group sifting for efficient symbolic state traversal of FSMs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.45-49, November 07-11, 1999, San Jose, California, United States
	Yukihiro Iguchi , Tsutomu Sasao , Munehiro Matsuura , Atsumu Iseno, A hardware simulation engine based on decision diagrams (short paper), Proceedings of the 2000 conference on Asia South Pacific design automation, p.73-76, January 2000, Yokohama, Japan
	Srilatha Manne , Dirk Grunwald , Fabio Somenzi, Remembrance of things past: locality and memory in BDDs, Proceedings of the 34th annual conference on Design automation, p.196-201, June 09-13, 1997, Anaheim, California, United States
	Christoph Scholl , Bernd Becker, Checking equivalence for partial implementations, Proceedings of the 38th conference on Design automation, p.238-243, June 2001, Las Vegas, Nevada, United States
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Rupesh S. Shelar , Sachin S. Sapatnekar, Recursive bipartitioning of BDDs for performance driven synthesis of pass transistor logic circuits, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Justin E. Harlow, III , Franc Brglez, Design of experiments in BDD variable ordering: lessons learned, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.646-652, November 08-12, 1998, San Jose, California, United States
	Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Faster SAT and smaller BDDs via common function structure, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Anuj Goel , Khurram Sajid , Hai Zhou , Adnan Aziz , Vigyan Singhal, BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, Formal Methods in System Design, v.22 n.3, p.205-224, May 2003
	Christoph Meinel , Christian Stangier, Algorithms and heuristics in VLSI design, Experimental algorithmics: from algorithm design to robust and efficient software, Springer-Verlag New York, Inc., New York, NY, 2002
	Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, FORCE: a fast and easy-to-implement variable-ordering heuristic, Proceedings of the 13th ACM Great Lakes symposium on VLSI, April 28-29, 2003, Washington, D. C., USA
	Stephen A. Edwards, Tutorial: Compiling concurrent languages for sequential processors, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.8 n.2, p.141-187, April 2003
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February 2003
	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
	Detlef Sieling, The complexity of minimizing and learning OBDDs and FBDDs, Discrete Applied Mathematics, v.122 n.1-3, p.263-282, 15 October 2002
	Ingo Wegener, BDDs: design, analysis, complexity, and applications, Discrete Applied Mathematics, v.138 n.1-2, p.229-251, 29 March 2004
	Thomas Eschbach , Wolfgang Günther , Bernd Becker, Orthogonal hypergraph routing for improved visibility, Proceedings of the 14th ACM Great Lakes symposium on VLSI, April 26-28, 2004, Boston, MA, USA
	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
	Wolfgang Günther , Rolf Drechsler, Minimization of free BDDs, Integration, the VLSI Journal, v.32 n.1-3, p.41-59, November 2002
	Yih-Chih Chou , Youn-Long Lin, A 3-step approach for performance-driven whole-chip routing, Proceedings of the 2001 conference on Asia South Pacific design automation, p.187-191, January 2001, Yokohama, Japan
	Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.629-634, June 03-07, 1996, Las Vegas, Nevada, 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
	Premal Buch , Amit Narayan , A. Richard Newton , A. Sangiovanni-Vincentelli, Logic synthesis for large pass transistor circuits, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.663-670, November 09-13, 1997, San Jose, California, United States
	S. Reda , A. Salem, Combinational equivalence checking using Boolean satisfiability and binary decision diagrams, Proceedings of the conference on Design, automation and test in Europe, p.122-126, March 2001, Munich, Germany
	Wolfgang Günther , Andreas Hett , Bernd Becker, Application of linearly transformed BDDs in sequential verification, Proceedings of the 2001 conference on Asia South Pacific design automation, p.91-96, January 2001, Yokohama, Japan
	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
	Amit Goel , Gagan Hasteer , Randal E. Bryant, Symbolic representation with ordered function templates, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Kavita Ravi , Kenneth L. McMillan , Thomas R. Shiple , Fabio Somenzi, Approximation and decomposition of binary decision diagrams, Proceedings of the 35th annual conference on Design automation, p.445-450, June 15-19, 1998, San Francisco, California, United States
	Yu-Liang Wu , Hongbing Fan , Malgorzata Marek-Sadowska , C. k. Wong, OBDD Minimization Based on Two-Level Representation of Boolean Functions, IEEE Transactions on Computers, v.49 n.12, p.1371-1379, December 2000
	Beate Bollig , Ingo Wegener, Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, v.45 n.9, p.993-1002, September 1996
	Christoph Meinel , Thorsten Theobald, Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines, Formal Methods in System Design, v.18 n.3, p.285-301, May 2001
	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
	Rolf Drechsler, Verifying integrity of decision diagrams, Integration, the VLSI Journal, v.32 n.1-3, p.61-75, November 2002
	Shi-Yu Huang , Kwang-Ting Cheng , Kuang-Chien Chen , Forrest Brewer , Chung-Yang Huang, AQUILA: An Equivalence Checking System for Large Sequential Designs, IEEE Transactions on Computers, v.49 n.5, p.443-464, May 2000
	Detlef Sieling, Lower bounds for linearly transformed OBDDs and FBDDs, Journal of Computer and System Sciences, v.64 n.2, p.419-438, March 2002
	Shinobu Nagayama , Tsutomu Sasao, Minimization of memory size for heterogeneous MDDs, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.871-874, January 27-30, 2004, Yokohama, Japan
	Tsutomu Sasao , Munehiro Matsuura, A method to decompose multiple-output logic functions, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
	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
	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
	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
	Enric Pastor , Jordi Cortadella , Oriol Roig, Symbolic Analysis of Bounded Petri Nets, IEEE Transactions on Computers, v.50 n.5, p.432-448, May 2001
	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
	Morten Heine Sørensen , Jens Peter Secher, From type inference to configuration, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	Rolf Drechsler , Bernd Becker , Stefan Ruppertz, The K*BMD: A Verification Data Structure, IEEE Design & Test, v.14 n.2, p.51-59, April 1997
	Camil Demestrescu , Irene Finocchi, Breaking cycles for minimizing crossings, Journal of Experimental Algorithmics (JEA), 6, p.2-es, 2001
	Detlef Sieling, The nonapproximability of OBDD minimization, Information and Computation, v.172 n.2, p.103-138, January 29, 2002
	John Lafferty , Alexander Vardy, Ordered Binary Decision Diagrams and Minimal Trellises, IEEE Transactions on Computers, v.48 n.9, p.971-986, September 1999
	Laura Heinrich-Litan , Paul Molitor, Least Upper Bounds for the Size of OBDDs Using Symmetry Properties, IEEE Transactions on Computers, v.49 n.4, p.360-368, April 2000
	Xiao-Tao Chen , Wei-Kang Huang , Nohpill Park , Fred J. Meyer , Fabrizio Lombardi, Design Verification of FPGA Implementations, IEEE Design & Test, v.16 n.2, p.66-73, April 1999
	Yukihiro Iguchi , Tsutomu Sasao , Munehiro Matsuura, Evaluation of multiple-output logic functions using decision diagrams, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
	Tsutomu Sasao , Munehiro Matsuura, BDD representation for incompletely specifiedvmultiple-output logic functions and its applications to functional decomposition, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
	Weibo Mao , Jinzhao Wu, Application of Wu's method to symbolic model checking, Proceedings of the 2005 international symposium on Symbolic and algebraic computation, p.237-244, July 24-27, 2005, Beijing, China
	Jon T. Butler , Tsutomu Sasao , Munehiro Matsuura, Average Path Length of Binary Decision Diagrams, IEEE Transactions on Computers, v.54 n.9, p.1041-1053, September 2005
	Tomas Bengtsson , Andrés Martinelli , Elena Dubrova, A BDD-based fast heuristic algorithm for disjoint decomposition, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
	Henrik Reif Andersen , Henrik Hulgaard, Boolean expression diagrams, Information and Computation, v.179 n.2, p.194-212, December 15, 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
	Yuke Wang , Mostafa Abd-el-Barr , Carl McCrosky, An Algorithm for Total Symmetric OBDD Detection, IEEE Transactions on Computers, v.46 n.6, p.731-733, June 1997
	Detlef Sieling , Ingo Wegener, A Comparison of Free BDDs and Transformed BDDs, Formal Methods in System Design, v.19 n.3, p.223-236, November 2001
	Neil Kettle , Andy King, An anytime symmetry detection algorithm for ROBDDs, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
	Hiroki Nakahara , Tsutomu Sasao , Munehiro Matsuura, A fast logic simulator using a look up table cascade emulator, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
	Rolf Drechsler , Bernd Becker , Andrea Jahnke, On Variable Ordering and Decomposition Type Choice in OKFDDs, IEEE Transactions on Computers, v.47 n.12, p.1398-1403, December 1998
	Yuke Wang , Carl McCrosky, Solving Boolean Equations Using ROSOP Forms, IEEE Transactions on Computers, v.47 n.2, p.171-177, February 1998
	Ziv Nevo , Monica Farkash, Distributed dynamic BDD reordering, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	G. Ciardo , R. L. Jones, III , A. S. Miner , R. I. Siminiceanu, Logic and stochastic modeling with SMART, Performance Evaluation, v.63 n.6, p.578-608, June 2006
	Christoph Meinel , Christian Stangier, Data structures for Boolean functions, Computational Discrete Mathematics: advanced lectures, Springer-Verlag New York, Inc., New York, NY, 2001
	Yi Feng , Xiaoyu Song, Minimization of multiway decision graphs for RTL verification by stochastic optimization, Proceedings of the 5th WSEAS International Conference on Circuits, Systems, Electronics, Control & Signal Processing, p.327-332, November 01-03, 2006, Dallas, Texas
	Robert Clarisó , Jordi Cortadella, The octahedron abstract domain, Science of Computer Programming, v.64 n.1, p.115-139, January, 2007
	Elsa Loekito , James Bailey, Fast mining of high dimensional expressive contrast patterns using zero-suppressed binary decision diagrams, Proceedings of the 12th ACM SIGKDD international conference on Knowledge discovery and data mining, August 20-23, 2006, Philadelphia, PA, USA
	Carsten Sinz , Albert Haag , Nina Narodytska , Toby Walsh , Esther Gelle , Mihaela Sabin , Ulrich Junker , Barry O'Sullivan , Rick Rabiser , Deepak Dhungana , Paul Grunbacher , Klaus Lehner , Christian Federspiel , Daniel Naus, Configuration, IEEE Intelligent Systems, v.22 n.1, p.78-90, January 2007
	Graham D. Price , John Giacomoni , Manish Vachharajani, Visualizing potential parallelism in sequential programs, Proceedings of the 17th international conference on Parallel architectures and compilation techniques, October 25-29, 2008, Toronto, Ontario, Canada
	P. Dziurzanskii , V. P. Shmerko , S. N. Yanushkevich, Representation of Logical Circuits by Linear Decision Diagrams with Extension to Nanostructures, Automation and Remote Control, v.65 n.6, p.920-937, June 2004
	A. Kolpakov , R. Kh. Latypov, Approximate Algorithms for Minimization of Binary Decision Diagrams on the Basis of Linear Transformations of Variables, Automation and Remote Control, v.65 n.6, p.938-954, June 2004
	Youpyo Hong , Peter A. Beerel, Symbolic reachability analysis of large finite state machines using don't cares, Proceedings of the conference on Design, automation and test in Europe, p.5-es, January 1999, Munich, Germany
	M. A. Thornton , J. P. Williams , R. Drechsler , N. Drechsler, Variable reordering for shared binary decision diagrams using output probabilities, Proceedings of the conference on Design, automation and test in Europe, p.15-es, January 1999, Munich, Germany
	Chao Wang , Gary D. Hachtel , Fabio Somenzi, The Compositional Far Side of Image Computation, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.334, November 09-13, 2003
	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
	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
	Rudiger Ebendt , Wolfgang Gunther , Rolf Drechsler, Combination of Lower Bounds in Exact BDD Minimization, Proceedings of the conference on Design, Automation and Test in Europe, p.10758, March 03-07, 2003
	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
	C. Scholl , S. Melchior , G. Hotz , P. Molitor, Minimizing ROBDD Sizes of Incompletely Specified Boolean Functions by Exploiting Strong Symmetries, Proceedings of the 1997 European conference on Design and Test, p.229, March 17-20, 1997
	Rolf Drechsler , Bernd Becker , Stefan Ruppertz, K*BMDs: A New Data Structure for Verification, Proceedings of the 1996 European conference on Design and Test, p.2, March 11-14, 1996
	C. A. J. Van Eijk , J. A. G. Jess, Exploiting Functional Dependencies in Finite State Machine Verification, Proceedings of the 1996 European conference on Design and Test, p.9, March 11-14, 1996
	Carla Piazza , Alberto Policriti, Ackermann encoding, bisimulations and OBDDs, Theory and Practice of Logic Programming, v.4 n.5-6, p.695-718, September 2004
	Rupesh S. Shelar , Sachin S. Sapatnekar, An Efficient Algorithm for Low Power Pass Transistor Logic Synthesis, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.87, January 07-11, 2002
	Newton Cheung , Sri Parameswaran , Jörg Henkel , Jeremy Chan, MINCE: Matching INstructions Using Combinational Equivalence for Extensible Processor, Proceedings of the conference on Design, automation and test in Europe, p.21020, February 16-20, 2004
	Shan-Tai Chen , Shun-Shii Lin , Li-Te Huang , Chun-Jen Wei, Towards the Exact Minimization of BDDs—An Elitism-Based Distributed Evolutionary Algorithm, Journal of Heuristics, v.10 n.3, p.337-355, May 2004
	Frank Schmiedle , Nicole Drechsler , Daniel Große , Rolf Drechsler, Heuristic Learning Based on Genetic Programming, Genetic Programming and Evolvable Machines, v.3 n.4, p.363-388, December 2002
	Bin Li , Michael S. Hsiao , Shuo Sheng, A Novel SAT All-Solutions Solver for Efficient Preimage Computation, Proceedings of the conference on Design, automation and test in Europe, p.10272, February 16-20, 2004
	Görschwin Fey , Anna Bernasconi , Valentina Ciriani , Rolf Drechsler, On the construction of small fully testable circuits with low depth, Microprocessors & Microsystems, v.32 n.5-6, p.263-269, August, 2008
	Lei Cheng , Deming Chen , Martin D. F. Wong, DDBDD: delay-driven BDD synthesis for FPGAs, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
	Christian Bachmaier, A Radial Adaptation of the Sugiyama Framework for Visualizing Hierarchical Information, IEEE Transactions on Visualization and Computer Graphics, v.13 n.3, p.583-594, May 2007
	Marcilio Mendonca , Andrzej Wasowski , Krzysztof Czarnecki , Donald Cowan, Efficient compilation techniques for large scale feature models, Proceedings of the 7th international conference on Generative programming and component engineering, October 19-23, 2008, Nashville, TN, USA
	Abusaleh Jabir , Dhiraj Pradhan , T. L. Rajaprabhu , A. K. Singh, A Technique for Representing Multiple Output Binary Functions with Applications to Verification and Simulation, IEEE Transactions on Computers, v.56 n.8, p.1133-1145, August 2007
	P. W. C. Prasad , Ali Assi , Bruce Mills, Binary decision diagrams: a mathematical model for the path-related objective functions, Proceedings of the 6th WSEAS International Conference on Simulation, Modelling and Optimization, p.179-185, September 22-24, 2006, Lisbon, Portugal
	Mehdi Mohammadi , Hossein Pazhoumand-dar , Mohsen Soryani , Hossein Moeinzadeh, HS-ROBDD: an efficient variable order binary decision diagram, Proceedings of the 11th annual conference companion on Genetic and evolutionary computation conference, July 08-12, 2009, Montreal, Québec, Canada
	Jesse Bingham, Automatic non-interference lemmas for parameterized model checking, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
	Munehiro Matsuura , Tsutomu Sasao, BDD Representation for Incompletely Specified Multiple-Output Logic Functions and Its Applications to the Design of LUT Cascades, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, v.E90-A n.12, p.2762-2769, December 2007
	Orna Grumberg , Shlomi Livne , Shaul Markovitch, Learning to order BDD variables in verification, Journal of Artificial Intelligence Research, v.18 n.1, p.83-116, January 2003
	Nina Narodytska , Toby Walsh, Constraint and variable ordering heuristics for compiling configuration problems, Proceedings of the 20th international joint conference on Artifical intelligence, p.149-154, January 06-12, 2007, Hyderabad, India
	Rolf Drechsler , Bernd Becker , Nicole Göckel, A genetic algorithm for the construction of small and highly testable OKFDD-circuits, Proceedings of the First Annual Conference on Genetic Programming, July 28-31, 1996, Stanford, California
	Rüdiger Ebendt , Rolf Drechsler, Weighted A∗ search -- unifying view and application, Artificial Intelligence, v.173 n.14, p.1310-1342, September, 2009
	Scott Sanner , David McAllester, Affine algebraic decision diagrams (AADDs) and their application to structured probabilistic inference, Proceedings of the 19th international joint conference on Artificial intelligence, p.1384-1390, July 30-August 05, 2005, Edinburgh, Scotland

Collaborative Colleagues:

Richard Rudell: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player