Abstract
Debugging, on average, has grown to consume more than 60% of today’s ASIC and SoC verification effort. Clearly, this is a topic the industry must address, and some organizations have done just that. Those that have adopted an assertion-based verification (ABV) methodology have seen significant reduction in simulation debugging time (as much as 50% [1]) due to improved observability. Furthermore, organizations that have embraced an ABV methodology are able to take advantage of more advanced verification techniques, such as formal verification, thus improving their overall verification quality and results. Nonetheless, even with multiple published industry case studies from various early adopters—each touting the benefits of applying ABV—the industry as a whole has resisted adopting assertion-based techniques. This tutorial provides an industry survey of today’s ABV landscape, ranging from myths to realities. Emerging challenges and possible research opportunities are discussed. The following extended abstract provides a reference on which the tutorial builds.
Chapter PDF
Similar content being viewed by others
Keywords
References
Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: FoCs—Automatic Generation of Simulation Checkers from Formal Specifications. In: Proc. 12th International Conference Computer Aided Verification, pp. 414–427 (2000)
2004 IC/ASIC Functional Verification Study, Industry report from Collett International Research, p. 34 (2004)
EDA Market Statistics Service Report, Far West Research (2008)
Turing, A.: In Report of a conference on high speed automatic calculating machines, pp. 67–69, Univ. Math. Laboratory, Cambridge (1949)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundation of Computer Science, pp. 46–57 (1977)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1/2), 72–99 (1983)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, Springer, Heidelberg (2001)
Iwashita, H., Nakata, T.: Forward Model Checking Techniques Oriented to Buggy Designs. In: International Conference on Computer Aided Design, ICCAD (1997)
Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002)
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)
Long, J., Seawright, A.: Synthesizing SVA Local Variables for Formal Verification. In: Proceedings of the 44th Design Automation Conference, DAC 2007, pp. 75–80 (2007)
Verification Census, extracted from the world-wide-web on April 16 (2008), http://www.deepchip.com/posts/dvcon07.html
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Foster, H. (2008). Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial). In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)