Anzeige
Erschienen in:
2018 | OriginalPaper | Buchkapitel
Functional Specification of Hardware via Temporal Logic
verfasst von : Cindy Eisner, Dana Fisman
Erschienen in: Handbook of Model Checking
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.