High-density reachability analysis

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

High-density reachability analysis

Full text

Publisher Site , Pdf

Pdf (221 KB)

Source

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

San Jose, California, United States

Pages: 154 - 158

Year of Publication: 1995

ISBN:0-8186-7213-7

Authors

Kavita Ravi	Dept. of Electrical and Computer Engineering, University of Colorado at Boulder
Fabio Somenzi	Dept. of Electrical and Computer Engineering, University of Colorado at Boulder

Sponsors

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

Publisher

IEEE Computer Society Washington, DC, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 14, Citation Count: 43

Additional Information:

abstract references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

ABSTRACT

We address the problem of reachability analysis for large finite state systems. Symbolic techniques have revolutionized reachability analysis but still have limitations in traversing large systems. We present techniques to improve the symbolic breadth-first traversal and compute a lower bound on the reachable states. We identify the problem as one of density during traversal and our techniques seek to improve the same. Our results show a marked improvement on the existing breadth-first traversal methods.

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	O. Coudert, C. Berthet, and J. C. Madre, "Verification of sequential machines using boolean functional vectors," in Proc. IFIP International Workshop on Applied Formal Methods for Correct VLSI Design (L. Claesen, ed.), (Leuven, Belgium), pp. 111-128, Nov. 1989.
	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, vol. 13, pp. 401-424, Apr. 1994.
	3	H. Cho, G. D. Hachtel, S.-W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi, "ATPG aspects of FSM verification," in Proc. ICCAD, pp. 134-137, Nov. 1990.
	4	S.-W. Jeong, B. Plessier, G. D. Hachtel, and F. Somenzi, "Variable ordering and selection for FSM traversal," in Proc. ICCAD , (Santa Clara, CA), pp. 476-479, Nov. 1991.
	5	Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Bernard Plessier , Fabio Somenzi, Algorithms for approximate FSM traversal, Proceedings of the 30th international conference on Design automation, p.25-30, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164555]
	6	Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Massimo Poncino , Fabio Somenzi, A Structural Approach to State Space Decomposition for Approximate Reachability Analysis, Proceedings of the1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, p.236-239, October 10-12, 1994
	7	David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
	8	A. Ghosh and S. Devadas, "A mixed depth-first/breadth-first technique for sequential logic verification," in IWLS , (MCNC, Research Triangle Park, NC), May 1991.
	9	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]
	10	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]
	11	Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
	12	J. Jain, J. Bitner, D. S. Fussell, and J. A. Abraham, "Functional partitioning for verification and related problems," in Brown/MIT VLSI Conference, Mar. 1992.
	13	H. Cho, G. D. Hachtel, E. Macii, M. Poncino, K. Ravi, and F. Somenzi, "Approximate finite state machine traversal: Extensions and new results." Presented at IWLS95, Lake Tahoe, CA., May 1995.

