Advanced Properties - SVA: The Power of Assertions in SystemVerilog - page 216

Chapter 10
Advanced Properties
No man acquires property without acquiring with it a little
arithmetic also.
— Ralph Waldo Emerson
This chapter briefly recapitulates the basic properties discussed in Chap. 5 and
discusses more complex property operators. First, we examine the property equiv-
alents of Boolean operators, namely, not , or , and , implies , iff , if else , and
case . Then we provide a description of temporal operators inspired by Linear
Temporal Logic. The operators are described informally; the reader interested
in formal semantics should consult Chap. 22 . Recursive properties are described
in Chap. 17 , and the abort operators accept_on , reject_on , sync_accept_on ,
sync_reject_on are discussed in Chap. 13 . In all examples, we assume that the
properties and assertions are in the scope of a default clocking declaration, hence no
explicit clocks are specified.
Most of the temporal operators come in two forms, weak and strong. The strong
forms are identified by a prefix s_ as in s_nexttime p . In simple terms, the strength
determines the property evaluation result when there are not enough clock ticks to
complete the evaluation of the operator, e.g., at the end of simulation or when the
source stops emitting them. More precise explanation is given in Chap. 21 .
Table 10.1 lists all the property operators available in the language. The order
of appearance is in decreasing precedence, beginning with the highest on the top.
Operators appearing in one block of the table have the same precedence. Blocks are
separated by horizontal lines. For example, not , nexttime , and s_nexttime have
the same precedence. Additionally, the precedence of any SystemVerilog expression
operator is higher than any property or sequence operator.