Decomposing image computation for symbolic reachability analysis using control flow information

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.
2. R. K. Brayton et al. VIS. In Formal Methods in Computer Aided Design, pages 248--256. Springer-Verlag, Berlin, Nov. 1996. LNCS 1166.
3. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, Aug. 1986.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.

Index Terms

• Computing methodologies

  • Computer graphics

    • Graphics systems and interfaces

      • Graphics processors

• Hardware

  • Electronic design automation

    • Physical design (EDA)

  • Hardware validation

  • Integrated circuits

  • Very large scale integration design

    • Application-specific VLSI designs

      • Application specific processors