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

Exposition of the semantics is simplified by the fact that only disable iff and
accept_on need be treated as primitive operators. The other resets are derived by
the following rules:
￿ reject_on ( b ) p not accept_on ( b ) not p.
￿ sync_reject_on ( b ) p not sync_accept_on ( b ) not p.
￿

p .p; c/.
The formal semantics of accept_on is simpler than that of disable iff
because it involves only the two dispositions “pass” and “fail”. It is defined as
follows:
w ˆ accept_on ( b ) p
iff

p . sync_accept_on ( b ) p; c/ D accept_on ( b && c ) T

T

either
w ˆ p

or

there exists 0 i< j w j such that w i ˆ b and w 0;i 1

!

ˆ p.
Thefirstcaseallows w to satisfy accept_on ( b ) p if w satisfies p itself, regardless
of the abort condition. The second case accounts for an occurrence of the abort con-
dition and replaces the suffix of w beginning at the letter where the abort condition
occurs by >

>

! before checking for satisfaction of the underlying property p.

Example 22.19. Derive direct semantics for reject_on ( b ) p.

Solution:

w ˆ reject_on ( b ) p
iff w ˆ not accept_on ( b ) not p
iff N w 6ˆ accept_on ( b ) not p
iff both

N w 6ˆ not p

and

for all 0 i< j w j such that N w i ˆ b W w 0;i 1

!

> 6ˆ not p

iff both

w ˆ p

and

for all 0 i< j w j such that N w i ˆ b W w 0;i 1

!

? ˆ p

t

It thus follows that reject_on.b/p succeeds when w satisfies p and this happens
before the earliest occurrence of b.
The “pass” and “fail” dispositions of a disable iff are defined formally as
follows:
w ˆ disable iff ( b ) p
iff either

w ˆ p and no letter of w satisfies b

or

for some i , w i ˆ b, and w 0;i 1

!

? ˆ p for the least such i .