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

5.5. What is the meaning of the following assertion (note that it does not belong to
an initial procedure)?
a1: assert property (@( posedge clk) s_eventually always !rst);

5.6. What is the meaning of the following properties?

(a) s_eventually nexttime p
(b) nexttime s_eventually p
(c) s_eventually nexttime always p
(d) always nexttime s_eventually p
5.7. What do the following properties mean?

(a) 1 until q
(b) p until 1
(c) 0 until q
(d) 0 until_with q
(e) p until 0
(f) nexttime (p until q)
(g) ( nexttime p) until q
(h) p until nexttime q
(i) p until_with nexttime q
(j) p1 until (p2 until p3)
(k) p1 until_with (p2 until_with p3)
(l) always (p until q)
(m) ( always p) until q
(n) p until always q
(o) p1 until (p2 until always p3)
5.8.

Prove that p until_with q is equivalent to p until (p and q) .