Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 103

Table 5.2 Initial trace
fragment for Example 5.20
.

Clock tick a b c d e
0 1 1 0 0 0

1 1 1 1 0 0

2 0 1 0 1 0

3 0 0 1 1 1

￿ a until d is true since a is true in clock ticks 0 and 1, and d is true in clock
tick 2.
￿ a until e is false since a is false in clock tick 2, and e is false in clock ticks 0,
1, and 2.
￿ b until_with a is true since both a and b aretrueinclocktick0.
￿ b until_with c is true since b is true in the clock ticks 0 and 1, and c is true in
clock tick 1.
￿ b until_with e is false since b is false in clock tick 3, and e is false in clock
ticks 0, 1, and 2.

t

Example 5.21. ready should be low until rst becomes inactive for the first time.
Solution:

initial a1: assert property (@( posedge clk) !ready until !rst);

t

Example 5.22. There cannot be a read before the first write :

Solution:

initial
a2: assert property (@( posedge clk) !read until_with write);

t

Exercises

5.1. Write a restriction saying that initially all bus drivers are disconnected (have a
high impedance value).

5.2. Write the following assertion: rdy should be low while rst is active.

5.3. What do the following properties mean?

(a) always nexttime always p
(b) nexttime always nexttime p
5.4. Discuss the usage of the always operator in assertions.