Approximate reachability don't cares for CTL model checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Approximate reachability don't cares for CTL model checking

Full text

Pdf (939 KB)

Source

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

San Jose, California, United States

Pages: 351 - 358

Year of Publication: 1998

ISBN:1-58113-008-2

Authors

In-Ho Moon	Dept. of ECE, University of Colorado, Boulder, CO
Jae-Young Jang	Dept. of ECE, University of Colorado, Boulder, CO
Gary D. Hachtel	Dept. of ECE, University of Colorado, Boulder, CO
Fabio Somenzi	Dept. of ECE, University of Colorado, Boulder, CO
Jun Yuan	Design Verification, Motorola Inc., Austin, TX
Carl Pixley	Design Verification, Motorola Inc., Austin, TX

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society
IEEE-EDS : Electronic Devices Society
IEEE-CAS : Circuits & Systems

Publisher

ACM New York, NY, USA

Bibliometrics

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

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/288548.289053 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. K. Brayton et al. VIS: A system for verification and synthesis. Technical Report UCB/ERL M95/104, Electronics Research Lab, Univ. of California, December 1995.
	2	J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer- Aided Design, 13(4):401.-424, April 1994.
	3	H. Cho, G. D. Hachtel, S.-W. Jeong, B. Plessier, E. Schwarz, and E Somenzi. ATPG aspects of FSM verification, in Proceedings of the IEEE International Conference on Computer Aided Design, pages 134-137, November 1990.
	4	H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and E Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. IEEE Transactions on Computer-Aided Design, 15(12):1465-1478, December 1996.
	5	H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and E Somenzi. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Transactions on Computer-Aided Design, 15(12):1451- 1464, December 1996.
	6	Y. Choueka. Theories of automata on w-tapes: A simplified approach. Journal of Computer and System Sciences, 8:117-141, 1974.
	7	O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages I I 1-128, Leuven, Belgium, November 1989.
	8	Daniel Geist , Ilan Beer, Efficient Model Checking by Automated Ordering of Transition Relation Partitions, Proceedings of the 6th International Conference on Computer Aided Verification, p.299-310, June 21-23, 1994
	9	Shankar G. Govindaraju , David L. Dill , Alan J. Hu , Mark A. Horowitz, Approximate reachability with BDDs using overlapping projections, Proceedings of the 35th annual conference on Design automation, p.451-456, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277169]
	10	Hiroaki Iwashita , Tsuneo Nakata, Forward model checking techniques oriented to buggy designs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.400-404, November 09-13, 1997, San Jose, California, United States
	11	Hiroaki Iwashita , Tsuneo Nakata , Fumiyasu Hirose, CTL model checking based on forward state traversal, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.82-87, November 10-14, 1996, San Jose, California, United States
	12	Thomas Lindner. Case Study "Production Cell": A Comparative Study in Formal Software Development, chapter 2, pages 9,21. FZI, 1994.
	13	Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
	14	Abelardo Pardo , Gary D. Hachtel, Automatic Abstraction Techniques for Propositional µ-calculus Model Checking, Proceedings of the 9th International Conference on Computer Aided Verification, p.12-23, June 22-25, 1997
	15	R.K. Ranjan, A. Aziz, R. K. Brayton, B. E Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA., May 1995.
	16	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
	17	H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDD's. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 130-133, November 1990.
	18	Jun Yuan , Jian Shen , Jacob A. Abraham , Adnan Aziz, On Combining Formal and Informal Verification, Proceedings of the 9th International Conference on Computer Aided Verification, p.376-387, June 22-25, 1997

CITED BY 10

	Jae-Young Jang , In-Ho Moon , Gary D. Hachtel, Iterative abstraction-based CTL model checking, Proceedings of the conference on Design, automation and test in Europe, p.502-509, March 27-30, 2000, Paris, France
	Chung-Yang Huang , Kwang-Ting Cheng, Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques, Proceedings of the 37th conference on Design automation, p.118-123, June 05-09, 2000, Los Angeles, California, United States
	In-Ho Moon , James Kukula , Tom Shiple , Fabio Somenzi, Least fixpoint approximations for reachability analysis, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.41-44, November 07-11, 1999, San Jose, California, United States
	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
	Sean Safarpour , Görschwin Fey , Andreas Veneris , Rolf Drechsler, Utilizing don't care states in SAT-based bounded sequential problems, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
	Chao Wang , Roderick Bloem , Gary D. Hachtel , Kavita Ravi , Fabio Somenzi, Compositional SCC Analysis for Language Emptiness, Formal Methods in System Design, v.28 n.1, p.5-36, January 2006
	Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Boosting the role of inductive invariants in model checking, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	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
	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
	Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals, Proceedings of the conference on Design, Automation and Test in Europe, p.10898, March 03-07, 2003