CITED BY 43

	G. Cabodi , P. Camurati , S. Quer, Biasing symbolic search by means of dynamic activity profiles, Proceedings of the conference on Design, automation and test in Europe, p.9-15, March 2001, Munich, Germany
	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
	Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Improving symbolic traversals by means of activity profiles, Proceedings of the 36th ACM/IEEE conference on Design automation, p.306-311, June 21-25, 1999, New Orleans, Louisiana, United States
	Chia-Chih Yen , Jing-Yang Jou , Kuang-Chien Chen, A Divide-and-Conquer-Based Algorithm for Automatic Simulation Vector Generation, IEEE Design & Test, v.21 n.2, p.111-120, March 2004
	Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Improved reachability analysis of large finite state machines, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.354-360, November 10-14, 1996, San Jose, California, United States
	S. Quer , G. Cabodi , P. Camurati, Decomposed symbolic forward traversals of large finite state machines, Proceedings of the conference on European design automation, p.170-175, September 1996, Geneva, Switzerland
	Valeria Bertacco , Kunle Olukotun, Efficient state representation for symbolic simulation, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Luca Benini , Enrico Macii , Massimo Poncino, Telescopic units: increasing the average throughput of pipelined designs by adaptive latency control, Proceedings of the 34th annual conference on Design automation, p.22-27, June 09-13, 1997, Anaheim, California, United States
	L. Benini , G. De Micheli , A. Lioy , E. Macii , G. Odasso , M. Poncino, Computational kernels and their application to sequential power optimization, Proceedings of the 35th annual conference on Design automation, p.764-769, June 15-19, 1998, San Francisco, California, United States
	L. Benini , G. De Micheli , E. Macii , G. Odasso , M. Poncino, Kernel-based power optimization of RTL components: exact and approximate extraction algorithms, Proceedings of the 36th ACM/IEEE conference on Design automation, p.247-252, June 21-25, 1999, New Orleans, Louisiana, United States
	Jules P. Bergmann , Mark A. Horowitz, Improving coverage analysis and test generation for large designs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.580-583, November 07-11, 1999, San Jose, California, United States
	L. Benini , G. De Micheli , E. Macii , M. Poncino , R. Scarsi, Symbolic synthesis of clock-gating logic for power optimization of control-oriented synchronous networks, Proceedings of the 1997 European conference on Design and Test, p.514, March 17-20, 1997
	Andreas Kuehlmann , Kenneth L. McMillan , Robert K. Brayton, Probabilistic state space search, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.574-579, November 07-11, 1999, San Jose, California, United States
	Shankar G. Govindaraju , David L. Dill, Verification by approximate forward and backward reachability, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.366-370, November 08-12, 1998, San Jose, California, United States
	Yael Abarbanel-Vinov , Neta Aizenbud-Reshef , Ilan Beer , Cindy Eisner , Daniel Geist , Tamir Heyman , Iris Reuveni , Eran Rippel , Irit Shitsevalov , Yaron Wolfsthal , Tali Yatzkar-Haham, On the Effective Deployment of Functional Formal Verification, Formal Methods in System Design, v.19 n.1, p.35-44, July 2001
	Andreas Hett , Christoph Scholl , Bernd Becker, Distance driven finite state machine traversal, Proceedings of the 37th conference on Design automation, p.39-42, June 05-09, 2000, Los Angeles, California, United States
	L. Benini , G. De Micheli , E. Macii , M. Poncino , R. Scarsi, Symbolic synthesis of clock-gating logic for power optimization of synchronous controllers, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.4, p.351-375, Oct. 1999
	Dong Wang , Pei-Hsin Jiang , James Kukula , Yunshan Zhu , Tony Ma , Robert Damiano, Formal property verification by abstraction refinement with formal, simulation and hybrid engines, Proceedings of the 38th conference on Design automation, p.35-40, June 2001, Las Vegas, Nevada, United States
	Adnan Aziz , Jim Kukula , Tom Shiple, Hybrid verification using saturated simulation, Proceedings of the 35th annual conference on Design automation, p.615-618, June 15-19, 1998, San Francisco, California, United States
	Abelardo Pardo , Gary D. Hachtel, Incremental CTL model checking using BDD subsetting, Proceedings of the 35th annual conference on Design automation, p.457-462, June 15-19, 1998, San Francisco, California, United States
	Fabrizio Ferrandi , Franco Fummi , Enrico Macii , Massimo Poncino , Donatella Sciuto, Symbolic optimization of FSM networks based on sequential ATPG techniques, Proceedings of the 33rd annual conference on Design automation, p.467-470, June 03-07, 1996, Las Vegas, Nevada, United States
	In-Ho Moon , Jae-Young Jang , Gary D. Hachtel , Fabio Somenzi , Jun Yuan , Carl Pixley, Approximate reachability don't cares for CTL model checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.351-358, November 08-12, 1998, San Jose, California, United States
	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
	G. Cabodi , P. Camurati , L. Garcia , M. Murciano , S. Nocco , S. Quer, Trading-off SAT search and variable quantifications for effective unbounded model checking, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
	Dominik Stoffel , Wolfgang Kunz, Record & play: a structural fixed point iteration for sequential circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.394-399, November 09-13, 1997, San Jose, California, United States
	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
	William Chan , Richard J. Anderson , Paul Beame , David H. Jones , David Notkin , William E. Warner, Decoupling synchronization from local control for efficient symbolic model checking of statecharts, Proceedings of the 21st international conference on Software engineering, p.142-151, May 16-22, 1999, Los Angeles, California, United States
	Christoph Meinel , Fabio Somenzi , Thorsten Theobald, Linear sifting of decision diagrams, Proceedings of the 34th annual conference on Design automation, p.202-207, June 09-13, 1997, Anaheim, California, United States
	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
	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
	Malay K. Ganai , Adnan Aziz , Andreas Kuehlmann, Enhancing simulation with BDDs and ATPG, Proceedings of the 36th ACM/IEEE conference on Design automation, p.385-390, June 21-25, 1999, New Orleans, Louisiana, United States
	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
	Malay Ganai , Praveen Yalagandula , Adnan Aziz , Andreas Kuehlmann , Vigyan Singhal, SIVA: A System for Coverage-Directed State Space Search, Journal of Electronic Testing: Theory and Applications, v.17 n.1, p.11-27, February 2001
	Orna Grumberg , Flavio Lerda , Ofer Strichman , Michael Theobald, Proof-guided underapproximation-widening for multi-process systems, ACM SIGPLAN Notices, v.40 n.1, p.122-131, January 2005
	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
	Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
	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
	William Chan , Richard J. Anderson , Paul Beame , David Notkin , David H. Jones , William E. Warner, Optimizing Symbolic Model Checking for Statecharts, IEEE Transactions on Software Engineering, v.27 n.2, p.170-190, February 2001
	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
	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
	Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
	Andreas Kuehlmann , Cornelis A. J. van Eijk, Combinational and sequential equivalence checking, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	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