iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-319-10575-8_24
Functional Specification of Hardware via Temporal Logic | SpringerLink
Skip to main content
Springer Nature Link
Log in

Functional Specification of Hardware via Temporal Logic

  • Chapter
  • First Online:
Handbook of Model Checking

Abstract

In the late 1970s, Amir Pnueli suggested that functional properties of reactive systems be formally expressed in temporal logic. For model checking such a logic to be possible, it must have sufficient expressive power, its semantics must be formally defined in a rigorous way, and the complexity of model checking it must be well understood and reasonable. In order to allow widespread adoption in industry, there is an additional requirement: functional specification must be made easy, allowing common properties to be expressed intuitively and succinctly. But while adding syntax is simple, defining semantics without breaking properties of the existing semantics is a different story. This chapter is about the various extensions to temporal logic included in the IEEE standards PSL and SVA, their motivation, and the subtle semantic issues encountered in their definition.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985)

    Article  MathSciNet  Google Scholar 

  3. Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)

    Article  Google Scholar 

  4. Armoni, R., Bustan, D., Kupferman, O., Vardi, M.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)

    Google Scholar 

  5. Armoni, R., Fisman, D., Jin, N.: SVA and PSL local variables—a practical approach. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 8044, pp. 197–212. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M., Zbar, Y.: The ForSpec temporal logic: a new temporal property-specification language. In: Katoen, J., Stevens, P. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  7. 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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Hu, A.J., Vardi, M.Y. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL (Deliverable 3.2/4). Tech. rep., PROSYD (2005)

    Google Scholar 

  10. Ben-David, S., Fisman, D., Ruah, S.: The safety simple subset. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 3875, pp. 14–29. Springer, Heidelberg (2005)

    Google Scholar 

  11. Ben-David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. Theor. Comput. Sci. 404(3), 202–218 (2008)

    Article  MathSciNet  Google Scholar 

  12. Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 222–235. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Tech. Rep. MCS05-04, The Weizmann Institute of Science (2005)

    Google Scholar 

  14. Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.: Regular vacuity. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Bustan, D., Havlicek, J.: Some complexity results for SystemVerilog assertions. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 205–218. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Cerny, E., Dudani, S., Havlicek, J., Korchemny, D.: The Power of Assertions in SystemVerilog. Springer, Heidelberg (2010)

    Book  Google Scholar 

  17. Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Workshop on Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  18. Eisner, C., Fisman, D.: Sugar 2.0 proposal presented to the Accellera Formal Verification Technical Committee (2002). At http://www.haifa.il.ibm.com/projects/verification/sugar/Sugar_2.0_Accellera.ps

  19. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, New York (2006)

    Google Scholar 

  20. Eisner, C., Fisman, D.: Augmenting a regular expression-based temporal logic with local variables. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 1–8. IEEE, Piscataway (2008)

    Google Scholar 

  21. Eisner, C., Fisman, D.: Structural contradictions. In: Chockler, H., Hu, A.J. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 5394, pp. 164–178. Springer, Heidelberg (2008)

    Google Scholar 

  22. Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: Aguilera, M.K., Aspnes, J. (eds.) Symp. on Principles of Distributed Computing (PODC), pp. 1–8. ACM, New York (2005)

    MATH  Google Scholar 

  23. Eisner, C., Fisman, D., Havlicek, J.: Safety and liveness, weakness and strength, and the underlying topological relations. ACM Trans. Comput. Log. 15(2), 13:1–13:44 (2014)

    Article  MathSciNet  Google Scholar 

  24. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Eisner, C., Fisman, D., Havlicek, J., Mårtensson, J.: The \(\top, \bot\) approach for truncated semantics. Tech. Rep. 2006.01, Accellera (2006)

    Google Scholar 

  26. Eisner, C., Fisman, D., Havlicek, J., McIsaac, A., Van Campenhout, D.: The definition of a temporal clock operator. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Intl. Coll. on Automata, Languages and Programming (ICALP). LNCS, vol. 2719, pp. 857–870. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  27. Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B, pp. 995–1072. Elsevier/MIT Press, Amsterdam/Cambridge (1990). Chap. 16

    Google Scholar 

  28. Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979)

    Article  MathSciNet  Google Scholar 

  29. Fisman, D.: On the characterization of until as a fixed point under clocked semantics. In: Yorav, K. (ed.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 4899, pp. 19–33. Springer, Heidelberg (2007)

    Google Scholar 

  30. French, T., Reynolds, M.: A sound and complete proof system for QPTL. In: Balbiani, P., Suzuki, N., Wolter, F., Zakharyaschev, M. (eds.) Advances in Modal Logic, pp. 127–148. King’s College Publications, London (2002)

    Google Scholar 

  31. Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Abrahams, P.W., Lipton, R.J., Bourne, S.R. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 163–173. ACM, New York (1980)

    Google Scholar 

  32. Gelade, W.: Succinctness of regular expressions with interleaving, intersection and counting. In: Ochmanski, E., Tyszkiewicz, J. (eds.) Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 5162. Springer, Heidelberg (2008)

    Google Scholar 

  33. Gelade, W., Neven, F.: Succinctness of the complement and intersection of regular expressions. In: Annual Symp. on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics, vol. 1, pp. 325–336. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl (2008)

    MATH  Google Scholar 

  34. Gordon, M.: Validating the PSL/Sugar semantics using automated reasoning. Form. Asp. Comput. 15(4), 406–421 (2003)

    Article  Google Scholar 

  35. Hafer, T., Thomas, W.: Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) Intl. Coll. on Automata, Languages and Programming (ICALP). LNCS, vol. 267, pp. 269–279. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  36. Halpern, J.Y., Manna, Z., Moszkowski, B.C.: A hardware semantics based on temporal intervals. In: Díaz, J. (ed.) Intl. Coll. on Automata, Languages and Programming (ICALP). LNCS, vol. 154, pp. 278–291. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  37. Harel, D., Kozen, D., Parikh, R.: Process logic: expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25(2), 144–170 (1982)

    Article  MathSciNet  Google Scholar 

  38. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  39. Harel, D., Peleg, D.: Process logic with regular formulas. Theor. Comput. Sci. 38, 307–322 (1985)

    Article  MathSciNet  Google Scholar 

  40. Havlicek, J., Shultz, K., Armoni, R., Dudani, S., Cerny, E.: Notes on the semantics of local variables in Accellera SystemVerilog 3.1 concurrent assertions. Tech. Rep. 2004.01, Accellera (2004)

    Google Scholar 

  41. Holzer, M., Jakobi, S.: State complexity of chop operations on unary and finite languages. In: Kutrib, M., Moreira, N., Reis, R. (eds.) Workshop on Descriptional Complexity of Formal Systems (DCFS). LNCS, vol. 7386, pp. 169–182. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  42. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)

    MATH  Google Scholar 

  43. IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850™-2005

    Google Scholar 

  44. IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850™-2010

    Google Scholar 

  45. IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language, Annex E. IEEE Std 1800™-2005

    Google Scholar 

  46. IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language, Annex F. IEEE Std 1800™-2009

    Google Scholar 

  47. Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, Univ. of California, Los Angeles (1968)

    Google Scholar 

  48. Kesten, Y., Pnueli, A.: A complete proof system for QPTL. In: Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 2–12. IEEE, Piscataway (1995)

    Chapter  Google Scholar 

  49. Kilpeläinen, P., Tuhkanen, R.: Regular expressions with numerical occurrence indicators—preliminary results. In: Kilpeläinen, P., Päivinen, N. (eds.) Symp. on Programming Languages and Software Tools (SPLST), pp. 163–173 (2003). University of Kuopio, Department of Computer Science

    Google Scholar 

  50. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 172–183. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  51. Lange, M.: Linear time logics around PSL: complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Vasconcelos, V.T. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 4703, pp. 90–104. Springer, Heidelberg (2007)

    Google Scholar 

  52. Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Kohlenbach, U., Abramsky, S. (eds.) Symp. on Logic in Computer Science (LICS), pp. 383–392. IEEE, Piscataway (2002)

    Google Scholar 

  53. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Deusen, M.S.V., Galil, Z., Reid, B.K. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 97–107. ACM, New York (1985)

    Google Scholar 

  54. Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  55. Long, J., Seawright, A., Kavalipati, P.: Multi-clock SVA synthesis without re-writing. In: Wakabayashi, K. (ed.) Asia and South Pacific Design Automation Conf. (ASPDAC), pp. 648–653. IEEE, Piscataway (2009)

    Google Scholar 

  56. Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 643–652. IEEE, Piscataway (2000)

    Google Scholar 

  57. McMillan, K.: Symbolic Model Checking. Kluwer Academic, Norwell (1993)

    Book  Google Scholar 

  58. McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT Research Monograph No. 65). MIT Press, Cambridge (1971)

    MATH  Google Scholar 

  59. Morley, M.: Semantics of temporal e. In: Melham, T.F., Moller, F.G. (eds.) Proc. Banff Higher Order Workshop. Formal Methods in Computation (1999). Univ. of Glasgow, Dept. of Computing Science. Technical Report

    Google Scholar 

  60. Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Symp. on Logic in Computer Science (LICS), pp. 422–427. IEEE, Piscataway (1988)

    Google Scholar 

  61. Oliveira, M.T., Hu, A.J.: High-level specification and automatic generation of IP interface monitors. In: Design Automation Conf. (DAC), pp. 129–134. ACM, New York (2002)

    Google Scholar 

  62. Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46–57. IEEE, Piscataway (1977)

    Google Scholar 

  63. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. Tech. rep., Massachusetts Inst. of Technology (1976)

    Google Scholar 

  64. Seawright, A., Brewer, F.: High-level symbolic construction technique for high performance sequential synthesis. In: Dunlop, A.E. (ed.) Design Automation Conf. (DAC), pp. 424–428. IEEE, Piscataway (1993)

    Google Scholar 

  65. Sistla, A.P.: Theoretical issues in the design and verification of distributed systems. Ph.D. thesis, Harvard Univ. (1983)

    Google Scholar 

  66. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)

    MathSciNet  MATH  Google Scholar 

  67. Sistla, A.P., Vardi, M.Y., Wolper, P.L.: The complementation problem for Büchi automata, with applications to temporal logic. Theor. Comput. Sci. 49, 217–237 (1987)

    Article  Google Scholar 

  68. Thomas, W.: Star-free regular sets of \(\omega\)-sequences. Inf. Control 42(2), 148–156 (1979)

    Article  MathSciNet  Google Scholar 

  69. Vardi, M.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)

    Google Scholar 

  70. Vardi, M.Y.: From Church and Prior to PSL. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 150–171. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  71. Vardi, M.Y., Wolper, P.: Yet another process logic (preliminary version). In: Clarke, E.M., Kozen, D. (eds.) Workshop on Logic of Programs. LNCS, vol. 164, pp. 501–512. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  72. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Symp. on Logic in Computer Science (LICS), pp. 332–344. IEEE, Piscataway (1986)

    Google Scholar 

  73. Winkelmann, K., Trylus, H., Stoffel, D., Fey, G.: Cost-efficient block verification for a UMTS up-link chip-rate coprocessor. In: Design, Automation & Test in Europe (DATE), pp. 162–167. IEEE, Piscataway (2004)

    Google Scholar 

  74. Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1/2), 72–99 (1983)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Research – Haifa, Haifa, Israel

    Cindy Eisner

  2. Ben-Gurion University, Be’er Sheva, Israel

    Dana Fisman

Authors
  1. Cindy Eisner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dana Fisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dana Fisman .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Eisner, C., Fisman, D. (2018). Functional Specification of Hardware via Temporal Logic. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation