Coverability Analysis Using Symbolic Model Checking

  • Gil Ratzaby
  • Shmuel Ur
  • Yaron Wolfsthal
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


In simulation based verification of hardware, as well as in software testing, one is faced with the challenge of maximizing coverage of testing while minimizing testing cost. To this end, sophisticated techniques are used to generate clever test cases, and equally sophisticated techniques are employed by engineers to determine the quality - a.k.a. coverage - attained by the tests. The latter activity is called Test Coverage Analysis.

While it is an essential component of the development process, test coverage can only be analyzed late in the design cycle when the tested entity and the test harness are both stable. To address this serious restriction, we introduce the notion of coverability, which intuitively refers to the degree to which a model can be covered when subjected to testing. We also show an implementation of coverability checking using Model Checking. The notion of coverability highlights a distinction between (1) whether a model has been covered by some test suite and (2) whether the model can ever be covered by any test suite. Coverability Analysis can be performed as soon as the hardware or software are written, before the test harness has been written.


Model Check Coverability Model Symbolic Model Check Dead Code Test Harness 
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.


  1. [AZ97]
    Adnan Aziz, Example of Hardware Verification Using VIS, The benchmark PCI local BUS,
  2. [BBEL96]
    I. Beer, S. Ben-David, C. Eisner, A. Landver, “RuleBase: an Industry-Oriented Formal Verification Tool”, Proc. DAC’96, pp. 655–660.Google Scholar
  3. [Beizer90]
    Boris Beizer, Software Testing Technique, 2/e. New York: Van Nostrand Reinhold, 1990.Google Scholar
  4. [CGP99]
    E.M. Clarke, O. Grumberg. D.A. Peled. Model Checking, MIT Press, 1999.Google Scholar
  5. [CFSM]
    D. Geist, M. Farkas, A. Landver, Y. Licthenstein, S. Ur and Y Wolfsthal, Coverage Directed Test Generation using Symbolic Techniques, FMCAD 96: Int. Conf. On Formal Methods in Computer-Aided Design, November 1996.Google Scholar
  6. [Hol91]
    G. J. Holtzman, Design and Validation of Computer Protocols, Prentice Hall, 1991.Google Scholar
  7. [Kaner95]
    C. Kaner, Software Negligence & Testing Coverage, Software QA Quarterly, Vol 2,#2, pp 18, 1995.Google Scholar
  8. [KN96]
    M. Kantrowitz, L. M. Noack, “I’m Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha Microprocessor”, Proc. DAC’96.Google Scholar
  9. [KPKR94]
    S. Kajihara, I. Pomerantz, K. Kinoshita and S. M. Reddy, “Cost Effective Generation of Minimal Test Sets for Stack-At Faults in Combinatorial logic Circuits”, 30th ACM/IEEE DAC, pp. 102–106, 1993.Google Scholar
  10. [LLU96]
    D. Levin, D. Lorentz and S. Ur, “A Methodology for Processor Implementation Verification”, FMCAD 96: Int. Conf. on Formal Methods in Computer-Aided Design, November 1996.Google Scholar
  11. [Marick95]
    B. Marick, The Craft of Software Testing: Subsystem Testing Including Object-Based and Object-Oriented Testing, Prentice-Hall, 1995.Google Scholar
  12. [McM93]
    K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.Google Scholar
  13. [Mil90]
    Raymond E. Miller, Protocol Verification: The first ten years, the next ten years; some personal observations, in Protocol specification, Testing, and Verification X, 1990.Google Scholar
  14. [RB]
    RuleBase User Manual V1.0, IBM Haifa Research Laboratory, 1996.Google Scholar
  15. [TCE]
    I. Beer, M. Dvir, B. Kozitsa. Y Lichtenstein, S. Mach, W.J. Nee, E. Rappaport. Q. Schmierer, Y Zandman, VHDL TEST COVERAGE in BDLS/AUSSIM Environment, IBM HRL Technical Report 88.342, December 1993.Google Scholar
  16. [VHDL93]
    D. L. Perry, VHDL Second Edition, McGraw-Hill Series on Computer Engineering, 1993.Google Scholar
  17. [Weyuker94]
    E. Weyuker, T. Goradia and A. Singh, Automatically Generating Test Data from a Boolean Specification, IEEE Transaction on Software Engineering, Vol 20, No 5 May 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Gil Ratzaby
    • 1
  • Shmuel Ur
    • 1
  • Yaron Wolfsthal
    • 1
  1. 1.IBM Haifa Research LaboratoryIsrael

Personalised recommendations