Abstract
SystemVerilog Assertions (SVA) is a linear temporal logic within the recently approved IEEE 1800 SystemVerilog standard. The complexities of the satisfiability and model-checking problems are studied for a basic subset of (SVA) and for extensions of the basic subset obtained by adding each of the following features: local variables, regular expression intersection, quantified variables, and property declarations with arguments. It is shown that the complexities for the basic subset are PSPACE-complete, while the complexities increase to EXPSPACE-complete in each of the extensions. Alternating Büchi automata constructions provide the upper bounds, while reductions from PSPACE and EXPSPACE tiling problems provide the lower bounds.
Chapter PDF
Similar content being viewed by others
Keywords
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
Accellera. SystemVerilog 3.1a Language Reference Manual: Accellera’s Extensions to Verilog (2004), http://www.eda.org/sv/SystemVerilog_3.1a.pdf
Alur, R., Henzinger, T.: Real-time logics: complexity and expressiveness. In: Proc. 5th Symp. on Logic in Computer Science, pp. 390–401 (June 1990)
Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
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 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)
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., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. In: Int’l. Symp. on Leveraging Applications of Formal Methods (2004)
Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science (May 2005)
Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)
Gordon, M.J.C.: Validating the PSL/Sugar semantics using automated reasoning. Formal Aspects of Computing 15(4), 406–421 (2003)
Havlicek, J., Shultz, K., Armoni, R., Dudani, S., Cerny, E.: Notes on the semantics of local variables in Accellera SystemVerilog 3.1 concurrent assertions. Technical Report 2004.01, Accellera (May 2004), Available from: www.accellera.org
Lewis, H.R.: Complexity of solvable cases of the decision problem for the predicate calculus. Foundations of Computer Science 19, 35–47 (1978)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)
IEEE Computer Society. 1800: IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language. IEEE (2005)
IEEE Computer Society. 1850: IEEE Standard for Property Specification Language (PSL). IEEE (2005)
van Emde Boas, P.: The convenience of tilings. In: Complexity, Logic and Recursion Theory. Lecture Notes in Pure and Applied Mathematics, vol. 187, pp. 331–363 (1997)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Verification guild: A community of verification professionals, http://verificationguild.com
Wang, H.: Dominoes and the AEA case of the decision problem. In: Symposium on the Mathematical Theory of Automata, pp. 23–55 (1962)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bustan, D., Havlicek, J. (2006). Some Complexity Results for SystemVerilog Assertions. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_21
Download citation
DOI: https://doi.org/10.1007/11817963_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)