Assertion System Functions and Tasks - SVA: The Power of Assertions in SystemVerilog - page 133

7.1.2 Check for Mutual Exclusion

System function $onehot0 checks that all bits of its single argument are mutually
exclusive. More precisely, it returns 1'b1 if at most one bit of its argument is set
to 1. Otherwise, it returns 1'b0 . Bits carrying the values x or z are treated as 0.
Example 7.2. All bus drivers, that is, the bits set to 1'b1 , of the vector bus_in must
be mutually exclusive.

Solution:

t

a_mutex: assert final ($onehot0(bus_in));

Example 7.3. read and write requests cannot appear together.
Solution:

a_norw: assert property (@( posedge clk)
$onehot0({read, write}));
We use a concatenation operator to build a bit vector from two signals.

Discussion: If one of the signals, say write , has value x then assertion a_norw
passes, which is problematic, because x may correspond to both 0 and 1, and
$onehot0 does not guarantee the mutual exclusion. Therefore, in order to consider
x and z as possible 1, it is safer to rewrite our assertion using $countbits :
a_norw_x: assert property (@( posedge clk)
$countbits({read, write}, 1'b1, 1'bx, 1'bz) <= 1);

t

7.1.3 One-Hot Encoding

System function $onehot checks that exactly one bit of its argument is set to 1.
If this condition is met, it returns 1'b1 , otherwise, it returns 1'b0 . In a similar way,
$onehot0 checks that at most one bit of its argument is set to 1. If this condition is
met, it returns 1'b1 , otherwise, it returns 1'b0 .
Example 7.4.

Check that a control state of an FSM has a one-hot encoding when

rst is low.
Solution:

a_onehot: assert property (@( posedge clk) disable iff (rst)
$onehot(state));

Discussion: To check one-cold encoding use $onehot(~state) . In the presence of
unknown values, $countbits function should be used to check one-hot and one-
cold encodings (see Exercise 7.2 ).

t