More Web Proxy on the site http://driver.im/

Article

Decomposing image computation for symbolic reachability analysis using control flow information

Authors:

Fabio SomenziAuthors Info & Claims

ICCAD '06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design

Pages 779 - 785

https://doi.org/10.1145/1233501.1233662

Published: 05 November 2006 Publication History

Abstract

The main challenge in BDD-based symbolic reachability analysis is represented by the sizes of the intermediate decision diagrams obtained during image computations. Methods proposed to mitigate this problem fall broadly into two categories: Search strategies that depart from breadth-first search, and efficient techniques for image computation. In this paper we present an algorithm that belongs to the latter category. It exploits define-use information along executable paths extracted from the control-flow graph of the model being analyzed; this information enables an effective constraining of the transition relation and a decomposition of the image computation process that often leads to much smaller intermediate BDDs. Our experiments confirm that this reduction in the size of the representation of state sets translates in significant decreases in CPU and memory requirements.

References

[1]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99), pages 193--207, Amsterdam, The Netherlands, Mar. 1999. LNCS 1579.

Digital Library

[2]

R. K. Brayton et al. VIS. In Formal Methods in Computer Aided Design, pages 248--256. Springer-Verlag, Berlin, Nov. 1996. LNCS 1166.

Digital Library

[3]

R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, Aug. 1986.

Digital Library

[4]

J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the Design Automation Conference, pages 403--407, San Francisco, CA, June 1991.

Digital Library

[5]

G. Cabodi, P. Camurati, L. Lavagno, and S. Quer. Disjunctive partitionining and partial iterative squaring: An effective approach for symbolic traversal of large circuits. In Proceedings of the Design Automation Conference, pages 728--733, Anaheim, CA, June 1997.

Digital Library

[6]

G. Cabodi, P. Camurati, and S. Quer. Improved reachability analysis of large finite state machines. In Proceedings of the International Conference on Computer-Aided Design, pages 354--360, Santa Clara, CA, Nov. 1996.

Digital Library

