Introduction - SVA: The Power of Assertions in SystemVerilog - page 24

1 logic a, b, c, d, cond, clk;
2 let onecold(sig) = $onehot(~sig);
3 // ...
4 always_comb begin
5 // ...
6 a1: assert (onecold({a, b, c}) || d);
7 end
8 a2: assert final (onecold({a, b, c}) -> d);
9 a3: assert property (@( posedge clk) cond |=> onecold({a, b, c}));

Fig. 1.10 Expression reuse

1 logic ready, request, grant, clk;
2 // ...
3 sequence falling(x);
4 (x ##1 !x);
5 endsequence
6 a1: assert property (@( posedge clk) falling(ready) |=> ready);
7 a2: assert property (@( posedge clk)request |=> falling(grant));

Fig. 1.11 Sequence reuse

ensuring that exactly one signal among a , b , and c is low when d is low. a2 is a final
assertion ensuring that when exactly one signal among a , b , and c is low, d must
be high. Another variation is the concurrent assertion a3 which specifies that after
condition cond is true, exactly one signal among a , b , and c is 0.
We describe the let statement in Sect. 8.1 .

Sequence Reuse

It is possible to assign names to sequences of signal values in time and to reference
these sequences by name in assertions, as shown in Fig. 1.11 .
falling is a sequence name, and x is its argument. (x ##1 !x) defines a
sequence of values of signal x in time. Its meaning is that the value x=1 is
followed by the value x=0 in the next clock cycle. 10 Sequence falling is reused
in concurrent assertions a1 and a2 .
Assertion a1 states that ready flag may drop at most for one clock cycle. More
precisely, if ready gets deasserted after being asserted then at the next clock cycle
ready should be asserted again. The operator |=> means “then at the next clock
cycle”, and it is called non-overlapping suffix implication . Assertion a2 states that

10 For simplicity, here and in future examples we ignore the possibility of unknown and high-
impedance values X and Z unless explicitly stated.