Formal Semantics - SVA: The Power of Assertions in SystemVerilog - page 486

As explained in Sect. 6.4 , nonoverlapping implication is a shortcut:

.s |=> p/ .s ##1 1 |-> p/:

22.3.6 Suffix Conjunction: Followed-by

The formal semantics of followed-by (also called suffix conjunction) is as follows:

w ˆ s #-# p iff for some i 0; w 0;i j s and w i:: ˆ p.

Followed-by and suffix implication are dual operations (Chap. 10.3 ):

.s #-# p/ . not ( s |-> not p ) /:

Indeed, property s |-> p is false iff at some tight satisfaction point of sequence s
property p does not hold.
Nonoverlapping followed-by is defined as a shortcut:

.s #=# p/ .s ##1 1 #-# p/:

22.4 Formal Semantics of Clocks

The following notations, with and without subscripts, are used throughout this
section: b, c, d , x, y, and z denote Boolean expressions; e denotes an event
expression; r denotes a sequence; p denotes a property; v denotes a local variable
(see Chap. 15 ); h denotes an expression.
The formal semantics treats clocks like Boolean expressions. If e is a clocking
event, then .e/ denotes the associated Boolean expression. The semantics of .e/
is that ` ˆ .e/ iff there is a tick of e in letter `. In this way, the question of whether
e occurs at a particular tick of the global clock is transformed into the question of
whether the Boolean expression .e/ is true at that tick of the global clock. is
defined as follows:

C1 If e is a named event, then .e/ is assumed to be understood as a Boolean
expression at the granularity of the global clock. 3
C2 . $global_clock / D 1'b1 .
C3 .b/ D $changing_gclk( b ) , where b is not $global_clock .

3 The formal semantics does not attempt to expand the meaning of a named event in terms of the
various code that may trigger the event.