[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 111--128, Leuven, Belgium, Nov. 1989.

[8]

O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 126--129, Nov. 1990.

[9]

X. Feng, A. J. Hu, and J. Yang. Partitioned model checking from software specifications. In Proceedings of the 10th Asia and South Pacific Design Automation Conference (ASP-DAC 2005), pages 583--587, 2005.

Digital Library

[10]

R. Fraer, G. Kamhi, B. Ziv, M. Y. Vardi, and L. Fix. Prioritized traversal: Efficient reachability analysis for verification and falsification. In E. A. Emerson and A. P. Sistla, editors, Twelfth Conference on Computer Aided Verification (CAV'00), pages 389--402. Springer-Verlag, Berlin, July 2000. LNCS 1855.

Digital Library

[11]

D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 299--310, Berlin, 1994. Springer-Verlag. LNCS 818.

Digital Library

[12]

A. Gupta, Z. Yang, P. Ashar, and A. Gupta. SAT-based image computation with application in reachability analysis. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 354--271. Springer-Verlag, Nov. 2000. LNCS 1954.

Digital Library

[13]

H. Higuchi and F. Somenzi. Lazy group sifting for efficient symbolic state traversal of FSMs. In Proceedings of the International Conference on Computer-Aided Design, pages 45--49, San Jose, CA, Nov. 1999.

Digital Library

[14]

Y. Hong, P. A. Beerel, J. R. Burch, and K. L. McMillan. Safe BDD minimization using don't cares. In Proceedings of the Design Automation Conference, pages 208--213, Anaheim, CA, June 1997.

Digital Library

[15]

ITC'99 benchmark home page. http://www.cerc.utexas.edu/itc99-benchmarks/bench.html.

[16]

J. C. Madre. Private communication, 1996.

[17]

K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.

Digital Library

[18]

C. Meinel and C. Stangier. Speeding up image computation by using RTL information. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 443--454. Springer-Verlag, Berlin, Nov. 2000. LNCS 1954.

Digital Library

[19]

C. Meinel and C. Stangier. Hierarchical image computation with dynamic conjunction scheduling. In Proceedings of the International Conference on Computer Design, Austin, TX, Sept. 2001.

Digital Library

[20]

C. Meinel and C. Stangier. Hierarchical image computation with dynamic conjunction scheduling. Presented at IWLS01, June 2001.

[21]

I.-H. Moon, G. D. Hachtel, and F. Somenzi. Border-block triangular form and conjunction schedule in image computation. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 73--90. Springer-Verlag, Nov. 2000. LNCS 1954.

Digital Library

[22]

I.-H. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23--28, Los Angeles, CA, June 2000.

Digital Library

[23]

A. Narayan, J. Jain, M. Fujita, and A. L. Sangiovanni-Vincentelli. Partition ROBDDs: A compact, canonical and efficiently manipulable representation for boolean functions. In Proceedings of the International Conference on Computer-Aided Design, pages 547--554, Santa Clara, CA, Nov. 1996.

Digital Library

[24]

R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA, May 1995.

[25]

K. Ravi, K. L. McMillan, T. R. Shiple, and F. Somenzi. Approximation and decomposition of decision diagrams. In Proceedings of the Design Automation Conference, pages 445--450, San Francisco, CA, June 1998.

Digital Library

[26]

K. Ravi and F. Somenzi. High-density reachability analysis. In Proceedings of the International Conference on Computer-Aided Design, pages 154--158, San Jose, CA, Nov. 1995.

Digital Library

[27]

K. Ravi and F. Somenzi. Hints to accelerate symbolic traversal. In Correct Hardware Design and Verification Methods (CHARME'99), pages 250--264, Berlin, Sept. 1999. Springer-Verlag. LNCS 1703.

Digital Library

[28]

T. R. Shiple, R. Hojati, A. L. Sangiovanni-Vincentelli, and R. K. Brayton. Heuristic minimization of BDDs using don't cares. In Proceedings of the Design Automation Conference, pages 225--231, San Diego, CA, June 1994.

Digital Library

[29]

F. Somenzi. CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp://vlsi.colorado.edu/pub/.

[30]

D. E. Thomas and P. R. Moorby. The Verilog Hardware Description Language. Kluwer Academic Publishers, Boston, MA, third edition, 1996.

Digital Library

[31]

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, Nov. 1990.

[32]

C. A. J. van Eijk. Formal Methods for the Verification of Digital Circuits. PhD thesis, Eindhoven University of Technology, Department of Electrical Engineering, Aug. 1997.

[33]

Vis verification benchmarks. http://vlsi.colorado.edu/~vis.

[34]

D. Ward and F. Somenzi. Automatic generation of hints for symbolic traversal. In Correct Hardware Design and Verification Methods (CHARME'05), pages 207--221, Saarbrucken, Germany, Oct. 2005. Springer-Verlag. LNCS 3725.

Digital Library

Cited By

Liu LVasudevan S(2014)Scaling Input Stimulus Generation through Hybrid Static and Dynamic Analysis of RTLACM Transactions on Design Automation of Electronic Systems10.1145/267654920:1(1-33)Online publication date: 18-Nov-2014
https://dl.acm.org/doi/10.1145/2676549
Ganai MWang CLi WScheffer LPhillips JHu A(2010)Efficient state space explorationProceedings of the International Conference on Computer-Aided Design10.5555/2133429.2133594(786-793)Online publication date: 7-Nov-2010
https://dl.acm.org/doi/10.5555/2133429.2133594
Ganai MWang CLi W(2010)Efficient state space exploration: Interleaving stateless and state-based model checking2010 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)10.1109/ICCAD.2010.5653863(786-793)Online publication date: Nov-2010
https://doi.org/10.1109/ICCAD.2010.5653863
Show More Cited By

Index Terms

Decomposing image computation for symbolic reachability analysis using control flow information
1. Computing methodologies
  1. Computer graphics
    1. Graphics systems and interfaces
      1. Graphics processors
2. Hardware

Recommendations

Reachability and reverse reachability analysis of CFSMs

Reachability analysis and the recently proposed reverse reachability analysis are two important verification techniques for communicating finite state machines (CFSM). The issue of the relative efficiency of reachability analysis and reverse ...
Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design

November 2006

147 pages

ISBN:1595933891

DOI:10.1145/1233501

General Chair:
Soha Hassoun
Tufts Univ., Medford, MA

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 November 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICCAD06

Sponsor:

SIGDA
IEEE-CAS
IEEE-CS

ICCAD06: The International Conference on Computer-Aided Design 2006

November 5 - 9, 2006

California, San Jose

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
143
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Liu LVasudevan S(2014)Scaling Input Stimulus Generation through Hybrid Static and Dynamic Analysis of RTLACM Transactions on Design Automation of Electronic Systems10.1145/267654920:1(1-33)Online publication date: 18-Nov-2014
https://dl.acm.org/doi/10.1145/2676549
Ganai MWang CLi WScheffer LPhillips JHu A(2010)Efficient state space explorationProceedings of the International Conference on Computer-Aided Design10.5555/2133429.2133594(786-793)Online publication date: 7-Nov-2010
https://dl.acm.org/doi/10.5555/2133429.2133594
Ganai MWang CLi W(2010)Efficient state space exploration: Interleaving stateless and state-based model checking2010 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)10.1109/ICCAD.2010.5653863(786-793)Online publication date: Nov-2010
https://doi.org/10.1109/ICCAD.2010.5653863
Ganai MGupta AFix L(2008)Tunneling and slicingProceedings of the 45th annual Design Automation Conference10.1145/1391469.1391507(137-142)Online publication date: 8-Jun-2008
https://dl.acm.org/doi/10.1145/1391469.1391507

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents