Representing circuits more efficiently in symbolic model checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Representing circuits more efficiently in symbolic model checking

Full text

Pdf (543 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 28th ACM/IEEE Design Automation Conference table of contents

San Francisco, California, United States

Pages: 403 - 407

Year of Publication: 1991

ISBN:0-89791-395-7

Authors

J. R. Burch	School of Computer Science, Carnegie Mellon University
E. M. Clarke	School of Computer Science, Carnegie Mellon University
D. E. Long	School of Computer Science, Carnegie Mellon University

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 20, Citation Count: 39

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/127601.127702 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	C. Berthet, O. Coudert, and J.-C. Madre. New ideas on symbolic manipulations of finite state machines. In ICCD, 1990.
	2	S. Bose and A. Fisher. Verifying pipelined hardware using symbolic logic simulation. In ICCD, 1989.
	3	Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
	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 , 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
	6	J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
	7	J. R. Butch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In LICS, 1990.
	8	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]
	9	O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
	10	Olivier Coudert , Jean Christophe Madre , Christian Berthet, Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.23-32, June 18-21, 1990
	11	R. Kurshan and E. M. Clarke, editors. Workshop on Computer-Aided Verification. DIMACS, June 1990. Technical Report 90-31.
	12	K. L. McMillan. Formal verification of the Gigamax cache consistency protocol, in international Symposium on Shared Memory Multiprocessing, 1991. To appear.
	13	:I. A. Rees, N. I. Adams, and :1. R. Meehan. The T Manual. Yale University, 4th edition, 1984.
	14	H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDD's. In 1CCAD, 1990.

