Abstract
SystemVerilog Assertions (SVA), as well as Property Specification Language (PSL) are linear temporal logics based on LTL [14], extended with regular expressions and local variables. In [6] Bustan and Havlicek show that the local variable extensions, as well as regular expressions with intersection, render the verification problem of SVA and PSL formulae EXPSPACE-complete. In this paper we show a practical approach for the verification problem of SVA and PSL with local variables. We show that in practice, for a significant and meaningful subsets of those languages, which we denote PSLpract, local variables do not increase the complexity of their verification problem, keeping it in PSPACE.
Chapter PDF
References
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.) TACAS 2002. LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002)
Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithm optimized for PSL. Technical Report Delivery 3.2/4, PROSYD (July 2005)
Ben-David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. Theor. Comput. Sci. 404(3), 202–218 (2008)
Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical report, Weizmann Institute of Science (May 2005)
Bustan, D., Havlicek, J.: Some complexity results for systemVerilog assertions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 205–218. Springer, Heidelberg (2006)
Havlicek, J., Korchemny, D., Cerny, E., Dudani, S.: Havlicek Korchemny Cerny and Dudani. Springer (2009)
Eisner, C., Fisman, D.: Eisner and Fisman. Springer (2006)
Eisner, C., Fisman, D.: Augmenting a regular expression-based temporal logic with local variables. In: Cimatti, A., Jones, R.B. (eds.) FMCAD, pp. 1–8. IEEE (2008)
IEEE Standard for Property Specification Language (PSL). IEEE Std 1850TM-2010 (2010)
IEEE Standard for SystemVerilog ? Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800TM-2009 (2009)
Martensson, J.: US patent US8225249: Static formal verification of a circuit design using properties defined with local variables. Jasper Design Automation, Inc. (June 2008)
Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society (1977)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armoni, R., Fisman, D., Jin, N. (2013). SVA and PSL Local Variables - A Practical Approach. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)