Formal verification of PowerPC arrays using symbolic trajectory evaluation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formal verification of PowerPC arrays using symbolic trajectory evaluation

Full text

Pdf (122 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 33rd annual Design Automation Conference table of contents

Las Vegas, Nevada, United States

Pages: 649 - 654

Year of Publication: 1996

ISBN:0-89791-779-0

Authors

Manish Pandey	School of Computer Science, Carnegie Mellon University Pittsburgh, PA
Richard Raimi	Motorola Inc., 6501 William Cannon Drive West, Austin, TX
Derek L. Beatty	Motorola Inc., 6501 William Cannon Drive West, Austin, TX
Randal E. Bryant	School of Computer Science, Carnegie Mellon University Pittsburgh, PA

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

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

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/240518.240641 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	Derek Lee Beatty, A methodology for formal hardware verification, with application to microprocessors, Carnegie Mellon University, Pittsburgh, PA, 1993
	2	Derek L. Beatty , Randal E. Bryant, Formally verifying a microprocessor using a simulation methodology, Proceedings of the 31st annual conference on Design automation, p.596-602, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196575]
	3	Derek L. Beatty , Randal E. Bryant , Carl-Johan H. Seger, Synchronous circuit verification by symbolic simulation: an illustration, Proceedings of the sixth MIT conference on Advanced research in VLSI, p.98-112, March 1990, Boston, Massachusetts, United States
	4	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]
	5	Randal E. Bryant, Symbolic simulation—techniques and applications, Proceedings of the 27th ACM/IEEE conference on Design automation, p.517-521, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.128296]
	6	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	7	A. Kuehlmann , A. Srinivasan , D. P. LaPotin, Verity—a formal verification program for custom CMOS circuits, IBM Journal of Research and Development, v.39 n.1-2, p.149-165, Jan./March 1995
	8	M. Pandey, R. E. Bryant, "Memory array state node identification tool," accepted for publication in Motorola Technical Developments, Motorola Inc.
	9	Laurence C. Paulson, ML for the working programmer, Cambridge University Press, New York, NY, 1991
	10	Carl-Johan H. Seger , Randal E. Bryant, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, v.6 n.2, p.147-189, March 1995 [doi>10.1007/BF01383966]
	11	Carl Seger, VOSS - A Formal Hardware Verification System User''s Guide, University of British Columbia, Vancouver, BC, Canada, 1993

CITED BY 17

	Li-C. Wang , Magdy S. Abadir, Experience in Validation of PowerPCTM Microprocessor Embedded Arrays, Journal of Electronic Testing: Theory and Applications, v.15 n.1-2, p.191-205, August-October 1999
	Narayanan Krishnamurthy , Andrew K. Martin , Magdy S. Abadir , Jacob A. Abraham, Validating PowerPC Microprocessor Custom Memories, IEEE Design & Test, v.17 n.4, p.61-76, October 2000
	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
	Tao Feng , Li-C. Wang , Kwang-Ting Cheng , Manish Pandey , Magdy S. Abadir, Enhanced symbolic simulation for efficient verification of embedded array systems, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
	Joel Grodstein , Rachid Rayess , Tad Truex , Linda Shattuck , Sue Lowell , Dan Bailey , David Bertucci , Gabriel Bischoff , Daniel Dever , Mike Gowan , Roy Lane , Brian Lilly , Krishna Nagalla , Rahul Shah , Emily Shriver , Shi-Huang Yin , Shannon Morton, Power and CAD considerations for the 1.75mbyte, 1.2ghz L2 cache on the alpha 21364 CPU, Proceedings of the 12th ACM Great Lakes symposium on VLSI, April 18-19, 2002, New York, New York, USA
	Li-C. Wang , Magdy S. Abadir , Nari Krishnamurthy, Automatic generation of assertions for formal verification of PowerPC microprocessor arrays using symbolic trajectory evaluation, Proceedings of the 35th annual conference on Design automation, p.534-537, June 15-19, 1998, San Francisco, California, United States
	Jin Yang , Carl-Johan H. Seger, Introduction to generalized symbolic trajectory evaluation, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.3, p.345-353, June 2003
	Narayanan Krishnamurthy , Magdy S. Abadir , Andrew K. Martin , Jacob A. Abraham, Design and Development Paradigm for Industrial Formal Verification CAD Tools, IEEE Design & Test, v.18 n.4, p.26-35, July 2001
	Manish Pandey , Richard Raimi , Randal E. Bryant , Magdy S. Abadir, Formal verification of content addressable memories using symbolic trajectory evaluation, Proceedings of the 34th annual conference on Design automation, p.167-172, June 09-13, 1997, Anaheim, California, United States
	Li-C. Wang , Magdy S. Abadir , Jing Zeng, On measuring the effectiveness of various design validation approaches for PowerPC microprocessor embedded arrays, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.4, p.524-532, Oct. 1998
	L.-C. Wang , M. S. Abadir , J. Zeng, Measuring the effectiveness of various design validation approaches for PowerPCTM microprocessor arrays, Proceedings of the conference on Design, automation and test in Europe, p.273-277, February 23-26, 1998, Le Palais des Congrés de Paris, France
	Magdy S. Abadir , Kenneth L. Albin , John Havlicek , Narayanan Krishnamurthy , Andrew K. Martin, Formal Verification Successes at Motorola, Formal Methods in System Design, v.22 n.2, p.117-123, March 2003
	Jin Yang , Amit Goel, GSTE through a case study, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.534-541, November 10-14, 2002, San Jose, California
	Jayanta Bhadra , Andrew K. Martin , Jacob A. Abraham, A formal framework for verification of embedded custom memories of the Motorola MPC7450 microprocessor, Formal Methods in System Design, v.27 n.1/2, p.67-112, September 2005
	Li-C. Wang , Magdy S. Abadir, Test Generation Based on High-Level Assertion Specification for PowerPCTM Microprocessor Embedded Arrays, Journal of Electronic Testing: Theory and Applications, v.13 n.2, p.121-135, Oct. 1998
	Alan J. Hu , Jeremy Casas , Jin Yang, Efficient Generation of Monitor Circuits for GSTE Assertion Graphs, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.154, November 09-13, 2003
	Malay K. Ganai , Aarti Gupta , Pranav Ashar, Verification of Embedded Memory Systems using Efficient Memory Modeling, Proceedings of the conference on Design, Automation and Test in Europe, p.1096-1101, March 07-11, 2005