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

begin : GEN_BAD

12

default disable iff bad;

13

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

14

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

15

a2: assert property (p);

16

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

17

end

18

endgenerate

19

module m_nested;

20

default disable iff reset && bad;

21

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

22

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

23

default disable iff retry;

24

a2: assert property (p);

25

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

26

endmodule

27

endmodule

28

13.3. Give an alternative encoding of the assertion in Fig. 13.11 that uses a simpler
abort condition.

13.4. Explain the meaning of the following properties:

1. accept_on ( a ) reject_on ( b ) p.
2. reject_on ( a ) accept_on ( b ) p.