Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 474

Example 21.34. Consider the following code fragment:

always @( posedge clk) begin
// ...
if (en) begin
// ...
a1: assert #0 ($onehot0({a, b});
end
end
In FV, the deferred assertion a1 is interpreted as a concurrent assertion:
always @( posedge clk) begin
// ...
if (en) begin
// ...
a1: assert property ($onehot0({a, b});
end
end

t

Exercises

21.1. Write a module implementing a counter modulo 4 and build the correspond-
ing FV model. Write a symbolic representation of its transition relation.

21.2. Build an automaton for the complement of the property always a[ * 3]
##1 b |=> c . Compare it with the automaton for the complement of the property
always a[+] ##1 b |=> c
21.3.

What do the following properties mean?

(1) @clk s_eventually always p .
(2) @clk s_nexttime nexttime p .
(3) @clk nexttime s_nexttime p .
(4) @clk p until s_nexttime q .
(5) @clk p s_until nexttime q .
21.4.

Rewrite the following properties without using negation:

(a) @clk not weak (a ##1 b)
(b) @clk not strong (s[->2]) .
21.5. What is the meaning of the property @clk p s_until_with always q ?