Linking BDD-based symbolic evaluation to interactive theorem-proving

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Linking BDD-based symbolic evaluation to interactive theorem-proving

Full text

Pdf (745 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 30th international Design Automation Conference table of contents

Dallas, Texas, United States

Pages: 469 - 474

Year of Publication: 1993

ISBN:0-89791-577-1

Authors

Jeffrey J. Joyce
Carl-Johan H. Seger

Sponsors

EDAC : Electronic Design Automation Consortium
IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 15, Citation Count: 6

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/157485.164981 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	Randal E. Bryant , Derek L. Beatty , Carl-Johan H. Seger, Formal hardware verification by symbolic ternary trajectory evaluation, Proceedings of the 28th conference on ACM/IEEE design automation, p.397-402, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127701]
	2	R.E. Bryant, "A Switch-Level Model and Simulator for MOS Digital Systems," IEEE Trans. on Computers Vol. C- 33, No. 2, February, 1984, pp. 160-177.
	3	R.E. Bryant, "Symbolic Verification of MOS Circuits", 1985 Chapel Hill Conferenceon VLSI, May, 1985, pp. 419- 438.
	4	R. E. Bryant , D. Beatty , K. Brace , K. Cho , T. Sheffler, COSMOS: a compiled simulator for MOS circuits, Proceedings of the 24th ACM/IEEE conference on Design automation, p.9-16, June 28-July 01, 1987, Miami Beach, Florida, United States [doi>10.1145/37888.37890]
	5	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]
	6	Randal E. Bryant , Carl-Johan H. Seger, Formal Verification of Digital Circuits Using Symbolic Ternary System Models, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.33-43, June 18-21, 1990
	7	Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
	8	Mark Genoe , Luc J. M. Claesen , Eric Verlind , Frank Proesmans , Hugo De Man, Illustration of the SFG-Tracing Multi-Level Behavioral Verification Methodology, by the Correctness Proof of a High to Low Level Synthesis Application in CATHEDRAL-II, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.338-341, October 14-16, 1991
	9	J. Joyce, Multi-Level Verification of Microprocessor-Based Systems, Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1989. Report No. 195, Computer Laboratory, Cambridge University, May 1990.
	10	M.J.C. Gordon et al., The HOL System Description, Cambridge Research Centre, SRI International, Suite 23, Miller's Yard, Cambridge CB2 1RQ, England.
	11	Carl Seger, An Introduction to Formal Hardware Verification, University of British Columbia, Vancouver, BC, Canada, 1992
	12	C-J. Seger, "The Voss Verification System--User's Guide", in preparation.
	13	Carl Seger , Jeffrey J. Joyce, A Mathematically Precise Two-Level Formal Hardware Verification Methodology*, University of British Columbia, Vancouver, BC, Canada, 1992
	14	C-J. Seger and R. E. Bryant, "Formal Verification of Digital Circuits by Symbolic Evaluation of Partially-Ordered Trajectories", in preparation.
	15	Silos llmLogic and Fault Simulator: User's manual, SIMUCAD, Palo Alto, 1988.

CITED BY 6

	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
	Mark D. Aagaard , Robert B. Jones , Carl-Johan H. Seger, Combining theorem proving and trajectory evaluation in an industrial environment, Proceedings of the 35th annual conference on Design automation, p.538-541, June 15-19, 1998, San Francisco, California, United States
	V. K. Pisini , S. Tahar , P. Curzon , O. Ait-Mohamed , X. Song, Formal hardware verification by integrating HOL and MDG, Proceedings of the 10th Great Lakes symposium on VLSI, p.23-28, March 02-04, 2000, Chicago, Illinois, United States
	T. Kuhn , T. Oppold , M. Winterholer , W. Rosenstiel , Marc Edwards , Yaron Kashai, A framework for object oriented hardware specification, verification, and synthesis, Proceedings of the 38th conference on Design automation, p.413-418, June 2001, Las Vegas, Nevada, United States
	Haiyan Xiong , Paul Curzon , Sofiène Tahar , Ann Blandford, Providing a formal linkage between MDG and HOL, Formal Methods in System Design, v.30 n.2, p.83-116, April 2007
	Jayanta Bhadra , Magdy S. Abadir , Li-C. Wang , Sandip Ray, A Survey of Hybrid Techniques for Functional Verification, IEEE Design & Test, v.24 n.2, p.112-122, March 2007