Verification of arithmetic circuits with binary moment diagrams

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verification of arithmetic circuits with binary moment diagrams

Full text

Pdf (168 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 32nd annual ACM/IEEE Design Automation Conference table of contents

San Francisco, California, United States

Pages: 535 - 541

Year of Publication: 1995

ISBN:0-89791-725-1

Authors

Randal E. Bryant	Carnegie Mellon University, Pittsburgh, PA
Yirng-An Chen	Carnegie Mellon University, Pittsburgh, PA

Sponsors

EDAC : Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 19, Citation Count: 71

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/217474.217583 What is a DOI?

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	R. Iris Bahar , Erica A. Frohm , Charles M. Gaona , Gary D. Hachtel , Enrico Macii , Abelardo Pardo , Fabio Somenzi, Algebraic decision diagrams and their applications, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.188-191, November 07-11, 1993, Santa Clara, California, United States
	2	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]
	3	Randy E. Bryant , Yirng Chen, Verification of Arithmetic Functions with Binary Moment Diagrams, Carnegie Mellon University, Pittsburgh, PA, 1994
	4	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 [doi>10.1145/127601.127703]
	5	E. M. Clarke , K. L. McMillan , X Zhao , M. Fujita , J. Yang, Spectral transforms for large boolean functions with applications to technology mapping, Proceedings of the 30th international conference on Design automation, p.54-60, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164569]
	6	R. Enders, "Note on the complexity of binary moment diagram representations," unpublished paper, Siemens AG, Munich Germany, 1994.
	7	J. Jain, J. Bitner, M. Abadir, J. A. Abraham, and D. S. Fussell, "Indexed BDDs: Algorithmic advances in techniques to represent and verify Boolean functions," submitted for publication, 1994.
	8	U. Kebschull, E. Schubert, and W. Rosentiel, "Multilevel logic based on functional decision diagrams," European Design Automation Conference, 1992, pp. 43-47.
	9	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
	10	Shin-ichi Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, Proceedings of the 30th international conference on Design automation, p.272-277, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164890]
	11	S.-i. Minato, "Implicit manipulation of polynomials using zerosuppressed BDDs," unpublished manuscript, 1994.
	12	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

