Formal verification of word-level specifications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formal verification of word-level specifications

Full text

Pdf (104 KB)

Source

Design, Automation, and Test in Europe archive
Proceedings of the conference on Design, automation and test in Europe table of contents

Munich, Germany

Article No. 11

Year of Publication: 1999

ISBN:1-58113-121-6

Authors

Stefan Höreth	Siemens Corporate R&D, Munich, Germany, and Department of Electrical & Computer Engineering, Darmstadt University of Technology
Rolf Drechsler	Institute of Computer Science, Albert-Ludwigs-University, Freiburg, Germany

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 12, Citation Count: 3

Additional Information:

references cited by index terms collaborative colleagues

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/307418.307447 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	Laurent Arditi, BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.34-48, November 06-08, 1996
	2	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
	3	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 [doi>10.1145/277044.277186]
	4	Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
	5	Randy E. Bryant , Yirng Chen, Verification of Arithmetic Functions with Binary Moment Diagrams, Carnegie Mellon University, Pittsburgh, PA, 1994
	6	Randal E. Bryant , Yirng-An Chen, Verification of arithmetic circuits with binary moment diagrams, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.535-541, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217583]
	7	Yirng-An Chen , Edmund M. Clarke , Pei-Hsin Ho , Yatin Vasant Hoskote , Timothy Kam , Manpreet Khaira , John W. O'Leary , Xudong Zhao, Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.19-33, November 06-08, 1996
	8	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
	9	[9] E. Clarke, M. Fujita, P. McGeer, K.L. McMillan, J. Yang, and X. Zhao. Multi terminal binary decision diagrams: An efficient data structure for matrix representation. In Int'l Workshop on Logic Synth., pages P6a:1-15, 1993.
	10	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
	11	Edmund Clarke , Xudong Zhao, Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits, Carnegie Mellon University, Pittsburgh, PA, 1995
	12	David Cyrluk , M. Oliver Möller , Harald Rueß, An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors, Proceedings of the 9th International Conference on Computer Aided Verification, p.60-71, June 22-25, 1997
	13	[13] R. Drechsler and B. Becker. Binary Decision Diagrams - Theory and Implementation. Kluwer Academic Publishers, 1998.
	14	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 [doi>10.1109/54.587742]
	15	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 [doi>10.1145/196244.196444]
	16	Stefan Höreth, Implementation of a multiple-domain decision diagram package, Proceedings of the IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods: Advances in Hardware Design and Verification, p.185-202, October 16-18, 1997
	17	[17] S. Höreth. Effiziente Konstruktion und Manipulation von binären Entscheidungsgraphen. Ph.D. thesis at Technische Universität, Darmstadt, 1998.
	18	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
	19	Gila Kamhi , Osnat Weissberg , Limor Fix, Automatic Datapath Extraction for Efficient Usage of HDD, Proceedings of the 9th International Conference on Computer Aided Verification, p.95-106, June 22-25, 1997
	20	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
	21	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 [doi>10.1145/288548.289114]

CITED BY 3

	Mohammad Ali Ghodrat , Tony Givargis , Alex Nicolau, Equivalence checking of arithmetic expressions using fast evaluation, Proceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems, September 24-27, 2005, San Francisco, California, USA
	K. Wahid , D. C. Lu , C. Rahman, HDL Constructs in Linear Word-Level Decision Diagram Based Specification, Automation and Remote Control, v.65 n.6, p.913-919, June 2004
	R. Drechsler, Using Word-Level Information in Formal Hardware Verification, Automation and Remote Control, v.65 n.6, p.963-977, June 2004