Resets - SVA: The Power of Assertions in SystemVerilog - page 299

10 20 30 40 50 60 70 80 90 100

clk

retry

bad

a

b

c

Fig. 13.13 Waveform for a_abort_subproperties

Exercises

13.1. Explain why assertions a1 and a2 below have the same passing and failing
evaluation behavior:

a1: assert property (@( posedge clk) sync_accept_on (a)
b[ * 2] |=> c

);
a2: assert property (@( posedge clk)
!a throughout b[ * 2] |=> a || c

);
Rewrite the following coverage assertion without using sync_reject_on :
c1: cover property (@( posedge clk) sync_reject_on (a)
b[ * 2] ##1 c

);

13.2. In the module below, determine for each occurrence of a nested disable
condition whether or not the nesting is legal. Also, for each concurrent assertion that
is not involved with an illegal nested disable clause, identify the disable condition
that governs it, if any.

module #( parameter BAD) m (

1

logic a, b, c, clk, reset, retry, bad

2

);

3

default clocking PCLK @( posedge clk); endclocking

4

default disable iff reset;

5

property p; disable iff (retry) b |=> c; endproperty

6

a0: assert property (a |=> b);

7

a1: assert property ( disable iff (retry) a |=> b);

8

a2: assert property (p);

9

a3: assert property (a |=> p);

10

generate if (BAD)

11