Transition-based coverage estimation for symbolic model checking

ABSTRACT

Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

REFERENCES

• 1: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 2: Yatin Hoskote , Timothy Kam , Pei-Hsin Ho , Xudong Zhao, Coverage estimation for symbolic model checking, Proceedings of the 36th ACM/IEEE conference on Design automation, p.300-305, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309936]
• 3: Nikhil Jayakumar , Mitra Purandare , Fabio Somenzi, Dos and don'ts of CTL state coverage estimation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775908]
• 4: X. Xu, S. Kimura, K. Horikawa, and T. Tsuchiya. "Transition Traversal Coverage Estimation for Symbolic Model Checking". In Proceedings of the 3rd ACM/IEEE international Confernece on Formal Methods and Models for Co-Design (MEMOCODE), page 259--260, 2005.
• 5: Sagi Katz , Orna Grumberg , Daniel Geist, "Have I written enough Properties?" - A Method of Comparison between Specification and Implementation, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.280-297, September 27-29, 1999
• 6: H. Chockler, O. Kupferman, and M. Y. Vardi. "Coverage Metrics for Formal Verification". In Proceedings of 12th ACM Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARM), page 111--125, 2003.
• 7: Hana Chockler , Orna Kupferman , Robert P. Kurshan , Moshe Y. Vardi, A Practical Approach to Coverage in Model Checking, Proceedings of the 13th International Conference on Computer Aided Verification, p.66-78, July 18-22, 2001
• 8: Franco Fummi , Graziano Pravadelli , Andrea Fedeli , Umberto Rossi , Franco Toto, On the Use of a High-Level Fault Model to Check Properties Incompleteness, Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'03), p.145, June 24-26, 2003
• 9: F. Wang, G.-D. Huang, F. Yu. "Numerical Coverage Estimation for the symbolic simulation of real-time systems". FORTE 2003, LNCS 2767, pages 160--176, 2003.
• 10: Serdar Tasiran , Kurt Keutzer, Coverage Metrics for Functional Validation of Hardware Designs, IEEE Design & Test, v.18 n.4, p.36-45, July 2001 [doi>10.1109/54.936247 ]
• 11: Yatin V. Hoskote , Dinos Moundanos , Jacob A. Abraham, Automatic extraction of the control flow machine and application to evaluating coverage of verification vectors, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.532-537, October 02-04, 1995
• 12: Richard C. Ho , C. Han Yang , Mark A. Horowitz , David L. Dill, Architecture validation for processors, Proceedings of the 22nd annual international symposium on Computer architecture, p.404-413, June 22-24, 1995, S. Margherita Ligure, Italy
• 13: A. Das , P. Basu , A. Banerjee , P. Dasgupta , P. P. Chakrabarti , C. Rama Mohan , L. Fix , R. Armoni, Formal verification coverage: computing the coverage gap between temporal specifications, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.198-203, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382571]
• 14: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 15: Aarti Gupta , Sharad Malik , Pranav Ashar, Toward formalizing a validation methodology using simulation coverage, Proceedings of the 34th annual conference on Design automation, p.740-745, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266359]
• 16: David Chaiken , Craig Fields , Kiyoshi Kurihara , Anant Agarwal, Directory-Based Cache Coherence in Large-Scale Multiprocessors, Computer, v.23 n.6, p.49-58, June 1990 [doi>10.1109/2.55500 ]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution

General Terms:
Design, Verification