Advertisement

Coverage Metrics for Formal Verification

  • Hana Chockler
  • Orna Kupferman
  • Moshe Y. Vardi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2860)

Abstract

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. The challenge of making the verification process as exhaustive as possible is even more crucial in simulation-based verification, where the infeasible task of checking all input sequences is replaced by checking a test suite consisting of a finite subset of them. It is very important to measure the exhaustiveness of the test suite, and indeed, there has been an extensive research in the simulation-based verification community on coverage metrics, which provide such a measure. It turns out that no single measure can be absolute, leading to the development of numerous coverage metrics whose usage is determined by industrial verification methodologies. On the other hand, prior research of coverage in formal verification has focused solely on state-based coverage. In this paper we adapt the work done on coverage in simulation-based verification to the formal-verification setting in order to obtain new coverage metrics. Thus, for each of the metrics used in simulation-based verification, we present a corresponding metric that is suitable for the setting of formal verification, and describe an algorithmic way to check it.

Keywords

Model Check Input Sequence Linear Temporal Logic Coverage Metrics Code Coverage 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [AFF+03]
    Armon, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Vardi, M.Y.: Enhanced vacuity detection for linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368–380. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. [AFG+02]
    Armoni, R., Fix, L., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Tiemeyer, A., Singerman, E., Vardi, M.Y., Zbar, Y.: The ForSpec temporal language: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. [BB94]
    Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: Proc. 31st DAC, pp. 596–602. IEEE Computer Society, Los Alamitos (1994)Google Scholar
  4. [BBER01]
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods in System Design 18(2), 141–162 (2001)MATHCrossRefGoogle Scholar
  5. [BCM+92]
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. I&C 98(2), 142–170 (1992)MATHMathSciNetGoogle Scholar
  6. [BF00]
    Bening, L., Foster, H.: Principles of verifiable RTL design – a functional coding style supporting verification processes. Kluwer Academic Publishers, Dordrecht (2000)MATHGoogle Scholar
  7. [BKM02]
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on java predicates. In: Proc. ISSTA, pp. 123–133 (2002)Google Scholar
  8. [Büc62]
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. ICLMP, pp. 1–12 (1962)Google Scholar
  9. [Bud81]
    Budd, T.A.: Mutation analysis: Ideas, examples, problems, and prospects. Computer Program Testing, 129–148 (1981)Google Scholar
  10. [Cad03]
    Cadence. Assertion-based verification (2003), http://www.cadence.com
  11. [CGMZ95]
    Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427–432 (1995)Google Scholar
  12. [CGP99]
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  13. [Cho03]
    Chockler, H.: Coverage metrics for model checking. PhD thesis, Hebrew University, Jerusalem, Israel (2003)Google Scholar
  14. [CK02]
    Chockler, H., Kupferman, O.: Coverage of implementations by simulating specifications. In: Proc. 2nd TCS, vol. 223, pp. 409–421. Kluwer Academic Publishers, Dordrecht (2002)Google Scholar
  15. [CKKV01]
    Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 66–78. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  16. [CKV01]
    Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 528–542. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  17. [Dil98]
    Dill, D.L.: What’s between simulation and formal verification? In. In: Proc. 35st DAC, pp. 328–329. IEEE Computer Society, Los Alamitos (1998)Google Scholar
  18. [DLS78]
    DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: Help for the practicing programmer. IEEE Computer 11(4), 34–43 (1978)Google Scholar
  19. [FLLO95]
    French, R.S., Lam, M.S., Levitt, J.R., Olukotun, K.: A general method for compiling event-driven simulations. In: Proc. DAC, pp. 151–156 (1995)Google Scholar
  20. [HH96]
    Ho, R.C., Horowitz, M.A.: Validation coverage analysis for complex digital designs. In: Proc. ICCAD, pp. 146–151 (1996)Google Scholar
  21. [HHK96]
    Hardin, R.H., Har’el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 423–427. Springer, Heidelberg (1996)Google Scholar
  22. [HKHZ99]
    Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proc. 36th DAC, pp. 300–305 (1999)Google Scholar
  23. [Hol97]
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering 23(5), 279–295 (1997); Special issue on Formal Methods in Software PracticeCrossRefMathSciNetGoogle Scholar
  24. [Hos95]
    Hoskote, Y.V.: Formal techniques for verification of synchronous sequential circuits. PhD thesis, The University of Texas at Austin (1995)Google Scholar
  25. [KGG99]
    Katz, S., Geist, D., Grumberg, O.: “Have I written enough properties?” a method of comparison between specification and implementation. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 280–297. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  26. [KN96]
    Kantrowitz, M., Noack, L.: I’m done simulating: Now what? verification coverage analysis and correctness checking of the dec chip 21164 alpha microprocessor. In: Proc. DAC, pp. 325–330 (1996)Google Scholar
  27. [Kur97]
    Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. DAC 1997, vol. 34, pp. 258–262 (1997)Google Scholar
  28. [Kur98]
    Kurshan, R.P.: FormalCheck User’s Manual. Cadence Design, Inc. (1998)Google Scholar
  29. [KV03]
    Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Journal on Software Tools For Technology Transfer 4(2), 224–233 (2003)CrossRefGoogle Scholar
  30. [Mar99]
    Marick, B.: How to misuse code coverage. In: Proc. 16th ICTCS (June 1999)Google Scholar
  31. [MP92]
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification (1992)Google Scholar
  32. [Pel01]
    Peled, D.: Software Reliability Methods (2001)Google Scholar
  33. [PS02]
    Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 485–499. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  34. [SA99]
    Shen, J., Abraham, J.A.: An RTL abstraction technique for processor microarchitecture validation and test generation. Journal of Electronic Testing 16(1-2), 67–81 (1999)Google Scholar
  35. [TK01]
    Tasiran, S., Keutzer, K.: Coverage metrics for functional validation of hardware designs. IEEE Design and Test of Computers 18(4), 36–45 (2001)CrossRefGoogle Scholar
  36. [UZ98]
    Ur, S., Ziv, A.: Off-the-shelf vs. custom made coverage models, which is the one for you? In: Proc. ICSTAR (1998)Google Scholar
  37. [Ver03]
    Verisity. Surecove’s code coverage technology (2003), http://www.verisity.com/products/surecov.html
  38. [VW86]
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332–344 (1986)Google Scholar
  39. [VW94]
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C 115(1), 1–37 (1994)MATHMathSciNetGoogle Scholar
  40. [ZHM97]
    Zhu, H., Hall, P.V., May, J.R.: Software unit test coverage and adequacy. ACM Computing Surveys 29(4), 366–427 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Hana Chockler
    • 1
  • Orna Kupferman
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.School of Engineering and Computer ScienceHebrew UniversityJerusalemIsrael
  2. 2.Department of Computer ScienceRice UniversityHoustonU.S.A.

Personalised recommendations