Section H

LRM-285

Change (changes in red and blue):

SystemVerilog Formal Semantics of Concurrent Assertions Semantics

Section H.3.3.2

LRM-293

Change (Note that |= is a single symbol and |/= is a single symbol (see previous two bullets for examples) (changes in red and blue):

· • “pending” or “holds weakly” otherwise.

· "holds (but does not hold strongly)" if w |= A and w |/= ⁺ A.

· "pending" if w |= ^- A and w |/= A.