CITED BY 71

	Shin-ichi Minato, Generation of BDDs from hardware algorithm descriptions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.644-649, November 10-14, 1996, San Jose, California, United States
	Harald Ruess , Natarajan Shankar , Mandayam K. Srivas, Modular Verification of SRT Division, Formal Methods in System Design, v.14 n.1, p.45-73, January 1999
	Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.156-166, Nov. 1996
	P. Dasgupta , P. Chakrabarti , A. Nandi , S. Krishna , A. Chakrabarti, Abstraction of word-level linear arithmetic functions from bit-level component descriptions, Proceedings of the conference on Design, automation and test in Europe, p.4-8, March 2001, Munich, Germany
	Randal E. Bryant, Bit-level analysis of an SRT divider circuit, Proceedings of the 33rd annual conference on Design automation, p.661-665, June 03-07, 1996, Las Vegas, Nevada, 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
	Ying-Tsai Chang , Kwang Ting, Self-referential verification of gate-level implementations of arithmetic circuits, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	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
	Martin Keim , Rolf Drechsler , Bernd Becker , Michael Martin , Paul Molitor, Polynomial Formal Verification of Multipliers, Formal Methods in System Design, v.22 n.1, p.39-58, January 2003
	E. M. Clarke , M. Fujita , X. Zhao, Hybrid decision diagrams, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.159-163, November 05-09, 1995, San Jose, California, United States
	Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States
	Sandro Wefel , Paul Molitor, Prove that a faulty multiplier is faulty!?, Proceedings of the 10th Great Lakes symposium on VLSI, p.43-46, March 02-04, 2000, Chicago, Illinois, United States
	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
	S. Höreth, Compilation of optimized OBDD-algorithms, Proceedings of the conference on European design automation, p.152-157, September 1996, Geneva, Switzerland
	Whitney J. Townsend , Mitchell A. Thornton , Rolf Drechsler , D. Michael Miller, Computing walsh, arithmetic, and reed-muller spectral decision diagrams using graph transformations, Proceedings of the 12th ACM Great Lakes symposium on VLSI, April 18-19, 2002, New York, New York, USA
	Yirng-An Chen , Randal E. Bryant, ACV: an arithmetic circuit verifier, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.361-365, November 10-14, 1996, San Jose, California, United States
	Jiunn-Chern Chen , Yirng-An Chen, Equivalence checking of integer multipliers, Proceedings of the 2001 conference on Asia South Pacific design automation, p.169-174, January 2001, Yokohama, Japan
	James Smith , Giovanni De Micheli, Polynomial methods for component matching and verification, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.678-685, November 08-12, 1998, San Jose, 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
	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
	Yufeng Luo , Tjahjadi Wongsonegoro , Adnan Aziz, Hybrid techniques for fast functional simulation, Proceedings of the 35th annual conference on Design automation, p.664-667, June 15-19, 1998, San Francisco, California, United States
	James Smith , Giovanni De Micheli, Polynomial circuit models for component matching in high-level synthesis, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.9 n.6, p.783-800, 12/1/2001
	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
	Ying Tsai Chang , Kwang Ting Tim Cheng, Induction-based gate-level verification of multipliers, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	E. M. Clarke , M. Khaira , X. Zhao, Word level model checking—avoiding the Pentium FDIV error, Proceedings of the 33rd annual conference on Design automation, p.645-648, June 03-07, 1996, Las Vegas, Nevada, United States
	Christoph Scholl , Bernd Becker , Thomas M. Weis, Word-level decision diagrams, WLCDs and division, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.672-677, November 08-12, 1998, San Jose, California, United States
	Dominik Stoffel , Wolfgang Kunz, Verification of integer multipliers on the arithmetic bit level, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Dhiraj K. Pradhan , Debjyoti Paul , Mitrajit Chatterjee, VERILAT: verification using logic augmentation and transformations, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.88-95, November 10-14, 1996, San Jose, California, United States
	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
	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
	Randal E. Bryant , Christoph Meinel, Ordered binary decision diagrams, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	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
	Stephen Edwards , Luciano Lavagno , Edward A. Lee , Alberto Sangiovanni-Vincentelli, Design of embedded systems: formal models, validation, and synthesis, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
	Katarzyna Radecka , Zeljko Zilic, Specifying and verifying imprecise sequential datapaths by Arithmetic Transforms, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.128-131, November 10-14, 2002, San Jose, California
	Tevfik Bultan , Richard Gerber , Christopher League, Verifying systems with integer constraints and Boolean predicates: a composite approach, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.113-123, March 1998
	Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000
	David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
	Katarzyna Radecka , Zeljko Zilic, Design Verification by Test Vectors and Arithmetic Transform Universal Test Set, IEEE Transactions on Computers, v.53 n.5, p.628-640, May 2004
	Rolf Drechsler, Verifying integrity of decision diagrams, Integration, the VLSI Journal, v.32 n.1-3, p.61-75, November 2002
	William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998
	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
	John Lafferty , Alexander Vardy, Ordered Binary Decision Diagrams and Minimal Trellises, IEEE Transactions on Computers, v.48 n.9, p.971-986, September 1999
	Christoph Scholl , Bernd Becker , Thomas Weis, On WLCDs and the Complexity of Word-Level Decision Diagrams—A Lower Bound for Division, Formal Methods in System Design, v.20 n.3, p.311-326, May 2002
	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
	Zhihong Zeng , Kesava R. Talupuru , Maciej Ciesielski, Functional test generation based on word-level SAT, Journal of Systems Architecture: the EUROMICRO Journal, v.51 n.8, p.488-511, August 2005
	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
	Jawahar Jain , James Bitner , Magdy S. Abadir , Jacob A. Abraham , Donald S. Fussell, Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions, IEEE Transactions on Computers, v.46 n.11, p.1230-1245, November 1997
	Louis Kruger , Somesh Jha , Eu-Jin Goh , Dan Boneh, Secure function evaluation with ordered binary decision diagrams, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
	V. P. Shmerko, Malyugin's Theorems: A New Concept in Logical Control, VLSI Design, and Data Structures for New Technologies, Automation and Remote Control, v.65 n.6, p.893-912, June 2004
	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
	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
	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Masahiro Fujita , Jacob A. Abraham , Donald S. Fussell, An efficient filter-based approach for combinational verification, Proceedings of the conference on Design, automation and test in Europe, p.31-es, January 1999, Munich, Germany
	Stefan Höreth , Rolf Drechsler, Formal verification of word-level specifications, Proceedings of the conference on Design, automation and test in Europe, p.11-es, January 1999, Munich, Germany
	Kanji Hirabayashi, A Method of Formal Verification of Cryptographic Circuits, Journal of Electronic Testing: Theory and Applications, v.13 n.3, p.321-322, Dec. 1998
	M. Huhn , K. Schneider , Th. Kropf , G. Logothetis, Verifying imprecisely working arithmetic circuits, Proceedings of the conference on Design, automation and test in Europe, p.13-es, January 1999, Munich, Germany
	James Smith , Giovanni De Micheli, Polynomial methods for allocating complex components, Proceedings of the conference on Design, automation and test in Europe, p.45-es, January 1999, Munich, Germany
	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
	Kanji Hirabayashi, An Algebraic Approach to Formal Verification of Microprocessors, Journal of Electronic Testing: Theory and Applications, v.17 n.6, p.543-544, December 2001
	P. Dziurzanski , V. Malyugin , V. Shmerko , S. Yanushkevich, Linear Models of Circuits Based on the Multivalued Components, Automation and Remote Control, v.63 n.6, p.960-980, June 2002
	Christian Jacobi , Kai Weber , Viresh Paruthi , Jason Baumgartner, Automatic Formal Verification of Fused-Multiply-Add FPUs, Proceedings of the conference on Design, Automation and Test in Europe, p.1298-1303, March 07-11, 2005
	Abusaleh M. Jabir , Dhiraj K. Pradhan, MODD: A New Decision Diagram and Representation for Multiple Output Binary Functions, Proceedings of the conference on Design, automation and test in Europe, p.21388, February 16-20, 2004
	Chao-Yue Lai , Chung-Yang (Ric) Huang , Kei-Yong Khoo, Improving constant-coefficient multiplier verification by partial product identification, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany
	Elsa Loekito , James Bailey, Are zero-suppressed binary decision diagrams good for mining frequent patterns in high dimensional datasets?, Proceedings of the sixth Australasian conference on Data mining and analytics, December 03-04, 2007, Gold Coast, Australia
	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
	Udo Krautz , Markus Wedler , Wolfgang Kunz , Kai Weber , Christian Jacobi , Matthias Pflanz, Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proof, Proceedings of the 2008 conference on Asia and South Pacific design automation, January 21-24, 2008, Seoul, Korea
	Shobha Vasudevan , Vinod Viswanath , Robert W. Sumners , Jacob A. Abraham, Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems, IEEE Transactions on Computers, v.56 n.10, p.1401-1414, October 2007
	Abusaleh M. Jabir , Dhiraj K. Pradhan, A Graph-Based Unified Technique for Computing and Representing Coefficients over Finite Fields, IEEE Transactions on Computers, v.56 n.8, p.1119-1132, August 2007
	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
	Stanislav StankoviĆ , Jaakko Astola, XML Framework for Various Types of Decision Diagrams for Discrete Functions, IEICE - Transactions on Information and Systems, v.E90-D n.11, p.1731-1740, November 2007
	Yuki Watanabe , Naofumi Homma , Takafumi Aoki , Tatsuo Higuchi, Arithmetic Circuit Verification Based on Symbolic Computer Algebra, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, v.E91-A n.10, p.3038-3046, October 2008