Journal of Electronic Testing

, Volume 26, Issue 2, pp 211–225 | Cite as

Defining and Providing Coverage for Assertion-Based Dynamic Verification

  • Jason G. Tong
  • Marc Boulé
  • Zeljko Zilic


With the emerging predominance of assertion-based dynamic verification, test generation is a key area where assertions can play a bigger role. Generation of test sequences from properties defined by assertions can help in finding failures in corner-cases of the design specification that without assertions may not be possible. As such, we rely on the duality between property checkers and test generators to take advantage of the information present in the assertions for effective test scenarios—a much needed endeavor given the increasing challenges in verification. To undertake such an effort, we first elaborate on the relation between the coverage of the assertion-based specification and the specific coverage metrics over finite nondeterministic automata representing the assertions. We finally present Airwolf-TG that generate test sequences from compact automata produced by the MBAC tool.


Assertions Verification Testing Coverage Test-generation Automata 


  1. 1.
    Ammann P, Offutt J (2008) Introduction to software testing. Cambridge University Press, New YorkMATHGoogle Scholar
  2. 2.
    Anderson TL (2005) Coverage is the heart of verification. EETimes. Available online:
  3. 3.
    Ball T, Kupferman O (2008) Vacuity in testing. In: Test and proofs, ser. Lecture notes in computer science, vol 4966. Springer, Berlin, pp 4–17CrossRefGoogle Scholar
  4. 4.
    Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in temporal model checking. Form Methods Syst Des 18(2):141–163MATHCrossRefGoogle Scholar
  5. 5.
    Bening L, Foster H (2001) Principles of verifiable RTL design. Kluwer Academic, NorwellGoogle Scholar
  6. 6.
    Boulé M, Chenard J, Zilic Z (2006) Adding debug enhancements to assertion checkers for hardware emulation and silicon debug. In: International conference on computer design, pp 294–299Google Scholar
  7. 7.
    Boulé M, Chenard J, Zilic Z (2007) Assertion checkers in verification, silicon debug and in-field diagnosis. In: Proceedings of the IEEE international symposium on quality electronic design, pp 613–620Google Scholar
  8. 8.
    Boulé M, Chenard J, Zilic Z (2007) Debug enhancements in assertion-checker generation. IET Comput Digit Tech 1(6):669–677CrossRefGoogle Scholar
  9. 9.
    Boulé M, Zilic Z (2007) Efficient automata-based assertion-checker synthesis of SEREs for hardware emulation. In: ASP-DAC ’07: proceedings of the 2007 conference on Asia South Pacific design automation. IEEE Computer Society, Washington, DC, pp 324–329Google Scholar
  10. 10.
    Boulé M, Zilic Z (2008) Automata-based assertion-checker synthesis of PSL properties. ACM Transact Des Automat Electron Syst 13(1):1–21CrossRefGoogle Scholar
  11. 11.
    Boulé M, Zilic Z (2008) Generating hardware assertion checkers: for hardware verification, emulation, post-fabrication debugging and on-line monitoring. Springer, BerlinGoogle Scholar
  12. 12.
    Brzozowski J (1962) Canonical regular expressions and minimal state graphs for definite events. Math Theory Automata 12:529–561Google Scholar
  13. 13.
    Calamé J (2006) Specification-based test generation with TGV. Centrum voor Wiskunde en InformaticaGoogle Scholar
  14. 14.
    Chatterjee D, Bertacco V (2009) Activity-based refinement for abstraction-guided simulation. In: Proceedings of IEEE high-level design validation and test workshop, pp 146–153Google Scholar
  15. 15.
    Cheng K, Krishnakumar A (1993) Automatic functional test generation using the extended finite state machine model. In: Proceedings of the 30th international conference on design automation. ACM, New York, pp 86–91Google Scholar
  16. 16.
    Eisner C, Fisman D (2006) A practical introduction to PSL (Series on integrated circuits and systems). Springer, New YorkGoogle Scholar
  17. 17.
    Foster H (2009) Applied assertion-based verification: an industry perspective. Found Trends Electron Des Autom 3(1):1–95CrossRefGoogle Scholar
  18. 18.
    Foster H, Lacey D, Krolnik A (2003) Assertion-based design. Kluwer Academic, NorwellGoogle Scholar
  19. 19.
    Hierons RM, et al (2009) Using formal specifications to support testing. ACM Comput Surv 41(2):1–76CrossRefGoogle Scholar
  20. 20.
    Hopcroft J, Motwani R, Ullman J (2000) Introduction to automata theory, languages, and computation, 2nd edn. Addison Wesley, ReadingGoogle Scholar
  21. 21.
    Koo H-M, Mishra P (2006) Test generation using SAT-based bounded model checking for validation of pipelined processors. In: GLSVLSI ’06: proceedings of the 16th ACM Great Lakes symposium on VLSI. ACM, New York,pp 362–365CrossRefGoogle Scholar
  22. 22.
    Kupferman O, Vardi M (2003) Vacuity detection in temporal model checking. Int J Softw Tools Technol Transf 4(2):224–233CrossRefGoogle Scholar
  23. 23.
    Mathaikutty DA, Ahuja S, Dingankar A, Shukla S (2007) Model-driven test generation for system level validation. In: High-level design, validation, and test workshop, IEEE international, pp 83–90Google Scholar
  24. 24.
    Oddos Y, Morin-Allory K, Borrione D, Boulé M, Zilic Z (2009) MYGEN: automata-based on-line test generator for assertion-based verification. In: GLSVLSI ’09: proceedings of the 19th ACM Great Lakes symposium on VLSI. ACM, New York, pp 75–80CrossRefGoogle Scholar
  25. 25.
    Pal B, Banerjee A, Sinha A, Dasgupta P (2008) Accelerating assertion coverage with adaptive testbenches. IEEE Trans Comput-Aided Des Integr Circuits Syst 27(5):967–972CrossRefGoogle Scholar
  26. 26.
    Shimizu K, Dill DL (2002) Deriving a simulation input generator and a coverage metric from a formal specification. In: DAC ’02: proceedings of the 39th annual design automation conference. ACM, New York, pp 801–806Google Scholar
  27. 27.
    Sordoillet J, Davey S (2006) Integrated, comprehensive assertion-based coverage. EDA Tech Forum 3(1):22–25Google Scholar
  28. 28.
    Vijayaraghavan S, Ramanathan M (2005) A practical guide for systemVerilog assertions. Springer, BerlinGoogle Scholar
  29. 29.
    Yuan J, Pixley C, Aziz A (2006) Constraint-based verification. Springer, BerlinMATHGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  1. 1.Department of Electrical and Computer Engineering, Integrated Microsystems LaboratoryMcGill UniversityMontréalCanada

Personalised recommendations