Abstract
Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described in standard temporal logics, describing a multiply-clocked design is cumbersome. Thus, it is desirable to have an easier way to formulate properties related to clocks in a temporal logic. In [6] a relatively simple solution built on top of the traditional ltl semantics was suggested and adopted by the IEEE standard temporal logic psl. The suggested semantics was examined relative to a list of design goals, and it was shown that it answered all requirements except for preserving the least fixed point characterization of the until operator under multiple clocks. In this work we show that with a minor addition to the semantics of [6] this requirement is met as well.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview 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.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, Springer, Heidelberg (2002)
Clarke, E., Emerson, E.: Characterizing correctness properties of parallel programs as fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, Springer, Heidelberg (1980)
Dam, M.: Temporal logic, automata and classical theories - an introduction. Lecture Notes for the 6th European Summer School on Logic, Language and Information (1994)
Eisner, C., Fisman, D.: Sugar 2.0 proposal presented to the Accellera Formal Verification Technical Committee (March 2002), http://www.haifa.il.ibm.com/projects/verification/sugar/Sugar_2.0_Accellera.ps
Eisner, C., Fisman, D.: A practical introduction to PSL. Springer, Heidelberg (2006)
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.) ICALP 2003. LNCS, vol. 2719, Springer, Heidelberg (2003)
Emerson, E.A.: Model checking and the Mu-calculus. In: Descriptive Complexity and Finite Models. DIMACS Series in Discrete Mathematics, vol. 31, pp. 185–214. American Mathematical Society, Providence, RI (1997)
Havlicek, J., Fisman, D., Eisner, C.: Basic results on the semantics of Accellera PSL 1.1 foundation language. Technical Report 2004.02 Accellera, (May 2004)
Havlicek, J., Levi, N., Miller, H., Shultz, K.: Extended CBV statement semantics, partial proposal presented to the Accellera Formal Verification Technical Committee (April 2002), http://www.eda.org/vfv/hm/att-0772/01-ecbv_statement_semantics.ps.gz
Annex E of IEEE Standard for SystemVerilog Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800TM (2005)
IEEE Standard for Property Specification Language (PSL). IEEE Std 1850TM (2005)
Kaivola, R.: A simple decision method for the linear-time mu-calculus (1995)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27(3), 333–354 (1983)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Specification. Springer, New York (1992)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68–93 (1984)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K. (ed.) Logics and Models of Concurrent Systems. NATO Advanced Summer Institute, vol. F-13, pp. 123–144. Springer, Heidelberg (1985)
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–309 (1955)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, pp. 238–266 (1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fisman, D. (2008). On the Characterization of Until as a Fixed Point Under Clocked Semantics. In: Yorav, K. (eds) Hardware and Software: Verification and Testing. HVC 2007. Lecture Notes in Computer Science, vol 4899. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77966-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-77966-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77964-3
Online ISBN: 978-3-540-77966-7
eBook Packages: Computer ScienceComputer Science (R0)