CITED BY 39

	B. A. Gennart , D. C. Luckham, Validating discrete event simulations using event pattern mappings, Proceedings of the 29th ACM/IEEE conference on Design automation, p.414-419, June 08-12, 1992, Anaheim, California, United States
	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
	J.-K. Rho , F. Somenzi, Inductive verification of iterative systems, Proceedings of the 29th ACM/IEEE conference on Design automation, p.628-633, June 08-12, 1992, Anaheim, California, United States
	Massimiliano Chiodo , Thomas R. Shiple , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Automatic compositional minimization in CTL model checking, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.172-178, November 1992, Santa Clara, California, United States
	Amit Narayan , Jawahar Jain , M. Fujita , A. Sangiovanni-Vincentelli, Partitioned ROBDDs—a compact, canonical and efficiently manipulable representation for Boolean functions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.547-554, November 10-14, 1996, San Jose, California, United States
	Ilan Beer , Shoham Ben-David , Cindy Eisner , Avner Landver, RuleBase: an industry-oriented formal verification tool, Proceedings of the 33rd annual conference on Design automation, p.655-660, June 03-07, 1996, Las Vegas, Nevada, United States
	Pranav Ashar , Aarti Gupta , Sharad Malik, Using complete-1-distinguishability for FSM equivalence checking, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.6 n.4, p.569-590, October 2001
	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States
	In-Ho Moon , James H. Kukula , Kavita Ravi , Fabio Somenzi, To split or to conjoin: the question in image computation, Proceedings of the 37th conference on Design automation, p.23-28, June 05-09, 2000, Los Angeles, California, United States
	Pranav Ashar , Aarti Gupta , Sharad Malik, Using complete-1-distinguishability for FSM equivalence checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.346-353, November 10-14, 1996, San Jose, California, United States
	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
	Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States
	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994
	Hiroyuki Higuchi , Fabio Somenzi, Lazy group sifting for efficient symbolic state traversal of FSMs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.45-49, November 07-11, 1999, San Jose, California, United States
	Benoit A. Gennart, Comparative design validation based on event pattern mappings, Proceedings of the 30th international conference on Design automation, p.373-378, June 14-18, 1993, Dallas, Texas, United States
	Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , Jim Kukula , Tom Shiple , Helmut Veith , Dong Wang, Non-linear quantification scheduling in image computation, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
	June-Kyung Rho , Fabio Somenzi , Carl Pixley, Minimum length synchronizing sequences of finite state machine, Proceedings of the 30th international conference on Design automation, p.463-468, June 14-18, 1993, Dallas, Texas, United States
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Yih-Chih Chou , Youn-Long Lin, A 3-step approach for performance-driven whole-chip routing, Proceedings of the 2001 conference on Asia South Pacific design automation, p.187-191, January 2001, Yokohama, Japan
	L. Ness, L.0: A Truly Concurrent Executable Temporal Logic Language for Protocols, IEEE Transactions on Software Engineering, v.19 n.4, p.410-423, April 1993
	Wolfgang Günther , Andreas Hett , Bernd Becker, Application of linearly transformed BDDs in sequential verification, Proceedings of the 2001 conference on Asia South Pacific design automation, p.91-96, January 2001, Yokohama, Japan
	Kavita Ravi , Kenneth L. McMillan , Thomas R. Shiple , Fabio Somenzi, Approximation and decomposition of binary decision diagrams, Proceedings of the 35th annual conference on Design automation, p.445-450, June 15-19, 1998, San Francisco, California, United States
	R. I. Bahar , E. A. Frohm , C. M. Gaona , G. D. Hachtel , E. Macii , A. Pardo , F. Somenzi, Algebric Decision Diagrams and Their Applications, Formal Methods in System Design, v.10 n.2-3, p.171-206, April -May 1997
	R. Alur , R. K. Brayton , T. A. Henzinger , S. Qadeer , S. K. Rajamani, Partial-Order Reduction in Symbolic State-Space Exploration, Formal Methods in System Design, v.18 n.2, p.97-116, March 1, 2001
	Giampiero Cabodi , Paolo Camurati , Fulvio Corno , Paolo Prinetto , Matteo Sonza Reorda, The General Product Machine: a New Model for Symbolic FSM Traversal, Formal Methods in System Design, v.12 n.3, p.267-289, April 1, 1998
	Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001
	Henrik Reif Andersen , Henrik Hulgaard, Boolean expression diagrams, Information and Computation, v.179 n.2, p.194-212, December 15, 2002
	Prakash M. Peranandam , Pradeep K. Nalla , Jürgen Ruf , Roland J. Weiss , Thomas Kropf , Wolfgang Rosenstiel, Fast falsification based on symbolic bounded property checking, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for embedded software verification, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
	David Ward , Fabio Somenzi, Decomposing image computation for symbolic reachability analysis using control flow information, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
	Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for software verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.2, p.10-es, April 2007
	M. D. Nguyen , D. Stoffel , M. Wedler , W. Kunz, Transition-by-transition FSM traversal for reachability analysis in bounded model checking, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1068-1075, November 06-10, 2005, San Jose, CA
	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
	Shuo Sheng , Michael Hsiao, Efficient Preimage Computation Using A Novel Success-Driven ATPG, Proceedings of the conference on Design, Automation and Test in Europe, p.10822, March 03-07, 2003
	Ansuman Banerjee , Pallab Dasgupta , P. P. Chakrabarti, Auxiliary state machines + context-triggered properties in verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.4, p.1-31, September 2008
	Gunjan Khanna , Mike Yu Cheng , Padma Varadharajan , Saurabh Bagchi , Miguel P. Correia , Paulo J. Veríssimo, Automated Rule-Based Diagnosis through a Distributed Monitor System, IEEE Transactions on Dependable and Secure Computing, v.4 n.4, p.266-279, October 2007
	Zijiang Yang , Chao Wang , Aarti Gupta , Franjo Ivanvčić, Model checking sequential software programs via mixed symbolic analysis, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.14 n.1, p.1-26, January 2009
	Hong-Zu Chou , I-Hui Lin , Ching-Sung Yang , Kai-Hui Chang , Sy-Yen Kuo, Enhancing bug hunting using high-level symbolic simulation, Proceedings of the 19th ACM Great Lakes symposium on VLSI, May 10-12, 2009, Boston Area, MA, USA