Question

主题

主题	描述
H.1 简介	This appendix presents a formal semantics for SystemVerilog concurrent assertions. Immediate assertions and coverage statements are not discussed here. Throughout this appendix, “assertion” is used to mean “concurrent assertion”. The semantics is defined by a relation that determines when a finite or infinite word (i.e., trace) satisfies an assertion. Intuitively, such a word represents a sequence of valuations of SystemVerilog variables sampled at the finest relevant granularity of time (e.g., at the granularity of simulator cycles). The process by which such words are produced is closely related to the SystemVerilog scheduling semantics and is not defined here. In this appendix,... more
H.2 抽象语法
H.3 语义	Let P be the set of atomic propositions. The semantics of assertions and properties is defined via a relation of satisfaction by empty, finite, and infinite words over the alphabet Σ = 2P U {T, ⊥}. Such a word is an empty, finite, or infinite sequence of elements of Σ. The number of elements in the sequence is called the length of the word, and the length of word w is denoted |w|. Note that |w| is either a non-negative integer or infinity. The sequence elements of a word are called its letters and are assumed to be indexed consecutively... more
H.4 Extended Expressions	This section describes the semantics of several constructs that are used like expressions, but whose meaning at a point in a word can depend both on the letter at that point and on previous letters in the word. By abuse of notation, the meanings of these extended expressions are defined for letters denoted “w j” even” though they depend also on letters w i for i < j. The reason for this abuse is to make clear the way these definitions should be used in combination with those in preceding sections.
H.5 Recursive Properties	This section defines the neutral semantics of instances of recursive properties in terms of the neutral semantics of instances of non-recursive properties. The latter can be expanded to properties in the abstract syntax by appropriate substitutions, and so their semantics is assumed to be understood. According to Restriction 1 in Section 17.11.3, it is understood below that the negation operator not cannot be applied to any property expression that instantiates a recursive property. Restriction 2 in Section 17.11.3 is not represented here because disable iff is treated as a general property-building operator in this appendix. A precise version of Restriction... more

链接

主题